Added theory lemma as possible premise for clauses

sat/res.ml

@@ -6,10 +6,10 @@ Copyright 2014 Simon Cruanes
 
 module type S = Res_intf.S
 
-module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
+module Make(St : Solver_types.S) = struct
 
   (* Type definitions *)
-  type lemma = Proof.proof
+  type lemma = St.proof
   type clause = St.clause
   type atom = St.atom
   type int_cl = clause * St.atom list
@@ -86,11 +86,11 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
 
   (* Adding hyptoheses *)
   let is_unit_hyp = function
-    | [a] -> St.(a.var.level = 0 && a.var.reason = None && a.var.vpremise <> [])
+    | [a] -> St.(a.var.level = 0 && a.var.reason = None && a.var.vpremise <> History [])
     | _ -> false
 
   let make_unit_hyp a =
-    let aux a = St.(make_clause (fresh_name ()) [a] 1 false []) in
+    let aux a = St.(make_clause (fresh_name ()) [a] 1 false (History [])) in
     if St.(a.is_true) then
       aux a
     else if St.(a.neg.is_true) then
@@ -114,8 +114,9 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     else if is_unit_hyp cl || not St.(c.learnt) then begin
       H.add proof cl Assumption;
       true
-    end else
+    end else match St.(c.cpremise) with
-      false
+      | St.Lemma p -> H.add proof cl (Lemma p); true
+      | St.History _ -> false
 
   let is_proven c = is_proved (c, to_list c)
 
@@ -131,7 +132,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     | [] -> raise (Resolution_error "No literal to resolve over")
     | [a] ->
       H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
-      let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true [c; d] in
+      let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) in
       Log.debug 5 "New clause : %a" St.pp_clause new_c;
       new_c, new_clause
     | _ -> raise (Resolution_error "Resolved to a tautology")
@@ -177,7 +178,9 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     if is_proved (c, cl) then
       []
     else
-      St.(c.cpremise)
+      match St.(c.cpremise) with
+      | St.History l -> l
+      | St.Lemma _ -> assert false
 
   let rec do_clause = function
     | [] -> ()

sat/res.mli

@@ -6,6 +6,6 @@ Copyright 2014 Simon Cruanes
 
 module type S = Res_intf.S
 
-module Make : functor (St : Solver_types.S)(Proof : sig type proof end)
+module Make : functor (St : Solver_types.S)
-  -> S with type atom= St.atom and type clause = St.clause and type lemma = Proof.proof
+  -> S with type atom= St.atom and type clause = St.clause and type lemma = St.proof
 (** Functor to create a module building proofs from a sat-solver unsat trace. *)

sat/solver.ml

@@ -13,8 +13,8 @@
 module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t) = struct
 
-  module St = Solver_types.Make(F)
+  module St = Solver_types.Make(F)(Th)
-  module Proof = Res.Make(St)(Th)
+  module Proof = Res.Make(St)
 
   open St
 
@@ -245,7 +245,7 @@ module Make (F : Formula_intf.S)
         a.neg.is_true <- false;
         a.var.level <- -1;
         a.var.reason <- None;
-        a.var.vpremise <- [];
+        a.var.vpremise <- History [];
         insert_var_order a.var
       done;
       Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
@@ -356,8 +356,8 @@ module Make (F : Formula_intf.S)
   let slice_get i = (Vec.get env.trail i).lit
   let slice_push lit l lemma =
     let atoms = List.rev_map add_atom (lit :: (List.rev_map F.neg l)) in
