Add missing operators (#417)

src/smtml/bitwuzla_mappings.default.ml

@@ -128,6 +128,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
     let to_real _ =
       Fmt.failwith "Bitwuzla_mappings: Int.to_real not implemented"
 
+    let to_bv _ = Fmt.failwith "Bitwuzla_mappings: Int.to_bv not implemented"
+
     let add _ = Fmt.failwith "Bitwuzla_mappings: Int.add not implemented"
 
     let sub _ = Fmt.failwith "Bitwuzla_mappings: Int.sub not implemented"
@@ -138,6 +140,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let rem _ = Fmt.failwith "Bitwuzla_mappings: Int.rem not implemented"
 
+    let mod_ _ = Fmt.failwith "Bitwuzla_mappings: Int.mod_ not implemented"
+
     let pow _ = Fmt.failwith "Bitwuzla_mappings: Int.pow not implemented"
 
     let lt _ = Fmt.failwith "Bitwuzla_mappings: Int.lt not implemented"
@@ -267,6 +271,9 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let lognot t = mk_term1 Kind.Bv_not t
 
+    let to_int ~signed:_ _t =
+      Fmt.failwith "Bitwuzla_mappings: Bitv.to_int not implemented"
+
     let add t1 t2 = mk_term2 Kind.Bv_add t1 t2
 
     let sub t1 t2 = mk_term2 Kind.Bv_sub t1 t2
@@ -289,6 +296,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let lshr t1 t2 = mk_term2 Kind.Bv_shr t1 t2
 
+    let smod t1 t2 = mk_term2 Kind.Bv_smod t1 t2
+
     let rem t1 t2 = mk_term2 Kind.Bv_srem t1 t2
 
     let rem_u t1 t2 = mk_term2 Kind.Bv_urem t1 t2
@@ -297,6 +306,19 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let rotate_right t1 t2 = mk_term2 Kind.Bv_ror t1 t2
 
+    let nego t = mk_term1 Kind.Bv_nego t
+
+    let addo ~signed t1 t2 =
+      mk_term2 (if signed then Kind.Bv_saddo else Kind.Bv_uaddo) t1 t2
+
+    let subo ~signed t1 t2 =
+      mk_term2 (if signed then Kind.Bv_ssubo else Kind.Bv_usubo) t1 t2
+
+    let mulo ~signed t1 t2 =
+      mk_term2 (if signed then Kind.Bv_smulo else Kind.Bv_umulo) t1 t2
+
+    let divo t1 t2 = mk_term2 Kind.Bv_sdivo t1 t2
+
     let lt t1 t2 = mk_term2 Kind.Bv_slt t1 t2
 
     let lt_u t1 t2 = mk_term2 Kind.Bv_ult t1 t2

src/smtml/cvc5_mappings.default.ml

@@ -116,6 +116,8 @@ module Fresh_cvc5 () = struct
 
     let to_real t = Term.mk_term tm Kind.To_real [| t |]
 
+    let to_bv _m _t = Fmt.failwith "Cvc5_mappings: Int.to_bv not implemented"
+
     let add t1 t2 = Term.mk_term tm Kind.Add [| t1; t2 |]
 
     let sub t1 t2 = Term.mk_term tm Kind.Sub [| t1; t2 |]
@@ -126,6 +128,8 @@ module Fresh_cvc5 () = struct
 
     let rem t1 t2 = Term.mk_term tm Kind.Ints_modulus [| t1; t2 |]
 
+    let mod_ t1 t2 = Term.mk_term tm Kind.Ints_modulus [| t1; t2 |]
+
     let pow t1 t2 = Term.mk_term tm Kind.Pow [| t1; t2 |]
 
     let lt t1 t2 = Term.mk_term tm Kind.Lt [| t1; t2 |]
@@ -251,6 +255,9 @@ module Fresh_cvc5 () = struct
 
     let lognot t = Term.mk_term tm Kind.Bitvector_not [| t |]
 
+    let to_int ~signed:_ _t =
+      Fmt.failwith "Cvc5_mappings: Int.to_int not implemented"
+
     let add t1 t2 = Term.mk_term tm Kind.Bitvector_add [| t1; t2 |]
 
     let sub t1 t2 = Term.mk_term tm Kind.Bitvector_sub [| t1; t2 |]
@@ -273,6 +280,8 @@ module Fresh_cvc5 () = struct
 
     let lshr t1 t2 = Term.mk_term tm Kind.Bitvector_lshr [| t1; t2 |]
 
+    let smod _ = Fmt.failwith "Cvc5_mappings: smod not implemented"
+
     let rem t1 t2 = Term.mk_term tm Kind.Bitvector_srem [| t1; t2 |]
 
     let rem_u t1 t2 = Term.mk_term tm Kind.Bitvector_urem [| t1; t2 |]
@@ -283,6 +292,16 @@ module Fresh_cvc5 () = struct
     let rotate_right t1 t2 =
       Term.mk_term tm Kind.Bitvector_rotate_right [| t1; t2 |]
 
+    let nego _ = Fmt.failwith "Cvc5_mappings: nego not implemented"
+
+    let addo ~signed:_ = Fmt.failwith "Cvc5_mappings: addo not implemented"
+
+    let subo ~signed:_ = Fmt.failwith "Cvc5_mappings: subo not implemented"
+
+    let mulo ~signed:_ = Fmt.failwith "Cvc5_mappings: mulo not implemented"
+
+    let divo _ = Fmt.failwith "Cvc5_mappings: divo not support not implemented"
+
     let lt t1 t2 = Term.mk_term tm Kind.Bitvector_slt [| t1; t2 |]
 
     let lt_u t1 t2 = Term.mk_term tm Kind.Bitvector_ult [| t1; t2 |]

src/smtml/dolmenexpr_to_expr.ml

@@ -216,6 +216,10 @@ module DolmenIntf = struct
     include DTerm.Int
 
     let neg = DTerm.Int.minus
+
+    let to_bv = DTerm.Bitv.of_int
+
+    let mod_ = DTerm.Int.rem_f
   end
 
   module Real = struct
@@ -305,6 +309,8 @@ module DolmenIntf = struct
 
     let lognot = DTerm.Bitv.not
 
+    let to_int ~signed:_ = DTerm.Bitv.to_nat
+
     let div = DTerm.Bitv.sdiv
 
     let div_u = DTerm.Bitv.udiv
@@ -329,17 +335,27 @@ module DolmenIntf = struct
 
     let rotate_right t1 t2 = DTerm.Bitv.rotate_right (int_of_term t2) t1
 
-    let lt t1 t2 = DTerm.Bitv.slt t1 t2
+    let nego _ = Fmt.failwith "Dolmenexpr: nego not implemented"
+
+    let addo ~signed:_ = Fmt.failwith "Dolmenexpr: addo not implemented"
+
+    let subo ~signed:_ = Fmt.failwith "Dolmenexpr: subo not implemented"
+
+    let mulo ~signed:_ = Fmt.failwith "Dolmenexpr: mulo not implemented"
+
+    let divo _ = Fmt.failwith "Dolmenexpr: divo not implemented"
+
+    let lt = DTerm.Bitv.slt
 
-    let lt_u t1 t2 = DTerm.Bitv.ult t1 t2
+    let lt_u = DTerm.Bitv.ult
 
     let le = DTerm.Bitv.sle
 
     let le_u = DTerm.Bitv.ule
 
-    let gt t1 t2 = DTerm.Bitv.sgt t1 t2
+    let gt = DTerm.Bitv.sgt
 
-    let gt_u t1 t2 = DTerm.Bitv.ugt t1 t2
+    let gt_u = DTerm.Bitv.ugt
 
     let ge = DTerm.Bitv.sge
 

src/smtml/dolmenexpr_to_expr.mli

@@ -125,6 +125,8 @@ module DolmenIntf : sig
 
     val to_real : term -> term
 
+    val to_bv : int -> term -> term
+
     val add : term -> term -> term
 
     val sub : term -> term -> term
@@ -135,6 +137,8 @@ module DolmenIntf : sig
 
     val rem : term -> term -> term
 
+    val mod_ : term -> term -> term
+
     val pow : term -> term -> term
 
     val lt : term -> term -> term
@@ -249,6 +253,8 @@ module DolmenIntf : sig
 
     val lognot : term -> term
 
+    val to_int : signed:bool -> term -> term
+
     val add : term -> term -> term
 
     val sub : term -> term -> term
@@ -271,6 +277,8 @@ module DolmenIntf : sig
 
     val lshr : term -> term -> term
 
+    val smod : term -> term -> term
+
     val rem : term -> term -> term
 
     val rem_u : term -> term -> term
@@ -279,6 +287,16 @@ module DolmenIntf : sig
 
     val rotate_right : term -> term -> term
 
+    val nego : term -> term
+
+    val addo : signed:bool -> term -> term -> term
+
+    val subo : signed:bool -> term -> term -> term
+
+    val mulo : signed:bool -> term -> term -> term
+
+    val divo : term -> term -> term
+
     val lt : term -> term -> term
 
     val lt_u : term -> term -> term

src/smtml/mappings.nop.ml

@@ -101,6 +101,8 @@ module Nop = struct
 
       let to_real _ = assert false
 
+      let to_bv _ = assert false
+
       let add _ = assert false
 
       let sub _ = assert false
@@ -111,6 +113,8 @@ module Nop = struct
 
       let rem _ = assert false
 
+      let mod_ _ = assert false
+
       let pow _ = assert false
 
       let lt _ = assert false
@@ -225,6 +229,8 @@ module Nop = struct
 
       let lognot _ = assert false
 
+      let to_int ~signed:_ = assert false
+
       let add _ = assert false
 
       let sub _ = assert false
@@ -247,6 +253,8 @@ module Nop = struct
 
       let lshr _ = assert false
 
+      let smod _ = assert false
+
       let rem _ = assert false
 
       let rem_u _ = assert false
@@ -255,6 +263,16 @@ module Nop = struct
 
       let rotate_right _ = assert false
 
+      let nego _ = assert false
+
+      let addo ~signed:_ = assert false
+
+      let subo ~signed:_ = assert false
+
+      let mulo ~signed:_ = assert false
+
+      let divo _ = assert false
+
       let lt _ = assert false
 
       let lt_u _ = assert false

src/smtml/mappings_intf.ml

@@ -165,6 +165,9 @@ module type M = sig
     (** [to_real t] converts the integer term [t] to a real number term. *)
     val to_real : term -> term
 
+    (** [to_bv m t] convertes integer [t] term into a bitvector of size [m]. *)
+    val to_bv : int -> term -> term
+
     (** [add t1 t2] constructs the sum of the integer terms [t1] and [t2]. *)
     val add : term -> term -> term
 
@@ -184,6 +187,9 @@ module type M = sig
     *)
     val rem : term -> term -> term
 
