feat(BV, Opt): Support bit-vector optimization

Since we track intervals for bit-vector variables, adding support for
optimization in the bit-vector theory is fairly inconsequential.

Fixes OCamlPro#884

src/lib/reasoners/bitv_rel.ml

@@ -78,6 +78,9 @@ let is_bv_r r = is_bv_ty @@ X.type_info r
 let bitwidth r =
   match X.type_info r with Tbitv n -> n | _ -> assert false
 
+let const sz n =
+  Shostak.Bitv.is_mine [ { bv = Cte (Z.extract n 0 sz); sz } ]
+
 module Interval_domain = struct
   type t = Intervals.Int.t
 
@@ -638,9 +641,6 @@ end = struct
   let propagate_interval ~ex c dom =
     propagate_interval_repr ~ex dom c.repr
 
-  let const sz n =
-    Shostak.Bitv.is_mine [ { bv = Cte (Z.extract n 0 sz); sz } ]
-
   let cast ty n =
     match ty with
     | Ty.Tbitv sz -> const sz n
@@ -1425,7 +1425,41 @@ let add env uf r t =
   in
   { env with delayed }, Uf.domains uf, eqs
 
-let optimizing_objective _env _uf _o = None
+let optimizing_objective _env uf Objective.Function.{ e; is_max; _ } =
+  let ty = E.type_info e in
+  if not (is_bv_ty ty) then None
+  else
+    let r = Uf.make uf e in
+    let rr, _ = Uf.find_r uf r in
+    match Shostak.Bitv.embed rr with
+    | [ { bv = Cte n ; sz }] ->
+      if Options.get_debug_optimize () then
+        Printer.print_dbg "%a has the value %a@."
+          E.print e
+          Z.pp_print n;
+
+      let value = Objective.Value.Value (E.BV.of_Z ~size:sz n) in
+      let case_split =
+        Uf.LX.mkv_eq r rr, true, Th_util.CS (Th_util.Th_bitv, Q.one)
+      in
+      Some Th_util.{ value ; case_split }
+    | _ ->
+      let ds = Uf.domains uf in
+      let int_domains = Uf.GlobalDomains.find (module Interval_domains) ds in
+      let int = Interval_domains.get rr int_domains in
+      let sz = bitwidth rr in
+      let value_z =
+        if is_max then
+          finite_upper_bound ~size:sz @@
+          fst (Intervals.Int.upper_bound int)
+        else
+          finite_lower_bound @@
+          fst (Intervals.Int.lower_bound int)
+      in
+      let value = Objective.Value.Value (E.BV.of_Z ~size:sz value_z) in
+      let lit = Uf.LX.mkv_eq r (const sz value_z) in
+      let case_split = lit, true, Th_util.CS (Th_util.Th_bitv, Q.one) in
+      Some { value ; case_split }
 
 let new_terms _ = Expr.Set.empty
 

src/lib/reasoners/intervalCalculus.ml

@@ -1990,11 +1990,10 @@ let middle_value env ~is_max ty p bound =
   let q = I.pick ~is_max interval in
   alien_of (P.create [] q ty)
 
-let optimizing_objective env uf Objective.Function.{ e; is_max; _ } =
+let optimizing_objective_for_ty ~is_max ty env uf e =
   (* soundness: if there are expressions to optmize, this should be
      done without waiting for ~for_model flag to be true *)
   let repr, _ = Uf.find uf e in
-  let ty = E.type_info e in
   let r1 = Uf.make uf e in (* instead of repr, which may be a constant *)
   let p = poly_of repr in
   match P.is_const p with
@@ -2011,7 +2010,7 @@ let optimizing_objective env uf Objective.Function.{ e; is_max; _ } =
     let case_split =
       LR.mkv_eq r1 r2, true, Th_util.CS (Th_util.Th_arith, Q.one)
     in
-    Some Th_util.{ value; case_split }
+    Th_util.{ value; case_split }
 
   | None ->
     begin
@@ -2054,7 +2053,7 @@ let optimizing_objective env uf Objective.Function.{ e; is_max; _ } =
           true,
           Th_util.CS (Th_util.Th_arith, Q.one)
         in
-        Some Th_util.{ value; case_split }
+        Th_util.{ value; case_split }
 
       | Sim.Core.Max (lazy Sim.Core.{ max_v; is_le }, _sol) ->
         let max_p = Q.add max_v.bvalue.v c in
@@ -2099,9 +2098,15 @@ let optimizing_objective env uf Objective.Function.{ e; is_max; _ } =
         let case_split =
           LR.mkv_eq r1 r2, true, Th_util.CS (Th_util.Th_arith, Q.one)
         in
-        Some { value; case_split }
+        { value; case_split }
     end
 
+let optimizing_objective env uf Objective.Function.{ e; is_max; _ } =
+  match E.type_info e with
+  | Tint | Treal as ty ->
+    Some (optimizing_objective_for_ty ~is_max ty env uf e)
+  | _ -> None
+
 (*** part dedicated to FPA reasoning ************************************)
 
 let best_interval_of optimized env p =

src/lib/reasoners/intervals.ml

@@ -771,7 +771,7 @@ module Legacy = struct
       of_real @@ Real.of_interval ~ex @@ Real.Interval.singleton v
     | Tint when Z.equal (Q.den v) Z.one ->
       of_int @@ Int.of_interval ~ex @@ Int.Interval.singleton @@ Q.num v
