Add an error for models of incremental problems

Plus some re-organizing of tests

src/model/loop.ml

@@ -33,6 +33,7 @@ type answer =
       evaluated_goals : bool located list;
       delayed : acc list Model.C.t;
     }
+  | Post_sat
 
 type 'st input =
   | Init
@@ -91,6 +92,13 @@ let code =
     ~category:"Model"
     ~descr:"on model verification errors"
 
+let incr_check_not_supported =
+  Dolmen_loop.Report.Error.mk ~code ~mnemonic:"incr-model-check"
+    ~message:(fun fmt () ->
+        Format.fprintf fmt "%a"
+          Format.pp_print_text "Incremental problems are not supported")
+    ~name:"Incremental model check" ()
+
 let type_def_in_model =
   Dolmen_loop.Report.Error.mk ~code ~mnemonic:"type-def-in-model"
     ~message:(fun fmt () ->
@@ -419,38 +427,40 @@ module Make
   (* Pipe function *)
   (* ************************************************************************ *)
 
+  let gen_answer gen st =
+    let file = State.get State.response_file st in
+    match (gen st : _ * _ option) with
+    | st, None -> st, None
+    | st, Some (answer : Dolmen.Std.Answer.t) ->
+      let loc = Dolmen.Std.Loc.{ file = file.loc; loc = answer.loc; } in
+      begin match answer.Dolmen.Std.Answer.descr with
+        | Unsat -> st, Unsat loc
+        | Error _ -> st, Error loc
+        | Sat None ->
+          st, Sat {
+            parsed = [];
+            model = Model.empty;
+            delayed = Model.C.empty;
+            evaluated_goals = [];
+          }
+        | Sat Some parsed ->
+          st, Sat {
+            parsed;
+            model = Model.empty;
+            delayed = Model.C.empty;
+            evaluated_goals = [];
+          }
+      end
+
   let next_answer st =
     let t = State.get check_state st in
     match t.input with
-    | Response_loaded gen -> gen st
+    | Response_loaded gen ->
+      gen st
     | Init ->
       let file = State.get State.response_file st in
       let st, gen = Parse.parse_response [] st file in
-      let answers st =
-        let file = State.get State.response_file st in
-        match gen st with
-        | st, None -> st, None
-        | st, Some answer ->
-          let loc = Dolmen.Std.Loc.{ file = file.loc; loc = answer.loc; } in
-          begin match answer.Dolmen.Std.Answer.descr with
-            | Unsat -> st, Unsat loc
-            | Error _ -> st, Error loc
-            | Sat None ->
-              st, Sat {
-                parsed = [];
-                model = Model.empty;
-                delayed = Model.C.empty;
-                evaluated_goals = [];
-              }
-            | Sat Some parsed ->
-              st, Sat {
-                parsed;
-                model = Model.empty;
-                delayed = Model.C.empty;
-                evaluated_goals = [];
-              }
-          end
-      in
+      let answers = gen_answer gen in
       let st =
         State.set check_state
           { t with input = Response_loaded answers; } st
@@ -461,8 +471,9 @@ module Make
      in the original problem (and not the model file) that triggered
      this module to read the model. Use multi-locs to better explain
      that. *)
-  let get_answer ~file ~loc st t = function
-    | (Unsat _ | Error _ | Sat _) as a -> st, a
+  let get_answer ~file ~loc st =
+    match (State.get check_state st).answer with
+    | (Unsat _ | Error _ | Sat _ | Post_sat) as a -> st, a
     | None ->
       let st, answer = next_answer st in
       let st =
@@ -475,16 +486,13 @@ module Make
         | Unsat loc ->
           let file = State.get State.response_file st in
           State.warn ~file ~loc st cannot_check_proofs ()
-        | Sat _ ->
+        | Sat _ | Post_sat ->
           st
       in
+      let t = State.get check_state st in
       let st = State.set check_state { t with answer; } st in
       st, answer
 
