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.

`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`

.

`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.