-    | _ -> Fmt.invalid_arg "point: %a" Q.pp_print v
+    | _ -> Fmt.invalid_arg "point: %a (as %a)" Q.pp_print v Ty.print ty
 
   let doesnt_contain_0 u =
     Option.map (fun ex -> (ex, [])) @@

src/lib/reasoners/satml_frontend.ml

@@ -1060,14 +1060,39 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
      If this run produces the answer [unsat], we know that [2] was the best
      model value for [x]. Otherwise, we got a better value for [x]. *)
 
-  let op is_max is_le =
+  type ty_op =
+    { lt : E.t -> E.t -> E.t
+    ; le : E.t -> E.t -> E.t }
+
+  let real_op = { lt = Expr.Reals.(<) ; le = Expr.Reals.(<=) }
+
+  let int_op = { lt = Expr.Ints.(<) ; le = Expr.Reals.(<=) }
+
+  let bitv_unsigned_op = { lt = Expr.BV.bvult ; le = Expr.BV.bvule }
+
+  let mk_le { le ; _ } = le
+
+  let mk_lt { lt ; _ } = lt
+
+  let mk_ge { le ; _ } x y = le y x
+
+  let mk_gt { lt ; _ } x y = lt y x
+
+  let op ty is_max is_le =
+    let ty_op =
+      match ty with
+      | Ty.Treal -> real_op
+      | Tint -> int_op
+      | Tbitv _ -> bitv_unsigned_op
+      | _ -> Fmt.invalid_arg "cannot optimize for type: %a" Ty.print ty
+    in
     if is_max then begin
-      if is_le then Expr.Reals.(<=)
-      else Expr.Reals.(<)
+      if is_le then mk_le ty_op
+      else mk_lt ty_op
     end
     else begin
-      if is_le then Expr.Reals.(>=)
-      else Expr.Reals.(>)
+      if is_le then mk_ge ty_op
+      else mk_gt ty_op
     end
 
   (* This function is called after receiving an `I_dont_know` exception from
@@ -1105,8 +1130,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
             (fun acc (e, tv, is_max, is_le) ->
                let eq = E.mk_eq e tv ~iff: false in
                let acc = E.Core.and_ acc eq in
-               E.Core.(or_ acc (not ((op is_max is_le) e tv)))
-            ) (E.Core.not ((op is_max is_le) e tv)) l
+               E.Core.(or_ acc (not ((op (E.type_info e) is_max is_le) e tv)))
+            ) (E.Core.not ((op (E.type_info e) is_max is_le) e tv)) l
         in
         if Options.get_debug_optimize () then
           Printer.print_dbg

src/lib/structures/expr.ml

@@ -3059,18 +3059,18 @@ end
 module BV = struct
   open Core
 
-  let of_bigint sz n =
+  let of_Z ~size:sz n =
     assert (sz > 0);
     mk_term (Sy.Bitv (sz, Z.extract n 0 sz)) [] (Tbitv sz)
 
   let of_bigint_like s n =
     match type_info s with
-    | Tbitv sz -> of_bigint sz n
+    | Tbitv sz -> of_Z ~size:sz n
     | _ -> invalid_arg "of_bigint_like"
 
   (* Constant symbols for all zeros and all ones *)
-  let bvzero m = of_bigint m Z.zero
-  let bvones m = of_bigint m Z.minus_one
+  let bvzero m = of_Z ~size:m Z.zero
+  let bvones m = of_Z ~size:m Z.minus_one
 
   (* Helpers *)
   let b = function

src/lib/structures/expr.mli

@@ -522,6 +522,8 @@ end
     https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml
     https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV *)
 module BV : sig
+  val of_Z : size:int -> Z.t -> t
+
   (* Conversion from and to integers *)
   val int2bv : int -> t -> t
   val bv2nat : t -> t

tests/models/bitv/optim-1.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 32) #xffffffff)
+)
+(objectives 
+  (x #xffffffff)
+)

tests/models/bitv/optim-1.models.smt2

@@ -0,0 +1,8 @@
+; Test basic functionality
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x (_ BitVec 32))
+(maximize x)
+(check-sat)
+(get-model)
+(get-objectives)

tests/models/bitv/optim-2.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 32) #xffffffff)
+)
+(objectives 
+  ((bvnot x) #x00000000)
+)

tests/models/bitv/optim-2.models.smt2

@@ -0,0 +1,8 @@
+; Test primitive optimization
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x (_ BitVec 32))
+(minimize (bvnot x))
+(check-sat)
+(get-model)
+(get-objectives)

tests/models/bitv/optim-3.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 32) #xfffffffe)
+)
+(objectives 
+  (x #xfffffffe)
+)

tests/models/bitv/optim-3.models.smt2

@@ -0,0 +1,9 @@
+; Test constrained optimization
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x (_ BitVec 32))
+(maximize x)
+(assert (bvslt x ((_ int2bv 32) (- 1))))
+(check-sat)
+(get-model)
+(get-objectives)

tests/models/bitv/optim-4.models.expected

@@ -0,0 +1,9 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 32) #xffffffff)
+  (define-fun P ((_arg_0 (_ BitVec 33))) Bool true)
+)
+(objectives 
+  ((bvabs32 x) #b011111111111111111111111111111111)
+)