Improve coverate of lia and interpreter

lib/interpret.ml

@@ -31,7 +31,7 @@ module Make (Solver : Solver_intf.S) = struct
     | GetModel ->
       assert (Solver.check solver []);
       let model = Solver.model solver in
-      Format.printf "%a" Model.pp (Option.get model);
+      Option.iter (Model.pp Format.std_formatter) model;
       st pc
 
   let rec loop (state : exec_state) : exec_state =

test/test_lia.expected

@@ -0,0 +1,2 @@
+(model
+  (x int 4))

test/test_lia.ml

@@ -4,24 +4,39 @@ open Expr
 module Solver = Solver.Z3_batch
 module Optimizer = Optimizer.Z3
 
-let symbol_x = Symbol.("x" @: Ty_int)
-let x = mk_symbol symbol_x
 let v i = Val (Int i) @: Ty_int
-let eq i1 i2 = Relop (Eq, i1, i2) @: Ty_bool
+let eq i1 i2 = Relop (Eq, i1, i2) @: Ty_int
+let ne i1 i2 = Relop (Ne, i1, i2) @: Ty_int
 let ( < ) i1 i2 = Relop (Lt, i1, i2) @: Ty_int
+let ( <= ) i1 i2 = Relop (Le, i1, i2) @: Ty_int
+let ( > ) i1 i2 = Relop (Gt, i1, i2) @: Ty_int
 let ( >= ) i1 i2 = Relop (Ge, i1, i2) @: Ty_int
+let ( + ) i1 i2 = Binop (Add, i1, i2) @: Ty_int
+let ( - ) i1 i2 = Binop (Sub, i1, i2) @: Ty_int
 let ( * ) i1 i2 = Binop (Mul, i1, i2) @: Ty_int
+let ( / ) i1 i2 = Binop (Div, i1, i2) @: Ty_int
+let rem i1 i2 = Binop (Rem, i1, i2) @: Ty_int
+let ( ** ) i1 i2 = Binop (Pow, i1, i2) @: Ty_int
+let neg i = Unop (Neg, i) @: Ty_int
 
 let () =
-  let opt = Optimizer.create () in
-  Optimizer.add opt [ x >= v 0; x < v 5 ];
-  Optimizer.push opt;
-  assert (Some (Value.Int 0) = Optimizer.minimize opt x);
-  Optimizer.pop opt;
-  assert (Some (Value.Int 4) = Optimizer.maximize opt x)
+  let solver = Solver.create ~logic:LIA () in
+  let x = mk_symbol Symbol.("x" @: Ty_int) in
+  Solver.add solver [ x > v 0; x <= v 10 ];
+  assert (Solver.check solver [ ne x (v 0) ]);
+  let y = mk_symbol Symbol.("y" @: Ty_int) in
+  assert (Solver.check solver [ eq (x + y - y) x ]);
+  assert (Solver.check solver [ eq (x * y / y) x ]);
+  assert (Solver.check solver [ rem y x < v 10 ]);
+  assert (Solver.check solver [ eq ((x ** v 2) / x) (x * x / x) ]);
+  let z = mk_symbol Symbol.("z" @: Ty_int) in
+  Solver.add solver [ z > v 0 ];
+  assert (Solver.check solver [ neg z < v 0 ])
 
 let () =
   let solver = Solver.create ~logic:LIA () in
+  let symbol_x = Symbol.("x" @: Ty_int) in
+  let x = mk_symbol symbol_x in
   assert (Solver.check solver []);
   assert (Solver.check solver [ x >= v 0 ]);
   assert ({ e = Val (Int 0); ty = Ty_int } = Solver.get_value solver x);
@@ -35,3 +50,15 @@ let () =
   let model = Solver.model solver in
   let val_x = Option.bind model (fun m -> Model.evaluate m symbol_x) in
   assert (Some (Value.Int 5) = val_x)
+
+let () =
+  let opt = Optimizer.create () in
+  let x = mk_symbol Symbol.("x" @: Ty_int) in
+  Optimizer.add opt [ x >= v 0; x < v 5 ];
+  Optimizer.push opt;
+  Optimizer.push opt;
+  assert (Some (Value.Int 0) = Optimizer.minimize opt x);
+  Optimizer.pop opt;
+  assert (Some (Value.Int 4) = Optimizer.maximize opt x);
+  let model = Optimizer.model opt in
+  Option.iter (Model.pp Format.std_formatter) model

test/test_parser.expected

@@ -1 +1,4 @@
 sat
+(model
+  (y real 4.)
+  (x real -2.))

test/test_parser.ml

@@ -3,13 +3,15 @@ module Batch = Solver.Batch (Z3_mappings)
 module Interpret = Interpret.Make (Batch)
 
 let () =
+  (* FIXME: when y = 2.0 this fails in Z3! *)
   let script =
     {|
     (declare-fun x real)
     (declare-fun y real)
     (assert (real.eq y (real.mul x x)))
-    (assert (real.eq y 2.0))
+    (assert (real.eq y 4.0))
     (check-sat)
+    (get-model)
     |}
   in
   Parse.from_string script |> Interpret.start |> ignore