Module type Smt_sig.S

module type S = sig .. end

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

val report : Format.formatter -> error -> unit

type check_strategy =

`\|`	`Lazy`
`\|`	`Eager`

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

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