From 2e4fd5e1c1cbb253739ff8a93d2c8b22deb5e46f Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 27 Nov 2021 15:30:45 -0500
Subject: [PATCH] update conflict resolution for better proofs, improve code

---
 src/core/Sidekick_core.ml     |  2 +-
 src/lra/sidekick_arith_lra.ml |  2 +-
 src/sat/Solver.ml             | 19 +++++++++----------
 3 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 95a0ca70..871b2d5e 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -1276,7 +1276,7 @@ end = struct
     else None
 
   let on_new_term self cc n (t:T.t) : unit =
-    Log.debugf 50 (fun k->k "@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);
+    (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*)
     let maybe_m, l = M.of_term cc n t in
     begin match maybe_m with
       | Some v ->
diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml
index dcab4b4d..fa334ace 100644
--- a/src/lra/sidekick_arith_lra.ml
+++ b/src/lra/sidekick_arith_lra.ml
@@ -627,7 +627,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   (* look for subterms of type Real, for they will need theory combination *)
   let on_subterm (self:state) _ (t:T.t) : unit =
-    Log.debugf 50 (fun k->k "lra: cc-on-subterm %a" T.pp t);
+    Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t);
     if A.has_ty_real t &&
        not (T.Tbl.mem self.needs_th_combination t) then (
       Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t);
diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index b24d438b..7acea724 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -1329,6 +1329,7 @@ module Make(Plugin : PLUGIN)
     AVec.clear learnt;
 
     let steps = self.temp_step_vec in (* for proof *)
+    assert (Step_vec.is_empty steps);
 
     (* loop variables *)
     let pathC  = ref 0 in
@@ -1371,16 +1372,14 @@ module Make(Plugin : PLUGIN)
           let atoms = Clause.atoms_a store clause in
           for j = 0 to Array.length atoms - 1 do
             let q = atoms.(j) in
-            assert (Atom.is_true store q ||
-                    Atom.is_false store q &&
-                    Atom.level store q >= 0); (* unsure? *)
-            if Atom.level store q <= 0 then (
+            assert (Atom.has_value store q);
+            assert (Atom.level store q >= 0);
+            if Atom.level store q = 0 then (
               assert (Atom.is_false store q);
-              begin match Atom.reason store q with
-                | Some (Bcp cl | Bcp_lazy (lazy cl)) when Proof.enabled self.proof ->
-                  Step_vec.push steps (Clause.proof_step self.store cl);
-                | _ -> ()
-              end
+              if Proof.enabled self.proof then (
+                let step = proof_of_atom_lvl0_ self (Atom.neg q) in
+                Step_vec.push steps step;
+              )
             );
             if not (Var.marked store (Atom.var q)) then (
               Var.mark store (Atom.var q);
@@ -1549,7 +1548,7 @@ module Make(Plugin : PLUGIN)
           (* cannot recover from this *)
           report_unsat self @@ US_false clause
         ) else if Atom.is_true store a then (
-          () (* atom is already true, nothing to do *)
+          () (* atom is already true, (at level 0) nothing to do *)
         ) else (
           Log.debugf 40
             (fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" (Atom.debug store) a);