-  let reset st =
-    let t = State.get check_state st in
-    State.set check_state { t with answer = None; } st
-
   (* Evaluation functions *)
   (* ************************************************************************ *)
 
@@ -606,13 +614,15 @@ module Make
 
   let check_acc st acc =
     let file, loc = file_loc_of_acc acc in
-    let t = State.get check_state st in
-    let st, answer = get_answer ~file ~loc st t t.answer in
+    let st, answer = get_answer ~file ~loc st in
     match answer with
+    | Post_sat ->
+      State.error ~file ~loc st incr_check_not_supported ()
     | Sat { parsed; model; delayed; evaluated_goals; } ->
       let st, parsed, model, delayed, evaluated_goals =
         eval_loop st parsed model delayed evaluated_goals acc
       in
+      let t = State.get check_state st in
       let t = { t with answer = Sat { parsed; model; delayed; evaluated_goals; } } in
       State.set check_state t st
     | _ -> st
@@ -681,14 +691,16 @@ module Make
       | _ -> st
     in
     (* **4** Reset the state *)
-    reset st
+    let t = State.get check_state st in
+    State.set check_state { t with answer = Post_sat; } st
 
   (* Pipe/toplevel function *)
   (* ************************************************************************ *)
 
   let check st (c : Typer_Pipe.typechecked Typer_Pipe.stmt) =
     let st =
-      if State.get check_model st then
+      if not (State.get check_model st) then st
+      else begin
         let file = State.get State.logic_file st in
         let loc = Dolmen.Std.Loc.{ file = file.loc; loc = c.loc; } in
         match c.contents with
