A clause.
Adds a collection of literals as a clause to the solver.
Adds a collection of literals as a clause to the solver.
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Method to use to effectively add a clause to the underlying Solver implementation.
Adds a list of literals as a clause to the solver.
Adds a list of literals as a clause to the solver.
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Add a header comment in the formula.
an iterator on the clauses currently in the solver.
Freeze the variable underlying the literal.
Reserve
Reserve
howmany
variables to express the problem, reserving dimacs variables identifiers in [1, howmany]. Next fresh variables identifiers will start at
howmany+1
howmany }}} Next fresh variables identifiers will start at
howmany+1
number of variables to create
The total variables used in the solver.
Creates a fresh variable in the solver.
Creates a fresh variable in the solver.
the number of variables created in the solver so far, equal to the fresh variable identifier.
Method to implement to effectively create a fresh var in the underlying representation.
Method to implement to effectively create a fresh var in the underlying representation.
Iterator over all header comments, in insertion order.
True iff the variable is frozen.
Returns a switching literal: if switch is Some( s ), returns this Some( s ), else if switchable is true, returns a Some( newSwitch ) else returns None.
the number of clauses of the formula.
the number of variables created using freshVar
An interface for building formulas in conjunctive normal form.