Module Smtlib.Make_Untyped

Parameters

module P : PARAM_S

Signature

include COMMON_S
type logic
type command
val qf_uf : logic
val qf_lia : logic
val qf_nia : logic
val qf_lra : logic
val qf_auflia : logic
val auflia : logic
val auflira : logic
val aufnira : logic
val lra : logic
val qf_idl : logic
val qf_rdl : logic
val qf_ufidl : logic
val qf_bv : logic
val qf_ax : logic
val qf_abv : logic
val qf_aubv : logic
val horn : logic
type satisfiable =
  1. | Sat
  2. | Unsat
  3. | Unknown
val check_sat : unit -> satisfiable
val set_logic : logic -> unit
val set_option : string -> unit
type sort
type value
val assert_ : value -> unit
val get_assignment : unit -> unit
val declare_var : ?name:string -> sort -> value
val define_var : ?name:string -> sort -> value -> value
val bool : sort
val let_ : ?name:string -> value -> (value -> value) -> value
val forall : ?name:string -> sort -> (value -> value) -> value
val exists : ?name:string -> sort -> (value -> value) -> value
val (=) : value -> value -> value
val (||) : value -> value -> value
val (&&) : value -> value -> value
val (=>) : value -> value -> value
val and_list : value list -> value
val or_list : value list -> value
val not : value -> value
val true_ : value
val false_ : value
val int : sort
val numeral : int -> value
val numeralz : Z.t -> value
val (<) : value -> value -> value
val (<=) : value -> value -> value
val (-) : value -> value -> value
val neg : value -> value
val (+) : value -> value -> value
val (*) : value -> value -> value
val div : value -> value -> value
val modu : value -> value -> value
val array : sort -> sort -> sort
val select : value -> value -> value
val store : value -> value -> value -> value
val bitvec : int -> sort
val bvlit : size:int -> Z.t -> value
val concat : value -> value -> value
val bvnot : value -> value
val bvneg : value -> value
val bvand : value -> value -> value
val bvor : value -> value -> value
val bvadd : value -> value -> value
val bvmul : value -> value -> value
val bvudiv : value -> value -> value
val bvurem : value -> value -> value
val bvshl : value -> value -> value
val bvlshr : value -> value -> value
val bvult : value -> value -> value
val extract : first:int -> last:int -> value -> value
val bvxor : value -> value -> value
val bvsdiv : value -> value -> value
val bvsrem : value -> value -> value
val bvsmod : value -> value -> value
val bvule : value -> value -> value
val bvslt : value -> value -> value
val bvsle : value -> value -> value
val bvashr : value -> value -> value
val sign_extend : int -> value -> value
val zero_extend : int -> value -> value