From 1f4cff5445cc145a88de2045a7fb4e7fcd6b3dd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Recoules?= Date: Wed, 8 Nov 2023 15:38:48 +0100 Subject: [PATCH] upgrade bitwuzla 'refactor-node-manager' --- bitwuzla-cxx.opam | 6 +- bitwuzla_cxx.ml | 1964 ++++++++++++++++- bitwuzla_cxx.mli | 926 ++++---- cxx_stubs.cpp | 275 ++- dune | 11 +- dune-project | 2 +- manager.ml | 3 + solver.ml | 2 +- vendor/bitwuzla | 2 +- vendor/dune | 23 +- ...NodeManager-global-from-thread-local.patch | 25 - ...x-compilation-with-older-GCC-version.patch | 27 - 12 files changed, 2569 insertions(+), 697 deletions(-) create mode 100644 manager.ml delete mode 100644 vendor/patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch delete mode 100644 vendor/patch/0003-Fix-compilation-with-older-GCC-version.patch diff --git a/bitwuzla-cxx.opam b/bitwuzla-cxx.opam index 06bc016..289b4e2 100644 --- a/bitwuzla-cxx.opam +++ b/bitwuzla-cxx.opam @@ -16,7 +16,7 @@ doc: "https://bitwuzla.github.io/docs/ocaml/" bug-reports: "https://github.com/bitwuzla/ocaml-bitwuzla/issues" depends: [ "dune" {>= "3.7"} - "ocaml" {>= "4.12" & < "5"} + "ocaml" {>= "4.12"} "conf-git" {build} "conf-gcc" {build} "conf-g++" {build} @@ -25,10 +25,6 @@ depends: [ "ppx_expect" {with-test & >= "v0.13"} "odoc" {with-doc} ] -conflicts: [ - "bitwuzla-c" - "bitwuzla" {< "0.1"} -] build: [ ["dune" "subst"] {dev} [ diff --git a/bitwuzla_cxx.ml b/bitwuzla_cxx.ml index 467cfa4..3d793ce 100644 --- a/bitwuzla_cxx.ml +++ b/bitwuzla_cxx.ml @@ -23,116 +23,118 @@ let () = Callback.register "Format.pp_close_box" Format.pp_close_box; init_format () -module Options = Options -module Sort = Sort - -external mk_array_sort : Sort.t -> Sort.t -> Sort.t +external mk_array_sort : Manager.t -> Sort.t -> Sort.t -> Sort.t = "ocaml_bitwuzla_cxx_mk_array_sort" -external mk_bool_sort : unit -> Sort.t = "ocaml_bitwuzla_cxx_mk_bool_sort" +external mk_bool_sort : Manager.t -> Sort.t = "ocaml_bitwuzla_cxx_mk_bool_sort" -external mk_bv_sort : (int[@untagged]) -> Sort.t +external mk_bv_sort : Manager.t -> (int[@untagged]) -> Sort.t = "ocaml_bitwuzla_cxx_mk_bv_sort" "native_bitwuzla_cxx_mk_bv_sort" -external mk_fp_sort : (int[@untagged]) -> (int[@untagged]) -> Sort.t +external mk_fp_sort : + Manager.t -> (int[@untagged]) -> (int[@untagged]) -> Sort.t = "ocaml_bitwuzla_cxx_mk_fp_sort" "native_bitwuzla_cxx_mk_fp_sort" -external mk_fun_sort : Sort.t array -> Sort.t -> Sort.t +external mk_fun_sort : Manager.t -> Sort.t array -> Sort.t -> Sort.t = "ocaml_bitwuzla_cxx_mk_fun_sort" -external mk_rm_sort : unit -> Sort.t = "ocaml_bitwuzla_cxx_mk_rm_sort" +external mk_rm_sort : Manager.t -> Sort.t = "ocaml_bitwuzla_cxx_mk_rm_sort" -external mk_uninterpreted_sort : ?symbol:string -> unit -> Sort.t +external mk_uninterpreted_sort : Manager.t -> ?symbol:string -> unit -> Sort.t = "ocaml_bitwuzla_cxx_mk_uninterpreted_sort" -module RoundingMode = RoundingMode -module Kind = Kind -module Term = Term +external mk_true : Manager.t -> Term.t = "ocaml_bitwuzla_cxx_mk_true" -external mk_true : unit -> Term.t = "ocaml_bitwuzla_cxx_mk_true" +external mk_false : Manager.t -> Term.t = "ocaml_bitwuzla_cxx_mk_false" -external mk_false : unit -> Term.t = "ocaml_bitwuzla_cxx_mk_false" +external mk_bv_zero : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_bv_zero" -external mk_bv_zero : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_zero" +external mk_bv_one : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_bv_one" -external mk_bv_one : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_one" +external mk_bv_ones : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_bv_ones" -external mk_bv_ones : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_ones" - -external mk_bv_min_signed : Sort.t -> Term.t +external mk_bv_min_signed : Manager.t -> Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_min_signed" -external mk_bv_max_signed : Sort.t -> Term.t +external mk_bv_max_signed : Manager.t -> Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_max_signed" -external mk_bv_value : Sort.t -> string -> (int[@untagged]) -> Term.t +external mk_bv_value : + Manager.t -> Sort.t -> string -> (int[@untagged]) -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_value" "native_bitwuzla_cxx_mk_bv_value" -external mk_bv_value_int : Sort.t -> (int[@untagged]) -> Term.t +external mk_bv_value_int : Manager.t -> Sort.t -> (int[@untagged]) -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_value_int" "native_bitwuzla_cxx_mk_bv_value_int64" -external mk_bv_value_int64 : Sort.t -> (int64[@unboxed]) -> Term.t +external mk_bv_value_int64 : Manager.t -> Sort.t -> (int64[@unboxed]) -> Term.t = "ocaml_bitwuzla_cxx_mk_bv_value_int64" "native_bitwuzla_cxx_mk_bv_value_int64" -external mk_fp_pos_zero : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_pos_zero" +external mk_fp_pos_zero : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_fp_pos_zero" -external mk_fp_neg_zero : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_neg_zero" +external mk_fp_neg_zero : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_fp_neg_zero" -external mk_fp_pos_inf : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_pos_inf" +external mk_fp_pos_inf : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_fp_pos_inf" -external mk_fp_neg_inf : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_neg_inf" +external mk_fp_neg_inf : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_fp_neg_inf" -external mk_fp_nan : Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_nan" +external mk_fp_nan : Manager.t -> Sort.t -> Term.t + = "ocaml_bitwuzla_cxx_mk_fp_nan" -external mk_fp_value : Term.t -> Term.t -> Term.t -> Term.t +external mk_fp_value : Manager.t -> Term.t -> Term.t -> Term.t -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_value" -external mk_fp_value_from_real : Sort.t -> Term.t -> string -> Term.t +external mk_fp_value_from_real : + Manager.t -> Sort.t -> Term.t -> string -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_value_from_real" external mk_fp_value_from_rational : - Sort.t -> Term.t -> string -> string -> Term.t + Manager.t -> Sort.t -> Term.t -> string -> string -> Term.t = "ocaml_bitwuzla_cxx_mk_fp_value_from_rational" -external mk_rm_value : (int[@untagged]) -> Term.t +external mk_rm_value : Manager.t -> (int[@untagged]) -> Term.t = "ocaml_bitwuzla_cxx_mk_rm_value" "native_bitwuzla_cxx_mk_rm_value" -let mk_rm_value t = mk_rm_value (RoundingMode.to_cxx t) - -external mk_term1 : (int[@untagged]) -> Term.t -> Term.t +external mk_term1 : Manager.t -> (int[@untagged]) -> Term.t -> Term.t = "ocaml_bitwuzla_cxx_mk_term1" "native_bitwuzla_cxx_mk_term1" -let mk_term1 k t = mk_term1 (Kind.to_cxx k) t - -external mk_term2 : (int[@untagged]) -> Term.t -> Term.t -> Term.t +external mk_term2 : Manager.t -> (int[@untagged]) -> Term.t -> Term.t -> Term.t = "ocaml_bitwuzla_cxx_mk_term2" "native_bitwuzla_cxx_mk_term2" -let mk_term2 k t1 t2 = mk_term2 (Kind.to_cxx k) t1 t2 - -external mk_term3 : (int[@untagged]) -> Term.t -> Term.t -> Term.t -> Term.t +external mk_term3 : + Manager.t -> (int[@untagged]) -> Term.t -> Term.t -> Term.t -> Term.t = "ocaml_bitwuzla_cxx_mk_term3" "native_bitwuzla_cxx_mk_term3" -let mk_term3 k t1 t2 t3 = mk_term3 (Kind.to_cxx k) t1 t2 t3 - external mk_term1_indexed1 : - (int[@untagged]) -> Term.t -> (int[@untagged]) -> Term.t + Manager.t -> (int[@untagged]) -> Term.t -> (int[@untagged]) -> Term.t = "ocaml_bitwuzla_cxx_mk_term1_indexed1" "native_bitwuzla_cxx_mk_term1_indexed1" -let mk_term1_indexed1 k t i = mk_term1_indexed1 (Kind.to_cxx k) t i - external mk_term1_indexed2 : - (int[@untagged]) -> Term.t -> (int[@untagged]) -> (int[@untagged]) -> Term.t + Manager.t -> + (int[@untagged]) -> + Term.t -> + (int[@untagged]) -> + (int[@untagged]) -> + Term.t = "ocaml_bitwuzla_cxx_mk_term1_indexed2" "native_bitwuzla_cxx_mk_term1_indexed2" -let mk_term1_indexed2 k t i j = mk_term1_indexed2 (Kind.to_cxx k) t i j - external mk_term2_indexed1 : - (int[@untagged]) -> Term.t -> Term.t -> (int[@untagged]) -> Term.t + Manager.t -> + (int[@untagged]) -> + Term.t -> + Term.t -> + (int[@untagged]) -> + Term.t = "ocaml_bitwuzla_cxx_mk_term2_indexed1" "native_bitwuzla_cxx_mk_term2_indexed1" -let mk_term2_indexed1 k t1 t2 i = mk_term2_indexed1 (Kind.to_cxx k) t1 t2 i - external mk_term2_indexed2 : + Manager.t -> (int[@untagged]) -> Term.t -> Term.t -> @@ -141,27 +143,1859 @@ external mk_term2_indexed2 : Term.t = "ocaml_bitwuzla_cxx_mk_term2_indexed2" "native_bitwuzla_cxx_mk_term2_indexed2" -let mk_term2_indexed2 k t1 t2 i j = mk_term2_indexed2 (Kind.to_cxx k) t1 t2 i j - -external mk_term : (int[@untagged]) -> Term.t array -> int array -> Term.t +external mk_term : + Manager.t -> (int[@untagged]) -> Term.t array -> int array -> Term.t = "ocaml_bitwuzla_cxx_mk_term" "native_bitwuzla_cxx_mk_term" -let mk_term k ?(indices = [||]) args = mk_term (Kind.to_cxx k) args indices - -external mk_const : ?symbol:string -> Sort.t -> Term.t +external mk_const : Manager.t -> ?symbol:string -> Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_const" -external mk_const_array : Sort.t -> Term.t -> Term.t +external mk_const_array : Manager.t -> Sort.t -> Term.t -> Term.t = "ocaml_bitwuzla_cxx_mk_const_array" -external mk_var : ?symbol:string -> Sort.t -> Term.t +external mk_var : Manager.t -> ?symbol:string -> Sort.t -> Term.t = "ocaml_bitwuzla_cxx_mk_var" -external substitute_term : Term.t -> (Term.t * Term.t) array -> Term.t +external substitute_term : + Manager.t -> Term.t -> (Term.t * Term.t) array -> Term.t = "ocaml_bitwuzla_cxx_substitute_term" -external substitute_terms : Term.t array -> (Term.t * Term.t) array -> unit +external substitute_terms : + Manager.t -> Term.t array -> (Term.t * Term.t) array -> unit = "ocaml_bitwuzla_cxx_substitute_terms" -module Result = Result -module Solver = Solver +module Options = Options + +module type S = sig + module Sort : sig + (** {1:sort Sort} *) + + type t + (** A Bitwuzla sort. *) + + (** {2:sort_util Util} *) + + val hash : t -> int + (** + [hash t] + compute the hash value for a sort. + + @param t The sort. + + @return The hash value of the sort. + *) + + val equal : t -> t -> bool + (** + [equal a b] + Syntactical equality operator. + + @param a The first sort. + @param b The second sort. + @return True if the given sorts are equal. + *) + + val compare : t -> t -> int + (** + [compare a b] + Syntactical comparison operator. + + @param a The first sort. + @param b The second sort. + @return Zero if the given sorts are equal, + a positive number if [a] > [b], + a negative number otherwise. + *) + + val pp : Format.formatter -> t -> unit + (** + [pp formatter t] + print sort. + + @param t The sort. + @param formatter The outpout formatter. + *) + + val to_string : t -> string + (** + [to_string t] + get string representation of this sort. + + @return String representation of this sort. + *) + + (** {2:sort_query Query} *) + + val id : t -> int64 + (** + [id t] + get the id of this sort. + + @param t The sort. + @return The id value of the sort. + *) + + val bv_size : t -> int + (** + [bv_size t] + get the size of a bit-vector sort. + + Requires that given sort is a bit-vector sort. + + @param t The sort. + + @return The size of the bit-vector sort. + *) + + val fp_exp_size : t -> int + (** + [fp_exp_size sort] + get the exponent size of a floating-point sort. + + Requires that given sort is a floating-point sort. + + @param t The sort. + + @return The exponent size of the floating-point sort. + *) + + val fp_sig_size : t -> int + (** + [fp_sig_size t] + get the significand size of a floating-point sort. + + Requires that given sort is a floating-point sort. + + @param t The sort. + + @return The significand size of the floating-point sort. + *) + + val array_index : t -> t + (** + [array_index t] + get the index sort of an array sort. + + Requires that given sort is an array sort. + + @param t The sort. + + @return The index sort of the array sort. + *) + + val array_element : t -> t + (** + [array_element t] + get the element sort of an array sort. + + Requires that given sort is an array sort. + + @param t The sort. + + @return The element sort of the array sort. + *) + + val fun_domain : t -> t array + (** + [fun_domain_sorts t] + get the domain sorts of a function sort. + + Requires that given sort is a function sort. + + @param t The sort. + + @return The domain sorts of the function sort as an array of sort. + *) + + val fun_codomain : t -> t + (** + [fun_codomain t] + get the codomain sort of a function sort. + + Requires that given sort is a function sort. + + @param t The sort. + + @return The codomain sort of the function sort. + *) + + val fun_arity : t -> int + (** + [fun_arity t] + get the arity of a function sort. + + @param t The sort. + + @return The number of arguments of the function sort. + *) + + val uninterpreted_symbol : t -> string + (** + [uninterpreted_symbol t] + get the symbol of an uninterpreted sort. + + @param t The sort. + + @return The symbol. + + @raise Not_found if no symbol is defined. + *) + + val is_array : t -> bool + (** + [is_array t] + determine if a sort is an array sort. + + @param t The sort. + + @return [true] if [t] is an array sort. + *) + + val is_bool : t -> bool + (** + [is_bool t] + determine if a sort is a Boolean sort. + + @param t The sort. + + @return [true] if [t] is a Boolean sort. + *) + + val is_bv : t -> bool + (** + [is_bv t] + determine if a sort is a bit-vector sort. + + @param t The sort. + + @return [true] if [t] is a bit-vector sort. + *) + + val is_fp : t -> bool + (** + [is_fp t] + determine if a sort is a floating-point sort. + + @param t The sort. + + @return [true] if [t] is a floating-point sort. + *) + + val is_fun : t -> bool + (** + [is_fun t] + determine if a sort is a function sort. + + @param t The sort. + + @return [true] if [t] is a function sort. + *) + + val is_rm : t -> bool + (** + [is_rm t] + determine if a sort is a Roundingmode sort. + + @param t The sort. + + @return [true] if [t] is a Roundingmode sort. + *) + + val is_uninterpreted : t -> bool + (** + [is_uninterpreted t] + determine if a sort is an uninterpreted sort. + + @param t The sort. + + @return [true] if [t] is an uninterpreted sort. + *) + end + + module RoundingMode : sig + (** + Rounding mode for floating-point operations. + + For some floating-point operations, infinitely precise results may not be + representable in a given format. Hence, they are rounded modulo one of five + rounding modes to a representable floating-point number. + + The following rounding modes follow the SMT-LIB theory for floating-point + arithmetic, which in turn is based on IEEE Standard 754. + The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE + Standard 754. + *) + type t = + | Rne + (** Round to the nearest even number. + If the two nearest floating-point numbers bracketing an unrepresentable + infinitely precise result are equally near, the one with an even least + significant digit will be delivered. + + SMT-LIB: [RNE] roundNearestTiesToEven + *) + | Rna + (** Round to the nearest number away from zero. + If the two nearest floating-point numbers bracketing an unrepresentable + infinitely precise result are equally near, the one with larger + magnitude will be selected. + + SMT-LIB: [RNA] roundNearestTiesToAway + *) + | Rtn + (** Round towards negative infinity (-oo). + The result shall be the format’s floating-point number (possibly -oo) + closest to and no less than the infinitely precise result. + + SMT-LIB: [RTN] roundTowardNegative + *) + | Rtp + (** Round towards positive infinity (+oo). + The result shall be the format’s floating-point number (possibly +oo) + closest to and no less than the infinitely precise result. + + SMT-LIB: [RTP] roundTowardPositive + *) + | Rtz + (** Round towards zero. + The result shall be the format’s floating-point number closest to and no + greater in magnitude than the infinitely precise result. + + SMT-LIB: [RTZ] roundTowardZero + *) + + val to_string : t -> string + (** + [to_string t] + get string representation of this rounding mode. + + @return String representation of this rounding mode. + *) + end + + module Kind : sig + (** The term kind. *) + type t = + | Constant (** First order constant. *) + | Const_array (** Constant array. *) + | Value (** Value. *) + | Variable (** Bound variable. *) + | And (** Boolean and. + + SMT-LIB: [and] *) + | Distinct (** Disequality. + + SMT-LIB: [distinct] *) + | Equal (** Equality. + + SMT-LIB: [=] *) + | Iff (** Boolean if and only if. + + SMT-LIB: [=] *) + | Implies (** Boolean implies. + + SMT-LIB: [=>] *) + | Not (** Boolean not. + + SMT-LIB: [not] *) + | Or (** Boolean or. + + SMT-LIB: [or] *) + | Xor (** Boolean xor. + + SMT-LIB: [xor] *) + | Ite (** If-then-else. + + SMT-LIB: [ite] *) + | Exists (** Existential quantification. + + SMT-LIB: [exists] *) + | Forall + (** Universal quantification. + + SMT-LIB: [forall] *) + | Apply (** Function application. *) + | Lambda (** Lambda. *) + | Select (** Array select. + + SMT-LIB: [select] *) + | Store (** Array store. + + SMT-LIB: [store] *) + | Bv_add (** Bit-vector addition. + + SMT-LIB: [bvadd] *) + | Bv_and (** Bit-vector and. + + SMT-LIB: [bvand] *) + | Bv_ashr + (** Bit-vector arithmetic right shift. + + SMT-LIB: [bvashr] *) + | Bv_comp + (** Bit-vector comparison. + + SMT-LIB: [bvcomp] *) + | Bv_concat + (** Bit-vector concat. + + SMT-LIB: [concat] *) + | Bv_dec + (** Bit-vector decrement. + + Decrement by one. *) + | Bv_inc + (** Bit-vector increment. + + Increment by one. *) + | Bv_mul + (** Bit-vector multiplication. + + SMT-LIB: [bvmul] *) + | Bv_nand (** Bit-vector nand. + + SMT-LIB: [bvnand] *) + | Bv_neg + (** Bit-vector negation (two's complement). + + SMT-LIB: [bvneg] *) + | Bv_nor (** Bit-vector nor. + + SMT-LIB: [bvnor] *) + | Bv_not + (** Bit-vector not (one's complement). + + SMT-LIB: [bvnot] *) + | Bv_or (** Bit-vector or. + + SMT-LIB: [bvor] *) + | Bv_redand + (** Bit-vector and reduction. + + Bit-wise {b and} reduction, all bits are {b and}'ed together into a single + bit. + This corresponds to bit-wise {b and} reduction as known from Verilog. *) + | Bv_redor + (** Bit-vector reduce or. + + Bit-wise {b or} reduction, all bits are {b or}'ed together into a single + bit. + This corresponds to bit-wise {b or} reduction as known from Verilog. *) + | Bv_redxor + (** Bit-vector reduce xor. + + Bit-wise {b xor} reduction, all bits are {b xor}'ed together into a + single bit. + This corresponds to bit-wise {b xor} reduction as known from Verilog. *) + | Bv_rol + (** Bit-vector rotate left (not indexed). + + This is a non-indexed variant of SMT-LIB [rotate_left]. *) + | Bv_ror + (** Bit-vector rotate right. + + This is a non-indexed variant of SMT-LIB [rotate_right]. *) + | Bv_saddo + (** Bit-vector signed addition overflow test. + + Single bit to indicate if signed addition produces an overflow. *) + | Bv_sdivo + (** Bit-vector signed division overflow test. + + Single bit to indicate if signed division produces an overflow. *) + | Bv_sdiv + (** Bit-vector signed division. + + SMT-LIB: [bvsdiv] *) + | Bv_sge + (** Bit-vector signed greater than or equal. + + SMT-LIB: [bvsge] *) + | Bv_sgt + (** Bit-vector signed greater than. + + SMT-LIB: [bvsgt] *) + | Bv_shl + (** Bit-vector logical left shift. + + SMT-LIB: [bvshl] *) + | Bv_shr + (** Bit-vector logical right shift. + + SMT-LIB: [bvshr] *) + | Bv_sle + (** Bit-vector signed less than or equal. + + SMT-LIB: [bvsle] *) + | Bv_slt (** Bit-vector signed less than. + + SMT-LIB: [bvslt] *) + | Bv_smod (** Bit-vector signed modulo. + + SMT-LIB: [bvsmod] *) + | Bv_smulo + (** Bit-vector signed multiplication overflow test. + + SMT-LIB: [bvsmod] *) + | Bv_srem + (** Bit-vector signed remainder. + + SMT-LIB: [bvsrem] *) + | Bv_ssubo + (** Bit-vector signed subtraction overflow test. + + Single bit to indicate if signed subtraction produces an overflow. *) + | Bv_sub + (** Bit-vector subtraction. + + SMT-LIB: [bvsub] *) + | Bv_uaddo + (** Bit-vector unsigned addition overflow test. + + Single bit to indicate if unsigned addition produces an overflow. *) + | Bv_udiv + (** Bit-vector unsigned division. + + SMT-LIB: [bvudiv] *) + | Bv_uge + (** Bit-vector unsigned greater than or equal. + + SMT-LIB: [bvuge] *) + | Bv_ugt + (** Bit-vector unsigned greater than. + + SMT-LIB: [bvugt] *) + | Bv_ule + (** Bit-vector unsigned less than or equal. + + SMT-LIB: [bvule] *) + | Bv_ult + (** Bit-vector unsigned less than. + + SMT-LIB: [bvult] *) + | Bv_umulo + (** Bit-vector unsigned multiplication overflow test. + + Single bit to indicate if unsigned multiplication produces + an overflow. *) + | Bv_urem + (** Bit-vector unsigned remainder. + + SMT-LIB: [bvurem] *) + | Bv_usubo + (** Bit-vector unsigned subtraction overflow test. + + Single bit to indicate if unsigned subtraction produces an overflow. *) + | Bv_xnor (** Bit-vector xnor. + + SMT-LIB: [bvxnor] *) + | Bv_xor (** Bit-vector xor. + + SMT-LIB: [bvxor] *) + | Bv_extract + (** Bit-vector extract. + + SMT-LIB: [extract] (indexed) *) + | Bv_repeat + (** Bit-vector repeat. + + SMT-LIB: [repeat] (indexed) *) + | Bv_roli + (** Bit-vector rotate left by integer. + + SMT-LIB: [rotate_left] (indexed) *) + | Bv_rori + (** Bit-vector rotate right by integer. + + SMT-LIB: [rotate_right] (indexed) *) + | Bv_sign_extend + (** Bit-vector sign extend. + + SMT-LIB: [sign_extend] (indexed) *) + | Bv_zero_extend + (** Bit-vector zero extend. + + SMT-LIB: [zero_extend] (indexed) *) + | Fp_abs + (** Floating-point absolute value. + + SMT-LIB: [fp.abs] *) + | Fp_add + (** Floating-point addition. + + SMT-LIB: [fp.add] *) + | Fp_div + (** Floating-point division. + + SMT-LIB: [fp.div] *) + | Fp_equal + (** Floating-point equality. + + SMT-LIB: [fp.eq] *) + | Fp_fma + (** Floating-point fused multiplcation and addition. + + SMT-LIB: [fp.fma] *) + | Fp_fp + (** Floating-point IEEE 754 value. + + SMT-LIB: [fp] *) + | Fp_geq + (** Floating-point greater than or equal. + + SMT-LIB: [fp.geq] *) + | Fp_gt + (** Floating-point greater than. + + SMT-LIB: [fp.gt] *) + | Fp_is_inf + (** Floating-point is infinity tester. + + SMT-LIB: [fp.isInfinite] *) + | Fp_is_nan + (** Floating-point is Nan tester. + + SMT-LIB: [fp.isNaN] *) + | Fp_is_neg + (** Floating-point is negative tester. + + SMT-LIB: [fp.isNegative] *) + | Fp_is_normal + (** Floating-point is normal tester. + + SMT-LIB: [fp.isNormal] *) + | Fp_is_pos + (** Floating-point is positive tester. + + SMT-LIB: [fp.isPositive] *) + | Fp_is_subnormal + (** Floating-point is subnormal tester. + + SMT-LIB: [fp.isSubnormal] *) + | Fp_is_zero + (** Floating-point is zero tester. + + SMT-LIB: [fp.isZero] *) + | Fp_leq + (** Floating-point less than or equal. + + SMT-LIB: [fp.leq] *) + | Fp_lt + (** Floating-point less than. + + SMT-LIB: [fp.lt] *) + | Fp_max (** Floating-point max. + + SMT-LIB: [fp.max] *) + | Fp_min (** Floating-point min. + + SMT-LIB: [fp.min] *) + | Fp_mul + (** Floating-point multiplcation. + + SMT-LIB: [fp.mul] *) + | Fp_neg + (** Floating-point negation. + + SMT-LIB: [fp.neg] *) + | Fp_rem + (** Floating-point remainder. + + SMT-LIB: [fp.rem] *) + | Fp_rti + (** Floating-point round to integral. + + SMT-LIB: [fp.roundToIntegral] *) + | Fp_sqrt + (** Floating-point round to square root. + + SMT-LIB: [fp.sqrt] *) + | Fp_sub + (** Floating-point round to subtraction. + + SMT-LIB: [fp.sqrt] *) + | Fp_to_fp_from_bv + (** Floating-point to_fp from IEEE 754 bit-vector. + + SMT-LIB: [to_fp] (indexed) *) + | Fp_to_fp_from_fp + (** Floating-point to_fp from floating-point. + + SMT-LIB: [to_fp] (indexed) *) + | Fp_to_fp_from_sbv + (** Floating-point to_fp from signed bit-vector value. + + SMT-LIB: [to_fp] (indexed) *) + | Fp_to_fp_from_ubv + (** Floating-point to_fp from unsigned bit-vector value. + + SMT-LIB: [to_fp_unsigned] (indexed) *) + | Fp_to_sbv + (** Floating-point to_sbv. + + SMT-LIB: [fp.to_sbv] (indexed) *) + | Fp_to_ubv + (** Floating-point to_ubv. + + SMT-LIB: [fp.to_ubv] (indexed) *) + + val to_string : t -> string + (** + [to_string t] + get string representation of this kind. + + @return String representation of this kind. + *) + end + + module Term : sig + (** {1:term Term} *) + + type t + (** A Bitwuzla term. *) + + (** {2:sort_util Util} *) + + val hash : t -> int + (** + [hash t] + compute the hash value for a term. + + @param t The term. + + @return The hash value of the term. + *) + + val equal : t -> t -> bool + (** + [equal a b] + Syntactical equality operator. + + @param a The first term. + @param b The second term. + @return True if the given terms are equal. + *) + + val compare : t -> t -> int + (** + [compare a b] + Syntactical comparison operator. + + @param a The first term. + @param b The second term. + @return Zero if the given term are equal, + a positive number if [a] > [b], + a negative number otherwise. + *) + + val pp : Format.formatter -> t -> unit + (** + [pp formatter t] + print term. + + (alias for {!val:pp_smt2}[ 2]) + + @param formatter The outpout formatter. + @param t The term. + *) + + val pp_smt2 : bv_format:int -> Format.formatter -> t -> unit + (** + [pp_smt2 base formatter t] + print term in SMTlib format. + + @param bv_format The bit-vector number format: + [2] for binary, [10] for decimal and [16] for hexadecimal. + @param formatter The output formatter. + @param t The term. + *) + + val to_string : ?bv_format:int -> t -> string + (** + [to_string t ~bv_format] + get string representation of this term. + + @param t The term. + @param bv_format The bit-vector number format: + [2] for binary \[{b default}\], + [10] for decimal and [16] for hexadecimal. + + @return String representation of this term. + *) + + (** {2:term_query Query} *) + + val id : t -> int64 + (** + [id t] + get the id of this term. + + @param t The term. + @return The id value of the term. + *) + + val kind : t -> Kind.t + (** + [kind t] + get the kind of a term. + + @param t The term. + + @return The kind of the given term. + *) + + val sort : t -> Sort.t + (** + [sort t] + get the sort of a term. + + @param t The term. + + @return The sort of the term. + *) + + val num_children : t -> int + (** + [num_children t] + get the number of child terms of a term. + + @param t The term. + + @return The number children of [t]. + *) + + val children : t -> t array + (** + [children t] + get the child terms of a term. + + @param t The term. + + @return The children of [t] as an array of terms. + *) + + val get : t -> int -> t + (** + [get t i] + return child at position [i]. + + Only valid to call if [num_children t > 0]. + + @param i The position of the child. + @return The child node at position [i]. + *) + + val num_indices : t -> int + (** + [num_indices t] + get the number of indices of an indexed term. + + Requires that given term is an indexed term. + + @param t The term. + + @return The number of indices of [t]. + *) + + val indices : t -> int array + (** + [indices t] + get the indices of an indexed term. + + Requires that given term is an indexed term. + + @param t The term. + + @return The children of [t] as an array of terms. + *) + + val symbol : t -> string + (** + [symbol t] + get the symbol of a term. + + @param t The term. + + @return The symbol of [t]. + + @raise Not_found if no symbol is defined. + *) + + val is_const : t -> bool + (** + [is_const t] + determine if a term is a constant. + + @param t The term. + + @return [true] if [t] is a constant. + *) + + val is_variable : t -> bool + (** + [is_variable t] + determine if a term is a variable. + + @param t The term. + + @return [true] if [t] is a variable. + *) + + val is_value : t -> bool + (** + [is_value t] + determine if a term is a value. + + @param t The term. + + @return [true] if [t] is a value. + *) + + val is_bv_value_zero : t -> bool + (** + [is_bv_value_zero t] + determine if a term is a bit-vector value representing zero. + + @param t The term. + + @return [true] if [t] is a bit-vector zero value. + *) + + val is_bv_value_one : t -> bool + (** + [is_bv_value_one t] + determine if a term is a bit-vector value representing one. + + @param t The term. + + @return [true] if [t] is a bit-vector one value. + *) + + val is_bv_value_ones : t -> bool + (** + [is_bv_value_ones t] + determine if a term is a bit-vector value with all bits set to one. + + @param t The term. + + @return [true] if [t] is a bit-vector value with all bits set to one. + *) + + val is_bv_value_min_signed : t -> bool + (** + [is_bv_value_min_signed t] + determine if a term is a bit-vector minimum signed value. + + @param t The term. + + @return [true] if [t] is a bit-vector value with the most significant bit + set to 1 and all other bits set to 0. + *) + + val is_bv_value_max_signed : t -> bool + (** + [is_bv_value_max_signed t] + determine if a term is a bit-vector maximum signed value. + + @param t The term. + + @return [true] if [t] is a bit-vector value with the most significant bit + set to 0 and all other bits set to 1. + *) + + val is_fp_value_pos_zero : t -> bool + (** + [is_fp_value_pos_zero t] + determine if a term is a floating-point positive zero (+zero) value. + + @param t The term. + + @return [true] if [t] is a floating-point +zero value. + *) + + val is_fp_value_neg_zero : t -> bool + (** + [is_fp_value_neg_zero t] + determine if a term is a floating-point value negative zero (-zero). + + @param t The term. + + @return [true] if [t] is a floating-point value negative zero. + *) + + val is_fp_value_pos_inf : t -> bool + (** + [is_fp_value_pos_inf t] + determine if a term is a floating-point positive infinity (+oo) value. + + @param t The term. + + @return [true] if [t] is a floating-point +oo value. + *) + + val is_fp_value_neg_inf : t -> bool + (** + [is_fp_value_neg_inf t] + determine if a term is a floating-point negative infinity (-oo) value. + + @param t The term. + + @return [true] if [t] is a floating-point -oo value. + *) + + val is_fp_value_nan : t -> bool + (** + [is_fp_value_nan t] + determine if a term is a floating-point NaN value. + + @param t The term. + + @return [true] if [t] is a floating-point NaN value. + *) + + val is_rm_value_rna : t -> bool + (** + [is_rm_value_rna t] + determine if a term is a rounding mode RNA value. + + @param t The term. + + @return [true] if [t] is a rounding mode RNA value. + *) + + val is_rm_value_rne : t -> bool + (** + [is_rm_value_rna t] + determine if a term is a rounding mode RNE value. + + @param t The term. + + @return [true] if [t] is a rounding mode RNE value. + *) + + val is_rm_value_rtn : t -> bool + (** + [is_rm_value_rna t] + determine if a term is a rounding mode RTN value. + + @param t The term. + + @return [true] if [t] is a rounding mode RTN value. + *) + + val is_rm_value_rtp : t -> bool + (** + [is_rm_value_rna t] + determine if a term is a rounding mode RTP value. + + @param t The term. + + @return [true] if [t] is a rounding mode RTP value. + *) + + val is_rm_value_rtz : t -> bool + (** + [is_rm_value_rna t] + determine if a term is a rounding mode RTZ value. + + @param t The term. + + @return [true] if [t] is a rounding mode RTZ value. + *) + + type _ cast = + | Bool : bool cast (** for Boolean values *) + | RoundingMode : RoundingMode.t cast (** for rounding mode values *) + | String : { base : int } -> string cast + (** for any value + (Boolean, RoundingMode, bit-vector and floating-point) *) + | IEEE_754 : (string * string * string) cast + (** for floating-point values as strings + for sign bit, exponent and significand *) + | Z : Z.t cast (** for bit-vector *) + + val value : 'a cast -> t -> 'a + (** + [value kind t] + get value from value term. + + @param kind The type of the value representation. + @return The value of [t] in a given representation. + *) + end + + module Result : sig + (** A satisfiability result. *) + type t = Sat (** sat *) | Unsat (** unsat *) | Unknown (** unknown *) + + val to_string : t -> string + (** + [to_string t] + get string representation of this result. + + @return String representation of this result. + *) + end + + module Solver : sig + (** {1 Solver} *) + + type t + (** The Bitwuzla solver. *) + + val configure_terminator : t -> (unit -> bool) option -> unit + (** + [configure_terminator t f] + configure a termination callback function. + + If terminator has been connected, Bitwuzla calls this function periodically + to determine if the connected instance should be terminated. + + @param t The Bitwuzla instance. + @param f The callback function, returns [true] if [t] should be terminated. + *) + + val create : Options.t -> t + (** + [create options] + create a new Bitwuzla instance. + + The returned instance can be deleted earlier via {!val:unsafe_delete}. + + @param options The associated options instance. + Options must be configured at this point. + + @return The created Bitwuzla instance. + *) + + (** {2 Formula} *) + + val push : t -> int -> unit + (** + [push t nlevels] + push context levels. + + @param t The Bitwuzla instance. + @param nlevels The number of context levels to push. + *) + + val pop : t -> int -> unit + (** + [pop t nlevels] + pop context levels. + + @param t The Bitwuzla instance. + @param nlevels The number of context levels to pop. + *) + + val assert_formula : t -> Term.t -> unit + (** + [mk_assert t term] + assert formula. + + @param t The Bitwuzla instance. + @param term The formula to assert. + *) + + val get_assertions : t -> Term.t array + (** + [get_assertions t] + get the set of currently asserted formulas. + + @return The assertion formulas. + *) + + val pp_formula : Format.formatter -> t -> unit + (** + [pp_formula formatter t] + print the current input formula. + + @param formatter The output formatter. + @param t The Bitwuzla instance. + *) + + (** {2 Check} *) + + val simplify : t -> unit + (** + [simplify t] + simplify the current input formula. + + @param t The Bitwuzla instance. + *) + + val check_sat : ?assumptions:Term.t array -> t -> Result.t + (** + [check_sat ~assumptions t] + check satisfiability of current input formula. + + An input formula consists of assertions added via {!val:assert_formula}. + The search for a solution can by guided by making assumptions via + [assumptions]. + + Assertions and assumptions are combined via Boolean [and]. + + @param t The Bitwuzla instance. + + @return {!constructor:Sat} if the input formula is satisfiable and + {!constructor:Unsat} if it is unsatisfiable, and {!constructor:Unknown} + when neither satisfiability nor unsatisfiability was determined. + This can happen when [t] was terminated via a termination callback. + *) + + (** {2 Sat} *) + + val get_value : t -> Term.t -> Term.t + (** + [get_value t term] + get a term representing the model value of a given term. + + Requires that the last {!val:check_sat} query returned [Sat]. + + @param t The Bitwuzla instance. + @param term The term to query a model value for. + + @return A term representing the model value of term [term]. + *) + + (** {2 Unsat} *) + + val is_unsat_assumption : t -> Term.t -> bool + (** + [is_unsat_assumption t term] + determine if an assumption is an unsat assumption. + + Unsat assumptions are assumptions that force an input formula to become + unsatisfiable. Unsat assumptions handling in Bitwuzla is analogous to + failed assumptions in MiniSAT. + + Requires that unsat assumption generation has been enabled via + {!val:Options.set}. + + Requires that the last {!val:check_sat} query returned [Unsat]. + + @param t The Bitwuzla instance. + @param term The assumption to check for. + + @return [true] if given assumption is an unsat assumption. + *) + + val get_unsat_assumptions : t -> Term.t array + (** + [get_unsat_assumptions t] + get the set of unsat assumptions. + + Unsat assumptions are assumptions that force an input formula to become + unsatisfiable. Unsat assumptions handling in Bitwuzla is analogous to + failed assumptions in MiniSAT. + + Requires that unsat assumption generation has been enabled via + {!val:Options.set}. + + Requires that the last {!val:check_sat} query returned [Unsat]. + + @param t The Bitwuzla instance. + + @return An array with unsat assumptions. + *) + + val get_unsat_core : t -> Term.t array + (** + [get_unsat_core t] + get the set unsat core (unsat assertions). + + The unsat core consists of the set of assertions that force + an input formula to become unsatisfiable. + + Requires that unsat core generation has been enabled via {!val:Options.set}. + + Requires that the last {!val:check_sat} query returned [Unsat]. + + @param t The Bitwuzla instance. + + @return An array with unsat assertions. + *) + + (** {2 Expert} *) + val unsafe_delete : t -> unit + (** + [delete t] + delete a Bitwuzla instance. + + UNSAFE: call this ONLY to release the resources earlier + if the instance is about to be garbage collected. + + @param t The Bitwuzla instance to delete. + *) + + val pp_statistics : Format.formatter -> t -> unit + end + + (** {2:sort_constructor Sort constructor} *) + + val mk_array_sort : Sort.t -> Sort.t -> Sort.t + (** + [mk_array_sort index element] + create an array sort. + + @param index The index sort of the array sort. + @param element The element sort of the array sort. + + @return An array sort which maps sort [index] to sort [element]. +*) + + val mk_bool_sort : unit -> Sort.t + (** + [mk_bool_sort ()] + create a Boolean sort. + + A Boolean sort is a bit-vector sort of size 1. + + @return A Boolean sort. +*) + + val mk_bv_sort : int -> Sort.t + (** + [mk_bv_sort size] + create a bit-vector sort of given size. + + @param size The size of the bit-vector sort. + + @return A bit-vector sort of given size. +*) + + val mk_fp_sort : int -> int -> Sort.t + (** + [mk_fp_sort exp_size sig_size] + create a floating-point sort of given exponent and significand size. + + @param exp_size The size of the exponent. + @param sig_size The size of the significand (including sign bit). + + @return A floating-point sort of given format. +*) + + val mk_fun_sort : Sort.t array -> Sort.t -> Sort.t + (** + [mk_fun_sort domain codomain] + create a function sort. + + @param domain The domain sorts (the sorts of the arguments). + @param codomain The codomain sort (the sort of the return value). + + @return A function sort of given domain and codomain sorts. +*) + + val mk_rm_sort : unit -> Sort.t + (** + [mk_rm_sort ()] + create a Roundingmode sort. + + @return A Roundingmode sort. +*) + + val mk_uninterpreted_sort : ?symbol:string -> unit -> Sort.t + (** + [mk_uninterpreted_sort name] + create an uninterpreted sort. + + Only 0-arity uninterpreted sorts are supported. + + @param symbol The symbol of the sort. + @return An uninterpreted sort. +*) + + (** {2:term_constructor Term constructor} *) + + (** {3 Value} *) + + val mk_true : unit -> Term.t + (** + [mk_true ()] + create a true value. + + This creates a bit-vector value 1 of size 1. + + @return A term representing the bit-vector value 1 of size 1. +*) + + val mk_false : unit -> Term.t + (** + [mk_false ()] + create a false value. + + This creates a bit-vector value 0 of size 1. + + @return A term representing the bit-vector value 0 of size 1. +*) + + val mk_bv_zero : Sort.t -> Term.t + (** + [mk_bv_zero sort] + create a bit-vector value zero. + + @param sort The sort of the value. + + @return A term representing the bit-vector value 0 of given sort. +*) + + val mk_bv_one : Sort.t -> Term.t + (** + [mk_bv_one sort] + create a bit-vector value one. + + @param sort The sort of the value. + + @return A term representing the bit-vector value 1 of given sort. +*) + + val mk_bv_ones : Sort.t -> Term.t + (** + [mk_bv_ones sort] + create a bit-vector value where all bits are set to 1. + + @param sort The sort of the value. + + @return A term representing the bit-vector value of given sort + where all bits are set to 1. +*) + + val mk_bv_min_signed : Sort.t -> Term.t + (** + [mk_bv_min_signed sort] + create a bit-vector minimum signed value. + + @param sort The sort of the value. + + @return A term representing the bit-vector value of given sort where the MSB + is set to 1 and all remaining bits are set to 0. +*) + + val mk_bv_max_signed : Sort.t -> Term.t + (** + [mk_bv_max_signed sort] + create a bit-vector maximum signed value. + + @param sort The sort of the value. + + @return A term representing the bit-vector value of given sort where the MSB + is set to 0 and all remaining bits are set to 1. +*) + + val mk_bv_value : Sort.t -> string -> int -> Term.t + (** + [mk_bv_value sort value base] + create a bit-vector value from its string representation. + + Parameter [base] determines the base of the string representation. + + Given value must fit into a bit-vector of given size (sort). + + @param sort The sort of the value. + @param value A string representing the value. + @param base The base in which the string is given. + + @return A term representing the bit-vector value of given sort. +*) + + val mk_bv_value_int : Sort.t -> int -> Term.t + (** + [mk_bv_value_int sort value] + create a bit-vector value from its unsigned integer representation. + + If given value does not fit into a bit-vector of given size (sort), + the value is truncated to fit. + + @param sort The sort of the value. + @param value The unsigned integer representation of the bit-vector value. + + @return A term representing the bit-vector value of given sort. +*) + + val mk_bv_value_int64 : Sort.t -> int64 -> Term.t + (** + [mk_bv_value_int64 sort value] + create a bit-vector value from its unsigned integer representation. + + If given value does not fit into a bit-vector of given size (sort), + the value is truncated to fit. + + @param sort The sort of the value. + @param value The unsigned integer representation of the bit-vector value. + + @return A term representing the bit-vector value of given sort. +*) + + val mk_fp_pos_zero : Sort.t -> Term.t + (** + [mk_fp_pos_zero sort] + create a floating-point positive zero value (SMT-LIB: [+zero]). + + @param sort The sort of the value. + + @return A term representing the floating-point positive zero value of given + floating-point sort. +*) + + val mk_fp_neg_zero : Sort.t -> Term.t + (** + [mk_fp_neg_zero sort] + create a floating-point negative zero value (SMT-LIB: [-zero]). + + @param sort The sort of the value. + + @return A term representing the floating-point negative zero value of given + floating-point sort. +*) + + val mk_fp_pos_inf : Sort.t -> Term.t + (** + [mk_fp_pos_inf sort] + create a floating-point positive infinity value (SMT-LIB: [+oo]). + + @param sort The sort of the value. + + @return A term representing the floating-point positive infinity value of + given floating-point sort. +*) + + val mk_fp_neg_inf : Sort.t -> Term.t + (** + [mk_fp_neg_inf sort] + create a floating-point negative infinity value (SMT-LIB: [-oo]). + + @param sort The sort of the value. + + @return A term representing the floating-point negative infinity value of + given floating-point sort. +*) + + val mk_fp_nan : Sort.t -> Term.t + (** + [mk_fp_nan sort] + create a floating-point NaN value. + + @param sort The sort of the value. + + @return A term representing the floating-point NaN value of given + floating-point sort. +*) + + val mk_fp_value : Term.t -> Term.t -> Term.t -> Term.t + (** + [mk_fp_value bv_sign bv_exponent bv_significand] + create a floating-point value from its IEEE 754 standard representation + given as three bitvectors representing the sign bit, the exponent and the + significand. + + @param bv_sign The sign bit. + @param bv_exponent The exponent bit-vector. + @param bv_significand The significand bit-vector. + + @return A term representing the floating-point value. +*) + + val mk_fp_value_from_real : Sort.t -> Term.t -> string -> Term.t + (** + [mk_fp_value_from_real t sort rm real] + create a floating-point value from its real representation, given as a + decimal string, with respect to given rounding mode. + + @param sort The sort of the value. + @param rm The rounding mode. + @param real The decimal string representing a real value. + + @return A term representing the floating-point value of given sort. +*) + + val mk_fp_value_from_rational : Sort.t -> Term.t -> string -> string -> Term.t + (** + [mk_fp_value_from_rational sort rm num den] + create a floating-point value from its rational representation, given as a + two decimal strings representing the numerator and denominator, with respect + to given rounding mode. + + @param sort The sort of the value. + @param rm The rounding mode. + @param num The decimal string representing the numerator. + @param den The decimal string representing the denominator. + + @return A term representing the floating-point value of given sort. +*) + + val mk_rm_value : RoundingMode.t -> Term.t + (** + [mk_rm_value rm] + create a rounding mode value. + + @param rm The rounding mode value. + + @return A term representing the rounding mode value. +*) + + (** {3 Expression} *) + + val mk_term1 : Kind.t -> Term.t -> Term.t + (** + [mk_term1 kind arg] + create a term of given kind with one argument term. + + @param kind The operator kind. + @param arg The argument to the operator. + + @return A term representing an operation of given kind. +*) + + val mk_term2 : Kind.t -> Term.t -> Term.t -> Term.t + (** + [mk_term2 kind arg0 arg1] + create a term of given kind with two argument terms. + + @param kind The operator kind. + @param arg0 The first argument to the operator. + @param arg1 The second argument to the operator. + + @return A term representing an operation of given kind. +*) + + val mk_term3 : Kind.t -> Term.t -> Term.t -> Term.t -> Term.t + (** + [mk_term3 kind arg0 arg1 arg2] + create a term of given kind with three argument terms. + + @param kind The operator kind. + @param arg0 The first argument to the operator. + @param arg1 The second argument to the operator. + @param arg2 The third argument to the operator. + + @return A term representing an operation of given kind. +*) + + val mk_term1_indexed1 : Kind.t -> Term.t -> int -> Term.t + (** + [mk_term1_indexed1 kind arg idx] + create an indexed term of given kind with one argument term and one index. + + @param kind The operator kind. + @param arg The argument term. + @param idx The index. + + @return A term representing an indexed operation of given kind. +*) + + val mk_term1_indexed2 : Kind.t -> Term.t -> int -> int -> Term.t + (** + [mk_term1_indexed2 kind arg idx0 idx1] + create an indexed term of given kind with one argument term and two indices. + + @param kind The operator kind. + @param arg The argument term. + @param idx0 The first index. + @param idx1 The second index. + + @return A term representing an indexed operation of given kind. +*) + + val mk_term2_indexed1 : Kind.t -> Term.t -> Term.t -> int -> Term.t + (** + [mk_term2_indexed1 t kind arg0 arg1 idx] + create an indexed term of given kind with two argument terms and one index. + + @param kind The operator kind. + @param arg0 The first argument term. + @param arg1 The second argument term. + @param idx The index. + + @return A term representing an indexed operation of given kind. +*) + + val mk_term2_indexed2 : Kind.t -> Term.t -> Term.t -> int -> int -> Term.t + (** + [mk_term2_indexed2 t kind arg0 arg1 idx0 idx1] + create an indexed term of given kind with two argument terms and two indices. + + @param kind The operator kind. + @param arg0 The first argument term. + @param arg1 The second argument term. + @param idx0 The first index. + @param idx1 The second index. + + @return A term representing an indexed operation of given kind. +*) + + val mk_term : Kind.t -> ?indices:int array -> Term.t array -> Term.t + (** + [mk_term kind args ~indices] + create an indexed term of given kind with the given argument terms and + indices. + + @param kind The operator kind. + @param args The argument terms. + @param indices The indices. + + @return A term representing an indexed operation of given kind. +*) + + val mk_const : ?symbol:string -> Sort.t -> Term.t + (** + [mk_const sort ~symbol] + create a (first-order) constant of given sort with given symbol. + + This creates a 0-arity function symbol. + + @param sort The sort of the constant. + @param symbol The symbol of the constant. + + @return A term representing the constant. +*) + + val mk_const_array : Sort.t -> Term.t -> Term.t + (** + [mk_const_array sort value] + create a one-dimensional constant array of given sort, initialized with + given value. + + @param sort The sort of the array. + @param value The value to initialize the elements of the array with. + + @return A term representing a constant array of given sort. +*) + + val mk_var : ?symbol:string -> Sort.t -> Term.t + (** + [mk_var sort ~symbol] + create a variable of given sort with given symbol. + + This creates a variable to be bound by quantifiers or lambdas. + + @param sort The sort of the variable. + @param symbol The symbol of the variable. + + @return A term representing the variable. +*) + + (** {2 Util} *) + + val substitute_term : Term.t -> (Term.t * Term.t) array -> Term.t + (** + [substitute t term map] + substitute a set of keys with their corresponding values in the given term. + + @param term The term in which the keys are to be substituted. + @param map The key/value associations. + + @return The resulting term from this substitution. +*) + + val substitute_terms : Term.t array -> (Term.t * Term.t) array -> unit + (** + [substitute_terms t terms map] + substitute a set of keys with their corresponding values in the set of given + terms. + + The terms in [terms] are replaced with the terms resulting from this + substitutions. + + @param terms The terms in which the keys are to be substituted. + @param map The key/value associations. +*) +end + +module Make () : S = struct + let t = Manager.create () + + module Sort = Sort + + let mk_array_sort = mk_array_sort t + + let mk_bool_sort () = mk_bool_sort t + + let mk_bv_sort = mk_bv_sort t + + let mk_fp_sort = mk_fp_sort t + + let mk_fun_sort = mk_fun_sort t + + let mk_rm_sort () = mk_rm_sort t + + let mk_uninterpreted_sort = mk_uninterpreted_sort t + + module RoundingMode = RoundingMode + module Kind = Kind + module Term = Term + + let mk_true () = mk_true t + + let mk_false () = mk_false t + + let mk_bv_zero = mk_bv_zero t + + let mk_bv_one = mk_bv_one t + + let mk_bv_ones = mk_bv_ones t + + let mk_bv_min_signed = mk_bv_min_signed t + + let mk_bv_max_signed = mk_bv_max_signed t + + let mk_bv_value = mk_bv_value t + + let mk_bv_value_int = mk_bv_value_int t + + let mk_bv_value_int64 = mk_bv_value_int64 t + + let mk_fp_pos_zero = mk_fp_pos_zero t + + let mk_fp_neg_zero = mk_fp_neg_zero t + + let mk_fp_pos_inf = mk_fp_pos_inf t + + let mk_fp_neg_inf = mk_fp_neg_inf t + + let mk_fp_nan = mk_fp_nan t + + let mk_fp_value = mk_fp_value t + + let mk_fp_value_from_real = mk_fp_value_from_real t + + let mk_fp_value_from_rational = mk_fp_value_from_rational t + + let mk_rm_value m = mk_rm_value t (RoundingMode.to_cxx m) + + let mk_term1 k x = mk_term1 t (Kind.to_cxx k) x + + let mk_term2 k x1 x2 = mk_term2 t (Kind.to_cxx k) x1 x2 + + let mk_term3 k x1 x2 x3 = mk_term3 t (Kind.to_cxx k) x1 x2 x3 + + let mk_term1_indexed1 k x i = mk_term1_indexed1 t (Kind.to_cxx k) x i + + let mk_term1_indexed2 k x i j = mk_term1_indexed2 t (Kind.to_cxx k) x i j + + let mk_term2_indexed1 k x1 x2 i = mk_term2_indexed1 t (Kind.to_cxx k) x1 x2 i + + let mk_term2_indexed2 k x1 x2 i j = + mk_term2_indexed2 t (Kind.to_cxx k) x1 x2 i j + + let mk_term k ?(indices = [||]) args = mk_term t (Kind.to_cxx k) args indices + + let mk_const = mk_const t + + let mk_const_array = mk_const_array t + + let mk_var = mk_var t + + let substitute_term = substitute_term t + + let substitute_terms = substitute_terms t + + module Result = Result + + module Solver = struct + include Solver + + let create = create t + end +end + +include Make () diff --git a/bitwuzla_cxx.mli b/bitwuzla_cxx.mli index 7d2da73..2edcb67 100644 --- a/bitwuzla_cxx.mli +++ b/bitwuzla_cxx.mli @@ -149,6 +149,20 @@ module Options : sig This is an expert option to configure the prop solver engine. *) + | Prop_opt_lt_concat_sext : bool key + (** Propagation-based local search solver engine: + Optimization for inverse value computation of inequalities over + concat and sign extension operands. + + When enabled, use optimized inverse value value computation for + inequalities over concats. + + Values: + - [true]: enable + - [false]: disable \[{b default}\] + + This is an expert option to configure the prop solver engine. + *) | Prop_path_sel : prop_path_sel key (** Propagation-based local search solver engine: Path selection. @@ -376,16 +390,25 @@ module Options : sig (** [get t opt] get the current option value. *) end -module Sort : sig - (** {1:sort Sort} *) +module type S = sig + (** Signature of a Bitwuzla instance. - type t - (** A Bitwuzla sort. *) + Each instance can create and share {!module:Term}s between several + {!module:Solver}s. + However, an instance is not thread safe. Thus multicore users should ensure + that only one Domain uses a bitwuzla instance at a given time. + *) - (** {2:sort_util Util} *) + module Sort : sig + (** {1:sort Sort} *) - val hash : t -> int - (** + type t + (** A Bitwuzla sort. *) + + (** {2:sort_util Util} *) + + val hash : t -> int + (** [hash t] compute the hash value for a sort. @@ -394,8 +417,8 @@ module Sort : sig @return The hash value of the sort. *) - val equal : t -> t -> bool - (** + val equal : t -> t -> bool + (** [equal a b] Syntactical equality operator. @@ -404,8 +427,8 @@ module Sort : sig @return True if the given sorts are equal. *) - val compare : t -> t -> int - (** + val compare : t -> t -> int + (** [compare a b] Syntactical comparison operator. @@ -416,8 +439,8 @@ module Sort : sig a negative number otherwise. *) - val pp : Format.formatter -> t -> unit - (** + val pp : Format.formatter -> t -> unit + (** [pp formatter t] print sort. @@ -425,18 +448,18 @@ module Sort : sig @param formatter The outpout formatter. *) - val to_string : t -> string - (** + val to_string : t -> string + (** [to_string t] get string representation of this sort. @return String representation of this sort. *) - (** {2:sort_query Query} *) + (** {2:sort_query Query} *) - val id : t -> int64 - (** + val id : t -> int64 + (** [id t] get the id of this sort. @@ -444,8 +467,8 @@ module Sort : sig @return The id value of the sort. *) - val bv_size : t -> int - (** + val bv_size : t -> int + (** [bv_size t] get the size of a bit-vector sort. @@ -456,8 +479,8 @@ module Sort : sig @return The size of the bit-vector sort. *) - val fp_exp_size : t -> int - (** + val fp_exp_size : t -> int + (** [fp_exp_size sort] get the exponent size of a floating-point sort. @@ -468,8 +491,8 @@ module Sort : sig @return The exponent size of the floating-point sort. *) - val fp_sig_size : t -> int - (** + val fp_sig_size : t -> int + (** [fp_sig_size t] get the significand size of a floating-point sort. @@ -480,8 +503,8 @@ module Sort : sig @return The significand size of the floating-point sort. *) - val array_index : t -> t - (** + val array_index : t -> t + (** [array_index t] get the index sort of an array sort. @@ -492,8 +515,8 @@ module Sort : sig @return The index sort of the array sort. *) - val array_element : t -> t - (** + val array_element : t -> t + (** [array_element t] get the element sort of an array sort. @@ -504,8 +527,8 @@ module Sort : sig @return The element sort of the array sort. *) - val fun_domain : t -> t array - (** + val fun_domain : t -> t array + (** [fun_domain_sorts t] get the domain sorts of a function sort. @@ -516,8 +539,8 @@ module Sort : sig @return The domain sorts of the function sort as an array of sort. *) - val fun_codomain : t -> t - (** + val fun_codomain : t -> t + (** [fun_codomain t] get the codomain sort of a function sort. @@ -528,8 +551,8 @@ module Sort : sig @return The codomain sort of the function sort. *) - val fun_arity : t -> int - (** + val fun_arity : t -> int + (** [fun_arity t] get the arity of a function sort. @@ -538,8 +561,8 @@ module Sort : sig @return The number of arguments of the function sort. *) - val uninterpreted_symbol : t -> string - (** + val uninterpreted_symbol : t -> string + (** [uninterpreted_symbol t] get the symbol of an uninterpreted sort. @@ -550,8 +573,8 @@ module Sort : sig @raise Not_found if no symbol is defined. *) - val is_array : t -> bool - (** + val is_array : t -> bool + (** [is_array t] determine if a sort is an array sort. @@ -560,8 +583,8 @@ module Sort : sig @return [true] if [t] is an array sort. *) - val is_bool : t -> bool - (** + val is_bool : t -> bool + (** [is_bool t] determine if a sort is a Boolean sort. @@ -570,8 +593,8 @@ module Sort : sig @return [true] if [t] is a Boolean sort. *) - val is_bv : t -> bool - (** + val is_bv : t -> bool + (** [is_bv t] determine if a sort is a bit-vector sort. @@ -580,8 +603,8 @@ module Sort : sig @return [true] if [t] is a bit-vector sort. *) - val is_fp : t -> bool - (** + val is_fp : t -> bool + (** [is_fp t] determine if a sort is a floating-point sort. @@ -590,8 +613,8 @@ module Sort : sig @return [true] if [t] is a floating-point sort. *) - val is_fun : t -> bool - (** + val is_fun : t -> bool + (** [is_fun t] determine if a sort is a function sort. @@ -600,8 +623,8 @@ module Sort : sig @return [true] if [t] is a function sort. *) - val is_rm : t -> bool - (** + val is_rm : t -> bool + (** [is_rm t] determine if a sort is a Roundingmode sort. @@ -610,8 +633,8 @@ module Sort : sig @return [true] if [t] is a Roundingmode sort. *) - val is_uninterpreted : t -> bool - (** + val is_uninterpreted : t -> bool + (** [is_uninterpreted t] determine if a sort is an uninterpreted sort. @@ -619,10 +642,10 @@ module Sort : sig @return [true] if [t] is an uninterpreted sort. *) -end + end -module RoundingMode : sig - (** + module RoundingMode : sig + (** Rounding mode for floating-point operations. For some floating-point operations, infinitely precise results may not be @@ -634,427 +657,439 @@ module RoundingMode : sig The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE Standard 754. *) - type t = - | Rne - (** Round to the nearest even number. + type t = + | Rne + (** Round to the nearest even number. If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with an even least significant digit will be delivered. SMT-LIB: [RNE] roundNearestTiesToEven *) - | Rna - (** Round to the nearest number away from zero. + | Rna + (** Round to the nearest number away from zero. If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with larger magnitude will be selected. SMT-LIB: [RNA] roundNearestTiesToAway *) - | Rtn - (** Round towards negative infinity (-oo). + | Rtn + (** Round towards negative infinity (-oo). The result shall be the format’s floating-point number (possibly -oo) closest to and no less than the infinitely precise result. SMT-LIB: [RTN] roundTowardNegative *) - | Rtp - (** Round towards positive infinity (+oo). + | Rtp + (** Round towards positive infinity (+oo). The result shall be the format’s floating-point number (possibly +oo) closest to and no less than the infinitely precise result. SMT-LIB: [RTP] roundTowardPositive *) - | Rtz - (** Round towards zero. + | Rtz + (** Round towards zero. The result shall be the format’s floating-point number closest to and no greater in magnitude than the infinitely precise result. SMT-LIB: [RTZ] roundTowardZero *) - val to_string : t -> string - (** + val to_string : t -> string + (** [to_string t] get string representation of this rounding mode. @return String representation of this rounding mode. *) -end + end -module Kind : sig - (** The term kind. *) - type t = - | Constant (** First order constant. *) - | Const_array (** Constant array. *) - | Value (** Value. *) - | Variable (** Bound variable. *) - | And (** Boolean and. + module Kind : sig + (** The term kind. *) + type t = + | Constant (** First order constant. *) + | Const_array (** Constant array. *) + | Value (** Value. *) + | Variable (** Bound variable. *) + | And (** Boolean and. SMT-LIB: [and] *) - | Distinct (** Disequality. + | Distinct (** Disequality. SMT-LIB: [distinct] *) - | Equal (** Equality. + | Equal (** Equality. SMT-LIB: [=] *) - | Iff (** Boolean if and only if. + | Iff (** Boolean if and only if. SMT-LIB: [=] *) - | Implies (** Boolean implies. + | Implies (** Boolean implies. SMT-LIB: [=>] *) - | Not (** Boolean not. + | Not (** Boolean not. SMT-LIB: [not] *) - | Or (** Boolean or. + | Or (** Boolean or. SMT-LIB: [or] *) - | Xor (** Boolean xor. + | Xor (** Boolean xor. SMT-LIB: [xor] *) - | Ite (** If-then-else. + | Ite (** If-then-else. SMT-LIB: [ite] *) - | Exists (** Existential quantification. + | Exists (** Existential quantification. SMT-LIB: [exists] *) - | Forall - (** Universal quantification. + | Forall + (** Universal quantification. SMT-LIB: [forall] *) - | Apply (** Function application. *) - | Lambda (** Lambda. *) - | Select (** Array select. + | Apply (** Function application. *) + | Lambda (** Lambda. *) + | Select (** Array select. SMT-LIB: [select] *) - | Store (** Array store. + | Store (** Array store. SMT-LIB: [store] *) - | Bv_add (** Bit-vector addition. + | Bv_add (** Bit-vector addition. SMT-LIB: [bvadd] *) - | Bv_and (** Bit-vector and. + | Bv_and (** Bit-vector and. SMT-LIB: [bvand] *) - | Bv_ashr - (** Bit-vector arithmetic right shift. + | Bv_ashr + (** Bit-vector arithmetic right shift. SMT-LIB: [bvashr] *) - | Bv_comp - (** Bit-vector comparison. + | Bv_comp + (** Bit-vector comparison. SMT-LIB: [bvcomp] *) - | Bv_concat - (** Bit-vector concat. + | Bv_concat + (** Bit-vector concat. SMT-LIB: [concat] *) - | Bv_dec (** Bit-vector decrement. + | Bv_dec + (** Bit-vector decrement. Decrement by one. *) - | Bv_inc (** Bit-vector increment. + | Bv_inc + (** Bit-vector increment. Increment by one. *) - | Bv_mul - (** Bit-vector multiplication. + | Bv_mul + (** Bit-vector multiplication. SMT-LIB: [bvmul] *) - | Bv_nand (** Bit-vector nand. + | Bv_nand (** Bit-vector nand. SMT-LIB: [bvnand] *) - | Bv_neg - (** Bit-vector negation (two's complement). + | Bv_neg + (** Bit-vector negation (two's complement). SMT-LIB: [bvneg] *) - | Bv_nor (** Bit-vector nor. + | Bv_nor (** Bit-vector nor. SMT-LIB: [bvnor] *) - | Bv_not - (** Bit-vector not (one's complement). + | Bv_not + (** Bit-vector not (one's complement). SMT-LIB: [bvnot] *) - | Bv_or (** Bit-vector or. + | Bv_or (** Bit-vector or. SMT-LIB: [bvor] *) - | Bv_redand - (** Bit-vector and reduction. + | Bv_redand + (** Bit-vector and reduction. Bit-wise {b and} reduction, all bits are {b and}'ed together into a single bit. This corresponds to bit-wise {b and} reduction as known from Verilog. *) - | Bv_redor - (** Bit-vector reduce or. + | Bv_redor + (** Bit-vector reduce or. Bit-wise {b or} reduction, all bits are {b or}'ed together into a single bit. This corresponds to bit-wise {b or} reduction as known from Verilog. *) - | Bv_redxor - (** Bit-vector reduce xor. + | Bv_redxor + (** Bit-vector reduce xor. Bit-wise {b xor} reduction, all bits are {b xor}'ed together into a single bit. This corresponds to bit-wise {b xor} reduction as known from Verilog. *) - | Bv_rol - (** Bit-vector rotate left (not indexed). + | Bv_rol + (** Bit-vector rotate left (not indexed). This is a non-indexed variant of SMT-LIB [rotate_left]. *) - | Bv_ror - (** Bit-vector rotate right. + | Bv_ror + (** Bit-vector rotate right. This is a non-indexed variant of SMT-LIB [rotate_right]. *) - | Bv_saddo - (** Bit-vector signed addition overflow test. + | Bv_saddo + (** Bit-vector signed addition overflow test. Single bit to indicate if signed addition produces an overflow. *) - | Bv_sdivo - (** Bit-vector signed division overflow test. + | Bv_sdivo + (** Bit-vector signed division overflow test. Single bit to indicate if signed division produces an overflow. *) - | Bv_sdiv (** Bit-vector signed division. + | Bv_sdiv + (** Bit-vector signed division. SMT-LIB: [bvsdiv] *) - | Bv_sge - (** Bit-vector signed greater than or equal. + | Bv_sge + (** Bit-vector signed greater than or equal. SMT-LIB: [bvsge] *) - | Bv_sgt (** Bit-vector signed greater than. + | Bv_sgt + (** Bit-vector signed greater than. SMT-LIB: [bvsgt] *) - | Bv_shl (** Bit-vector logical left shift. + | Bv_shl + (** Bit-vector logical left shift. SMT-LIB: [bvshl] *) - | Bv_shr (** Bit-vector logical right shift. + | Bv_shr + (** Bit-vector logical right shift. SMT-LIB: [bvshr] *) - | Bv_sle - (** Bit-vector signed less than or equal. + | Bv_sle + (** Bit-vector signed less than or equal. SMT-LIB: [bvsle] *) - | Bv_slt (** Bit-vector signed less than. + | Bv_slt (** Bit-vector signed less than. SMT-LIB: [bvslt] *) - | Bv_smod (** Bit-vector signed modulo. + | Bv_smod (** Bit-vector signed modulo. SMT-LIB: [bvsmod] *) - | Bv_smulo - (** Bit-vector signed multiplication overflow test. + | Bv_smulo + (** Bit-vector signed multiplication overflow test. SMT-LIB: [bvsmod] *) - | Bv_srem (** Bit-vector signed remainder. + | Bv_srem + (** Bit-vector signed remainder. SMT-LIB: [bvsrem] *) - | Bv_ssubo - (** Bit-vector signed subtraction overflow test. + | Bv_ssubo + (** Bit-vector signed subtraction overflow test. Single bit to indicate if signed subtraction produces an overflow. *) - | Bv_sub (** Bit-vector subtraction. + | Bv_sub + (** Bit-vector subtraction. SMT-LIB: [bvsub] *) - | Bv_uaddo - (** Bit-vector unsigned addition overflow test. + | Bv_uaddo + (** Bit-vector unsigned addition overflow test. Single bit to indicate if unsigned addition produces an overflow. *) - | Bv_udiv - (** Bit-vector unsigned division. + | Bv_udiv + (** Bit-vector unsigned division. SMT-LIB: [bvudiv] *) - | Bv_uge - (** Bit-vector unsigned greater than or equal. + | Bv_uge + (** Bit-vector unsigned greater than or equal. SMT-LIB: [bvuge] *) - | Bv_ugt - (** Bit-vector unsigned greater than. + | Bv_ugt + (** Bit-vector unsigned greater than. SMT-LIB: [bvugt] *) - | Bv_ule - (** Bit-vector unsigned less than or equal. + | Bv_ule + (** Bit-vector unsigned less than or equal. SMT-LIB: [bvule] *) - | Bv_ult (** Bit-vector unsigned less than. + | Bv_ult + (** Bit-vector unsigned less than. SMT-LIB: [bvult] *) - | Bv_umulo - (** Bit-vector unsigned multiplication overflow test. + | Bv_umulo + (** Bit-vector unsigned multiplication overflow test. Single bit to indicate if unsigned multiplication produces an overflow. *) - | Bv_urem - (** Bit-vector unsigned remainder. + | Bv_urem + (** Bit-vector unsigned remainder. SMT-LIB: [bvurem] *) - | Bv_usubo - (** Bit-vector unsigned subtraction overflow test. + | Bv_usubo + (** Bit-vector unsigned subtraction overflow test. Single bit to indicate if unsigned subtraction produces an overflow. *) - | Bv_xnor (** Bit-vector xnor. + | Bv_xnor (** Bit-vector xnor. SMT-LIB: [bvxnor] *) - | Bv_xor (** Bit-vector xor. + | Bv_xor (** Bit-vector xor. SMT-LIB: [bvxor] *) - | Bv_extract - (** Bit-vector extract. + | Bv_extract + (** Bit-vector extract. SMT-LIB: [extract] (indexed) *) - | Bv_repeat - (** Bit-vector repeat. + | Bv_repeat + (** Bit-vector repeat. SMT-LIB: [repeat] (indexed) *) - | Bv_roli - (** Bit-vector rotate left by integer. + | Bv_roli + (** Bit-vector rotate left by integer. SMT-LIB: [rotate_left] (indexed) *) - | Bv_rori - (** Bit-vector rotate right by integer. + | Bv_rori + (** Bit-vector rotate right by integer. SMT-LIB: [rotate_right] (indexed) *) - | Bv_sign_extend - (** Bit-vector sign extend. + | Bv_sign_extend + (** Bit-vector sign extend. SMT-LIB: [sign_extend] (indexed) *) - | Bv_zero_extend - (** Bit-vector zero extend. + | Bv_zero_extend + (** Bit-vector zero extend. SMT-LIB: [zero_extend] (indexed) *) - | Fp_abs (** Floating-point absolute value. + | Fp_abs + (** Floating-point absolute value. SMT-LIB: [fp.abs] *) - | Fp_add - (** Floating-point addition. + | Fp_add + (** Floating-point addition. SMT-LIB: [fp.add] *) - | Fp_div - (** Floating-point division. + | Fp_div + (** Floating-point division. SMT-LIB: [fp.div] *) - | Fp_equal - (** Floating-point equality. + | Fp_equal + (** Floating-point equality. SMT-LIB: [fp.eq] *) - | Fp_fma - (** Floating-point fused multiplcation and addition. + | Fp_fma + (** Floating-point fused multiplcation and addition. SMT-LIB: [fp.fma] *) - | Fp_fp - (** Floating-point IEEE 754 value. + | Fp_fp + (** Floating-point IEEE 754 value. SMT-LIB: [fp] *) - | Fp_geq - (** Floating-point greater than or equal. + | Fp_geq + (** Floating-point greater than or equal. SMT-LIB: [fp.geq] *) - | Fp_gt - (** Floating-point greater than. + | Fp_gt + (** Floating-point greater than. SMT-LIB: [fp.gt] *) - | Fp_is_inf - (** Floating-point is infinity tester. + | Fp_is_inf + (** Floating-point is infinity tester. SMT-LIB: [fp.isInfinite] *) - | Fp_is_nan - (** Floating-point is Nan tester. + | Fp_is_nan + (** Floating-point is Nan tester. SMT-LIB: [fp.isNaN] *) - | Fp_is_neg - (** Floating-point is negative tester. + | Fp_is_neg + (** Floating-point is negative tester. SMT-LIB: [fp.isNegative] *) - | Fp_is_normal - (** Floating-point is normal tester. + | Fp_is_normal + (** Floating-point is normal tester. SMT-LIB: [fp.isNormal] *) - | Fp_is_pos - (** Floating-point is positive tester. + | Fp_is_pos + (** Floating-point is positive tester. SMT-LIB: [fp.isPositive] *) - | Fp_is_subnormal - (** Floating-point is subnormal tester. + | Fp_is_subnormal + (** Floating-point is subnormal tester. SMT-LIB: [fp.isSubnormal] *) - | Fp_is_zero - (** Floating-point is zero tester. + | Fp_is_zero + (** Floating-point is zero tester. SMT-LIB: [fp.isZero] *) - | Fp_leq - (** Floating-point less than or equal. + | Fp_leq + (** Floating-point less than or equal. SMT-LIB: [fp.leq] *) - | Fp_lt (** Floating-point less than. + | Fp_lt + (** Floating-point less than. SMT-LIB: [fp.lt] *) - | Fp_max (** Floating-point max. + | Fp_max (** Floating-point max. SMT-LIB: [fp.max] *) - | Fp_min (** Floating-point min. + | Fp_min (** Floating-point min. SMT-LIB: [fp.min] *) - | Fp_mul (** Floating-point multiplcation. + | Fp_mul + (** Floating-point multiplcation. SMT-LIB: [fp.mul] *) - | Fp_neg - (** Floating-point negation. + | Fp_neg + (** Floating-point negation. SMT-LIB: [fp.neg] *) - | Fp_rem - (** Floating-point remainder. + | Fp_rem + (** Floating-point remainder. SMT-LIB: [fp.rem] *) - | Fp_rti - (** Floating-point round to integral. + | Fp_rti + (** Floating-point round to integral. SMT-LIB: [fp.roundToIntegral] *) - | Fp_sqrt - (** Floating-point round to square root. + | Fp_sqrt + (** Floating-point round to square root. SMT-LIB: [fp.sqrt] *) - | Fp_sub - (** Floating-point round to subtraction. + | Fp_sub + (** Floating-point round to subtraction. SMT-LIB: [fp.sqrt] *) - | Fp_to_fp_from_bv - (** Floating-point to_fp from IEEE 754 bit-vector. + | Fp_to_fp_from_bv + (** Floating-point to_fp from IEEE 754 bit-vector. SMT-LIB: [to_fp] (indexed) *) - | Fp_to_fp_from_fp - (** Floating-point to_fp from floating-point. + | Fp_to_fp_from_fp + (** Floating-point to_fp from floating-point. SMT-LIB: [to_fp] (indexed) *) - | Fp_to_fp_from_sbv - (** Floating-point to_fp from signed bit-vector value. + | Fp_to_fp_from_sbv + (** Floating-point to_fp from signed bit-vector value. SMT-LIB: [to_fp] (indexed) *) - | Fp_to_fp_from_ubv - (** Floating-point to_fp from unsigned bit-vector value. + | Fp_to_fp_from_ubv + (** Floating-point to_fp from unsigned bit-vector value. SMT-LIB: [to_fp_unsigned] (indexed) *) - | Fp_to_sbv - (** Floating-point to_sbv. + | Fp_to_sbv + (** Floating-point to_sbv. SMT-LIB: [fp.to_sbv] (indexed) *) - | Fp_to_ubv - (** Floating-point to_ubv. + | Fp_to_ubv + (** Floating-point to_ubv. SMT-LIB: [fp.to_ubv] (indexed) *) - val to_string : t -> string - (** + val to_string : t -> string + (** [to_string t] get string representation of this kind. @return String representation of this kind. *) -end + end -module Term : sig - (** {1:term Term} *) + module Term : sig + (** {1:term Term} *) - type t - (** A Bitwuzla term. *) + type t + (** A Bitwuzla term. *) - (** {2:sort_util Util} *) + (** {2:sort_util Util} *) - val hash : t -> int - (** + val hash : t -> int + (** [hash t] compute the hash value for a term. @@ -1063,8 +1098,8 @@ module Term : sig @return The hash value of the term. *) - val equal : t -> t -> bool - (** + val equal : t -> t -> bool + (** [equal a b] Syntactical equality operator. @@ -1073,8 +1108,8 @@ module Term : sig @return True if the given terms are equal. *) - val compare : t -> t -> int - (** + val compare : t -> t -> int + (** [compare a b] Syntactical comparison operator. @@ -1085,8 +1120,8 @@ module Term : sig a negative number otherwise. *) - val pp : Format.formatter -> t -> unit - (** + val pp : Format.formatter -> t -> unit + (** [pp formatter t] print term. @@ -1096,8 +1131,8 @@ module Term : sig @param t The term. *) - val pp_smt2 : bv_format:int -> Format.formatter -> t -> unit - (** + val pp_smt2 : bv_format:int -> Format.formatter -> t -> unit + (** [pp_smt2 base formatter t] print term in SMTlib format. @@ -1107,8 +1142,8 @@ module Term : sig @param t The term. *) - val to_string : ?bv_format:int -> t -> string - (** + val to_string : ?bv_format:int -> t -> string + (** [to_string t ~bv_format] get string representation of this term. @@ -1120,10 +1155,10 @@ module Term : sig @return String representation of this term. *) - (** {2:term_query Query} *) + (** {2:term_query Query} *) - val id : t -> int64 - (** + val id : t -> int64 + (** [id t] get the id of this term. @@ -1131,8 +1166,8 @@ module Term : sig @return The id value of the term. *) - val kind : t -> Kind.t - (** + val kind : t -> Kind.t + (** [kind t] get the kind of a term. @@ -1141,8 +1176,8 @@ module Term : sig @return The kind of the given term. *) - val sort : t -> Sort.t - (** + val sort : t -> Sort.t + (** [sort t] get the sort of a term. @@ -1151,8 +1186,8 @@ module Term : sig @return The sort of the term. *) - val num_children : t -> int - (** + val num_children : t -> int + (** [num_children t] get the number of child terms of a term. @@ -1161,8 +1196,8 @@ module Term : sig @return The number children of [t]. *) - val children : t -> t array - (** + val children : t -> t array + (** [children t] get the child terms of a term. @@ -1171,8 +1206,8 @@ module Term : sig @return The children of [t] as an array of terms. *) - val get : t -> int -> t - (** + val get : t -> int -> t + (** [get t i] return child at position [i]. @@ -1182,8 +1217,8 @@ module Term : sig @return The child node at position [i]. *) - val num_indices : t -> int - (** + val num_indices : t -> int + (** [num_indices t] get the number of indices of an indexed term. @@ -1194,8 +1229,8 @@ module Term : sig @return The number of indices of [t]. *) - val indices : t -> int array - (** + val indices : t -> int array + (** [indices t] get the indices of an indexed term. @@ -1206,8 +1241,8 @@ module Term : sig @return The children of [t] as an array of terms. *) - val symbol : t -> string - (** + val symbol : t -> string + (** [symbol t] get the symbol of a term. @@ -1218,8 +1253,8 @@ module Term : sig @raise Not_found if no symbol is defined. *) - val is_const : t -> bool - (** + val is_const : t -> bool + (** [is_const t] determine if a term is a constant. @@ -1228,8 +1263,8 @@ module Term : sig @return [true] if [t] is a constant. *) - val is_variable : t -> bool - (** + val is_variable : t -> bool + (** [is_variable t] determine if a term is a variable. @@ -1238,8 +1273,8 @@ module Term : sig @return [true] if [t] is a variable. *) - val is_value : t -> bool - (** + val is_value : t -> bool + (** [is_value t] determine if a term is a value. @@ -1248,8 +1283,8 @@ module Term : sig @return [true] if [t] is a value. *) - val is_bv_value_zero : t -> bool - (** + val is_bv_value_zero : t -> bool + (** [is_bv_value_zero t] determine if a term is a bit-vector value representing zero. @@ -1258,8 +1293,8 @@ module Term : sig @return [true] if [t] is a bit-vector zero value. *) - val is_bv_value_one : t -> bool - (** + val is_bv_value_one : t -> bool + (** [is_bv_value_one t] determine if a term is a bit-vector value representing one. @@ -1268,8 +1303,8 @@ module Term : sig @return [true] if [t] is a bit-vector one value. *) - val is_bv_value_ones : t -> bool - (** + val is_bv_value_ones : t -> bool + (** [is_bv_value_ones t] determine if a term is a bit-vector value with all bits set to one. @@ -1278,8 +1313,8 @@ module Term : sig @return [true] if [t] is a bit-vector value with all bits set to one. *) - val is_bv_value_min_signed : t -> bool - (** + val is_bv_value_min_signed : t -> bool + (** [is_bv_value_min_signed t] determine if a term is a bit-vector minimum signed value. @@ -1289,8 +1324,8 @@ module Term : sig set to 1 and all other bits set to 0. *) - val is_bv_value_max_signed : t -> bool - (** + val is_bv_value_max_signed : t -> bool + (** [is_bv_value_max_signed t] determine if a term is a bit-vector maximum signed value. @@ -1300,8 +1335,8 @@ module Term : sig set to 0 and all other bits set to 1. *) - val is_fp_value_pos_zero : t -> bool - (** + val is_fp_value_pos_zero : t -> bool + (** [is_fp_value_pos_zero t] determine if a term is a floating-point positive zero (+zero) value. @@ -1310,8 +1345,8 @@ module Term : sig @return [true] if [t] is a floating-point +zero value. *) - val is_fp_value_neg_zero : t -> bool - (** + val is_fp_value_neg_zero : t -> bool + (** [is_fp_value_neg_zero t] determine if a term is a floating-point value negative zero (-zero). @@ -1320,8 +1355,8 @@ module Term : sig @return [true] if [t] is a floating-point value negative zero. *) - val is_fp_value_pos_inf : t -> bool - (** + val is_fp_value_pos_inf : t -> bool + (** [is_fp_value_pos_inf t] determine if a term is a floating-point positive infinity (+oo) value. @@ -1330,8 +1365,8 @@ module Term : sig @return [true] if [t] is a floating-point +oo value. *) - val is_fp_value_neg_inf : t -> bool - (** + val is_fp_value_neg_inf : t -> bool + (** [is_fp_value_neg_inf t] determine if a term is a floating-point negative infinity (-oo) value. @@ -1340,8 +1375,8 @@ module Term : sig @return [true] if [t] is a floating-point -oo value. *) - val is_fp_value_nan : t -> bool - (** + val is_fp_value_nan : t -> bool + (** [is_fp_value_nan t] determine if a term is a floating-point NaN value. @@ -1350,8 +1385,8 @@ module Term : sig @return [true] if [t] is a floating-point NaN value. *) - val is_rm_value_rna : t -> bool - (** + val is_rm_value_rna : t -> bool + (** [is_rm_value_rna t] determine if a term is a rounding mode RNA value. @@ -1360,8 +1395,8 @@ module Term : sig @return [true] if [t] is a rounding mode RNA value. *) - val is_rm_value_rne : t -> bool - (** + val is_rm_value_rne : t -> bool + (** [is_rm_value_rna t] determine if a term is a rounding mode RNE value. @@ -1370,8 +1405,8 @@ module Term : sig @return [true] if [t] is a rounding mode RNE value. *) - val is_rm_value_rtn : t -> bool - (** + val is_rm_value_rtn : t -> bool + (** [is_rm_value_rna t] determine if a term is a rounding mode RTN value. @@ -1380,8 +1415,8 @@ module Term : sig @return [true] if [t] is a rounding mode RTN value. *) - val is_rm_value_rtp : t -> bool - (** + val is_rm_value_rtp : t -> bool + (** [is_rm_value_rna t] determine if a term is a rounding mode RTP value. @@ -1390,8 +1425,8 @@ module Term : sig @return [true] if [t] is a rounding mode RTP value. *) - val is_rm_value_rtz : t -> bool - (** + val is_rm_value_rtz : t -> bool + (** [is_rm_value_rna t] determine if a term is a rounding mode RTZ value. @@ -1400,48 +1435,48 @@ module Term : sig @return [true] if [t] is a rounding mode RTZ value. *) - type _ cast = - | Bool : bool cast (** for Boolean values *) - | RoundingMode : RoundingMode.t cast (** for rounding mode values *) - | String : { base : int } -> string cast - (** for any value + type _ cast = + | Bool : bool cast (** for Boolean values *) + | RoundingMode : RoundingMode.t cast (** for rounding mode values *) + | String : { base : int } -> string cast + (** for any value (Boolean, RoundingMode, bit-vector and floating-point) *) - | IEEE_754 : (string * string * string) cast - (** for floating-point values as strings + | IEEE_754 : (string * string * string) cast + (** for floating-point values as strings for sign bit, exponent and significand *) - | Z : Z.t cast (** for bit-vector *) + | Z : Z.t cast (** for bit-vector *) - val value : 'a cast -> t -> 'a - (** + val value : 'a cast -> t -> 'a + (** [value kind t] get value from value term. @param kind The type of the value representation. @return The value of [t] in a given representation. *) -end + end -module Result : sig - (** A satisfiability result. *) - type t = Sat (** sat *) | Unsat (** unsat *) | Unknown (** unknown *) + module Result : sig + (** A satisfiability result. *) + type t = Sat (** sat *) | Unsat (** unsat *) | Unknown (** unknown *) - val to_string : t -> string - (** + val to_string : t -> string + (** [to_string t] get string representation of this result. @return String representation of this result. *) -end + end -module Solver : sig - (** {1 Solver} *) + module Solver : sig + (** {1 Solver} *) - type t - (** The Bitwuzla solver. *) + type t + (** The Bitwuzla solver. *) - val configure_terminator : t -> (unit -> bool) option -> unit - (** + val configure_terminator : t -> (unit -> bool) option -> unit + (** [configure_terminator t f] configure a termination callback function. @@ -1452,8 +1487,8 @@ module Solver : sig @param f The callback function, returns [true] if [t] should be terminated. *) - val create : Options.t -> t - (** + val create : Options.t -> t + (** [create options] create a new Bitwuzla instance. @@ -1465,10 +1500,10 @@ module Solver : sig @return The created Bitwuzla instance. *) - (** {2 Formula} *) + (** {2 Formula} *) - val push : t -> int -> unit - (** + val push : t -> int -> unit + (** [push t nlevels] push context levels. @@ -1476,8 +1511,8 @@ module Solver : sig @param nlevels The number of context levels to push. *) - val pop : t -> int -> unit - (** + val pop : t -> int -> unit + (** [pop t nlevels] pop context levels. @@ -1485,8 +1520,8 @@ module Solver : sig @param nlevels The number of context levels to pop. *) - val assert_formula : t -> Term.t -> unit - (** + val assert_formula : t -> Term.t -> unit + (** [mk_assert t term] assert formula. @@ -1494,16 +1529,16 @@ module Solver : sig @param term The formula to assert. *) - val get_assertions : t -> Term.t array - (** + val get_assertions : t -> Term.t array + (** [get_assertions t] get the set of currently asserted formulas. @return The assertion formulas. *) - val pp_formula : Format.formatter -> t -> unit - (** + val pp_formula : Format.formatter -> t -> unit + (** [pp_formula formatter t] print the current input formula. @@ -1511,18 +1546,18 @@ module Solver : sig @param t The Bitwuzla instance. *) - (** {2 Check} *) + (** {2 Check} *) - val simplify : t -> unit - (** + val simplify : t -> unit + (** [simplify t] simplify the current input formula. @param t The Bitwuzla instance. *) - val check_sat : ?assumptions:Term.t array -> t -> Result.t - (** + val check_sat : ?assumptions:Term.t array -> t -> Result.t + (** [check_sat ~assumptions t] check satisfiability of current input formula. @@ -1540,10 +1575,10 @@ module Solver : sig This can happen when [t] was terminated via a termination callback. *) - (** {2 Sat} *) + (** {2 Sat} *) - val get_value : t -> Term.t -> Term.t - (** + val get_value : t -> Term.t -> Term.t + (** [get_value t term] get a term representing the model value of a given term. @@ -1555,10 +1590,10 @@ module Solver : sig @return A term representing the model value of term [term]. *) - (** {2 Unsat} *) + (** {2 Unsat} *) - val is_unsat_assumption : t -> Term.t -> bool - (** + val is_unsat_assumption : t -> Term.t -> bool + (** [is_unsat_assumption t term] determine if an assumption is an unsat assumption. @@ -1577,8 +1612,8 @@ module Solver : sig @return [true] if given assumption is an unsat assumption. *) - val get_unsat_assumptions : t -> Term.t array - (** + val get_unsat_assumptions : t -> Term.t array + (** [get_unsat_assumptions t] get the set of unsat assumptions. @@ -1596,8 +1631,8 @@ module Solver : sig @return An array with unsat assumptions. *) - val get_unsat_core : t -> Term.t array - (** + val get_unsat_core : t -> Term.t array + (** [get_unsat_core t] get the set unsat core (unsat assertions). @@ -1613,9 +1648,9 @@ module Solver : sig @return An array with unsat assertions. *) - (** {2 Expert} *) - val unsafe_delete : t -> unit - (** + (** {2 Expert} *) + val unsafe_delete : t -> unit + (** [delete t] delete a Bitwuzla instance. @@ -1625,13 +1660,13 @@ module Solver : sig @param t The Bitwuzla instance to delete. *) - val pp_statistics : Format.formatter -> t -> unit -end + val pp_statistics : Format.formatter -> t -> unit + end -(** {2:sort_constructor Sort constructor} *) + (** {2:sort_constructor Sort constructor} *) -val mk_array_sort : Sort.t -> Sort.t -> Sort.t -(** + val mk_array_sort : Sort.t -> Sort.t -> Sort.t + (** [mk_array_sort index element] create an array sort. @@ -1641,8 +1676,8 @@ val mk_array_sort : Sort.t -> Sort.t -> Sort.t @return An array sort which maps sort [index] to sort [element]. *) -val mk_bool_sort : unit -> Sort.t -(** + val mk_bool_sort : unit -> Sort.t + (** [mk_bool_sort ()] create a Boolean sort. @@ -1651,8 +1686,8 @@ val mk_bool_sort : unit -> Sort.t @return A Boolean sort. *) -val mk_bv_sort : int -> Sort.t -(** + val mk_bv_sort : int -> Sort.t + (** [mk_bv_sort size] create a bit-vector sort of given size. @@ -1661,8 +1696,8 @@ val mk_bv_sort : int -> Sort.t @return A bit-vector sort of given size. *) -val mk_fp_sort : int -> int -> Sort.t -(** + val mk_fp_sort : int -> int -> Sort.t + (** [mk_fp_sort exp_size sig_size] create a floating-point sort of given exponent and significand size. @@ -1672,8 +1707,8 @@ val mk_fp_sort : int -> int -> Sort.t @return A floating-point sort of given format. *) -val mk_fun_sort : Sort.t array -> Sort.t -> Sort.t -(** + val mk_fun_sort : Sort.t array -> Sort.t -> Sort.t + (** [mk_fun_sort domain codomain] create a function sort. @@ -1683,16 +1718,16 @@ val mk_fun_sort : Sort.t array -> Sort.t -> Sort.t @return A function sort of given domain and codomain sorts. *) -val mk_rm_sort : unit -> Sort.t -(** + val mk_rm_sort : unit -> Sort.t + (** [mk_rm_sort ()] create a Roundingmode sort. @return A Roundingmode sort. *) -val mk_uninterpreted_sort : ?symbol:string -> unit -> Sort.t -(** + val mk_uninterpreted_sort : ?symbol:string -> unit -> Sort.t + (** [mk_uninterpreted_sort name] create an uninterpreted sort. @@ -1702,12 +1737,12 @@ val mk_uninterpreted_sort : ?symbol:string -> unit -> Sort.t @return An uninterpreted sort. *) -(** {2:term_constructor Term constructor} *) + (** {2:term_constructor Term constructor} *) -(** {3 Value} *) + (** {3 Value} *) -val mk_true : unit -> Term.t -(** + val mk_true : unit -> Term.t + (** [mk_true ()] create a true value. @@ -1716,8 +1751,8 @@ val mk_true : unit -> Term.t @return A term representing the bit-vector value 1 of size 1. *) -val mk_false : unit -> Term.t -(** + val mk_false : unit -> Term.t + (** [mk_false ()] create a false value. @@ -1726,8 +1761,8 @@ val mk_false : unit -> Term.t @return A term representing the bit-vector value 0 of size 1. *) -val mk_bv_zero : Sort.t -> Term.t -(** + val mk_bv_zero : Sort.t -> Term.t + (** [mk_bv_zero sort] create a bit-vector value zero. @@ -1736,8 +1771,8 @@ val mk_bv_zero : Sort.t -> Term.t @return A term representing the bit-vector value 0 of given sort. *) -val mk_bv_one : Sort.t -> Term.t -(** + val mk_bv_one : Sort.t -> Term.t + (** [mk_bv_one sort] create a bit-vector value one. @@ -1746,8 +1781,8 @@ val mk_bv_one : Sort.t -> Term.t @return A term representing the bit-vector value 1 of given sort. *) -val mk_bv_ones : Sort.t -> Term.t -(** + val mk_bv_ones : Sort.t -> Term.t + (** [mk_bv_ones sort] create a bit-vector value where all bits are set to 1. @@ -1757,8 +1792,8 @@ val mk_bv_ones : Sort.t -> Term.t where all bits are set to 1. *) -val mk_bv_min_signed : Sort.t -> Term.t -(** + val mk_bv_min_signed : Sort.t -> Term.t + (** [mk_bv_min_signed sort] create a bit-vector minimum signed value. @@ -1768,8 +1803,8 @@ val mk_bv_min_signed : Sort.t -> Term.t is set to 1 and all remaining bits are set to 0. *) -val mk_bv_max_signed : Sort.t -> Term.t -(** + val mk_bv_max_signed : Sort.t -> Term.t + (** [mk_bv_max_signed sort] create a bit-vector maximum signed value. @@ -1779,8 +1814,8 @@ val mk_bv_max_signed : Sort.t -> Term.t is set to 0 and all remaining bits are set to 1. *) -val mk_bv_value : Sort.t -> string -> int -> Term.t -(** + val mk_bv_value : Sort.t -> string -> int -> Term.t + (** [mk_bv_value sort value base] create a bit-vector value from its string representation. @@ -1795,8 +1830,8 @@ val mk_bv_value : Sort.t -> string -> int -> Term.t @return A term representing the bit-vector value of given sort. *) -val mk_bv_value_int : Sort.t -> int -> Term.t -(** + val mk_bv_value_int : Sort.t -> int -> Term.t + (** [mk_bv_value_int sort value] create a bit-vector value from its unsigned integer representation. @@ -1809,8 +1844,8 @@ val mk_bv_value_int : Sort.t -> int -> Term.t @return A term representing the bit-vector value of given sort. *) -val mk_bv_value_int64 : Sort.t -> int64 -> Term.t -(** + val mk_bv_value_int64 : Sort.t -> int64 -> Term.t + (** [mk_bv_value_int64 sort value] create a bit-vector value from its unsigned integer representation. @@ -1823,8 +1858,8 @@ val mk_bv_value_int64 : Sort.t -> int64 -> Term.t @return A term representing the bit-vector value of given sort. *) -val mk_fp_pos_zero : Sort.t -> Term.t -(** + val mk_fp_pos_zero : Sort.t -> Term.t + (** [mk_fp_pos_zero sort] create a floating-point positive zero value (SMT-LIB: [+zero]). @@ -1834,8 +1869,8 @@ val mk_fp_pos_zero : Sort.t -> Term.t floating-point sort. *) -val mk_fp_neg_zero : Sort.t -> Term.t -(** + val mk_fp_neg_zero : Sort.t -> Term.t + (** [mk_fp_neg_zero sort] create a floating-point negative zero value (SMT-LIB: [-zero]). @@ -1845,8 +1880,8 @@ val mk_fp_neg_zero : Sort.t -> Term.t floating-point sort. *) -val mk_fp_pos_inf : Sort.t -> Term.t -(** + val mk_fp_pos_inf : Sort.t -> Term.t + (** [mk_fp_pos_inf sort] create a floating-point positive infinity value (SMT-LIB: [+oo]). @@ -1856,8 +1891,8 @@ val mk_fp_pos_inf : Sort.t -> Term.t given floating-point sort. *) -val mk_fp_neg_inf : Sort.t -> Term.t -(** + val mk_fp_neg_inf : Sort.t -> Term.t + (** [mk_fp_neg_inf sort] create a floating-point negative infinity value (SMT-LIB: [-oo]). @@ -1867,8 +1902,8 @@ val mk_fp_neg_inf : Sort.t -> Term.t given floating-point sort. *) -val mk_fp_nan : Sort.t -> Term.t -(** + val mk_fp_nan : Sort.t -> Term.t + (** [mk_fp_nan sort] create a floating-point NaN value. @@ -1878,8 +1913,8 @@ val mk_fp_nan : Sort.t -> Term.t floating-point sort. *) -val mk_fp_value : Term.t -> Term.t -> Term.t -> Term.t -(** + val mk_fp_value : Term.t -> Term.t -> Term.t -> Term.t + (** [mk_fp_value bv_sign bv_exponent bv_significand] create a floating-point value from its IEEE 754 standard representation given as three bitvectors representing the sign bit, the exponent and the @@ -1892,8 +1927,8 @@ val mk_fp_value : Term.t -> Term.t -> Term.t -> Term.t @return A term representing the floating-point value. *) -val mk_fp_value_from_real : Sort.t -> Term.t -> string -> Term.t -(** + val mk_fp_value_from_real : Sort.t -> Term.t -> string -> Term.t + (** [mk_fp_value_from_real t sort rm real] create a floating-point value from its real representation, given as a decimal string, with respect to given rounding mode. @@ -1905,8 +1940,8 @@ val mk_fp_value_from_real : Sort.t -> Term.t -> string -> Term.t @return A term representing the floating-point value of given sort. *) -val mk_fp_value_from_rational : Sort.t -> Term.t -> string -> string -> Term.t -(** + val mk_fp_value_from_rational : Sort.t -> Term.t -> string -> string -> Term.t + (** [mk_fp_value_from_rational sort rm num den] create a floating-point value from its rational representation, given as a two decimal strings representing the numerator and denominator, with respect @@ -1920,8 +1955,8 @@ val mk_fp_value_from_rational : Sort.t -> Term.t -> string -> string -> Term.t @return A term representing the floating-point value of given sort. *) -val mk_rm_value : RoundingMode.t -> Term.t -(** + val mk_rm_value : RoundingMode.t -> Term.t + (** [mk_rm_value rm] create a rounding mode value. @@ -1930,10 +1965,10 @@ val mk_rm_value : RoundingMode.t -> Term.t @return A term representing the rounding mode value. *) -(** {3 Expression} *) + (** {3 Expression} *) -val mk_term1 : Kind.t -> Term.t -> Term.t -(** + val mk_term1 : Kind.t -> Term.t -> Term.t + (** [mk_term1 kind arg] create a term of given kind with one argument term. @@ -1943,8 +1978,8 @@ val mk_term1 : Kind.t -> Term.t -> Term.t @return A term representing an operation of given kind. *) -val mk_term2 : Kind.t -> Term.t -> Term.t -> Term.t -(** + val mk_term2 : Kind.t -> Term.t -> Term.t -> Term.t + (** [mk_term2 kind arg0 arg1] create a term of given kind with two argument terms. @@ -1955,8 +1990,8 @@ val mk_term2 : Kind.t -> Term.t -> Term.t -> Term.t @return A term representing an operation of given kind. *) -val mk_term3 : Kind.t -> Term.t -> Term.t -> Term.t -> Term.t -(** + val mk_term3 : Kind.t -> Term.t -> Term.t -> Term.t -> Term.t + (** [mk_term3 kind arg0 arg1 arg2] create a term of given kind with three argument terms. @@ -1968,8 +2003,8 @@ val mk_term3 : Kind.t -> Term.t -> Term.t -> Term.t -> Term.t @return A term representing an operation of given kind. *) -val mk_term1_indexed1 : Kind.t -> Term.t -> int -> Term.t -(** + val mk_term1_indexed1 : Kind.t -> Term.t -> int -> Term.t + (** [mk_term1_indexed1 kind arg idx] create an indexed term of given kind with one argument term and one index. @@ -1980,8 +2015,8 @@ val mk_term1_indexed1 : Kind.t -> Term.t -> int -> Term.t @return A term representing an indexed operation of given kind. *) -val mk_term1_indexed2 : Kind.t -> Term.t -> int -> int -> Term.t -(** + val mk_term1_indexed2 : Kind.t -> Term.t -> int -> int -> Term.t + (** [mk_term1_indexed2 kind arg idx0 idx1] create an indexed term of given kind with one argument term and two indices. @@ -1993,8 +2028,8 @@ val mk_term1_indexed2 : Kind.t -> Term.t -> int -> int -> Term.t @return A term representing an indexed operation of given kind. *) -val mk_term2_indexed1 : Kind.t -> Term.t -> Term.t -> int -> Term.t -(** + val mk_term2_indexed1 : Kind.t -> Term.t -> Term.t -> int -> Term.t + (** [mk_term2_indexed1 t kind arg0 arg1 idx] create an indexed term of given kind with two argument terms and one index. @@ -2006,8 +2041,8 @@ val mk_term2_indexed1 : Kind.t -> Term.t -> Term.t -> int -> Term.t @return A term representing an indexed operation of given kind. *) -val mk_term2_indexed2 : Kind.t -> Term.t -> Term.t -> int -> int -> Term.t -(** + val mk_term2_indexed2 : Kind.t -> Term.t -> Term.t -> int -> int -> Term.t + (** [mk_term2_indexed2 t kind arg0 arg1 idx0 idx1] create an indexed term of given kind with two argument terms and two indices. @@ -2020,8 +2055,8 @@ val mk_term2_indexed2 : Kind.t -> Term.t -> Term.t -> int -> int -> Term.t @return A term representing an indexed operation of given kind. *) -val mk_term : Kind.t -> ?indices:int array -> Term.t array -> Term.t -(** + val mk_term : Kind.t -> ?indices:int array -> Term.t array -> Term.t + (** [mk_term kind args ~indices] create an indexed term of given kind with the given argument terms and indices. @@ -2033,8 +2068,8 @@ val mk_term : Kind.t -> ?indices:int array -> Term.t array -> Term.t @return A term representing an indexed operation of given kind. *) -val mk_const : ?symbol:string -> Sort.t -> Term.t -(** + val mk_const : ?symbol:string -> Sort.t -> Term.t + (** [mk_const sort ~symbol] create a (first-order) constant of given sort with given symbol. @@ -2046,8 +2081,8 @@ val mk_const : ?symbol:string -> Sort.t -> Term.t @return A term representing the constant. *) -val mk_const_array : Sort.t -> Term.t -> Term.t -(** + val mk_const_array : Sort.t -> Term.t -> Term.t + (** [mk_const_array sort value] create a one-dimensional constant array of given sort, initialized with given value. @@ -2058,8 +2093,8 @@ val mk_const_array : Sort.t -> Term.t -> Term.t @return A term representing a constant array of given sort. *) -val mk_var : ?symbol:string -> Sort.t -> Term.t -(** + val mk_var : ?symbol:string -> Sort.t -> Term.t + (** [mk_var sort ~symbol] create a variable of given sort with given symbol. @@ -2071,10 +2106,10 @@ val mk_var : ?symbol:string -> Sort.t -> Term.t @return A term representing the variable. *) -(** {2 Util} *) + (** {2 Util} *) -val substitute_term : Term.t -> (Term.t * Term.t) array -> Term.t -(** + val substitute_term : Term.t -> (Term.t * Term.t) array -> Term.t + (** [substitute t term map] substitute a set of keys with their corresponding values in the given term. @@ -2084,8 +2119,8 @@ val substitute_term : Term.t -> (Term.t * Term.t) array -> Term.t @return The resulting term from this substitution. *) -val substitute_terms : Term.t array -> (Term.t * Term.t) array -> unit -(** + val substitute_terms : Term.t array -> (Term.t * Term.t) array -> unit + (** [substitute_terms t terms map] substitute a set of keys with their corresponding values in the set of given terms. @@ -2096,3 +2131,12 @@ val substitute_terms : Term.t array -> (Term.t * Term.t) array -> unit @param terms The terms in which the keys are to be substituted. @param map The key/value associations. *) +end + +module Make () : S +(** + Create a new independent Bitwuzla instance that can run in parallel + to all other ones. + *) + +include S diff --git a/cxx_stubs.cpp b/cxx_stubs.cpp index 196da17..d752b17 100644 --- a/cxx_stubs.cpp +++ b/cxx_stubs.cpp @@ -96,6 +96,35 @@ int Format::overflow (int c) } \ catch (bitwuzla::Exception &e) { caml_invalid_argument(e.msg().c_str()); } +#define Manager_val(v) (*(bitwuzla::TermManager **)Data_custom_val(v)) + +static void manager_delete (value vt) +{ + delete Manager_val(vt); +} + +static struct custom_operations manager_operations = + { + "https://bitwuzla.github.io", + manager_delete, + custom_compare_default, + custom_hash_default, + custom_serialize_default, + custom_deserialize_default, + custom_compare_ext_default, + custom_fixed_length_default + }; + +extern "C" CAMLprim value +ocaml_bitwuzla_cxx_manager_new () +{ + bitwuzla::TermManager *t = new bitwuzla::TermManager(); + value vt = caml_alloc_custom(&manager_operations, + sizeof(bitwuzla::TermManager *), 0, 1); + Manager_val(vt) = t; + return vt; +} + class Options : public bitwuzla::Options { public: @@ -446,53 +475,55 @@ ocaml_bitwuzla_cxx_sort_pp (mlvalue vf, mlvalue vt) } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_array_sort (mlvalue vi, mlvalue ve) +ocaml_bitwuzla_cxx_mk_array_sort (mlvalue vm, mlvalue vi, mlvalue ve) { CAMLparam2(vi, ve); mlvalue custom; - new(&sort_operations, &custom) Sort(bitwuzla::mk_array_sort(*Sort_val(vi), - *Sort_val(ve))); + new(&sort_operations, &custom) + Sort(Manager_val(vm)->mk_array_sort(*Sort_val(vi), *Sort_val(ve))); CAMLreturn(custom); } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bool_sort () +ocaml_bitwuzla_cxx_mk_bool_sort (mlvalue vm) { mlvalue custom; - new(&sort_operations, &custom) Sort(bitwuzla::mk_bool_sort()); + new(&sort_operations, &custom) Sort(Manager_val(vm)->mk_bool_sort()); return custom; } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_bv_sort (intnat size) +native_bitwuzla_cxx_mk_bv_sort (mlvalue vm, intnat size) { mlvalue custom; - new(&sort_operations, &custom) Sort(bitwuzla::mk_bv_sort(size)); + new(&sort_operations, &custom) Sort(Manager_val(vm)->mk_bv_sort(size)); return custom; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_sort (mlvalue vsize) +ocaml_bitwuzla_cxx_mk_bv_sort (mlvalue vm, mlvalue vsize) { - return native_bitwuzla_cxx_mk_bv_sort(Long_val(vsize)); + return native_bitwuzla_cxx_mk_bv_sort(vm, Long_val(vsize)); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_fp_sort (intnat exp_size, intnat sig_size) +native_bitwuzla_cxx_mk_fp_sort (mlvalue vm, intnat exp_size, intnat sig_size) { mlvalue custom; - new(&sort_operations, &custom) Sort(bitwuzla::mk_fp_sort(exp_size, sig_size)); + new(&sort_operations, &custom) + Sort(Manager_val(vm)->mk_fp_sort(exp_size, sig_size)); return custom; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_sort (mlvalue vexp_size, mlvalue vsig_size) +ocaml_bitwuzla_cxx_mk_fp_sort (mlvalue vm, mlvalue vexp_size, mlvalue vsig_size) { - return native_bitwuzla_cxx_mk_fp_sort(Long_val(vexp_size), Long_val(vsig_size)); + return native_bitwuzla_cxx_mk_fp_sort(vm, Long_val(vexp_size), + Long_val(vsig_size)); } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fun_sort (mlvalue vdomain, mlvalue vcodomain) +ocaml_bitwuzla_cxx_mk_fun_sort (mlvalue vm, mlvalue vdomain, mlvalue vcodomain) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vcodomain); @@ -503,28 +534,29 @@ ocaml_bitwuzla_cxx_mk_fun_sort (mlvalue vdomain, mlvalue vcodomain) for (size_t i = 0; i < arity; i += 1) domain.emplace_back(*Sort_val(Field(vdomain, i))); new(&sort_operations, &custom) - Sort(bitwuzla::mk_fun_sort(domain, *Sort_val(vcodomain))); + Sort(Manager_val(vm)->mk_fun_sort(domain, *Sort_val(vcodomain))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_rm_sort () +ocaml_bitwuzla_cxx_mk_rm_sort (mlvalue vm) { mlvalue custom; - new(&sort_operations, &custom) Sort(bitwuzla::mk_rm_sort()); + new(&sort_operations, &custom) Sort(Manager_val(vm)->mk_rm_sort()); return custom; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_uninterpreted_sort (mlvalue vopt) +ocaml_bitwuzla_cxx_mk_uninterpreted_sort (mlvalue vm, mlvalue vopt) { CAMLparam1(vopt); mlvalue custom; std::optional symbol; if (Is_some(vopt)) symbol.emplace(std::string(String_val(Field(vopt, 0)))); - new(&sort_operations, &custom) Sort(bitwuzla::mk_uninterpreted_sort(symbol)); + new(&sort_operations, &custom) + Sort(Manager_val(vm)->mk_uninterpreted_sort(symbol)); CAMLreturn(custom); } @@ -923,209 +955,215 @@ ocaml_bitwuzla_cxx_term_zarith_value (mlvalue vt) } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_true () +ocaml_bitwuzla_cxx_mk_true (mlvalue vm) { mlvalue custom; - new(&term_operations, &custom) Term(bitwuzla::mk_true()); + new(&term_operations, &custom) Term(Manager_val(vm)->mk_true()); return custom; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_false () +ocaml_bitwuzla_cxx_mk_false (mlvalue vm) { mlvalue custom; - new(&term_operations, &custom) Term(bitwuzla::mk_false()); + new(&term_operations, &custom) Term(Manager_val(vm)->mk_false()); return custom; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_zero (mlvalue vs) +ocaml_bitwuzla_cxx_mk_bv_zero (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; - new(&term_operations, &custom) Term(bitwuzla::mk_bv_zero(*Sort_val(vs))); + new(&term_operations, &custom) + Term(Manager_val(vm)->mk_bv_zero(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_one (mlvalue vs) +ocaml_bitwuzla_cxx_mk_bv_one (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; - new(&term_operations, &custom) Term(bitwuzla::mk_bv_one(*Sort_val(vs))); + new(&term_operations, &custom) + Term(Manager_val(vm)->mk_bv_one(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_ones (mlvalue vs) +ocaml_bitwuzla_cxx_mk_bv_ones (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; - new(&term_operations, &custom) Term(bitwuzla::mk_bv_ones(*Sort_val(vs))); + new(&term_operations, &custom) + Term(Manager_val(vm)->mk_bv_ones(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_min_signed (mlvalue vs) +ocaml_bitwuzla_cxx_mk_bv_min_signed (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_bv_min_signed(*Sort_val(vs))); + Term(Manager_val(vm)->mk_bv_min_signed(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_max_signed (mlvalue vs) +ocaml_bitwuzla_cxx_mk_bv_max_signed (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_bv_max_signed(*Sort_val(vs))); + Term(Manager_val(vm)->mk_bv_max_signed(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_bv_value (mlvalue vs, mlvalue vv, intnat base) +native_bitwuzla_cxx_mk_bv_value +(mlvalue vm, mlvalue vs, mlvalue vv, intnat base) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); const std::string val = String_val(vv); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_bv_value(*Sort_val(vs), val, base)); + Term(Manager_val(vm)->mk_bv_value(*Sort_val(vs), val, base)); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_value (mlvalue vs, mlvalue vv, intnat base) +ocaml_bitwuzla_cxx_mk_bv_value (mlvalue vm, mlvalue vs, mlvalue vv, intnat base) { - return native_bitwuzla_cxx_mk_bv_value(vs, vv, Long_val(base)); + return native_bitwuzla_cxx_mk_bv_value(vm, vs, vv, Long_val(base)); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_bv_value_int64 (mlvalue vs, intnat val) +native_bitwuzla_cxx_mk_bv_value_int64 (mlvalue vm, mlvalue vs, intnat val) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_bv_value_int64(*Sort_val(vs), val)); + Term(Manager_val(vm)->mk_bv_value_int64(*Sort_val(vs), val)); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_value_int (mlvalue vs, mlvalue vv) +ocaml_bitwuzla_cxx_mk_bv_value_int (mlvalue vm, mlvalue vs, mlvalue vv) { - return native_bitwuzla_cxx_mk_bv_value_int64(vs, Long_val(vv)); + return native_bitwuzla_cxx_mk_bv_value_int64(vm, vs, Long_val(vv)); } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_bv_value_int64 (mlvalue vs, mlvalue vv) +ocaml_bitwuzla_cxx_mk_bv_value_int64 (mlvalue vm, mlvalue vs, mlvalue vv) { - return native_bitwuzla_cxx_mk_bv_value_int64(vs, Int64_val(vv)); + return native_bitwuzla_cxx_mk_bv_value_int64(vm, vs, Int64_val(vv)); } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_pos_zero (mlvalue vs) +ocaml_bitwuzla_cxx_mk_fp_pos_zero (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_pos_zero(*Sort_val(vs))); + Term(Manager_val(vm)->mk_fp_pos_zero(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_neg_zero (mlvalue vs) +ocaml_bitwuzla_cxx_mk_fp_neg_zero (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_neg_zero(*Sort_val(vs))); + Term(Manager_val(vm)->mk_fp_neg_zero(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_pos_inf (mlvalue vs) +ocaml_bitwuzla_cxx_mk_fp_pos_inf (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_pos_inf(*Sort_val(vs))); + Term(Manager_val(vm)->mk_fp_pos_inf(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_neg_inf (mlvalue vs) +ocaml_bitwuzla_cxx_mk_fp_neg_inf (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_neg_inf(*Sort_val(vs))); + Term(Manager_val(vm)->mk_fp_neg_inf(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_nan (mlvalue vs) +ocaml_bitwuzla_cxx_mk_fp_nan (mlvalue vm, mlvalue vs) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam1(vs); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_nan(*Sort_val(vs))); + Term(Manager_val(vm)->mk_fp_nan(*Sort_val(vs))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_value (mlvalue v1, mlvalue v2, mlvalue v3) +ocaml_bitwuzla_cxx_mk_fp_value (mlvalue vm, mlvalue v1, mlvalue v2, mlvalue v3) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam3(v1, v2, v3); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_value(*Term_val(v1), *Term_val(v2), *Term_val(v3))); + Term(Manager_val(vm)->mk_fp_value(*Term_val(v1), *Term_val(v2), + *Term_val(v3))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_value_from_real (mlvalue vs, mlvalue vrm, mlvalue vv) +ocaml_bitwuzla_cxx_mk_fp_value_from_real +(mlvalue vm, mlvalue vs, mlvalue vrm, mlvalue vv) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam2(vs, vrm); const std::string val(String_val(vv)); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_value(*Sort_val(vs), *Term_val(vrm), val)); + Term(Manager_val(vm)->mk_fp_value(*Sort_val(vs), *Term_val(vrm), val)); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_fp_value_from_rational (mlvalue vs, mlvalue vrm, - mlvalue vnum, mlvalue vden) +ocaml_bitwuzla_cxx_mk_fp_value_from_rational +(mlvalue vm, mlvalue vs, mlvalue vrm, mlvalue vnum, mlvalue vden) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam2(vs, vrm); @@ -1133,175 +1171,186 @@ ocaml_bitwuzla_cxx_mk_fp_value_from_rational (mlvalue vs, mlvalue vrm, const std::string den(String_val(vden)); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_fp_value(*Sort_val(vs), *Term_val(vrm), num, den)); + Term(Manager_val(vm)->mk_fp_value(*Sort_val(vs), *Term_val(vrm), num, den)); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_const_array (mlvalue vs, mlvalue vv) +ocaml_bitwuzla_cxx_mk_const_array (mlvalue vm, mlvalue vs, mlvalue vv) { BITWUZLA_TRY_CATCH_BEGIN; CAMLparam2(vs, vv); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_const_array(*Sort_val(vs), *Term_val(vv))); + Term(Manager_val(vm)->mk_const_array(*Sort_val(vs), *Term_val(vv))); CAMLreturn(custom); BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_rm_value (intnat rm) +native_bitwuzla_cxx_mk_rm_value (mlvalue vm, intnat rm) { mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_rm_value((bitwuzla::RoundingMode)rm)); + Term(Manager_val(vm)->mk_rm_value((bitwuzla::RoundingMode)rm)); return custom; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_rm_value (mlvalue vrm) +ocaml_bitwuzla_cxx_mk_rm_value (mlvalue vm, mlvalue vrm) { - return native_bitwuzla_cxx_mk_rm_value(Long_val(vrm)); + return native_bitwuzla_cxx_mk_rm_value(vm, Long_val(vrm)); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term1 (intnat k, mlvalue v1) +native_bitwuzla_cxx_mk_term1 (mlvalue vm, intnat k, mlvalue v1) { BITWUZLA_TRY_CATCH_BEGIN; const std::vector args{ *Term_val(v1) }; mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term1 (intnat vk, mlvalue v1) +ocaml_bitwuzla_cxx_mk_term1 (mlvalue vm, intnat vk, mlvalue v1) { - return native_bitwuzla_cxx_mk_term1(Long_val(vk), v1); + return native_bitwuzla_cxx_mk_term1(vm, Long_val(vk), v1); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term2 (intnat k, mlvalue v1, mlvalue v2) +native_bitwuzla_cxx_mk_term2 (mlvalue vm, intnat k, mlvalue v1, mlvalue v2) { BITWUZLA_TRY_CATCH_BEGIN; const std::vector args{ *Term_val(v1), *Term_val(v2) }; mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term2 (intnat vk, mlvalue v1, mlvalue v2) +ocaml_bitwuzla_cxx_mk_term2 (mlvalue vm, intnat vk, mlvalue v1, mlvalue v2) { - return native_bitwuzla_cxx_mk_term2(Long_val(vk), v1, v2); + return native_bitwuzla_cxx_mk_term2(vm, Long_val(vk), v1, v2); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term3 (intnat k, mlvalue v1, mlvalue v2, mlvalue v3) +native_bitwuzla_cxx_mk_term3 +(mlvalue vm, intnat k, mlvalue v1, mlvalue v2, mlvalue v3) { BITWUZLA_TRY_CATCH_BEGIN; const std::vector args{ *Term_val(v1), *Term_val(v2), *Term_val(v3) }; mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term3 (intnat vk, mlvalue v1, mlvalue v2, mlvalue v3) +ocaml_bitwuzla_cxx_mk_term3 +(mlvalue vm, intnat vk, mlvalue v1, mlvalue v2, mlvalue v3) { - return native_bitwuzla_cxx_mk_term3(Long_val(vk), v1, v2, v3); + return native_bitwuzla_cxx_mk_term3(vm, Long_val(vk), v1, v2, v3); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term1_indexed1 (intnat k, mlvalue v1, intnat i) +native_bitwuzla_cxx_mk_term1_indexed1 +(mlvalue vm, intnat k, mlvalue v1, intnat i) { BITWUZLA_TRY_CATCH_BEGIN; const std::vector args{ *Term_val(v1) }; const std::vector indices{ (uint64_t)i }; mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args, indices)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args, indices)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term1_indexed1 (intnat vk, mlvalue v1, mlvalue vi) +ocaml_bitwuzla_cxx_mk_term1_indexed1 +(mlvalue vm, intnat vk, mlvalue v1, mlvalue vi) { - return native_bitwuzla_cxx_mk_term1_indexed1(Long_val(vk), v1, Long_val(vi)); + return native_bitwuzla_cxx_mk_term1_indexed1(vm, Long_val(vk), + v1, Long_val(vi)); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term1_indexed2 (intnat k, mlvalue v1, intnat i, intnat j) +native_bitwuzla_cxx_mk_term1_indexed2 +(mlvalue vm, intnat k, mlvalue v1, intnat i, intnat j) { BITWUZLA_TRY_CATCH_BEGIN; const std::vector args{ *Term_val(v1) }; const std::vector indices{ (uint64_t)i, (uint64_t)j }; mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args, indices)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args, indices)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term1_indexed2 (intnat vk, mlvalue v1, mlvalue vi, mlvalue vj) +ocaml_bitwuzla_cxx_mk_term1_indexed2 +(mlvalue vm, intnat vk, mlvalue v1, mlvalue vi, mlvalue vj) { - return native_bitwuzla_cxx_mk_term1_indexed2(Long_val(vk), v1, - Long_val(vi), Long_val(vj)); + return native_bitwuzla_cxx_mk_term1_indexed2(vm, Long_val(vk), v1, + Long_val(vi), Long_val(vj)); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term2_indexed1 (intnat k, mlvalue v1, mlvalue v2, intnat i) +native_bitwuzla_cxx_mk_term2_indexed1 +(mlvalue vm, intnat k, mlvalue v1, mlvalue v2, intnat i) { BITWUZLA_TRY_CATCH_BEGIN; const std::vector args{ *Term_val(v1), *Term_val(v2) }; const std::vector indices{ (uint64_t)i }; mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args, indices)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args, indices)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term2_indexed1 (intnat vk, mlvalue v1, mlvalue v2, mlvalue vi) +ocaml_bitwuzla_cxx_mk_term2_indexed1 +(mlvalue vm, intnat vk, mlvalue v1, mlvalue v2, mlvalue vi) { - return native_bitwuzla_cxx_mk_term2_indexed1(Long_val(vk), v1, v2, Long_val(vi)); + return native_bitwuzla_cxx_mk_term2_indexed1(vm, Long_val(vk), v1, + v2, Long_val(vi)); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term2_indexed2 (intnat k, mlvalue v1, mlvalue v2, - intnat i, intnat j) +native_bitwuzla_cxx_mk_term2_indexed2 +(mlvalue vm, intnat k, mlvalue v1, mlvalue v2, intnat i, intnat j) { BITWUZLA_TRY_CATCH_BEGIN; const std::vector args{ *Term_val(v1), *Term_val(v2) }; const std::vector indices{ (uint64_t)i, (uint64_t)j }; mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args, indices)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args, indices)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term2_indexed2 (intnat vk, mlvalue v1, mlvalue v2, - mlvalue vi, mlvalue vj) +ocaml_bitwuzla_cxx_mk_term2_indexed2 +(mlvalue vm, intnat vk, mlvalue v1, mlvalue v2, mlvalue vi, mlvalue vj) { - return native_bitwuzla_cxx_mk_term2_indexed2(Long_val(vk), v1, v2, - Long_val(vi), Long_val(vj)); + return native_bitwuzla_cxx_mk_term2_indexed2(vm, Long_val(vk), v1, v2, + Long_val(vi), Long_val(vj)); } extern "C" CAMLprim mlvalue -native_bitwuzla_cxx_mk_term (intnat k, mlvalue vargs, mlvalue vindices) +native_bitwuzla_cxx_mk_term +(mlvalue vm, intnat k, mlvalue vargs, mlvalue vindices) { BITWUZLA_TRY_CATCH_BEGIN; std::vector args; @@ -1316,19 +1365,20 @@ native_bitwuzla_cxx_mk_term (intnat k, mlvalue vargs, mlvalue vindices) indices.emplace_back((uint64_t)Long_val(Field(vindices, i))); mlvalue custom; new(&term_operations, &custom) - Term(bitwuzla::mk_term((bitwuzla::Kind)k, args, indices)); + Term(Manager_val(vm)->mk_term((bitwuzla::Kind)k, args, indices)); return custom; BITWUZLA_TRY_CATCH_END; } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_term (intnat vk, mlvalue vargs, mlvalue vindices) +ocaml_bitwuzla_cxx_mk_term +(mlvalue vm, intnat vk, mlvalue vargs, mlvalue vindices) { - return native_bitwuzla_cxx_mk_term(Long_val(vk), vargs, vindices); + return native_bitwuzla_cxx_mk_term(vm, Long_val(vk), vargs, vindices); } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_const (mlvalue vopt, mlvalue vs) +ocaml_bitwuzla_cxx_mk_const (mlvalue vm, mlvalue vopt, mlvalue vs) { CAMLparam2(vopt, vs); mlvalue custom; @@ -1336,12 +1386,12 @@ ocaml_bitwuzla_cxx_mk_const (mlvalue vopt, mlvalue vs) if (Is_some(vopt)) symbol.emplace(std::string(String_val(Field(vopt, 0)))); new(&term_operations, &custom) - Term(bitwuzla::mk_const(*Sort_val(vs), symbol)); + Term(Manager_val(vm)->mk_const(*Sort_val(vs), symbol)); CAMLreturn(custom); } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_mk_var (mlvalue vopt, mlvalue vs) +ocaml_bitwuzla_cxx_mk_var (mlvalue vm, mlvalue vopt, mlvalue vs) { CAMLparam2(vopt, vs); mlvalue custom; @@ -1349,12 +1399,12 @@ ocaml_bitwuzla_cxx_mk_var (mlvalue vopt, mlvalue vs) if (Is_some(vopt)) symbol.emplace(std::string(String_val(Field(vopt, 0)))); new(&term_operations, &custom) - Term(bitwuzla::mk_var(*Sort_val(vs), symbol)); + Term(Manager_val(vm)->mk_var(*Sort_val(vs), symbol)); CAMLreturn(custom); } extern "C" CAMLprim mlvalue -ocaml_bitwuzla_cxx_substitute_term (mlvalue vt, mlvalue vmap) +ocaml_bitwuzla_cxx_substitute_term (mlvalue vm, mlvalue vt, mlvalue vmap) { CAMLparam1(vt); mlvalue custom; @@ -1366,12 +1416,12 @@ ocaml_bitwuzla_cxx_substitute_term (mlvalue vt, mlvalue vmap) *Term_val(Field(Field(vmap, i), 1)))); } new(&term_operations, &custom) - Term(bitwuzla::substitute_term(*Term_val(vt), map)); + Term(Manager_val(vm)->substitute_term(*Term_val(vt), map)); CAMLreturn(custom); } extern "C" CAMLprim void -ocaml_bitwuzla_cxx_substitute_terms (mlvalue va, mlvalue vmap) +ocaml_bitwuzla_cxx_substitute_terms (mlvalue vm, mlvalue va, mlvalue vmap) { CAMLparam1(va); std::unordered_map map; @@ -1387,7 +1437,7 @@ ocaml_bitwuzla_cxx_substitute_terms (mlvalue va, mlvalue vmap) for (size_t i = 0; i < n; i += 1) { terms.emplace_back(*Term_val(Field(va, i))); } - bitwuzla::substitute_terms(terms, map); + Manager_val(vm)->substitute_terms(terms, map); for (size_t i = 0; i < n; i += 1) { mlvalue custom; new(&term_operations, &custom) Term(terms[i]); @@ -1451,9 +1501,10 @@ static struct custom_operations bitwuzla_operations = }; extern "C" CAMLprim value -ocaml_bitwuzla_cxx_new (mlvalue voptions) +ocaml_bitwuzla_cxx_new (mlvalue vm, mlvalue voptions) { - bitwuzla::Bitwuzla *t = new bitwuzla::Bitwuzla(*Options_val(voptions)); + bitwuzla::Bitwuzla *t = + new bitwuzla::Bitwuzla(*Manager_val(vm), *Options_val(voptions)); Terminator *terminator = new Terminator(); t->configure_terminator(terminator); value vt = caml_alloc_custom(&bitwuzla_operations, sizeof(struct t), 0, 1); diff --git a/dune b/dune index 7fd1002..c14f445 100644 --- a/dune +++ b/dune @@ -1,7 +1,16 @@ (library (public_name bitwuzla-cxx) (name bitwuzla_cxx) - (modules options sort roundingMode kind term result solver bitwuzla_cxx) + (modules + manager + options + sort + roundingMode + kind + term + result + solver + bitwuzla_cxx) (libraries zarith) (foreign_stubs (language cxx) diff --git a/dune-project b/dune-project index 44b4629..be759b5 100644 --- a/dune-project +++ b/dune-project @@ -19,7 +19,7 @@ OCaml binding for the SMT solver Bitwuzla C++ API. Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”.") (documentation "https://bitwuzla.github.io/docs/ocaml/") (depends - (ocaml (and (>= 4.12) (< 5))) + (ocaml (>= 4.12)) (conf-git :build) (conf-gcc :build) (conf-g++ :build) diff --git a/manager.ml b/manager.ml new file mode 100644 index 0000000..9058e91 --- /dev/null +++ b/manager.ml @@ -0,0 +1,3 @@ +type t + +external create : unit -> t = "ocaml_bitwuzla_cxx_manager_new" diff --git a/solver.ml b/solver.ml index 10a5470..87a4725 100644 --- a/solver.ml +++ b/solver.ml @@ -11,7 +11,7 @@ type t -external create : Options.t -> t = "ocaml_bitwuzla_cxx_new" +external create : Manager.t -> Options.t -> t = "ocaml_bitwuzla_cxx_new" external unsafe_delete : t -> unit = "ocaml_bitwuzla_cxx_delete" diff --git a/vendor/bitwuzla b/vendor/bitwuzla index f148a8c..3aa7bee 160000 --- a/vendor/bitwuzla +++ b/vendor/bitwuzla @@ -1 +1 @@ -Subproject commit f148a8c4d97f214d717940bd0a678a083cfe0aca +Subproject commit 3aa7bee27bbecb026b19ade44b967e0d445feff9 diff --git a/vendor/dune b/vendor/dune index 833a88f..dca0d69 100644 --- a/vendor/dune +++ b/vendor/dune @@ -138,6 +138,7 @@ floating_point fp_solver rounding_mode + symfpu_nm symfpu_wrapper word_blaster fun_solver @@ -151,16 +152,12 @@ type type_data type_manager + hash_pair logger + resources statistics) (include_dirs include src src/lib ../symfpu ../cadical) - (flags - :standard - -std=c++17 - -Isrc/lib/ - -I../cadical/src - -I.. - -DNDEBUG) + (flags :standard -std=c++17 -Isrc/lib/ -I../cadical/src -I.. -DNDEBUG) (extra_deps ../.bitwuzla_tree))) (subdir @@ -178,11 +175,7 @@ (deps (source_tree bitwuzla) (:p0001 - (file patch/0001-api-Add-hook-for-ocaml-z-value.patch)) - (:p0002 - (file patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch)) - (:p0003 - (file patch/0003-Fix-compilation-with-older-GCC-version.patch))) + (file patch/0001-api-Add-hook-for-ocaml-z-value.patch))) (target .bitwuzla_tree) (action (no-infer @@ -190,10 +183,4 @@ (with-stdin-from %{p0001} (run patch -p1 --directory bitwuzla)) - (with-stdin-from - %{p0002} - (run patch -p1 --directory bitwuzla)) - (with-stdin-from - %{p0003} - (run patch -p1 --directory bitwuzla)) (write-file %{target} ""))))) diff --git a/vendor/patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch b/vendor/patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch deleted file mode 100644 index 2235cce..0000000 --- a/vendor/patch/0002-ocaml-make-NodeManager-global-from-thread-local.patch +++ /dev/null @@ -1,25 +0,0 @@ -From 6552cf5d2f3281f408b7e3d540ab4c0b69368387 Mon Sep 17 00:00:00 2001 -From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Recoules?= -Date: Mon, 31 Jul 2023 11:03:14 +0200 -Subject: [PATCH 2/2] ocaml: make NodeManager global (from thread local) - ---- - src/node/node_manager.cpp | 2 +- - 1 file changed, 1 insertion(+), 1 deletion(-) - -diff --git a/src/node/node_manager.cpp b/src/node/node_manager.cpp -index e9f64060..14449729 100644 ---- a/src/node/node_manager.cpp -+++ b/src/node/node_manager.cpp -@@ -26,7 +26,7 @@ using namespace node; - NodeManager& - NodeManager::get() - { -- thread_local static NodeManager mgr; -+ /* thread_local */ static NodeManager mgr; - return mgr; - } - --- -2.34.1 - diff --git a/vendor/patch/0003-Fix-compilation-with-older-GCC-version.patch b/vendor/patch/0003-Fix-compilation-with-older-GCC-version.patch deleted file mode 100644 index 0039568..0000000 --- a/vendor/patch/0003-Fix-compilation-with-older-GCC-version.patch +++ /dev/null @@ -1,27 +0,0 @@ -From 4ee5c40699d5a60e5adc9e54523f82da3f1ac7ad Mon Sep 17 00:00:00 2001 -From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Recoules?= -Date: Fri, 1 Sep 2023 11:09:32 +0200 -Subject: [PATCH] Fix compilation with older GCC version - ---- - src/solver/bv/bv_prop_solver.cpp | 4 +++- - 1 file changed, 3 insertions(+), 1 deletion(-) - -diff --git a/src/solver/bv/bv_prop_solver.cpp b/src/solver/bv/bv_prop_solver.cpp -index 64d189d3..b56cee00 100644 ---- a/src/solver/bv/bv_prop_solver.cpp -+++ b/src/solver/bv/bv_prop_solver.cpp -@@ -275,7 +275,9 @@ BvPropSolver::mk_node(const Node& node) - } - - std::string symbol = -- node.symbol() ? *node.symbol() : "@t" + std::to_string(node.id()); -+ node.symbol() -+ ? (std::string) *node.symbol() -+ : "@t" + std::to_string(node.id()); - - switch (node.kind()) - { --- -2.34.1 -