From 2f3a044271f175540abaeac2aeb311dcc430df4e Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 30 Mar 2017 18:41:35 +0200
Subject: [PATCH] Add local assumptions support to msat binary

---
 src/main.ml         | 64 ++++++++++++++++++++++++++++++---------------
 src/sat/type_sat.ml |  8 ++++++
 src/smt/type_smt.ml |  7 +++++
 src/util/type.ml    |  3 +++
 4 files changed, 61 insertions(+), 21 deletions(-)

diff --git a/src/main.ml b/src/main.ml
index 86d35d7f..2c7abeec 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -38,6 +38,40 @@ module Make
 
   let hyps = ref []
 
+  let check_model state =
+    let check_clause c =
+      let l = List.map (function a ->
+          Log.debugf 99 "Checking value of %a"
+            (fun k -> k S.St.pp_atom (S.St.add_atom a));
+          state.Solver_intf.eval a) c in
+      List.exists (fun x -> x) l
+    in
+    let l = List.map check_clause !hyps in
+    List.for_all (fun x -> x) l
+
+  let prove ~assumptions =
+    let res = S.solve () in
+    let t = Sys.time () in
+    begin match res with
+      | S.Sat state ->
+        if !p_check then
+          if not (check_model state) then
+            raise Incorrect_model;
+        let t' = Sys.time () -. t in
+        Format.printf "Sat (%f/%f)@." t t'
+      | S.Unsat state ->
+        if !p_check then begin
+          let p = state.Solver_intf.get_proof () in
+          S.Proof.check p;
+          if !p_dot_proof <> "" then begin
+            let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in
+            D.print fmt p
+          end
+        end;
+        let t' = Sys.time () -. t in
+        Format.printf "Unsat (%f/%f)@." t t'
+    end
+
   let do_task s =
     match s.Dolmen.Statement.descr with
     | Dolmen.Statement.Def (id, t) -> T.def id t
@@ -50,28 +84,16 @@ module Make
       let cnf = T.antecedent t in
       hyps := cnf @ !hyps;
       S.assume cnf
+    | Dolmen.Statement.Pack [
+        { Dolmen.Statement.descr = Dolmen.Statement.Push 1; };
+        { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f; };
+        { Dolmen.Statement.descr = Dolmen.Statement.Prove; };
+        { Dolmen.Statement.descr = Dolmen.Statement.Pop 1; };
+      ] ->
+      let assumptions = T.assumptions f in
+      prove ~assumptions
     | Dolmen.Statement.Prove ->
-      let res = S.solve () in
-      let t = Sys.time () in
-      begin match res with
-        | S.Sat state ->
-          if !p_check then
-            if not (List.for_all (List.exists state.Solver_intf.eval) !hyps) then
-              raise Incorrect_model;
-          let t' = Sys.time () -. t in
-          Format.printf "Sat (%f/%f)@." t t'
-        | S.Unsat state ->
-          if !p_check then begin
-            let p = state.Solver_intf.get_proof () in
-            S.Proof.check p;
-            if !p_dot_proof <> "" then begin
-              let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in
-              D.print fmt p
-            end
-          end;
-          let t' = Sys.time () -. t in
-          Format.printf "Unsat (%f/%f)@." t t'
-      end
+      prove ~assumptions:[]
     | _ ->
       Format.printf "Command not supported:@\n%a@."
         Dolmen.Statement.print s
diff --git a/src/sat/type_sat.ml b/src/sat/type_sat.ml
index 6c58d98b..3c45b9cb 100644
--- a/src/sat/type_sat.ml
+++ b/src/sat/type_sat.ml
@@ -68,6 +68,14 @@ let decl _ t =
 let def _ t =
   raise (Typing_error ("Definitions are not allowed in pure sat", t))
 
+let assumptions t =
+  let f = parse t in
+  let cnf = Formula.make_cnf f in
+  List.map (function
+      | [ x ] -> x
+      | _ -> assert false
+    ) cnf
+
 let antecedent t =
   let f = parse t in
   Formula.make_cnf f
diff --git a/src/smt/type_smt.ml b/src/smt/type_smt.ml
index 89fac586..a3f55125 100644
--- a/src/smt/type_smt.ml
+++ b/src/smt/type_smt.ml
@@ -609,6 +609,13 @@ let formula t =
   Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t);
   parse_formula env t
 
+let assumptions t =
+  let cnf = Expr.Formula.make_cnf (formula t) in
+  List.map (function
+      | [ x ] -> x
+      | _ -> assert false
+    ) cnf
+
 let antecedent t =
   Expr.Formula.make_cnf (formula t)
 
diff --git a/src/util/type.ml b/src/util/type.ml
index 788328a3..693f35ce 100644
--- a/src/util/type.ml
+++ b/src/util/type.ml
@@ -16,6 +16,9 @@ module type S = sig
   val def  : Dolmen.Id.t -> Dolmen.Term.t -> unit
   (** New definition, i.e an identifier and the term it is equal to. *)
 
+  val assumptions : Dolmen.Term.t -> atom list
+  (** Parse a list of local assumptions. *)
+
   val consequent : Dolmen.Term.t -> atom list list
   val antecedent : Dolmen.Term.t -> atom list list
   (** Parse a formula, and return a cnf ready to be given to the solver.