Up  

Module type Smt.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 Alt-Ergo Zero use the functor Smt.Make.

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

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

type state
The type of the internal state of the solver (see Smt.Solver.save_state and Smt.Solver.restore_state).

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.Solver.check.

Main API of the solver


val clear : unit -> unit
clear () clears the context of the solver. Use this after Smt.Solver.check raised Smt.Unsat or if you want to restart the solver.
val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
assume ~profiling:b f id adds the formula f to the context of the solver with idetifier id. This function only performs unit propagation.
profiling : if set to true then profiling information (time) will be computed (expensive because of system calls).

Raises Smt.Unsat if the context becomes inconsistent after unit propagation.

val check : ?profiling:bool -> unit -> unit
check () runs Alt-Ergo Zero on its context. If () is returned then the context is satifiable.
profiling : if set to true then profiling information (time) will be computed (expensive because of system calls).

Raises Smt.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 save_state : unit -> state
save_state () returns a copy of the current state of the solver.
val restore_state : state -> unit
restore_state s restores a previously saved state s.
val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
entails ~id f returns true if the context of the solver entails the formula f. It doesn't modify the context of the solver (the state is saved when this function is called and restored on exit).