-    let c = St.make_clause (St.fresh_name ()) atoms (List.length atoms) true [] in
+    let c = make_clause (fresh_name ()) atoms (List.length atoms) true (Lemma lemma) in
-    enqueue (St.add_atom lit) (decision_level ()) (Some c)
+    enqueue (add_atom lit) (decision_level ()) (Some c)
 
   let current_slice () = Th.({
       start = env.tatoms_qhead;
@@ -373,7 +373,7 @@ module Make (F : Formula_intf.S)
       propagate ()
     | Th.Unsat (l, p) ->
       let l = List.rev_map St.add_atom l in
-      let c = St.make_clause (St.fresh_name ()) l (List.length l) true [] in
+      let c = St.make_clause (St.fresh_name ()) l (List.length l) true (History []) in
       Some c
 
   and propagate () =
@@ -544,81 +544,12 @@ module Make (F : Formula_intf.S)
     var_decay_activity ();
     clause_decay_activity ()
 
-
-  (*
-  let theory_analyze dep = 0, [], [], 1
-    let atoms, sz, max_lvl, c_hist =
-      Ex.fold_atoms
-        (fun a (acc, sz, max_lvl, c_hist) ->
-           let c_hist = List.rev_append a.var.vpremise c_hist in
-           let c_hist = match a.var.reason with
-             | None -> c_hist | Some r -> r:: c_hist in
-           if a.var.level = 0 then acc, sz, max_lvl, c_hist
-           else a.neg :: acc, sz + 1, max max_lvl a.var.level, c_hist
-        ) dep ([], 0, 0, [])
-    in
-    if atoms = [] then begin
-      (* check_inconsistency_of dep; *)
-      report_t_unsat dep
-      (* une conjonction de faits unitaires etaient deja unsat *)
-    end;
-    let name = fresh_dname() in
-    let c_clause = make_clause name atoms sz false c_hist in
-    (* eprintf "c_clause: %a@." Debug.clause c_clause; *)
-    c_clause.removed <- true;
-
-    let pathC  = ref 0 in
-    let learnt = ref [] in
-    let cond   = ref true in
-    let blevel = ref 0 in
-    let seen   = ref [] in
-    let c      = ref c_clause in
-    let tr_ind = ref (Vec.size env.trail - 1) in
-    let size   = ref 1 in
-    let history = ref [] in
-    while !cond do
-      if !c.learnt then clause_bump_activity !c;
-      history := !c :: !history;
-      (* visit the current predecessors *)
-      for j = 0 to Vec.size !c.atoms - 1 do
-        let q = Vec.get !c.atoms j in
-        (*printf "I visit %a@." D1.atom q;*)
-        assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *)
-        if not q.var.seen && q.var.level > 0 then begin
-          var_bump_activity q.var;
-          q.var.seen <- true;
-          seen := q :: !seen;
-          if q.var.level >= max_lvl then incr pathC
-          else begin
-            learnt := q :: !learnt;
-            incr size;
-            blevel := max !blevel q.var.level
-          end
-        end
-      done;
-
-      (* look for the next node to expand *)
-      while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done;
-      decr pathC;
-      let p = Vec.get env.trail !tr_ind in
-      decr tr_ind;
-      match !pathC, p.var.reason with
-      | 0, _ ->
-        cond := false;
-        learnt := p.neg :: (List.rev !learnt)
-      | n, None   -> assert false
-      | n, Some cl -> c := cl
-    done;
-    List.iter (fun q -> q.var.seen <- false) !seen;
-    !blevel, !learnt, !history, !size
-    *)
-
   let add_boolean_conflict confl =
     env.conflicts <- env.conflicts + 1;
     if decision_level() = 0 then report_unsat confl; (* Top-level conflict *)
     let blevel, learnt, history, size = analyze confl in
     cancel_until blevel;
-    record_learnt_clause blevel learnt history size
+    record_learnt_clause blevel learnt (History history) size
 
   let search n_of_conflicts n_of_learnts =
     let conflictC = ref 0 in
@@ -700,9 +631,11 @@ module Make (F : Formula_intf.S)
           if a.var.level = 0 then raise Trivial
           else (a::trues) @ unassigned @ falses @ r, init
         else if a.neg.is_true then
-          if a.var.level = 0 then
+          if a.var.level = 0 then match a.var.vpremise with
+          | History v ->
             partition_aux trues unassigned falses
-              (List.rev_append (a.var.vpremise) init) r
+              (List.rev_append v init) r
+          | Lemma _ -> assert false
           else partition_aux trues unassigned (a::falses) init r
         else partition_aux trues (a::unassigned) falses init r
     in
@@ -712,15 +645,16 @@ module Make (F : Formula_intf.S)
   let add_clause ~cnumber atoms =
     if env.is_unsat then raise Unsat;
     let init_name = string_of_int cnumber in
-    let init0 = make_clause init_name atoms (List.length atoms) false [] in
+    let init0 = make_clause init_name atoms (List.length atoms) false (History []) in
     try
       let atoms, init =
         if decision_level () = 0 then
           let atoms, init = List.fold_left
               (fun (atoms, init) a ->
                  if a.is_true then raise Trivial;
-                 if a.neg.is_true then
+                 if a.neg.is_true then match a.var.vpremise with
-                   atoms, (List.rev_append (a.var.vpremise) init)
+                 | History v -> atoms, (List.rev_append v init)
+                 | Lemma p -> assert false
                  else a::atoms, init
               ) ([], [init0]) atoms in
           List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
@@ -733,7 +667,7 @@ module Make (F : Formula_intf.S)
 
       | a::_::_ ->
         let name = fresh_name () in
-        let clause = make_clause name atoms size false init in
+        let clause = make_clause name atoms size false (History init) in
         attach_clause clause;
         Vec.push env.clauses clause;
         if a.neg.is_true then begin
@@ -744,7 +678,7 @@ module Make (F : Formula_intf.S)
 
       | [a]   ->
         cancel_until 0;
-        a.var.vpremise <- init;
+        a.var.vpremise <- History init;
         enqueue a 0 None;
         match propagate () with
           None -> () | Some confl -> report_unsat confl

sat/solver_types.ml

@@ -15,9 +15,10 @@ open Printf
 
 module type S = Solver_types_intf.S
 
-module Make (F : Formula_intf.S) = struct
+module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct
 
   type formula = F.t
+  type proof = Th.proof
 
   type var =
     {  vid : int;
@@ -47,7 +48,9 @@ module Make (F : Formula_intf.S) = struct
 
   and reason = clause option
 
-  and premise = clause list
+  and premise =
+      | History of clause list
+      | Lemma of proof
 
   let dummy_lit = F.dummy
 
@@ -59,7 +62,7 @@ module Make (F : Formula_intf.S) = struct
       reason = None;
       weight = -1.;
       seen = false;
-      vpremise = [] }
+      vpremise = History [] }
   and dummy_atom =
     { var = dummy_var;
       lit = dummy_lit;
@@ -76,7 +79,7 @@ module Make (F : Formula_intf.S) = struct
       activity = -1.;
       removed = false;
       learnt = false;
-      cpremise = [] }
+      cpremise = History [] }
 
   let () =
     dummy_atom.watched <- Vec.make_empty dummy_clause
