Functor Smt.Make

module Make: functor (Dummy : sig
end) -> Solver

Functor to create several instances of the solver

Parameters:

Dummy : 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).