trim

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

src/cmd_context/extra_cmds/proof_cmds.cpp

@@ -189,6 +189,8 @@ class proof_trim {
     cmd_context& ctx;
     ast_manager& m;
     sat::proof_trim trim;
+    vector<expr_ref_vector> m_clauses;
+    bool_vector             m_is_infer;
     
     void mk_clause(expr_ref_vector const& clause) {
         trim.init_clause();
@@ -214,9 +216,11 @@ public:
         trim(gparams::get_module("sat"), m.limit()) {            
     }
     
-    void assume(expr_ref_vector const& _clause, bool is_initial = true) {        
+    void assume(expr_ref_vector const& clause) {
-        mk_clause(_clause);
+        mk_clause(clause);
-        trim.assume(true);
+        trim.assume(m_clauses.size());
+        m_clauses.push_back(clause);
+        m_is_infer.push_back(false);
     }
     
     void del(expr_ref_vector const& _clause) {
@@ -224,14 +228,42 @@ public:
         trim.del();
     }
     
-    void infer(expr_ref_vector const& _clause, app*) {
+    void infer(expr_ref_vector const& clause, app* hint) {
-        mk_clause(_clause);
+        mk_clause(clause);
-        trim.infer();
+        trim.infer(m_clauses.size());
+        m_clauses.push_back(clause);
+        if (hint)
+            m_clauses.back().push_back(hint);
+        m_is_infer.push_back(true);
     }
     
     void updt_params(params_ref const& p) {
         trim.updt_params(p);
     }
+
+    void do_trim(std::ostream& out) {
+        ast_pp_util pp(m);
+        auto ids = trim.trim();
+        for (unsigned id : ids) {
+            auto const& clause = m_clauses[id];
+            bool is_infer = m_is_infer[id];
+            for (expr* e : clause) 
+                pp.collect(e);
+            pp.display_decls(out);
+            for (expr* e : clause) 
+                pp.define_expr(out, e);
+
+            if (!is_infer)
+                out << "(assume ";
+            else
+                out << "(infer";
+            for (expr* e : clause) 
+                pp.display_expr_def(out << " ", e);
+            out << ")\n";
+        }
+    }
+
+    
 };
 
 class proof_saver {

src/sat/sat_proof_trim.cpp

@@ -29,12 +29,13 @@ namespace sat {
        Output: reduced trail - result                                                                           
     */        
 
-    vector<literal_vector> proof_trim::trim() {
+    unsigned_vector proof_trim::trim() {
-        vector<literal_vector> result;
+        unsigned_vector result;
         m_core_literals.reset();
         m_core_literals.insert(literal_vector());
+        m_propagated.resize(num_vars(), false);
         for (unsigned i = m_trail.size(); i-- > 0; ) {
-            auto const& [cl, clp, is_add, is_initial] = m_trail[i];
+            auto const& [id, cl, clp, is_add, is_initial] = m_trail[i];
             if (!is_add) {
                 revive(cl, clp);
                 continue;
@@ -43,7 +44,7 @@ namespace sat {
             del(cl, clp);
             if (!in_core(cl, clp))
                 continue;
-            result.push_back(cl);
+            result.push_back(id);
             if (is_initial)
                 continue;
             conflict_analysis_core(cl, clp);            
@@ -73,15 +74,15 @@ namespace sat {
              (l1 == cl[2] && l2 == cl[0] && l3 == cl[1]));
     }
 
-            /**
+    /**
-         * cl is on the trail if there is some literal l that is implied by cl
+     * cl is on the trail if there is some literal l that is implied by cl
-         * Remove all clauses after cl that are in the cone of influence of cl.
+     * Remove all clauses after cl that are in the cone of influence of cl.
-         * The coi is defined inductively: C is in coi of cl if it contains ~l
+     * The coi is defined inductively: C is in coi of cl if it contains ~l
-         * or it contains ~l' where l' is implied by a clause in the coi of cl.
+     * or it contains ~l' where l' is implied by a clause in the coi of cl.
-         * Possible optimization: 
+     * Possible optimization: 
-         * - check if clause contains a literal that is on implied on the trail
+     * - check if clause contains a literal that is on implied on the trail
-         *   if it doesn't contain any such literal, bypass the trail adjustment.
+     *   if it doesn't contain any such literal, bypass the trail adjustment.
-         */
+     */
 
     void proof_trim::prune_trail(literal_vector const& cl, clause* cp) {
         m_in_clause.reset();
@@ -90,6 +91,12 @@ namespace sat {
         for (literal lit : cl) 
             m_in_clause.insert(lit.index());
 
+        auto unassign_literal = [&](literal l) {
+            m_in_coi.insert((~l).index());
+            s.m_assignment[l.index()] = l_undef;
+            s.m_assignment[(~l).index()] = l_undef;
+        };
+        
         bool on_trail = false;
         unsigned j = 0;
         for (unsigned i = 0; i < s.trail_size(); ++i) {
@@ -97,9 +104,7 @@ namespace sat {
             if (m_in_clause.contains(l.index())) {
                 SASSERT(!on_trail);
                 on_trail = true;
-                m_in_coi.insert((~l).index());
+                unassign_literal(l);
-                s.m_assignment[l.index()] = l_undef;
-                s.m_assignment[(~l).index()] = l_undef;
                 continue;
             }
             if (!on_trail) {
@@ -119,11 +124,8 @@ namespace sat {
             else
                 UNREACHABLE(); // approach does not work for external justifications
             
-            if (in_coi) {
+            if (in_coi) 
-                m_in_coi.insert((~l).index());
+                unassign_literal(l);
-                s.m_assignment[l.index()] = l_undef;
-                s.m_assignment[(~l).index()] = l_undef;
-            }
             else
                 s.m_trail[j++] = s.m_trail[i];
         }            
@@ -171,52 +173,59 @@ namespace sat {
             s.propagate(false);
         }
         SASSERT(s.inconsistent());
-
+        for (unsigned i = trail_size0; i < s.m_trail.size(); ++i)
-        auto add_dependency = [&](literal lit) {
+            m_propagated[s.m_trail[i].var()] = true;
-            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);                
-            }
-            else if (s.lvl(v) == 2) 
-                s.mark(v);
-        };
-
-        auto add_jdependency = [&](justification j) {
-            switch (j.get_kind()) {
-            case justification::BINARY:
-                add_dependency(j.get_literal());
-                break;
-            case justification::TERNARY:
-                add_dependency(j.get_literal1());
-                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;
-            }            
-        };
 
         if (s.m_not_l != null_literal)
             add_dependency(s.m_not_l);
-        add_jdependency(s.m_conflict);
+        add_dependency(s.m_conflict);
         
         for (unsigned i = s.m_trail.size(); i-- > trail_size0; ) {
             bool_var v = s.m_trail[i].var();
+            m_propagated[v] = false;
             if (!s.is_marked(v))
                 continue;
             s.reset_mark(v);
-            add_jdependency(s.m_justification[v]);
+            add_dependency(s.get_justification(v));
         }
         s.pop(2);                
     }
 
+    void proof_trim::add_dependency(literal lit) {
+        bool_var v = lit.var();
+        if (m_propagated[v]) // literal was propagated after assuming ~C
+            s.mark(v);        
+        else if (s.lvl(v) == 0) { // literal depends on level 0, it is not assumed by ~C
+            // inefficient for repeated insertions ? 
+            auto j = s.get_justification(v);
+            literal lit = literal(v, s.value(v) == l_false);
+            add_core(lit, j);                
+        }
+    }
+    
+    void proof_trim::add_dependency(justification j) {
+        switch (j.get_kind()) {
+        case justification::BINARY:
+            add_dependency(j.get_literal());
+            break;
+        case justification::TERNARY:
+            add_dependency(j.get_literal1());
+            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;
+        case justification::EXT_JUSTIFICATION:
+            UNREACHABLE();
+            break;
+        default:
+            break;
+        }            
+    }
+
+
     void proof_trim::add_core(literal l, justification j) {
         m_clause.reset();
         switch (j.get_kind()) {
@@ -256,7 +265,6 @@ namespace sat {
             s.mk_clause(cl, status::redundant());            
     }
 
-
     clause* proof_trim::del(literal_vector const& cl) {
         clause* cp = nullptr;
         IF_VERBOSE(3, verbose_stream() << "del: " << cl << "\n");
@@ -285,17 +293,15 @@ namespace sat {
         v.push_back(cl);
     }    
 
-    
-
     proof_trim::proof_trim(params_ref const& p, reslimit& lim):
         s(p, lim)
     {}
 
-    void proof_trim::assume(bool is_initial) {
+    void proof_trim::assume(unsigned id, bool is_initial) {
         std::sort(m_clause.begin(), m_clause.end());
         IF_VERBOSE(3, verbose_stream() << "add: " << m_clause << "\n");
         auto* cl = s.mk_clause(m_clause, status::redundant());
-        m_trail.push_back({ m_clause, cl, true, is_initial });
+        m_trail.push_back({ id, m_clause, cl, true, is_initial });
         s.propagate(false);
         save(m_clause, cl);
     }
@@ -303,11 +309,11 @@ namespace sat {
     void proof_trim::del() {
         std::sort(m_clause.begin(), m_clause.end());
         clause* cp = del(m_clause);
-        m_trail.push_back({ m_clause, cp, false, true });
+        m_trail.push_back({ 0, m_clause, cp, false, true });
     }
     
-    void proof_trim::infer() {
+    void proof_trim::infer(unsigned id) {
-        assume(false);        
+        assume(id, false);        
     }
 
 

src/sat/sat_proof_trim.h

@@ -33,7 +33,7 @@ namespace sat {
         literal_vector m_clause;
         uint_set       m_in_clause;
         uint_set       m_in_coi;
-        vector<std::tuple<literal_vector, clause*, bool, bool>> m_trail;
+        vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail;
         
         
         struct hash {
@@ -49,6 +49,7 @@ namespace sat {
         map<literal_vector, clause_vector, hash, eq> m_clauses;
 
         hashtable<literal_vector, hash, eq> m_core_literals;
+        bool_vector                         m_propagated;
 
         void del(literal_vector const& cl, clause* cp);
 
@@ -57,6 +58,8 @@ namespace sat {
 
         void prune_trail(literal_vector const& cl, clause* cp);
         void conflict_analysis_core(literal_vector const& cl, clause* cp);
+        void add_dependency(literal lit);
+        void add_dependency(justification j);
         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);        
@@ -73,12 +76,12 @@ namespace sat {
         void add_literal(bool_var v, bool sign) { m_clause.push_back(literal(v, sign)); }
         unsigned num_vars() { return s.num_vars(); }
 
-        void assume(bool is_initial = true);
+        void assume(unsigned id, bool is_initial = true);
         void del();
-        void infer();
+        void infer(unsigned id);
         void updt_params(params_ref const& p) { s.updt_params(p); }
 
-        vector<literal_vector> trim();
+        unsigned_vector trim();
 
     };
 }