Module Smtlib.Make_Typed

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 'a sort
type 'a value
val assert_ : bool value -> unit
val bool : bool sort
val let_ : ?name:string -> 'a value -> ('a value -> 'b value) -> 'b value
val forall : ?name:string -> 'a sort -> ('a value -> bool value) -> bool value
val exists : ?name:string -> 'a sort -> ('a value -> bool value) -> bool value
val (=) : 'a value -> 'a value -> bool value
val (||) : bool value -> bool value -> bool value
val int : int sort
val numeral : int -> int value
val (<) : int value -> int value -> bool value
type ('a, 'b) array
val array : 'a sort -> 'b sort -> ('a, 'b) array sort
val select : ('a, 'b) array value -> 'a value -> 'b value
val store : ('a, 'b) array value -> 'a value -> 'b value -> ('a, 'b) array value
type bitvector
val bitvec : int -> bitvector sort
val bvlit : size:int -> Z.t -> bitvector value
val bvult : bitvector value -> bitvector value -> bool value
val bvule : bitvector value -> bitvector value -> bool value
val bvslt : bitvector value -> bitvector value -> bool value
val bvsle : bitvector value -> bitvector value -> bool value