Module type Smt_sig.S.Solver

module type Solver = sig .. end

This SMT solver is imperative in the sense that it maintains a global context. To create different instances of this solver use the functor Smt.Make.

A typical use of this solver is to do the following :

          clear ();
          assume f_1;
          ...
            assume f_n;
          check ();

val check_strategy : Smt_sig.S.check_strategy

The stragey used for preforming check-sat. Lazy means that we chech the context only when needed, whereas Eager means the context should be checked after each assertion.

Profiling functions

val get_time : unit -> float

get_time () returns the cumulated time spent in the solver in seconds.

val get_calls : unit -> int

get_calls () returns the cumulated number of calls to Smt_sig.S.Solver.check.

Main API of the solver

val clear : unit -> unit

clear () clears the context of the solver. Use this after Smt_sig.S.Solver.check raised Smt_sig.S.Unsat or if you want to restart the solver.

val assume : id:int -> Smt_sig.S.Formula.t -> unit

assume id f adds the formula f to the context of the solver with identifier id. This function only performs unit propagation.

Raises Smt_sig.S.Unsat if the context becomes inconsistent after unit propagation.

val check : unit -> unit

check () runs the solver on its context. If () is returned then the context is satifiable.

Raises Smt_sig.S.Unsat [id_1; ...; id_n] if the context is unsatisfiable. id_1, ..., id_n is the unsat core (returned as the identifiers of the formulas given to the solver).

val entails : Smt_sig.S.Formula.t -> bool

entails f returns true if the context of the solver entails the formula f. It doesn't modify the context of the solver (the effect is as if the state is saved when this function is called and restored on exit).

val push : unit -> unit

Push the current context on a stack.

val pop : unit -> unit

Pop the last context from the stack and forget what was done since the last push.