package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module implements the interface with the Z3 (or other) SMT solver

module Big_int = Nat_big_num
val opt_smt_verbose : bool Stdlib.ref

Print generated SMT problems (for debugging)

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 call_smt_solve_bitvector : Ast.l -> string -> (int * string) list -> (int * Ast.lit) list option
val solve_all_smt : Ast.l -> Ast.n_constraint -> Ast.kid -> Libsail.Ast_util.Big_int.num list option
val solve_unique_smt : Ast.l -> Ast.n_constraint -> Ast.kid -> Libsail.Ast_util.Big_int.num option