api: annotate input clauses with theory proofs, too

this replaces the old "tag" system

src/backend/Coq.ml

@@ -124,7 +124,7 @@ module Make(S : Msat.S)(A : Arg with type hyp := S.clause
   let prove_node t fmt node =
     let clause = node.P.conclusion in
     match node.P.step with
-    | P.Hypothesis ->
+    | P.Hypothesis _ ->
       A.prove_hyp fmt (name clause) clause
     | P.Assumption ->
       A.prove_assumption fmt (name clause) clause

src/backend/Dot.ml

@@ -110,7 +110,7 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom
   let print_contents fmt n =
     match P.(n.step) with
     (* Leafs of the proof tree *)
-    | P.Hypothesis ->
+    | P.Hypothesis _ ->
       let rule, color, l = A.hyp_info P.(n.conclusion) in
       let color = match color with None -> "LIGHTBLUE" | Some c -> c in
       print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l

src/core/Internal.ml

@@ -70,7 +70,7 @@ module Make(Plugin : PLUGIN)
   (* TODO: remove, replace with user-provided proof trackng device?
      for pure SAT, [reason] is sufficient *)
   and premise =
-    | Hyp
+    | Hyp of lemma
     | Local
     | Lemma of lemma
     | History of clause list
@@ -113,7 +113,7 @@ module Make(Plugin : PLUGIN)
   let iter_elt st f = Vec.iter f st.vars
 
   let name_of_clause c = match c.cpremise with
-    | Hyp -> "H" ^ string_of_int c.name
+    | Hyp _ -> "H" ^ string_of_int c.name
     | Lemma _ -> "T" ^ string_of_int c.name
     | Local -> "L" ^ string_of_int c.name
     | History _ -> "C" ^ string_of_int c.name
@@ -391,7 +391,7 @@ module Make(Plugin : PLUGIN)
       Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms
 
     let debug_premise out = function
-      | Hyp -> Format.fprintf out "hyp"
+      | Hyp _ -> Format.fprintf out "hyp"
       | Lemma _ -> Format.fprintf out "th_lemma"
       | Local -> Format.fprintf out "local"
       | History v ->
@@ -530,7 +530,7 @@ module Make(Plugin : PLUGIN)
       step : step;
     }
     and step =
-      | Hypothesis
+      | Hypothesis of lemma
       | Assumption
       | Lemma of lemma
       | Duplicate of t * atom list
@@ -565,8 +565,8 @@ module Make(Plugin : PLUGIN)
         {conclusion; step = Lemma l; }
       | Local ->
         { conclusion; step = Assumption; }
-      | Hyp ->
-        { conclusion; step = Hypothesis; }
+      | Hyp l ->
+        { conclusion; step = Hypothesis l; }
       | History [] ->
         error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion
       | History [c] ->
@@ -585,21 +585,21 @@ module Make(Plugin : PLUGIN)
 
     (* Proof nodes manipulation *)
     let is_leaf = function
-      | Hypothesis
+      | Hypothesis _
       | Assumption
       | Lemma _ -> true
       | Duplicate _
       | Resolution _ -> false
 
     let parents = function
-      | Hypothesis
+      | Hypothesis _
       | Assumption
       | Lemma _ -> []
       | Duplicate (p, _) -> [p]
       | Resolution (p, p', _) -> [p; p']
 
     let expl = function
-      | Hypothesis -> "hypothesis"
+      | Hypothesis _ -> "hypothesis"
       | Assumption -> "assumption"
       | Lemma _ -> "lemma"
       | Duplicate _ -> "duplicate"
@@ -615,7 +615,7 @@ module Make(Plugin : PLUGIN)
           if not @@ Clause.visited c then (
             Clause.set_visited c true;
             match c.cpremise with
-            | Hyp | Lemma _ | Local -> aux (c :: res) acc r
+            | Hyp _ | Lemma _ | Local -> aux (c :: res) acc r
             | History h ->
               let l = List.fold_left (fun acc c ->
                   if not @@ Clause.visited c then c :: acc else acc) r h in
@@ -653,7 +653,7 @@ module Make(Plugin : PLUGIN)
             | Resolution (p1, p2, _) ->
               Stack.push (Enter p2) s;
               Stack.push (Enter p1) s
-            | Hypothesis | Assumption | Lemma _ -> ()
+            | Hypothesis _ | Assumption | Lemma _ -> ()
           end
         end;
         fold_aux s h f acc
@@ -1319,7 +1319,7 @@ module Make(Plugin : PLUGIN)
           Log.debugf debug (fun k->k"(@[sat.analyze-conflict.resolve@ %a@])"  Clause.debug clause);
           begin match clause.cpremise with
             | History _ -> clause_bump_activity st clause
-            | Hyp | Local | Lemma _ -> ()
+            | Hyp _ | Local | Lemma _ -> ()
           end;
           history := clause :: !history;
           (* visit the current predecessors *)
@@ -1953,11 +1953,11 @@ module Make(Plugin : PLUGIN)
       done
     with E_sat -> ()
 
-  let assume st cnf =
+  let assume st cnf lemma =
     List.iter
       (fun l ->
          let atoms = List.rev_map (mk_atom st) l in
-         let c = Clause.make atoms Hyp in
+         let c = Clause.make atoms (Hyp lemma) in
          Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])" Clause.debug c);
          Vec.push st.clauses_to_add c)
       cnf
