Up  

Functor Internal.Make

module Make: 
functor (St : Solver_types.S) -> 
functor (Th : Plugin_intf.S  with type term = St.term and type formula = St.formula and type proof = St.proof) -> 
functor (Dummy : sig
end) -> sig .. end
Parameters:
St : Solver_types.S
Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof
Dummy : sig end

Functor to create a solver parametrised by the atomic formulas and a theory.

Solving facilities

exception Unsat
exception UndecidedLit
val solve : unit -> unit

Try and solves the current set of assumptions.

val assume : ?tag:int -> St.formula list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val new_lit : St.term -> unit

Add a new litteral (i.e term) to the solver. This term will be decided on at some point during solving, wether it appears in clauses or not.

val new_atom : St.formula -> unit

Add a new atom (i.e propositional formula) to the solver. This formula will be decided on at some point during solving, wether it appears in clauses or not.

val push : unit -> unit

Create a decision level for local assumptions.

val pop : unit -> unit

Pop a decision level for local assumptions.

val local : St.formula list -> unit

Add local assumptions

Propositional models

val eval : St.formula -> bool

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

val eval_level : St.formula -> 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.

val model : unit -> (St.term * St.term) list

Returns the model found if the formula is satisfiable.

val check : unit -> bool

Check the satisfiability of the current model. Only has meaning if the solver finished proof search and has returned Sat.

Proofs and Models

module Proof: Res.S  with module St = St
val unsat_conflict : unit -> St.clause option

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

val full_slice : unit -> (St.term, St.formula, St.proof) Plugin_intf.slice

View the current state of the trail as a slice. Mainly useful when the solver has reached a SAT conclusion.

Internal data

These functions expose some internal data stored by the solver, as such great care should be taken to ensure not to mess with the values returned.

val trail : unit -> St.t Vec.t

Returns the current trail. *DO NOT MUTATE*

val hyps : unit -> St.clause Vec.t

Returns the vector of assumptions used by the solver. May be slightly different from the clauses assumed because of top-level simplification of clauses. *DO NOT MUTATE*

val temp : unit -> St.clause Vec.t

Returns the clauses coreesponding to the local assumptions. All clauses in this vec are assured to be unit clauses. *DO NOT MUTATE*

val history : unit -> St.clause Vec.t

Returns the history of learnt clauses, with no guarantees on order. *DO NOT MUTATE*