Module Actlit

val fresh_actlit : unit -> UfSymbol.t

Creates a fresh actlit as a bool UF constant.

val fresh_actlit_count : unit -> int

Returns the number of fresh actlits created this far.

val reset_fresh_actlit_count : unit -> unit

Resets the internal counter for fresh actlits.

/!\ Dangerous, use only if all solvers do use any of the old actlits or will not use any of the new ones.

val term_of_actlit : UfSymbol.t -> Term.t

Returns the term corresponding to the input actlit.