wip - trim

src/cmd_context/extra_cmds/proof_cmds.cpp

@@ -189,8 +189,10 @@ class proof_trim {
     cmd_context& ctx;
     ast_manager& m;
     sat::proof_trim trim;
+    euf::proof_checker m_checker;
     vector<expr_ref_vector> m_clauses;
     bool_vector             m_is_infer;
+    symbol                  m_rup;
     
     void mk_clause(expr_ref_vector const& clause) {
         trim.init_clause();
@@ -208,12 +210,18 @@ class proof_trim {
         bool sign = m.is_not(arg, arg);
         trim.add_literal(mk_var(arg), sign);
     }
+
+    bool is_rup(expr* hint) const {
+        return hint && is_app(hint) && to_app(hint)->get_decl()->get_name() == m_rup;
+    }
       
 public:
     proof_trim(cmd_context& ctx):
         ctx(ctx),
         m(ctx.m()),
-        trim(gparams::get_module("sat"), m.limit()) {            
+        trim(gparams::get_module("sat"), m.limit()),
+        m_checker(m) {
+        m_rup = symbol("rup");
     }
     
     void assume(expr_ref_vector const& clause) {
@@ -227,14 +235,52 @@ public:
         mk_clause(_clause);
         trim.del();
     }
+
+    /**
+     * Theory axioms are treated as assumptions.
+     * Some literals in the theory axioms may have been removed
+     * because they are false at base level. To reconstruct this
+     * dependency rely on the proof_checker to produce the original
+     * clauses. Thus, trim isn't correct for theory axioms that don't
+     * have a way to return clauses.
+     * The clauses can be retrieved directly from the justification
+     * that is used internally, so adding clause retrieval for every
+     * theory axiom is possible even if there are no checkers.
+     * In this case, the proof_checker::check dependency should not
+     * be used.
+     */
     
     void infer(expr_ref_vector const& clause, app* hint) {
+        if (hint && !is_rup(hint) && m_checker.check(hint)) {
+            auto clause1 = m_checker.clause(hint);
+            if (clause1.size() != clause.size()) {
+                mk_clause(clause1);
+                trim.assume(m_clauses.size());
+                clause1.push_back(hint);
+                m_clauses.push_back(clause1);                
+                m_is_infer.push_back(false);
+                mk_clause(clause);
+                trim.infer(m_clauses.size());
+                m_clauses.push_back(clause);
+                m_clauses.back().push_back(hint);
+                m_is_infer.push_back(true);
+                if (clause.empty()) 
+                    do_trim(std::cout);
+                return;
+            }
+        }
+
         mk_clause(clause);
-        trim.infer(m_clauses.size());
+        if (is_rup(hint))
+            trim.infer(m_clauses.size());
+        else
+            trim.assume(m_clauses.size());
         m_clauses.push_back(clause);
         if (hint)
             m_clauses.back().push_back(hint);
-        m_is_infer.push_back(true);
+        m_is_infer.push_back(is_rup(hint));
+        if (clause.empty()) 
+            do_trim(std::cout);
     }
     
     void updt_params(params_ref const& p) {
@@ -254,7 +300,7 @@ public:
                 pp.define_expr(out, e);
 
             if (!is_infer)
-                out << "(assume ";
+                out << "(assume";
             else
                 out << "(infer";
             for (expr* e : clause) 

src/sat/sat_proof_trim.cpp

@@ -40,7 +40,10 @@ namespace sat {
                 revive(cl, clp);
                 continue;
             }
+            IF_VERBOSE(0, s.display(verbose_stream()));
             prune_trail(cl, clp);
+            IF_VERBOSE(0, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} ");
+            IF_VERBOSE(0, s.display(verbose_stream() << "\n"));
             del(cl, clp);
             if (!in_core(cl, clp))
                 continue;
@@ -88,6 +91,9 @@ namespace sat {
         m_in_clause.reset();
         m_in_coi.reset();
         
+        if (cl.empty())
+            return;
+
         for (literal lit : cl) 
             m_in_clause.insert(lit.index());
 
@@ -130,6 +136,9 @@ namespace sat {
                 s.m_trail[j++] = s.m_trail[i];
         }            
         s.m_trail.shrink(j);
+        s.m_inconsistent = false; 
+        s.m_qhead = s.m_trail.size();
+        s.propagate(false);
     }
 
 
@@ -160,24 +169,38 @@ namespace sat {
        
     */
     void proof_trim::conflict_analysis_core(literal_vector const& cl, clause* cp) {
-
+        IF_VERBOSE(3, verbose_stream() << "core " << cl << "\n");
+        
+        if (cl.empty()) {
+            add_core(~s.m_not_l, s.m_conflict);
+            add_core(s.m_not_l, s.get_justification(s.m_not_l));
+            return;
+        }
+        SASSERT(!s.inconsistent());
         s.push();
         unsigned lvl = s.scope_lvl();
         for (auto lit : cl)
             s.assign(~lit, justification(lvl));
         unsigned trail_size0 = s.m_trail.size();
-        s.push();
         s.propagate(false);
         if (!s.inconsistent()) {
             s.m_qhead = 0;
             s.propagate(false);
         }
+        if (!s.inconsistent())
+            IF_VERBOSE(0, s.display(verbose_stream()));
+        
         SASSERT(s.inconsistent());
         for (unsigned i = trail_size0; i < s.m_trail.size(); ++i)
             m_propagated[s.m_trail[i].var()] = true;
 
-        if (s.m_not_l != null_literal)
+        SASSERT(s.inconsistent());
+        IF_VERBOSE(3, verbose_stream() << s.m_not_l << " " << s.m_conflict << "\n");
+        if (s.m_not_l != null_literal) {
+            if (s.lvl(s.m_not_l) == 0)
+                add_core(~s.m_not_l, s.m_conflict);
             add_dependency(s.m_not_l);
+        }
         add_dependency(s.m_conflict);
         
         for (unsigned i = s.m_trail.size(); i-- > trail_size0; ) {
@@ -188,7 +211,7 @@ namespace sat {
             s.reset_mark(v);
             add_dependency(s.get_justification(v));
         }
-        s.pop(2);                
+        s.pop(1);                
     }
 
     void proof_trim::add_dependency(literal lit) {
@@ -230,7 +253,8 @@ namespace sat {
         m_clause.reset();
         switch (j.get_kind()) {
         case justification::NONE:
-            return;                
+            m_clause.push_back(l);
+            break;                
         case justification::BINARY:
             m_clause.push_back(l);
             m_clause.push_back(j.get_literal());
@@ -242,12 +266,14 @@ namespace sat {
             break;
         case justification::CLAUSE:
             s.get_clause(j).mark_used();
+            IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n");
             return;
         default:
             UNREACHABLE();
             break;
         }
         std::sort(m_clause.begin(), m_clause.end());
+        IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n");
         m_core_literals.insert(m_clause);
     }
 
@@ -268,7 +294,7 @@ namespace sat {
     clause* proof_trim::del(literal_vector const& cl) {
         clause* cp = nullptr;
         IF_VERBOSE(3, verbose_stream() << "del: " << cl << "\n");
-        if (m_clause.size() == 2) {
+        if (cl.size() == 2) {
             s.detach_bin_clause(cl[0], cl[1], true);
             return cp;
         }
@@ -294,12 +320,13 @@ namespace sat {
     }    
 
     proof_trim::proof_trim(params_ref const& p, reslimit& lim):
-        s(p, lim)
+        s(p, lim) {
-    {}
+        s.set_trim();
+    }
 
     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");
+        IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n");
         auto* cl = s.mk_clause(m_clause, status::redundant());
         m_trail.push_back({ id, m_clause, cl, true, is_initial });
         s.propagate(false);

src/sat/sat_solver.cpp

@@ -416,7 +416,7 @@ namespace sat {
         bool logged = false;
         if (!redundant || !st.is_sat()) {
             unsigned old_sz = num_lits;
-            bool keep = simplify_clause(num_lits, lits);
+            bool keep = m_trim || simplify_clause(num_lits, lits);
             TRACE("sat_mk_clause", tout << "mk_clause (after simp), keep: " << keep << "\n" << mk_lits_pp(num_lits, lits) << "\n";);
             if (!keep) {
                 return nullptr; // clause is equivalent to true.
@@ -461,16 +461,16 @@ namespace sat {
         m_touched[l1.var()] = m_touch_index;
         m_touched[l2.var()] = m_touch_index;
         
-        if (redundant && find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) {
+        if (redundant && !m_trim && find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) {
             assign_unit(l1);
             return;
         }
-        if (redundant && find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) {
+        if (redundant && !m_trim && find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) {
             assign_unit(l2);
             return;
         }
         watched* w0 = redundant ? find_binary_watch(get_wlist(~l1), l2) : nullptr;
-        if (w0) {
+        if (w0 && !m_trim) {
             TRACE("sat", tout << "found binary " << l1 << " " << l2 << "\n";);
             if (w0->is_learned() && !redundant) {
                 w0->set_learned(false);
@@ -487,9 +487,10 @@ namespace sat {
         if (m_config.m_drat) 
             m_drat.add(l1, l2, st);
         if (propagate_bin_clause(l1, l2)) {
-            if (at_base_lvl())
+            if (!at_base_lvl())
+                push_reinit_stack(l1, l2);
+            else if (!m_trim)
                 return;
-            push_reinit_stack(l1, l2);
         }
         else if (has_variables_to_reinit(l1, l2))
             push_reinit_stack(l1, l2);
@@ -950,7 +951,8 @@ namespace sat {
         if (j.level() == 0) {
             if (m_config.m_drat) 
                 drat_log_unit(l, j);
-            j = justification(0); // erase justification for level 0
+            if (!m_trim)
+                j = justification(0); // erase justification for level 0
         }
         else {
             VERIFY(!at_base_lvl());

src/sat/sat_solver.h

@@ -174,6 +174,7 @@ namespace sat {
         literal_vector          m_trail;
         clause_wrapper_vector   m_clauses_to_reinit;
         std::string             m_reason_unknown;
+        bool                    m_trim = false;
 
         svector<unsigned>       m_visited;
         unsigned                m_visited_ts;
@@ -203,7 +204,7 @@ namespace sat {
         class lookahead*        m_cuber;
         class i_local_search*   m_local_search;
 
-        statistics              m_aux_stats;
+        statistics              m_aux_stats;        
 
         void del_clauses(clause_vector& clauses);
 
@@ -283,6 +284,8 @@ namespace sat {
 
         random_gen& rand() { return m_rand; }
 
+        void set_trim() { m_trim = true; }
+
     protected:
         void reset_var(bool_var v, bool ext, bool dvar);
 
@@ -399,7 +402,7 @@ namespace sat {
             }
         }
         void update_assign(literal l, justification j) {
-            if (j.level() == 0) 
+            if (j.level() == 0 && !m_trim) 
                 m_justification[l.var()] = j;
         }
         void assign_unit(literal l) { assign(l, justification(0)); }

src/smt/theory_user_propagator.cpp

@@ -323,10 +323,12 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
         ctx.set_conflict(js);
     }
     else {
+#if 1
         for (auto& lit : m_lits)
             lit.neg();
         for (auto const& [a,b] : m_eqs)
             m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
+#endif
         
         literal lit; 
         if (has_quantifiers(prop.m_conseq)) {
@@ -339,8 +341,20 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
         else 
             lit = mk_literal(prop.m_conseq);            
         ctx.mark_as_relevant(lit);
+
+#if 0
+        justification* js =
+            ctx.mk_justification(
+                ext_theory_propagation_justification(
+                    get_id(), ctx, m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), lit));
+
+        ctx.assign(lit, js);
+#endif
+        
+#if 1           
         m_lits.push_back(lit);
         ctx.mk_th_lemma(get_id(), m_lits);
+#endif
         TRACE("user_propagate", ctx.display(tout););
     }
 }