fixes to trim

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_proof_trim.cpp

@@ -27,46 +27,12 @@ namespace sat {
        Pseudo-code from Gurfinkel, Vizel, FMCAD 2014
        Input: trail (a0,d0), ..., (an,dn) = ({},bot)
        Output: reduced trail - result                                                                           
-       result = []
-       C = { an }
-       for i = n to 0 do
-           if s.is_deleted(ai) then s.revive(ai)
-           else 
-              if s.isontrail(ai) then
-                  s.undotrailcore(ai,C)
-              s.delete(ai)
-              if ai in C then 
-                  if ai is not initial then
-                      s.savetrail()
-                      s.enqueue(not ai)
-                      c = s.propagate()
-                      s.conflictanalysiscore(c, C)
-                      s.restoretrail()
-                   result += [ai]
-       reverse(result)
-            
-       is_deleted(ai):
-          clause was detached
-       revive(ai):
-          attach clause ai
-       isontrail(ai):
-          some literal on the current trail in s is justified by ai
-       undotrailcore(ai, C):
-          pop the trail until dependencies on ai are gone
-       savetrail:
-          store current trail so it can be restored
-       enqueue(not ai):
-          assert negations of ai at a new decision level
-       conflictanalysiscore(c, C):
-          ?
-       restoretrail:
-          restore the trail to the position before enqueue
-                                                                          
     */        
 
-    void proof_trim::trim() {
+    vector<literal_vector> proof_trim::trim() {
-        vector<literal_vector> result, clauses;
+        vector<literal_vector> result;
-        clauses.push_back(literal_vector());
+        m_core_literals.reset();
+        m_core_literals.insert(literal_vector());
         for (unsigned i = m_trail.size(); i-- > 0; ) {
             auto const& [cl, clp, is_add, is_initial] = m_trail[i];
             if (!is_add) {
@@ -75,22 +41,15 @@ namespace sat {
             }
             prune_trail(cl, clp);
             del(cl, clp);
-            if (!clauses.contains(cl))
+            if (!in_core(cl, clp))
                 continue;
             result.push_back(cl);
             if (is_initial)
                 continue;
-            s.push();
+            conflict_analysis_core(cl, clp);            
-            unsigned init_sz = s.m_trail.size();
-            unsigned lvl = s.scope_lvl();
-            for (auto lit : cl)
-                s.assign(~lit, justification(lvl));
-            s.propagate(false);
-            SASSERT(s.inconsistent());
-            conflict_analysis_core(init_sz, clauses);
-            s.pop(1);                
         }
         result.reverse();
+        return result;
     }
     
     void proof_trim::del(literal_vector const& cl, clause* cp) {
@@ -176,14 +135,15 @@ namespace sat {
        The current state is in conflict.
        Chase justifications for conflict to extract clauses that are in coi of conflict.
 
+
        Assume:
        F | G, ~C |- []
        Let T (trail) be the extension of G, ~C that derives the empty clause.
        T := G, ~C, l1:j1, l2:j2, ..., lk:jk
        The goal is to extract clauses in T that are used to derive C.
-       - some of the literals in ~C that are not set to true already (they must be unassigned relative)
+       This is achieved by collecting all literals from j1, j2, ... jk 
-       are used to derive the empty clause.
+       and the conflict clause that are at level below ~C and using the clauses that justify those literals. 
-       - some literals in ~C that are assigned to true may also be used to derive the empty clause.
+      
              
        Example:
        C = c or d or e
@@ -197,44 +157,67 @@ namespace sat {
        queried for their explanation. Their explanation is added to the clauses.
        
     */
-    void proof_trim::conflict_analysis_core(unsigned init_sz, vector<literal_vector>& clauses) {
+    void proof_trim::conflict_analysis_core(literal_vector const& cl, clause* cp) {
-        justification j = s.m_conflict;
+
-        literal consequent = null_literal;
+        s.push();
-        unsigned idx = s.m_trail.size() - 1;
+        unsigned lvl = s.scope_lvl();
-        unsigned old_sz = s.m_unmark.size();
+        for (auto lit : cl)
-        bool_var c_var;
+            s.assign(~lit, justification(lvl));
-        auto add_dependency = [&](bool_var v) {
+        unsigned trail_size0 = s.m_trail.size();
+        s.push();
+        s.propagate(false);
+        if (!s.inconsistent()) {
+            s.m_qhead = 0;
+            s.propagate(false);
+        }
+        SASSERT(s.inconsistent());
+
+        auto add_dependency = [&](literal lit) {
+            bool_var v = lit.var();
+            if (s.lvl(v) == 0) {
+                // inefficient for repeated insertions ? 
                 auto j = s.m_justification[v];
                 literal lit = literal(v, s.value(v) == l_false);
-            add_core(lit, j, clauses);            
+                add_core(lit, j);                
+            }
+            else if (s.lvl(v) == 2) 
+                s.mark(v);
         };
 
-        if (s.m_not_l != null_literal) {
+        auto add_jdependency = [&](justification j) {
-            s.process_antecedent_for_unsat_core(s.m_not_l);
+            switch (j.get_kind()) {
-            add_core(s.m_not_l, s.m_justification[s.m_not_l.var()], clauses);
+            case justification::BINARY:
-            add_core(~s.m_not_l, j, clauses);
+                add_dependency(j.get_literal());
-            consequent = ~s.m_not_l;                
-        }
-        while (true) {
-            s.process_consequent_for_unsat_core(consequent, j);
-            while (idx >= init_sz) {
-                consequent = s.m_trail[idx];
-                c_var = consequent.var();
-                if (s.is_marked(c_var))
                 break;
-                --idx;
+            case justification::TERNARY:
-            }
+                add_dependency(j.get_literal1());
-            if (idx < init_sz)
+                add_dependency(j.get_literal2());
+                break;
+            case justification::CLAUSE: 
+                for (auto lit : s.get_clause(j))
+                    if (s.value(lit) == l_false)
+                        add_dependency(lit);
+                break;
+            default:
                 break;
-            j = s.m_justification[c_var];
-            --idx;
             }            
-        for (unsigned i = s.m_mark.size(); i-- > old_sz; ) 
+        };
-            add_dependency(s.m_unmark[i]);
+
-        s.reset_unmark(old_sz);
+        if (s.m_not_l != null_literal)
+            add_dependency(s.m_not_l);
+        add_jdependency(s.m_conflict);
+        
+        for (unsigned i = s.m_trail.size(); i-- > trail_size0; ) {
+            bool_var v = s.m_trail[i].var();
+            if (!s.is_marked(v))
+                continue;
+            s.reset_mark(v);
+            add_jdependency(s.m_justification[v]);
+        }
+        s.pop(2);                
     }
 
-    void proof_trim::add_core(literal l, justification j, vector<literal_vector>& clauses) {
+    void proof_trim::add_core(literal l, justification j) {
         m_clause.reset();
         switch (j.get_kind()) {
         case justification::NONE:
@@ -249,17 +232,22 @@ namespace sat {
             m_clause.push_back(j.get_literal2());
             break;
         case justification::CLAUSE:
-            for (auto lit : s.get_clause(j))
+            s.get_clause(j).mark_used();
-                m_clause.push_back(lit);
+            return;
-            break;
         default:
             UNREACHABLE();
             break;
         }
         std::sort(m_clause.begin(), m_clause.end());
-        clauses.insert(m_clause);            
+        m_core_literals.insert(m_clause);
     }
 
+    bool proof_trim::in_core(literal_vector const& cl, clause* cp) const {
+        if (cp)
+            return cp->was_used();
+        else
+            return m_core_literals.contains(cl);
+    }
 
     void proof_trim::revive(literal_vector const& cl, clause* cp) {
         if (cp) 

src/sat/sat_proof_trim.h

@@ -35,6 +35,7 @@ namespace sat {
         uint_set       m_in_coi;
         vector<std::tuple<literal_vector, clause*, bool, bool>> m_trail;
         
+        
         struct hash {
             unsigned operator()(literal_vector const& v) const {
                 return string_hash((char const*)v.begin(), v.size()*sizeof(literal), 3);
@@ -47,18 +48,22 @@ namespace sat {
         };
         map<literal_vector, clause_vector, hash, eq> m_clauses;
 
+        hashtable<literal_vector, hash, eq> m_core_literals;
+
         void del(literal_vector const& cl, clause* cp);
 
         bool match_clause(literal_vector const& cl, literal l1, literal l2) const;
         bool match_clause(literal_vector const& cl, literal l1, literal l2, literal l3) const;
 
         void prune_trail(literal_vector const& cl, clause* cp);
-        void conflict_analysis_core(unsigned init_sz, vector<literal_vector>& clauses);
+        void conflict_analysis_core(literal_vector const& cl, clause* cp);
-        void add_core(literal l, justification j, vector<literal_vector>& clauses);
+        void add_core(literal l, justification j);
+        bool in_core(literal_vector const& cl, clause* cp) const;
         void revive(literal_vector const& cl, clause* cp);        
         clause* del(literal_vector const& cl);
         void save(literal_vector const& lits, clause* cl);
 
+        
     public:
 
         proof_trim(params_ref const& p, reslimit& lim);
@@ -73,7 +78,7 @@ namespace sat {
         void infer();
         void updt_params(params_ref const& p) { s.updt_params(p); }
 
-        void trim();
+        vector<literal_vector> trim();
 
     };
 }