+    (** [mod t1 t2] constructs the modules operator *)
+    val mod_ : term -> term -> term
+
     (** [pow t1 t2] constructs the power of the integer terms [t1] and [t2]. *)
     val pow : term -> term -> term
 
@@ -397,6 +403,9 @@ module type M = sig
     (** [lognot t] constructs the bitwise NOT of the bitvector term [t]. *)
     val lognot : term -> term
 
+    (** [to_int ~signed t] convertes the bitvector term [t] into an integer. *)
+    val to_int : signed:bool -> term -> term
+
     (** [add t1 t2] constructs the sum of the bitvector terms [t1] and [t2]. *)
     val add : term -> term -> term
 
@@ -437,6 +446,10 @@ module type M = sig
     (** [lshr t1 t2] constructs the logical right shift of [t1] by [t2]. *)
     val lshr : term -> term -> term
 
+    (** [smod t1 t2] two's complement signed remainder (sign follows divisor).
+    *)
+    val smod : term -> term -> term
+
     (** [rem t1 t2] constructs the remainder of the bitvector terms [t1] and
         [t2]. *)
     val rem : term -> term -> term
@@ -451,6 +464,38 @@ module type M = sig
     (** [rotate_right t1 t2] constructs the right rotation of [t1] by [t2]. *)
     val rotate_right : term -> term -> term
 
