Fixes batch solver

lib/solver.ml

@@ -42,10 +42,13 @@ module Batch (Mappings : Mappings_intf.S) = struct
   let clone ({ solver; top; stack } : t) : t =
     { solver; top; stack = Stack.copy stack }
 
-  let push ({ top; stack; _ } : t) : unit = Stack.push top stack
+  let push ({ top; stack; solver } : t) : unit =
+    Mappings.push solver;
+    Stack.push top stack
 
   let pop (s : t) (lvl : int) : unit =
     assert (lvl <= Stack.length s.stack);
+    Mappings.pop s.solver lvl;
     for _ = 1 to lvl do
       s.top <- Stack.pop s.stack
     done
@@ -59,9 +62,10 @@ module Batch (Mappings : Mappings_intf.S) = struct
   let get_assertions (s : t) : Expr.t list = s.top [@@inline]
 
   let check (s : t) (es : Expr.t list) : bool =
-    let es' = es @ s.top in
+    Mappings.add_solver s.solver s.top;
+    s.top <- [];
     solver_count := !solver_count + 1;
-    let sat = time_call (fun () -> Mappings.check s.solver es') solver_time in
+    let sat = time_call (fun () -> Mappings.check s.solver es) solver_time in
     match Mappings.satisfiability sat with
     | Mappings_intf.Satisfiable -> true
     | Mappings_intf.Unsatisfiable -> false

test/test_batch.ml

@@ -3,40 +3,49 @@ open Ty
 open Expr
 module Batch = Solver.Batch (Z3_mappings)
 
-let solver = Batch.create ()
 let symb_x = Symbol.("x" @: Ty_int)
 let symb_y = Symbol.("y" @: Ty_bool)
 let x = Expr.mk_symbol symb_x
 let y = Expr.mk_symbol symb_y
-let%test "check []" = Batch.check solver []
+
+let%test "check []" =
+  let solver = Batch.create ~logic:QF_LIA () in
+  Batch.check solver []
 
 let%test "check [ x > 0 ]" =
+  let solver = Batch.create ~logic:QF_LIA () in
   Batch.check solver [ Relop (Gt, x, Val (Int 0) @: Ty_int) @: Ty_int ]
 
 let%test "get_value x" =
-  let pc = [ Relop (Eq, x, Val (Int 0) @: Ty_int) @: Ty_int ] in
-  assert (Batch.check solver pc);
+  let solver = Batch.create ~logic:QF_LIA () in
+  Batch.add solver [ Relop (Eq, x, Val (Int 0) @: Ty_int) @: Ty_int ];
+  assert (Batch.check solver []);
   let v = Batch.get_value solver x in
   Val (Int 0) = v.e
 
 let%test "get_value (x * x)" =
-  let pc = [ Relop (Eq, x, Val (Int 3) @: Ty_int) @: Ty_int ] in
-  assert (Batch.check solver pc);
+  let solver = Batch.create ~logic:QF_LIA () in
+  Batch.add solver [ Relop (Eq, x, Val (Int 3) @: Ty_int) @: Ty_int ];
+  assert (Batch.check solver []);
   let v = Batch.get_value solver (Binop (Mul, x, x) @: Ty_int) in
   Val (Int 9) = v.e
 
 let%test "eval []" =
+  let solver = Batch.create ~logic:QF_LIA () in
   assert (Batch.check solver []);
   let m = Batch.model ~symbols:[ symb_x ] solver |> Option.get in
   Option.is_some @@ Model.evaluate m symb_x
 
 let%test "eval [ x = 5 ]" =
-  assert (Batch.check solver [ Relop (Eq, x, Val (Int 5) @: Ty_int) @: Ty_int ]);
+  let solver = Batch.create ~logic:QF_LIA () in
+  Batch.add solver [ Relop (Eq, x, Val (Int 5) @: Ty_int) @: Ty_int ];
+  assert (Batch.check solver []);
   let m = Batch.model ~symbols:[ symb_x ] solver in
   Some (Value.Int 5) = Model.evaluate (Option.get m) symb_x
 
 let%test "eval [ y = false ]" =
-  let pc = [ Relop (Eq, y, Val False @: Ty_bool) @: Ty_bool ] in
-  assert (Batch.check solver pc);
+  let solver = Batch.create ~logic:QF_LIA () in
+  Batch.add solver [ Relop (Eq, y, Val False @: Ty_bool) @: Ty_bool ];
+  assert (Batch.check solver []);
   let model = Option.get (Batch.model solver) in
   Some Value.False = Model.evaluate model symb_y

test/test_regression.ml

@@ -3,20 +3,20 @@ open Ty
 open Expr
 module Batch = Solver.Batch (Z3_mappings)
 
-let solver = Batch.create ()
-
 let%test _ =
+  let solver = Batch.create () in
   let x = mk_symbol Symbol.("x" @: Ty_fp S32) in
   let const = Val (Num (F32 (Int32.bits_of_float 50.0))) @: Ty_fp S32 in
-  let es = [ Relop (Eq, x, const) @: Ty_fp S32 ] in
-  assert (Batch.check solver es);
+  Batch.add solver [ Relop (Eq, x, const) @: Ty_fp S32 ];
+  assert (Batch.check solver []);
   Batch.get_value solver x = const
 
 let%test _ =
+  let solver = Batch.create () in
   let x = mk_symbol Symbol.("x" @: Ty_fp S64) in
   let const = Val (Num (F64 (Int64.bits_of_float 50.0))) @: Ty_fp S64 in
-  let es = [ Relop (Eq, x, const) @: Ty_fp S64 ] in
-  assert (Batch.check solver es);
+  Batch.add solver [ Relop (Eq, x, const) @: Ty_fp S64 ];
+  assert (Batch.check solver []);
   Batch.get_value solver x = const
 
 let cvtop = Eval_numeric.eval_cvtop