From 4989026f06b1a478897ab2c78aaf310ec64ae99d Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 25 Aug 2017 18:33:42 +0200
Subject: [PATCH] Fix mcsat conflict analysis

When analyzing an mcst conflict clause and looking at a semantic
propagation in the trail, the last resolved clause was looked at again,
which caused an invalid history to be generated (the computation of the
backtrack clause was not affected because the second resolution of the clause
was basically a no-op thanks to the 'seen' field), thus it did not
introduce any soundness bug, just a faulty clause history which was
caught during proof expansion.
---
 src/core/internal.ml | 75 +++++++++++++++++++++++++-------------------
 1 file changed, 43 insertions(+), 32 deletions(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 5fac1e30..916ba91a 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -617,47 +617,57 @@ module Make
     let cond   = ref true in
     let blevel = ref 0 in
     let seen   = ref [] in
-    let c      = ref c_clause in
+    let c      = ref (Some c_clause) in
     let tr_ind = ref (Vec.size env.elt_queue - 1) in
     let history = ref [] in
     assert (decision_level () > 0);
     let conflict_level =
       Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms
     in
+    Log.debugf debug "Analyzing conflict (%d): %a"
+      (fun k -> k conflict_level St.pp_clause c_clause);
     while !cond do
-      begin match !c.cpremise with
-        | History _ -> clause_bump_activity !c
-        | Hyp | Local | Lemma _ -> ()
-      end;
-      history := !c :: !history;
-      (* visit the current predecessors *)
-      for j = 0 to Array.length !c.atoms - 1 do
-        let q = !c.atoms.(j) in
-        assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *)
-        if q.var.v_level <= 0 then begin
-          assert (q.neg.is_true);
-          match q.var.reason with
-          | Some Bcp cl -> history := cl :: !history
-          | _ -> assert false
-        end;
-        if not (q.var.seen = Both) then begin
-          q.var.seen <- Both;
-          seen := q :: !seen;
-          if q.var.v_level > 0 then begin
-            var_bump_activity q.var;
-            if q.var.v_level >= conflict_level then begin
-              incr pathC;
-            end else begin
-              learnt := q :: !learnt;
-              blevel := max !blevel q.var.v_level
+      begin match !c with
+        | None ->
+          Log.debugf debug "  skipping resolution for semantic propagation" (fun k->k)
+        | Some clause ->
+          Log.debugf debug "  Resolving clause: %a" (fun k->k St.pp_clause clause);
+          begin match clause.cpremise with
+            | History _ -> clause_bump_activity clause
+            | Hyp | Local | Lemma _ -> ()
+          end;
+          history := clause :: !history;
+          (* visit the current predecessors *)
+          for j = 0 to Array.length clause.atoms - 1 do
+            let q = clause.atoms.(j) in
+            assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *)
+            if q.var.v_level <= 0 then begin
+              assert (q.neg.is_true);
+              match q.var.reason with
+              | Some Bcp cl -> history := cl :: !history
+              | _ -> assert false
+            end;
+            if not (q.var.seen = Both) then begin
+              q.var.seen <- Both;
+              seen := q :: !seen;
+              if q.var.v_level > 0 then begin
+                var_bump_activity q.var;
+                if q.var.v_level >= conflict_level then begin
+                  incr pathC;
+                end else begin
+                  learnt := q :: !learnt;
+                  blevel := max !blevel q.var.v_level
+                end
+              end
             end
-          end
-        end
-      done;
+          done
+      end;
 
       (* look for the next node to expand *)
       while
-        match Vec.get env.elt_queue !tr_ind with
+        let a = Vec.get env.elt_queue !tr_ind in
+        Log.debugf debug "  looking at: %a" (fun k -> k St.pp a);
+        match a with
         | Atom q ->
           (not (q.var.seen = Both)) ||
           (q.var.v_level < conflict_level)
@@ -674,11 +684,12 @@ module Make
         learnt := p.neg :: (List.rev !learnt)
       | n, Some Semantic ->
         assert (n > 0);
-        learnt := p.neg :: !learnt
+        learnt := p.neg :: !learnt;
+        c := None
       | n, Some Bcp cl ->
         assert (n > 0);
         assert (p.var.v_level >= conflict_level);
-        c := cl
+        c := Some cl
       | n, _ -> assert false
     done;
     List.iter (fun q -> clear q.var) !seen;