+    (** [nego t] constructs a predicate that checks that whether the bit-wise
+        negation of [t] does not overflow. *)
+    val nego : term -> term
+
+    (** [addo ~signed t1 t2] constructs a predicate that checks whether the
+        bitwise addition of [t1] and [t2] does not overflow.
+
+        The [signed] argument is a boolean:
+        - [true] -> for signed addition
+        - [false] -> for unsigned addition *)
+    val addo : signed:bool -> term -> term -> term
+
+    (** [subo ~signed t1 t2] constructs a predicate that checks whether the
+        bitwise subtraction of [t1] and [t2] does not overflow.
+
+        The [signed] argument is a boolean:
+        - [true] -> for signed subtraction
+        - [false] -> for unsigned subtraction *)
+    val subo : signed:bool -> term -> term -> term
+
+    (** [mulo ~signed t1 t2] constructs a predicate that checks whether the
+        bitwise multiplication of [t1] and [t2] does not overflow.
+
+        The [signed] argument is a boolean:
+        - [true] -> for signed multiplication
+        - [false] -> for unsigned multiplication *)
+    val mulo : signed:bool -> term -> term -> term
+
+    (** [divo t1 t2] constructs a predicate that checks whether the bitwise
+        division of [t1] and [t2] does not overflow. *)
+    val divo : term -> term -> term
+
     (** [lt t1 t2] constructs the less-than relation between bitvector terms
         [t1] and [t2]. *)
     val lt : term -> term -> term