package sail

  1. Overview
  2. Docs
module Big_int = Nat_big_num
val opt_smt_verbose : bool ref
val set_solver : string -> unit
type smt_result =
  1. | Unknown
  2. | Sat
  3. | Unsat
val load_digests : unit -> unit
val save_digests : unit -> unit
val call_smt : Ast.l -> Ast.n_constraint -> smt_result
val solve_smt : Ast.l -> Ast.n_constraint -> Ast.kid -> Ast_util.Big_int.num option
val solve_all_smt : Ast.l -> Ast.n_constraint -> Ast.kid -> Ast_util.Big_int.num list option
val solve_unique_smt : Ast.l -> Ast.n_constraint -> Ast.kid -> Ast_util.Big_int.num option