Module Smt (.ml)

module Smt: sig .. end
The Alt-Ergo zero SMT library

This SMT solver is derived from Alt-Ergo. It uses an efficient SAT solver and supports the following quantifier free theories:

This API makes heavy use of hash-consed strings. Please take a moment to look at Hstring.


Error handling


type error = 
| DuplicateTypeName of Hstring.t (*raised when a type is already declared*)
| DuplicateSymb of Hstring.t (*raised when a symbol is already declared*)
| UnknownType of Hstring.t (*raised when the given type is not declared*)
| UnknownSymb of Hstring.t (*raised when the given symbol is not declared*)
exception Error of error

Typing


module Type: sig .. end
Typing
module Symbol: sig .. end
Function symbols
module Variant: sig .. end
Variants

Building terms


module Term: sig .. end

Building formulas


module Formula: sig .. end

The SMT solver


exception Unsat of int list
The exception raised by Smt.Solver.check and Smt.Solver.assume when the formula is unsatisfiable.
val set_cc : bool -> unit
set_cc false deactivates congruence closure algorithm (true by default).
val set_arith : bool -> unit
set_arith false deactivates the theory of arithmetic (true by default).
val set_sum : bool -> unit
set_sum false deactivates the theory of enumerated data types (true by default).
module type Solver = sig .. end
module Make: 
functor (Options : sig
val profiling : bool
end) -> Solver
Functor to create several instances of the solver