feat: check-all-sat support

src/bin/common/parse_command.ml

@@ -366,8 +366,8 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
     `Ok()
 
 let mk_output_opt
-    interpretation use_underscore unsat_core output_format model_type
-    () () () ()
+    interpretation use_underscore all_models show_prop_model unsat_core
+    output_format model_type () () () ()
   =
   set_infer_output_format (Option.is_none output_format);
   let output_format = match output_format with
@@ -380,6 +380,8 @@ let mk_output_opt
   in
   set_interpretation interpretation;
   set_interpretation_use_underscore use_underscore;
+  set_all_models all_models;
+  set_show_prop_model show_prop_model;
   set_unsat_core unsat_core;
   set_output_format output_format;
   set_model_type model_type;
@@ -1032,11 +1034,29 @@ let parse_output_opt =
     let docv = "VAL" in
     Arg.(value & flag & info
            ["interpretation-use-underscore";"use-underscore"]
-           ~docv ~docs:s_models ~doc ~deprecated) in
+           ~docv ~docs:s_models ~doc ~deprecated)
+  in
+  let all_models =
+    let doc = "Enable all-models (or all-sat) feature, in which case, \
+               all possible boolean models will be explored. If \
+               --interpretation is also set, an interpretation for \
+               each boolean model will also be displayed. Note that \
+               timeouts are set per model/SAT branch in this case."
+    in
+    Arg.(value & flag & info ["all-models"; "all-sat"] ~docs:s_models ~doc)
+  in
+  let show_prop_model =
+    let doc = " also show the propositional if a model is requested \
+               (with --interpretation or with --all-models options)."
+    in
+    Arg.(value & flag & info
+           ["show-prop-model"; "show-propositional-model"] ~docs:s_models ~doc)
+  in
 
   let unsat_core =
     let doc = "Experimental support for computing and printing unsat-cores." in
-    Arg.(value & flag & info ["u"; "unsat-core"] ~doc ~docs) in
+    Arg.(value & flag & info ["u"; "unsat-core"] ~doc ~docs)
+  in
 
   let output_format =
     let doc =
@@ -1082,8 +1102,9 @@ let parse_output_opt =
   in
 
   Term.(ret (const mk_output_opt $
-             interpretation $ use_underscore $ unsat_core $
-             output_format $ model_type $
+             interpretation $ use_underscore $
+             all_models $ show_prop_model $
+             unsat_core $ output_format $ model_type $
              set_dump_models $ set_dump_models_on $
              set_sat_options $ set_frontend
             ))

src/bin/common/solving_loop.ml

@@ -121,7 +121,7 @@ let main () =
           | Ty.Cut ->
             { state with solver_ctx =
                            { state.solver_ctx with local = []}}
-          | Ty.Thm | Ty.Sat ->
+          | Ty.Thm | Ty.Sat | Ty.AllSat _ ->
             { state with solver_ctx = {
                   state.solver_ctx with global = []; local = []}}
         end
@@ -223,7 +223,7 @@ let main () =
     State.create_key ~pipe:"" "solving_state"
   in
 
-  let partial_model_key: SAT.t option State.key =
+  let partial_model_key: Models.t Lazy.t option State.key =
     State.create_key ~pipe:"" "sat_state"
   in
 
@@ -453,20 +453,20 @@ let main () =
             List.rev (cnf :: hyps), is_thm
           | _ -> assert false
         in
-        let partial_model = solve all_context (cnf, name) in
+        let sat_env = solve all_context (cnf, name) in
         if is_thm
         then
           State.set solver_ctx_key (
             let solver_ctx = State.get solver_ctx_key st in
             { solver_ctx with global = []; local = [] }
           ) st
-          |> State.set partial_model_key partial_model
+          |> State.set partial_model_key (Option.bind sat_env SAT.get_model)
         else
           State.set solver_ctx_key (
             let solver_ctx = State.get solver_ctx_key st in
             { solver_ctx with local = [] }
           ) st
-          |> State.set partial_model_key partial_model
+          |> State.set partial_model_key (Option.bind sat_env SAT.get_model)
 
       | {contents = `Set_option
              { DStd.Term.term =
@@ -481,17 +481,10 @@ let main () =
       | {contents = `Get_model; _ } ->
         if Options.get_interpretation () then
           match State.get partial_model_key st with
-          | Some partial_model ->
-            begin
-              match SAT.get_model partial_model with
-              | Some (lazy model) ->
-                Models.output_concrete_model
-                  (Options.Output.get_fmt_regular ()) model;
-                st
-              | _ ->
-                (* TODO: is it reachable? *)
-                st
-            end
+          | Some (lazy model) ->
+            Models.output_concrete_model ~pp_prop_model:false
+              (Options.Output.get_fmt_regular ()) model;
+            st
           | None ->
             (* TODO: add the location of the statement. *)
             Printer.print_smtlib_err "No model produced.";

src/bin/js/worker_js.ml

@@ -145,7 +145,107 @@ let main worker_id content =
         begin match kind with
           | Ty.Check
           | Ty.Cut -> { state with local = []; }
-          | Ty.Thm | Ty.Sat -> { state with global = []; local = []; }
+          | Ty.Thm | Ty.Sat | Ty.AllSat _ ->
+            { state with global = []; local = []; }
+        end
+      | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s ->
+        let cnf = Cnf.make state.global td in
+        { state with global = cnf; }
+      | Typed.TAxiom (_, s, _, _) when Ty.is_local_hyp s ->
+        let cnf = Cnf.make state.local td in
+        { state with local = cnf; }
+      | _ ->
+        let cnf = Cnf.make state.ctx td in
+        { state with ctx = cnf; }
+    in
+
+    let (module I : Input.S) = Input.find (Options.get_frontend ()) in
+    let parsed () =
+      try
+        Options.Time.start ();
+        I.parse_file ~content ~format:None
+      with
+      | Parsing.Parse_error ->
+        Printer.print_err "%a" Errors.report
+          (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),""));
+        raise Exit
+      | Errors.Error e ->
+        begin match e with
+          | Errors.Run_error r -> begin
+              match r with
+              | Steps_limit _ ->
+                returned_status :=
+                  Worker_interface.LimitReached "Steps limit"
+              | _ -> returned_status := Worker_interface.Error "Run error"
+            end
+          | _ -> returned_status := Worker_interface.Error "Error"
+        end;
+        Printer.print_err "%a" Errors.report e;
+        raise Exit
+    in
+    let all_used_context = FE.init_all_used_context () in
+    let assertion_stack = Stack.create () in
+    let typing_loop state p =
+      try
+        let l, env = I.type_parsed state.env assertion_stack p in
+        List.fold_left (typed_loop all_used_context) { state with env; } l
+      with Errors.Error e ->
+        Printer.print_err "%a" Errors.report e;
+        raise Exit
+    in
+
+    let state = {
+      env = I.empty_env;
+      ctx = [];
+      local = [];
+      global = [];
+    } in
+
+    begin
+      try let _ : _ state =
+            Seq.fold_left typing_loop state (parsed ()) in ()
+      with Exit -> () end;
+
+    let get_status_and_print status n =
+      returned_status :=
+        begin match status with
+          | FE.Unsat _ -> Worker_interface.Unsat n
+          | FE.Inconsistent _ -> Worker_interface.Inconsistent n
+          | FE.Sat _ -> Worker_interface.Sat n
+          | FE.Unknown _ -> Worker_interface.Unknown n
+          | FE.Timeout _ -> Worker_interface.LimitReached "timeout"
+          | FE.Preprocess -> Worker_interface.Unknown n
+        end;
+      FE.print_status status n
+    in
+
+    let solve all_context (cnf, goal_name) =
+      let used_context = FE.choose_used_context all_context ~goal_name in
+      let consistent_dep_stack = Stack.create () in
+      SAT.reset_refs ();
+      let _,_,dep =
+        let env = SAT.empty_with_inst add_inst in
+        List.fold_left
+          (FE.process_decl
+             get_status_and_print used_context consistent_dep_stack)
+          (env, `Unknown env, Explanation.empty) cnf
+      in
+      if Options.get_unsat_core () then begin
+        unsat_core := Explanation.get_unsat_core dep;
+      end;
+    in
+
+    let typed_loop all_context state td =
+      match td.Typed.c with
+      | Typed.TGoal (_, kind, name, _) ->
+        let l = state.local @ state.global @ state.ctx in
+        let cnf = List.rev @@ Cnf.make l td in
+        let () = solve all_context (cnf, name) in
+        begin match kind with
+          | Ty.Check
+          | Ty.Cut -> { state with local = []; }
+          | Ty.Thm | Ty.Sat | Ty.AllSat _ ->
+            { state with global = []; local = []; }
         end
       | Typed.TAxiom (_, s, _, _) when Ty.is_global_hyp s ->
         let cnf = Cnf.make state.global td in
@@ -224,13 +324,12 @@ let main worker_id content =
             end
           | Some r ->
             let b,e = r.loc in
-            (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,
-             !nb,Worker_interface.Used)
+            (r.name,b.Lexing.pos_lnum,e.Lexing.pos_lnum,!nb,
+             Worker_interface.Used)
             :: acc
         ) tbl []
     in
 
-
     (* returns a records with compatible worker_interface fields *)
     {
       Worker_interface.worker_id = worker_id;

src/bin/text/main_text.ml

@@ -40,6 +40,7 @@ let parse_cmdline () =
   try Parse_command.parse_cmdline_arguments ()
   with Parse_command.Exit_parse_command i -> exit i
 
+
 let () =
   register_input ();
   parse_cmdline ();