@@ -708,8 +720,7 @@ module Make
           check_clause ~file ~loc st contents
         | `Solve (hyps, goals) ->
           check_solve ~file ~loc st hyps goals
-      else
-        st
+      end
     in
     st, c
 

tests/model/error/bad_div_zero.expected → tests/model/int/bad_div_zero.expected

@@ -1,4 +1,4 @@
-File "tests/model/error/bad_div_zero.rsmt2", line 13, character 2 to line 14, character 30:
+File "tests/model/int/bad_div_zero.rsmt2", line 13, character 2 to line 14, character 30:
 13 | ..(define-fun div ((x Int) (y Int)) Bool
 14 |     (and (= x 21238) (= y 0)))
 Error Incoherent redefinition for term constant `div`.

tests/model/int/dune

@@ -33,6 +33,38 @@
   (action (diff add.expected add.full)))
 
 
+; Test for bad_div_zero.smt2
+; Incremental test
+
+(rule
+   (target  bad_div_zero.incremental)
+   (deps    (:response bad_div_zero.rsmt2) (:input bad_div_zero.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bad_div_zero.expected bad_div_zero.incremental)))
+
+; Full mode test
+
+(rule
+   (target  bad_div_zero.full)
+   (deps    (:response bad_div_zero.rsmt2) (:input bad_div_zero.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bad_div_zero.expected bad_div_zero.full)))
+
+
 ; Test for div.smt2
 ; Incremental test
 

tests/model/error/dune → tests/model/misc/dune

@@ -1,12 +1,12 @@
 ; File auto-generated by gentests.ml
 
 ; Auto-generated part begin
-; Test for bad_div_zero.smt2
+; Test for fo.smt2
 ; Incremental test
 
 (rule
-   (target  bad_div_zero.incremental)
-   (deps    (:response bad_div_zero.rsmt2) (:input bad_div_zero.smt2))
+   (target  fo.incremental)
+   (deps    (:response fo.rsmt2) (:input fo.smt2))
    (package dolmen_bin)
    (action (chdir %{workspace_root}
             (with-outputs-to %{target}
@@ -15,13 +15,13 @@
 (rule
   (alias runtest)
   (package dolmen_bin)
-  (action (diff bad_div_zero.expected bad_div_zero.incremental)))
+  (action (diff fo.expected fo.incremental)))
 
 ; Full mode test
 
 (rule
-   (target  bad_div_zero.full)
-   (deps    (:response bad_div_zero.rsmt2) (:input bad_div_zero.smt2))
+   (target  fo.full)
+   (deps    (:response fo.rsmt2) (:input fo.smt2))
    (package dolmen_bin)
    (action (chdir %{workspace_root}
             (with-outputs-to %{target}
@@ -30,15 +30,15 @@
 (rule
   (alias runtest)
   (package dolmen_bin)
-  (action (diff bad_div_zero.expected bad_div_zero.full)))
+  (action (diff fo.expected fo.full)))
 
 
-; Test for fo.smt2
+; Test for incr.smt2
 ; Incremental test
 
 (rule
-   (target  fo.incremental)
-   (deps    (:response fo.rsmt2) (:input fo.smt2))
+   (target  incr.incremental)
+   (deps    (:response incr.rsmt2) (:input incr.smt2))
    (package dolmen_bin)
    (action (chdir %{workspace_root}
             (with-outputs-to %{target}
@@ -47,13 +47,13 @@
 (rule
   (alias runtest)
   (package dolmen_bin)
-  (action (diff fo.expected fo.incremental)))
+  (action (diff incr.expected incr.incremental)))
 
 ; Full mode test
 
 (rule
-   (target  fo.full)
-   (deps    (:response fo.rsmt2) (:input fo.smt2))
+   (target  incr.full)
+   (deps    (:response incr.rsmt2) (:input incr.smt2))
    (package dolmen_bin)
    (action (chdir %{workspace_root}
             (with-outputs-to %{target}
@@ -62,7 +62,7 @@
 (rule
   (alias runtest)
   (package dolmen_bin)
-  (action (diff fo.expected fo.full)))
+  (action (diff incr.expected incr.full)))
 
 
 ; Test for missing_answer.smt2

tests/model/error/fo.expected → tests/model/misc/fo.expected

@@ -1,8 +1,8 @@
-File "tests/model/error/fo.rsmt2", line 3, character 15-22:
+File "tests/model/misc/fo.rsmt2", line 3, character 15-22:
 3 | (define-fun p ((x Int)) Bool true)
                    ^^^^^^^
 Warning The following function parameter is unused: `x`
-File "tests/model/error/fo.smt2", line 3, character 0-33:
+File "tests/model/misc/fo.smt2", line 3, character 0-33:
 3 | (assert (forall ((x Int)) (p x)))
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error Models cannot be checked for formulas that contain quantifiers

tests/model/misc/incr.expected

@@ -0,0 +1,4 @@
+File "tests/model/misc/incr.smt2", line 8, character 0-22:
+8 | (assert (< 0 (* a b)))
+    ^^^^^^^^^^^^^^^^^^^^^^
+Error Incremental problems are not supported

tests/model/misc/incr.rsmt2

@@ -0,0 +1,13 @@
+sat
+(
+  (define-fun a () Int (- 1))
+  (define-fun b () Int 1)
+)
+sat
+(
+  ; This is not a correct model, as this only
+  ; satisfies the last assertion (a*b>0), and not
+  ; the first one (a < 0).
+  (define-fun a () Int 1)
+  (define-fun b () Int 1)
+)

tests/model/misc/incr.smt2

@@ -0,0 +1,10 @@
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+(assert (< a 0))
+(check-sat)
+
+(assert (< 0 (* a b)))
+(check-sat)
+

tests/model/error/missing_answer.expected → tests/model/misc/missing_answer.expected

@@ -1,4 +1,4 @@
-File "tests/model/error/missing_answer.smt2", line 2, character 0-14:
+File "tests/model/misc/missing_answer.smt2", line 2, character 0-14:
 2 | (assert false)
     ^^^^^^^^^^^^^^
 Error This statement requires a model in the response file in order to be