drat

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

src/sat/sat_drat.cpp

@@ -209,17 +209,17 @@ namespace sat {
         IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
         if (st.is_redundant() && st.is_sat()) 
             verify(1, &l);
-        
+
+        if (m_trim)
+            m_proof.push_back({mk_clause(1, &l, st.is_redundant()), st});
+
         if (st.is_deleted()) 
             return;
         
-        if (m_check_unsat) 
+        if (m_check_unsat) {
             assign_propagate(l);
-
+            m_units.push_back({l, nullptr});
-        if (m_trim)
+        }
-            append(mk_clause(1, &l, st.is_redundant()), st);
-
-        m_units.push_back(l);
     }
 
     void drat::append(literal l1, literal l2, status st) {
@@ -230,8 +230,8 @@ namespace sat {
 
         IF_VERBOSE(20, trace(verbose_stream(), 2, lits, st););
         if (st.is_deleted()) {
-            // noop
+            if (m_trim)
-            // don't record binary as deleted.
+                m_proof.push_back({mk_clause(2, lits, true), st});
         }
         else {
             if (st.is_redundant() && st.is_sat()) 
@@ -367,9 +367,10 @@ namespace sat {
         }
 
         for (unsigned i = num_units; i < m_units.size(); ++i) 
-            m_assignment[m_units[i].var()] = l_undef;
+            m_assignment[m_units[i].first.var()] = l_undef;
-        
+
-        units.append(m_units.size() - num_units, m_units.data() + num_units);
+        for (unsigned i = num_units; i < m_units.size(); ++i)
+            units.push_back(m_units[i].first);
         m_units.shrink(num_units);
         bool ok = m_inconsistent;
         m_inconsistent = false;
@@ -387,63 +388,12 @@ namespace sat {
         
         DEBUG_CODE(if (!m_inconsistent) validate_propagation(););        
         DEBUG_CODE(
-            for (literal u : m_units) 
+            for (auto const& [u,c] : m_units) 
                 SASSERT(m_assignment[u.var()] != l_undef);
             );
 
-#if 0
-        if (!m_inconsistent) {
-            literal_vector lits(n, c);
-            IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
-            for (unsigned v = 0; v < m_assignment.size(); ++v) {
-                lbool val = m_assignment[v];
-                if (val != l_undef) {
-                    IF_VERBOSE(0, verbose_stream() << literal(v, false) << " |-> " << val << "\n");
-                }
-            }
-            for (clause* cp : s.m_clauses) {
-                clause& cl = *cp;
-                bool found = false;
-                for (literal l : cl) {
-                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
-                        found = true;
-                        break;
-                    }
-                }
-                if (!found) {
-                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
-                }
-            }
-            for (clause* cp : s.m_learned) {
-                clause& cl = *cp;
-                bool found = false;
-                for (literal l : cl) {
-                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
-                        found = true;
-                        break;
-                    }
-                }
-                if (!found) {
-                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
-                }
-            }
-            svector<sat::solver::bin_clause> bin;
-            s.collect_bin_clauses(bin, true);
-            for (auto& b : bin) {
-                bool found = false;
-                if (m_assignment[b.first.var()] != (b.first.sign() ? l_true : l_false)) found = true;
-                if (m_assignment[b.second.var()] != (b.second.sign() ? l_true : l_false)) found = true;
-                if (!found) {
-                    IF_VERBOSE(0, verbose_stream() << "Bin clause is false under assignment: " << b.first << " " << b.second << "\n");
-                }
-            }
-            IF_VERBOSE(0, s.display(verbose_stream()));
-            exit(0);
-        }
-#endif
-
         for (unsigned i = num_units; i < m_units.size(); ++i) 
-            m_assignment[m_units[i].var()] = l_undef;
+            m_assignment[m_units[i].first.var()] = l_undef;
         
         m_units.shrink(num_units);
         bool ok = m_inconsistent;
@@ -540,7 +490,10 @@ namespace sat {
         }
         switch (j.get_kind()) {
         case justification::NONE:
-            return m_units.contains(c);
+            for (auto const& [u, j] : m_units)
+                if (u == c)
+                    return true;
+            return false;
         case justification::BINARY:
             return contains(c, j.get_literal());
         case justification::TERNARY:
@@ -588,7 +541,11 @@ namespace sat {
     }
 
     void drat::display(std::ostream& out) const {
-        out << "units: " << m_units << "\n";
+        
+        out << "units: ";
+        for (auto const& [u, c] : m_units)
+            out << u << " ";
+        out << "\n";
         for (unsigned i = 0; i < m_assignment.size(); ++i) {
             lbool v = value(literal(i, false));
             if (v != l_undef)
@@ -650,7 +607,7 @@ namespace sat {
             break;
         case l_undef:
             m_assignment.setx(l.var(), new_value, l_undef);
-            m_units.push_back(l);
+            m_units.push_back({l, nullptr});
             break;
         }
     }
@@ -661,7 +618,7 @@ namespace sat {
         unsigned num_units = m_units.size();
         assign(l);
         for (unsigned i = num_units; !m_inconsistent && i < m_units.size(); ++i) 
-            propagate(m_units[i]);        
+            propagate(m_units[i].first);        
     }
 
     void drat::propagate(literal l) {
@@ -843,6 +800,21 @@ namespace sat {
         if (m_check) append(mk_clause(c.size(), c.begin(), true), status::deleted());        
     }
 
+    //
+    // placeholder for trim function.
+    // 1. forward pass replaying propositional proof, populate trail stack.
+    // 2. backward pass to prune.
+    // 
+    svector<std::pair<clause&, status>> drat::trim() {
+        SASSERT(m_units.empty());
+        svector<std::pair<clause&, status>> proof;
+        for (auto const& [c, st] : m_proof)
+            if (!st.is_deleted())
+                proof.push_back({c,st});
+        return proof;
+    }
+
+
     void drat::check_model(model const& m) {
     }
 
@@ -1014,4 +986,56 @@ namespace sat {
     }
 #endif
 
+
+#if 0
+        if (!m_inconsistent) {
+            literal_vector lits(n, c);
+            IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
+            for (unsigned v = 0; v < m_assignment.size(); ++v) {
+                lbool val = m_assignment[v];
+                if (val != l_undef) {
+                    IF_VERBOSE(0, verbose_stream() << literal(v, false) << " |-> " << val << "\n");
+                }
+            }
+            for (clause* cp : s.m_clauses) {
+                clause& cl = *cp;
+                bool found = false;
+                for (literal l : cl) {
+                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
+                }
+            }
+            for (clause* cp : s.m_learned) {
+                clause& cl = *cp;
+                bool found = false;
+                for (literal l : cl) {
+                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
+                }
+            }
+            svector<sat::solver::bin_clause> bin;
+            s.collect_bin_clauses(bin, true);
+            for (auto& b : bin) {
+                bool found = false;
+                if (m_assignment[b.first.var()] != (b.first.sign() ? l_true : l_false)) found = true;
+                if (m_assignment[b.second.var()] != (b.second.sign() ? l_true : l_false)) found = true;
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Bin clause is false under assignment: " << b.first << " " << b.second << "\n");
+                }
+            }
+            IF_VERBOSE(0, s.display(verbose_stream()));
+            exit(0);
+        }
+#endif
+    
 }

src/sat/sat_drat.h

@@ -80,7 +80,7 @@ namespace sat {
         std::ostream*           m_out = nullptr;
         std::ostream*           m_bout = nullptr;
         svector<std::pair<clause&, status>> m_proof;
-        literal_vector          m_units;
+        svector<std::pair<literal, clause*>> m_units;
         vector<watch>           m_watches;
         svector<lbool>          m_assignment;
         vector<std::string>     m_theory;
@@ -172,9 +172,12 @@ namespace sat {
         void collect_statistics(statistics& st) const;
 
         bool inconsistent() const { return m_inconsistent; }
-        literal_vector const& units() { return m_units; }
+        svector<std::pair<literal, clause*>> const& units() { return m_units; }
         bool is_drup(unsigned n, literal const* c, literal_vector& units);
         solver& get_solver() { return s; }
+
+        svector<std::pair<clause&, status>> trim();
+        
     };
 
 }

src/sat/smt/array_internalize.cpp

@@ -247,6 +247,14 @@ namespace array {
         return false;
     }
 
+    bool solver::is_beta_redex(euf::enode* p, euf::enode* n) const {
+        if (a.is_select(p->get_expr()))
+            return p->get_arg(0)->get_root() == n->get_root();
+        if (a.is_map(p->get_expr()))
+            return true;
+        return false;
+    }
+
     func_decl_ref_vector const& solver::sort2diff(sort* s) {
         func_decl_ref_vector* result = nullptr;
         if (m_sort2diff.find(s, result))

src/sat/smt/array_solver.h

@@ -299,6 +299,7 @@ namespace array {
         euf::theory_var mk_var(euf::enode* n) override;
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override;
+        bool is_beta_redex(euf::enode* p, euf::enode* n) const override;
         bool enable_self_propagate() const override { return true; }
         void relevant_eh(euf::enode* n) override;
         bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_array(n->get_sort()); }

src/sat/smt/euf_internalize.cpp

@@ -358,6 +358,7 @@ namespace euf {
         for (auto const& p : euf::enode_th_vars(n)) {
             family_id id = p.get_id();
             if (m.get_basic_family_id() != id) {
+                
                 if (th_id != m.get_basic_family_id())
                     return true;
                 th_id = id;               
@@ -369,6 +370,8 @@ namespace euf {
         for (enode* parent : euf::enode_parents(n)) {
             app* p = to_app(parent->get_expr());
             family_id fid = p->get_family_id();
+            if (is_beta_redex(parent, n))
+                continue;
             if (fid != th_id && fid != m.get_basic_family_id())
                 return true;
         }
@@ -407,6 +410,13 @@ namespace euf {
         return false;
     }
 
+    bool solver::is_beta_redex(enode* p, enode* n) const {
+        for (auto const& th : enode_th_vars(p))
+            if (fid2solver(th.get_id())->is_beta_redex(p, n))
+                return true;
+        return false;
+    }
+
     expr_ref solver::mk_eq(expr* e1, expr* e2) {
         expr_ref _e1(e1, m);
         expr_ref _e2(e2, m);

src/sat/smt/euf_solver.h

@@ -371,6 +371,7 @@ namespace euf {
         th_rewriter& get_rewriter() { return m_rewriter; }
         void rewrite(expr_ref& e) { m_rewriter(e); }
         bool is_shared(euf::enode* n) const;
+        bool is_beta_redex(euf::enode* p, euf::enode* n) const;
         bool enable_ackerman_axioms(expr* n) const;
         bool is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain);
 

src/sat/smt/sat_th.h

@@ -127,6 +127,13 @@ namespace euf {
         */
         virtual bool is_shared(theory_var v) const { return false; }
 
+
+        /**
+           \brief Determine if argument n of parent p is a beta redex position
+         */
+
+        virtual bool is_beta_redex(euf::enode* p, euf::enode* n) const { return false; }
+
         sat::status status() const { return sat::status::th(m_is_redundant, get_id()); }
 
     };

src/shell/drat_frontend.cpp

@@ -77,11 +77,12 @@ class smt_checker {
         auto const& units = m_drat.units();
 #if 0
         for (unsigned i = m_units.size(); i < units.size(); ++i) {
-            sat::literal lit = units[i];            
+            sat::literal lit = units[i].first;            
             m_lemma_solver->assert_expr(lit2expr(lit));
         }
 #endif
-        m_units.append(units.size() - m_units.size(), units.data() + m_units.size());
+        for (unsigned i = m_units.size(); i < units.size(); ++i)
+            m_units.push_back(units[i].first);
     }
 
     void check_assertion_redundant(sat::literal_vector const& input) {