Module Smt

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

module Type: sig .. end

Typing

module Symbol: sig .. end

Function symbols

module Variant: sig .. end

Variants

module Term: sig .. end

module Formula: sig .. end

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

module type Solver = sig .. end

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

Functor to create several instances of the solver