SAT API available without process_decl in Frontend (OCamlPro#927)

Now OptimAE has been merged, we can export the API at the frontend level without a too violent rebase. This PR mostly refactors the Frontend module to export the most basic API functions (corresponding to Commands instructions).
bclement-ocp · Nov 8, 2023 · a72dcbb · a72dcbb
1 parent 825ee5d
commit a72dcbb
Show file tree

Hide file tree

Showing 4 changed files with 238 additions and 124 deletions.
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -120,7 +120,6 @@ let main () =
         goal_name
         Fmt.(list ~sep:sp Commands.print) cnf;
     let used_context = Frontend.choose_used_context all_context ~goal_name in
-    let consistent_dep_stack = Stack.create () in
     Signals_profiling.init_profiling ();
     try
       if Options.get_timelimit_per_goal() then
@@ -129,11 +128,11 @@ let main () =
           Options.Time.set_timeout (Options.get_timelimit ());
         end;
       SAT.reset_refs ();
-      let _, consistent, _ =
+      let ftdn_env =
         List.fold_left
-          (FE.process_decl
-             Frontend.print_status used_context consistent_dep_stack)
-          (SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty) cnf
+          (FE.process_decl ~hook_on_status:Frontend.print_status)
+          (FE.init_env used_context)
+          cnf
       in
       if Options.get_timelimit_per_goal() then
         Options.Time.unset_timeout ();
@@ -144,7 +143,7 @@ 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. *)
-      match consistent with
+      match ftdn_env.FE.res with
       | `Sat partial_model | `Unknown partial_model ->
         Some (Model ((module SAT), partial_model))
       | `Unsat -> None

diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml
@@ -122,17 +122,16 @@ let main worker_id content =
 
     let solve all_context (cnf, goal_name) =
       let used_context = Frontend.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 =
+      let sat_env = SAT.empty_with_inst add_inst in
+      let ftnd_env =
         List.fold_left
-          (FE.process_decl
-             get_status_and_print used_context consistent_dep_stack)
-          (env, `Unknown env, Explanation.empty) cnf in
-
+          (FE.process_decl ~hook_on_status:get_status_and_print)
+          (FE.init_env ~sat_env used_context)
+          cnf
+      in
       if Options.get_unsat_core () then begin
-        unsat_core := Explanation.get_unsat_core dep;
+        unsat_core := Explanation.get_unsat_core ftnd_env.FE.expl;
       end;
     in