Use post-solve SAT environment for model generation (#789)

* Return the right environment

* Promote tests

* Use an adt to save the results of queries

* Use an adt to save the results of queries (bis)

* Fix lib_usage and worker_js

examples/dune

@@ -0,0 +1,16 @@
+(executable
+ (name Lib_usage)
+ (libraries AltErgoLib)
+ (modules Lib_usage)
+)
+
+(rule
+ (alias runtest)
+ (action
+  (ignore-stdout
+   (ignore-stderr
+    (run ./Lib_usage.exe)
+   )
+  )
+ )
+)

examples/lib_usage.ml

@@ -65,7 +65,7 @@ open AltErgoLib
 
 module PA = Parsed_interface
 
-let x = PA.mk_var_type Loc.dummy "'a"
+let _x = PA.mk_var_type Loc.dummy "'a"
 
 let one = PA.mk_int_const Loc.dummy "1"
 let two = PA.mk_int_const Loc.dummy "2"
@@ -80,7 +80,7 @@ let goal_3 = PA.mk_goal Loc.dummy "toy_3" (PA.mk_not Loc.dummy eq1)
 
 let parsed = [goal_1; goal_2; goal_3]
 
-let typed, env = Typechecker.type_file parsed
+let typed, _env = Typechecker.type_file parsed
 
 let pbs = Typechecker.split_goals_and_cnf typed
 
@@ -89,16 +89,19 @@ module FE = Frontend.Make(SAT)
 
 let () =
   List.iter
-    (fun (pb, goal_name) ->
+    (fun (pb, _goal_name) ->
        let ctxt = FE.init_all_used_context () in
-       let acc0 = SAT.empty (), true, Explanation.empty in
+       let acc0 = SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty in
        let s = Stack.create () in
-       let _, consistent, ex =
+       let _env, consistent, _ex =
          List.fold_left
            (fun acc d ->
               FE.process_decl (fun _ _ -> ()) ctxt s acc d
-           )acc0 pb
+           ) acc0 pb
        in
-       Format.printf "%s@."
-         (if consistent then "unknown" else "unsat")
+       match consistent with
+       | `Sat _ | `Unknown _ ->
+         Format.printf "unknown"
+       | `Unsat ->
+         Format.printf "unsat"
     )pbs

src/bin/common/solving_loop.ml

@@ -81,10 +81,10 @@ let main () =
           Options.Time.set_timeout (Options.get_timelimit ());
         end;
       SAT.reset_refs ();
-      let partial_model, consistent, _ =
+      let _, consistent, _ =
         List.fold_left
           (FE.process_decl FE.print_status used_context consistent_dep_stack)
-          (SAT.empty (), true, Explanation.empty) cnf
+          (SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty) cnf
       in
       if Options.get_timelimit_per_goal() then
         Options.Time.unset_timeout ();
@@ -96,9 +96,10 @@ let main () =
       (* If the status of the SAT environment is inconsistent,
          we have to drop the partial model in order to prevent
          printing wrong model. *)
-      if consistent then
+      match consistent with
+      | `Sat partial_model | `Unknown partial_model ->
         Some partial_model
-      else None
+      | `Unsat -> None
     with Util.Timeout ->
       if not (Options.get_timelimit_per_goal()) then exit 142;
       None

src/bin/js/worker_js.ml

@@ -130,11 +130,12 @@ let main worker_id content =
       let used_context = FE.choose_used_context all_context ~goal_name in
       let consistent_dep_stack = Stack.create () in
       SAT.reset_refs ();
+      let env = SAT.empty_with_inst add_inst in
       let _,_,dep =
         List.fold_left
           (FE.process_decl
              get_status_and_print used_context consistent_dep_stack)
-          (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in
+          (env, `Unknown env, Explanation.empty) cnf in
 
       if Options.get_unsat_core () then begin
         unsat_core := Explanation.get_unsat_core dep;

src/lib/frontend/frontend.ml

@@ -39,6 +39,12 @@ module type S = sig
   type sat_env
   type used_context
 
+  type res = [
+    | `Sat of sat_env
+    | `Unknown of sat_env
+    | `Unsat
+  ]
+
   type status =
     | Unsat of Commands.sat_tdecl * Ex.t
     | Inconsistent of Commands.sat_tdecl
@@ -50,10 +56,10 @@ module type S = sig
   val process_decl:
     (status -> int -> unit) ->
     used_context ->
-    (bool * Ex.t) Stack.t ->
-    sat_env * bool * Ex.t ->
+    (res * Ex.t) Stack.t ->
+    sat_env * res * Ex.t ->
     Commands.sat_tdecl ->
-    sat_env * bool * Ex.t
+    sat_env * res * Ex.t
 
   val print_status : status -> int -> unit
 
@@ -65,9 +71,14 @@ end
 module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   type sat_env = SAT.t
-
   type used_context = Util.SS.t option
 
+  type res = [
+    | `Sat of sat_env
+    | `Unknown of sat_env
+    | `Unsat
+  ]
+
   type status =
     | Unsat of Commands.sat_tdecl * Ex.t
     | Inconsistent of Commands.sat_tdecl
@@ -149,12 +160,12 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       match d.st_decl with
       | Push n ->
         Util.loop ~f:(fun _n env () -> Stack.push env consistent_dep_stack)
-          ~max:n ~elt:(consistent,dep) ~init:();
+          ~max:n ~elt:(consistent, dep) ~init:();
         SAT.push env n, consistent, dep
       | Pop n ->
-        let consistent,dep =
+        let consistent, dep =
           Util.loop ~f:(fun _n () _env -> Stack.pop consistent_dep_stack)
-            ~max:n ~elt:() ~init:(consistent,dep)
+            ~max:n ~elt:() ~init:(consistent, dep)
         in
         SAT.pop env n, consistent, dep
       | Assume(n, f, mf) ->
@@ -163,23 +174,27 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
           acc
         else
           let dep = if is_hyp then Ex.empty else mk_root_dep n f d.st_loc in
-          if consistent then
-            SAT.assume env
-              {E.ff=f;
-               origin_name = n;
-               gdist = -1;
-               hdist = (if is_hyp then 0 else -1);
-               trigger_depth = max_int;
-               nb_reductions = 0;
-               age=0;
-               lem=None;
-               mf=mf;
-               gf=false;
-               from_terms = [];
-               theory_elim = true;
-              } dep,
-            consistent, dep
-          else env, consistent, dep
+          begin
+            match consistent with
+            | `Sat _ | `Unknown _ ->
+              SAT.assume env
+                {E.ff=f;
+                 origin_name = n;
+                 gdist = -1;
+                 hdist = (if is_hyp then 0 else -1);
+                 trigger_depth = max_int;
+                 nb_reductions = 0;
+                 age=0;
+                 lem=None;
+                 mf=mf;
+                 gf=false;
+                 from_terms = [];
+                 theory_elim = true;
+                } dep,
+              consistent, dep
+            | `Unsat ->
+              env, consistent, dep
+          end
       | PredDef (f, name) ->
         if unused_context name used_context then acc
         else
@@ -190,7 +205,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
       | Query(n, f, sort) ->
         let dep =
-          if consistent then
+          match consistent with
+          | `Sat _ | `Unknown _ ->
             let dep' = SAT.unsat env
                 {E.ff=f;
                  origin_name = n;
@@ -206,45 +222,47 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
                  theory_elim = true;
                 } in
             Ex.union dep' dep
-          else dep
+          | `Unsat -> dep
         in
         if get_debug_unsat_core () then check_produced_unsat_core dep;
         if get_save_used_context () then output_used_context n dep;
         print_status (Unsat (d, dep)) (Steps.get_steps ());
-        env, false, dep
+        env, `Unsat, dep
 
       | ThAssume ({ Expr.ax_name; Expr.ax_form ; _ } as th_elt) ->
         if unused_context ax_name used_context then
           acc
         else
-        if consistent then
-          let dep = mk_root_dep ax_name ax_form d.st_loc in
-          let env = SAT.assume_th_elt env th_elt dep in
-          env, consistent, dep
-        else env, consistent, dep
+          match consistent with
+          | `Sat _ | `Unknown _ ->
+            let dep = mk_root_dep ax_name ax_form d.st_loc in
+            let env = SAT.assume_th_elt env th_elt dep in
+            env, consistent, dep
+          | `Unsat ->
+            env, consistent, dep
 
     with
     | SAT.Sat t ->
       (* This case should mainly occur when a query has a non-unsat result,
          so we want to print the status in this case. *)
       print_status (Sat (d,t)) (Steps.get_steps ());
       (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*)
-      env , consistent, dep
+      env, `Sat t, dep
     | SAT.Unsat dep' ->
       (* This case should mainly occur when a new assumption results in an unsat
          env, in which case we do not want to print status, since the correct
          status should be printed at the next query. *)
       let dep = Ex.union dep dep' in
       if get_debug_unsat_core () then check_produced_unsat_core dep;
       (* print_status (Inconsistent d) (Steps.get_steps ()); *)
-      env , false, dep
+      env, `Unsat, dep
     | SAT.I_dont_know t ->
       (* In this case, it's not clear whether we want to print the status.
          Instead, it'd be better to accumulate in `consistent` a 3-case adt
          and not a simple bool. *)
       print_status (Unknown (d, t)) (Steps.get_steps ());
       (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*)
-      env , consistent, dep
+      env, `Unknown t, dep
     | Util.Timeout as e ->
       (* In this case, we obviously want to print the status,
          since we exit right after  *)

src/lib/frontend/frontend.mli

@@ -31,9 +31,14 @@
 module type S = sig
 
   type sat_env
-
   type used_context
 
+  type res = [
+    | `Sat of sat_env
+    | `Unknown of sat_env
+    | `Unsat
+  ]
+
   type status =
     | Unsat of Commands.sat_tdecl * Explanation.t
     | Inconsistent of Commands.sat_tdecl
@@ -45,10 +50,10 @@ module type S = sig
   val process_decl:
     (status -> int -> unit) ->
     used_context ->
-    (bool * Explanation.t) Stack.t ->
-    sat_env * bool * Explanation.t ->
+    (res * Explanation.t) Stack.t ->
+    sat_env * res * Explanation.t ->
     Commands.sat_tdecl ->
-    sat_env * bool * Explanation.t
+    sat_env * res * Explanation.t
 
   val print_status : status -> int -> unit
 

tests/dune.inc

@@ -170907,6 +170907,26 @@
 
 ; Auto-generated part begin
 (subdir issues
+  (rule
+   (target 777.models_tableaux.output)
+   (deps (:input 777.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff 777.models.expected 777.models_tableaux.output)))
   (rule
    (target 696_ci_cdcl_no_minimal_bj.output)
    (deps (:input 696.ae))

tests/issues/777.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun i () Int 2)
+)

tests/issues/777.models.smt2

@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const i Int)
+(define-fun C ((j Int)) Bool (> j 0))
+(assert (C i))
+(check-sat)
+(get-model)

tests/models/bool/bool1.models.expected

@@ -1,6 +1,7 @@
 
 unknown
 (
+  (define-fun q () Bool false)
 )
 
 unknown