sig
type error =
DuplicateTypeName of Hstring.t
| DuplicateSymb of Hstring.t
| UnknownType of Hstring.t
| UnknownSymb of Hstring.t
exception Error of Smt.error
module Type :
sig
type t = Hstring.t
val type_int : Smt.Type.t
val type_real : Smt.Type.t
val type_bool : Smt.Type.t
val type_proc : Smt.Type.t
val declare : Hstring.t -> Hstring.t list -> unit
val all_constructors : unit -> Hstring.t list
val constructors : Smt.Type.t -> Hstring.t list
end
module Symbol :
sig
type t = Hstring.t
val declare : Hstring.t -> Smt.Type.t list -> Smt.Type.t -> unit
val type_of : Smt.Symbol.t -> Smt.Type.t list * Smt.Type.t
val has_abstract_type : Smt.Symbol.t -> bool
val has_type_proc : Smt.Symbol.t -> bool
val declared : Smt.Symbol.t -> bool
end
module Variant :
sig
val init : (Smt.Symbol.t * Smt.Type.t) list -> unit
val close : unit -> unit
val assign_constr : Smt.Symbol.t -> Hstring.t -> unit
val assign_var : Smt.Symbol.t -> Smt.Symbol.t -> unit
val print : unit -> unit
val get_variants : Smt.Symbol.t -> Hstring.HSet.t
end
module rec Term :
sig
type t
type operator = Plus | Minus | Mult | Div | Modulo
val make_int : Num.num -> Smt.Term.t
val make_real : Num.num -> Smt.Term.t
val make_app : Smt.Symbol.t -> Smt.Term.t list -> Smt.Term.t
val make_arith :
Smt.Term.operator -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
val make_ite : Smt.Formula.t -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
val is_int : Smt.Term.t -> bool
val is_real : Smt.Term.t -> bool
val t_true : Smt.Term.t
val t_false : Smt.Term.t
end
and Formula :
sig
type comparator = Eq | Neq | Le | Lt
type combinator = And | Or | Imp | Not
type t =
Lit of Literal.LT.t
| Comb of Smt.Formula.combinator * Smt.Formula.t list
val f_true : Smt.Formula.t
val f_false : Smt.Formula.t
val make_lit :
Smt.Formula.comparator -> Smt.Term.t list -> Smt.Formula.t
val make :
Smt.Formula.combinator -> Smt.Formula.t list -> Smt.Formula.t
val make_cnf : Smt.Formula.t -> Literal.LT.t list list
val print : Format.formatter -> Smt.Formula.t -> unit
end
exception Unsat of int list
val set_cc : bool -> unit
module type Solver =
sig
type state
val get_time : unit -> float
val get_calls : unit -> int
val clear : unit -> unit
val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
val check : ?profiling:bool -> unit -> unit
val save_state : unit -> Smt.Solver.state
val restore_state : Smt.Solver.state -> unit
val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
end
module Make : functor (Dummy : sig end) -> Solver
end