Module Solver_intf

module Solver_intf: sig .. end

Interface for Solvers

This modules defines the safe external interface for solvers. Solvers that implements this interface can be obtained using the Make functor in Solver or Mcsolver.

type ('term, 'form) sat_state = {

`eval : 'form -> bool;`	`(*`	Returns the valuation of a formula in the current state of the sat solver. Raises `UndecidedLit` if the literal is not decided	`*)`
`eval_level : 'form -> bool * int;`	`(*`	Return the current assignement of the literals, as well as its decision level. If the level is 0, then it is necessary for the atom to have this value; otherwise it is due to choices that can potentially be backtracked. Raises `UndecidedLit` if the literal is not decided	`*)`
`iter_trail : ('form -> unit) -> ('term -> unit) -> unit;`	`(*`	Iter thorugh the formulas and terms in order of decision/propagation (starting from the first propagation, to the last propagation).	`*)`
`model : unit -> ('term * 'term) list;`	`(*`	Returns the model found if the formula is satisfiable.	`*)`

}

The type of values returned when the solver reaches a SAT state.

type ('clause, 'proof) unsat_state = {

	`unsat_conflict : unit -> 'clause;`	`(*`	Returns the unsat clause found at the toplevel	`*)`
	`get_proof : unit -> 'proof;`	`(*`	returns a persistent proof of the empty clause from the Unsat result.	`*)`

}

The type of values returned when the solver reaches an UNSAT state.

module type S = sig .. end

The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.