package libsail

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

Module Libsail.ConstraintSource

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

module Big_int = Nat_big_num
Sourceval opt_smt_verbose : bool ref

Print generated SMT problems (for debugging)

Sourceval set_solver : string -> unit
Sourcetype smt_result =
  1. | Unknown
  2. | Sat
  3. | Unsat
Sourceval load_digests : unit -> unit
Sourceval save_digests : unit -> unit
Sourceval constraint_to_smt : Ast.l -> Ast.n_constraint -> string * (Ast.kid -> string * bool) * string list
Sourceval call_smt_solve_bitvector : Ast.l -> string -> (int * string) list -> (int * Ast.lit) list option
Sourceval solve_smt : Ast.l -> Ast.kind Ast_util.Bindings.t -> Ast.n_constraint -> Ast.kid -> Libsail.Ast_util.Big_int.num option
Sourceval solve_all_smt : Ast.l -> Ast.kind Ast_util.Bindings.t -> Ast.n_constraint -> Ast.kid -> Libsail.Ast_util.Big_int.num list option
Sourceval solve_unique_smt : Ast.l -> Ast.kind Ast_util.Bindings.t -> Ast.n_constraint -> Ast.kid -> Libsail.Ast_util.Big_int.num option