@@ -2053,12 +2053,12 @@ module Make(Plugin : PLUGIN)
     in
     { Solver_intf.unsat_conflict; get_proof; unsat_assumptions; }
 
-  let[@inline] add_clause_a st c : unit =
-    let c = Clause.make_a c Hyp in
+  let[@inline] add_clause_a st c lemma : unit =
+    let c = Clause.make_a c (Hyp lemma) in
     add_clause_ st c
 
-  let[@inline] add_clause st c : unit =
-    let c = Clause.make c Hyp in
+  let[@inline] add_clause st c lemma : unit =
+    let c = Clause.make c (Hyp lemma) in
     add_clause_ st c
 
   let solve ?(assumptions=[]) (st:t) : res =
@@ -2110,13 +2110,13 @@ module Make_mcsat(Plugin : Solver_intf.PLUGIN_MCSAT) =
   end)
 [@@inline][@@specialise]
 
-module Make_pure_sat(F: Solver_intf.FORMULA) =
+module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) =
   Make(struct
-  module Formula = F
+  module Formula = Plugin.Formula
   module Term = Void_
   module Value = Void_
   type t = unit
-  type proof = Solver_intf.void
+  type proof = Plugin.proof
   let push_level () = ()
   let pop_levels _ _ = ()
   let partial_check () _ = ()

src/core/Solver.mli

@@ -25,10 +25,10 @@ module Make_mcsat(Th : Solver_intf.PLUGIN_MCSAT)
        and type lemma = Th.proof
        and type theory = Th.t
 
-module Make_pure_sat(F: Solver_intf.FORMULA)
+module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
   : S with type Term.t = Solver_intf.void
-       and module Formula = F
-       and type lemma = Solver_intf.void
+       and module Formula = Th.Formula
+       and type lemma = Th.proof
        and type theory = unit
 
 

src/core/Solver_intf.ml

@@ -240,7 +240,13 @@ module type PLUGIN_MCSAT = sig
 
   val eval : t -> Formula.t -> Term.t eval_res
   (** Returns the evaluation of the Formula.t in the current assignment *)
+end
 
+(** Signature for pure SAT solvers *)
+module type PLUGIN_SAT = sig
+  module Formula : FORMULA
+
+  type proof
 end
 
 module type PROOF = sig
@@ -269,7 +275,7 @@ module type PROOF = sig
 
   (** The type of reasoning steps allowed in a proof. *)
   and step =
-    | Hypothesis
+    | Hypothesis of lemma
     (** The conclusion is a user-provided hypothesis *)
     | Assumption
     (** The conclusion has been locally assumed by the user *)
@@ -361,6 +367,7 @@ module type S = sig
   type theory
 
   type lemma
+  (** A theory lemma or an input axiom *)
 
   type solver
 
@@ -423,14 +430,14 @@ module type S = sig
 
   (** {2 Base operations} *)
 
-  val assume : t -> formula list list -> unit
+  val assume : t -> formula list list -> lemma -> unit
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place. *)
 
-  val add_clause : t -> atom list -> unit
+  val add_clause : t -> atom list -> lemma -> unit
   (** Lower level addition of clauses *)
 
-  val add_clause_a : t -> atom array -> unit
+  val add_clause_a : t -> atom array -> lemma -> unit
   (** Lower level addition of clauses *)
 
   val solve : ?assumptions:atom list -> t -> res

src/main/main.ml

@@ -62,7 +62,7 @@ module Process = struct
   let conv_c c = List.rev_map S.Int_lit.make c
 
   let add_clauses cs =
-    S.assume st @@ CCList.map conv_c cs
+    S.assume st (CCList.map conv_c cs) ()
 end
 
 let parse_file f =

src/sat/Msat_sat.ml

@@ -4,5 +4,8 @@ Copyright 2016 Guillaume Bury
 *)
 
 module Int_lit = Int_lit
-include Msat.Make_pure_sat(Int_lit)
+include Msat.Make_pure_sat(struct
+    module Formula = Int_lit
+    type proof = unit
+  end)
 

src/sat/Msat_sat.mli

@@ -11,6 +11,9 @@ Copyright 2016 Guillaume Bury
 
 module Int_lit = Int_lit
 
-include Msat.S with type Formula.t = Int_lit.t and type theory = unit
+include Msat.S
+  with type Formula.t = Int_lit.t
+   and type theory = unit
+   and type lemma = unit
 (** A functor that can generate as many solvers as needed. *)
 

tests/icnf-solve/icnf_solve.ml

@@ -64,7 +64,7 @@ module Solver = struct
 
   let make () = S.create()
   let mklit s i = S.make_atom s (let v = F.make (abs i) in if i>0 then v else F.neg v)
-  let add_clause s c = S.add_clause_a s c; true
+  let add_clause s c = S.add_clause_a s c (); true
   let to_int a : int = F.to_int @@ S.Atom.formula a
   let solve s ass =
     let ass = Array.to_list ass in

tests/test_api.ml

@@ -72,10 +72,10 @@ module Test = struct
       List.iter
         (function
           | A_assume cs ->
-            S.assume st cs
+            S.assume st cs ()
           | A_solve (assumptions, expect) ->
             let assumptions = List.map (S.make_atom st) assumptions in
-            match S.solve st ~assumptions (), expect with
+            match S.solve ~assumptions st, expect with
               | S.Sat _, `Expect_sat -> ()
               | S.Unsat us, `Expect_unsat ->
                 let p = us.Msat.get_proof () in