@@ -102,7 +105,7 @@ module Make (F : Formula_intf.S) = struct
             reason = None;
             weight = 0.;
             seen = false;
-            vpremise = [];
+            vpremise = History [];
           }
         and pa =
           { var = var;
@@ -140,7 +143,7 @@ module Make (F : Formula_intf.S) = struct
       activity = 0.;
       cpremise = premise}
 
-  let empty_clause = make_clause "Empty" [] 0 false []
+  let empty_clause = make_clause "Empty" [] 0 false (History [])
 
   let fresh_lname =
     let cpt = ref 0 in
@@ -188,8 +191,9 @@ module Make (F : Formula_intf.S) = struct
     else if a.neg.is_true then sprintf "[F%s]" (level a)
     else ""
 
-  let pp_premise b v =
+  let pp_premise b = function
-    List.iter (fun {name=name} -> bprintf b "%s," name) v
+      | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v
+      | Lemma _ -> bprintf b "th_lemma"
 
   let pp_atom b a =
     bprintf b "%s%d%s [lit:%s] vpremise={{%a}}"

sat/solver_types.mli

@@ -13,5 +13,6 @@
 
 module type S = Solver_types_intf.S
 
-module Make : functor (F : Formula_intf.S) -> S with type formula = F.t
+module Make : functor (F : Formula_intf.S)(Th : Theory_intf.S)
+  -> S with type formula = F.t and type proof = Th.proof
 (** Functor to instantiate the types of clauses for the Solver. *)

sat/solver_types_intf.ml

@@ -15,6 +15,8 @@ module type S = sig
   (** The signatures of clauses used in the Solver. *)
 
   type formula
+  type proof
+
   type varmap
   val ma : varmap ref
 
@@ -48,7 +50,9 @@ module type S = sig
   }
 
   and reason = clause option
-  and premise = clause list
+  and premise =
+      | History of clause list
+      | Lemma of proof
   (** Recursive types for literals (atoms) and clauses *)
 
   val dummy_var : var