Index of values

Returns the atom associated with the given formula

Returns the variable associated with the term

Returns an assignment value for the given term.

Add the list of clauses to the current set of assumptions.

Add the list of clauses to the current set of assumptions.

Assume the formulas in the slice, possibly pushing new formulas to be propagated, and returns the result of the new assumptions.

Assume the formulas in the slice, possibly pushing new formulas to be propagated, and returns the result of the new assumptions.

Backtrack to the given level.

Backtrack to the given level.

Check the satisfiability of the current model.

Check the contents of a proof.

Return the current level of the theory (either the empty/beginning state, or the last level returned by the assume function).

Return the current level of the theory (either the empty/beginning state, or the last level returned by the assume function).

Simpler version of Log.debug, without formatting

Emit a debug message at the given level.

Constant formula.

A dummy level.

A dummy level.

Formula constant.

Dummy values for use in vector dummys

Constructors & destructor for elements

The empty clause

Equality over formulas.

Equality over terms.

Equality over formulas.

Returns the valuation of a formula in the current state of the sat solver.

Returns the evaluation of the formula in the current assignment

Return the current assignement of the literals, as well as its decision level.

Return the proof step at the root of a given proof.

Prints the entire set of clauses in the input problem (including hypothesis, lemmas and local assumptions), in the dimacs format.

Export the current problem contents to iCNF format.

The false formula, i.e a formula that cannot be satisfied.

The true formula, i.e a formula that is always satisfied.

fold f acc p, fold f over the proof p and all its node.

Make a fresh atom

Generate fresh formulas (that are different from any other).

Fresh names for clauses

View the current state of the trail as a slice.

Current debug level

Recover tag from a clause, if any

Hashing function for formulas.

Hashing function for terms.

Hashing function for formulas.

Returns the history of learnt clauses, with no guarantees on order.

Returns the vector of assumptions used by the solver.

Called at the end of the search in case a model has been found.

Called at the end of the search in case a model has been found.

An iterator over the subterms of a formula that should be assigned a value (usually the poure subterms)

Read access to the vector of variables created

Generate some information about a theory specific lemmas.

Add local assumptions

Make a proposition from an integer.

Creates the conjunction of a list of formulas.

make_atom p builds the boolean formula equivalent to the atomic formula p.

Returns the variable linked with the given formula, and whether the atom associated with the formula is var.pa or var.na

make_clause name atoms size premise creates a clause with the given attributes.

make_cnf f returns a conjunctive normal form of f under the form: a list (which is a conjunction) of lists (which are disjunctions) of atomic formulas.

make_equiv p q creates the boolena formula "p is equivalent to q".

make_imply p q creates the boolean formula "p implies q".

Creates the negation of a boolean formula.

Creates the disjunction of a list of formulas.

make_xor p q creates the boolean formula "p xor q".

TODO:deprecate.

Merge two sorted atom list using a suitable comparison function.

Returns the model found if the formula is satisfiable.

Negation of atomic formulas.

Formula negation

Formula negation.

Add a new atom (i.e propositional formula) to the solver.

Add a new atom (i.e propositional formula) to the solver.

Add a new litteral (i.e term) to the solver.

Add a new litteral (i.e term) to the solver.

Returns a 'normalized' form of the formula, possibly negated (in which case return Negated).

Returns a 'normalized' form of the formula, possibly negated (in which case return Negated).

Constructors and destructors

Pop a decision level for local assumptions.

Debug function for atoms and clauses (very verbose)

A function for printing proofs in the desired format.

print fmt f prints the formula on the formatter fmt.

Print the given formula.

Printing function used among other thing for debugging.

Printing function used among other for debugging.

Printing function used among other thing for debugging.

Print the contents of the given atomic formulas.

Pretty printing functions for atoms and clauses

A nice looking printer for clauses, which sort the atoms before printing.

Given a clause, return a proof of that clause.

Given an atom a, returns a proof of the clause [a] if a is true at level 0

Given a conflict clause c, returns a proof of the empty clause.

Create a decision level for local assumptions.

Performs a "resolution step" on a sorted list of atoms.

Set debug level

Change the output formatter.

Accessors for elements

Try and solves the current set of assumptions.

Try and solves the current set of assumptions.

Returns the clauses coreesponding to the local assumptions.

Returns the sorted list of atoms of a clause.

Returns the current trail.

true_at_level0 a returns true if a was proved at level0, i.e.

Returns the unsat clause found at the toplevel, if it exists (i.e if solve has raised Unsat)

Returns the unsat core of a given proof.

Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof.