elaborate on smt/drat format outline, expose euf mode as config

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

src/sat/sat_config.cpp

@@ -248,8 +248,10 @@ namespace sat {
         sat_simplifier_params sp(_p);
         m_elim_vars = sp.elim_vars();
 
+#if 0
         if (m_drat && (m_xor_solver || m_card_solver)) 
             throw sat_param_exception("DRAT checking only works for pure CNF");
+#endif
     }
 
     void config::collect_param_descrs(param_descrs & r) {

src/sat/sat_drat.cpp

@@ -71,8 +71,8 @@ namespace sat {
     std::ostream& operator<<(std::ostream& out, drat::status st) {
         switch (st) {
         case drat::status::learned:  return out << "l";
-        case drat::status::asserted: return out << "a";
         case drat::status::deleted:  return out << "d";
+        case drat::status::asserted: return out << "c a";
         case drat::status::ba:       return out << "c ba";
         case drat::status::euf:      return out << "c euf";
         default: return out;
@@ -80,7 +80,7 @@ namespace sat {
     }
 
     void drat::dump(unsigned n, literal const* c, status st) {
-        if (st == status::asserted)
+        if (st == status::asserted && !s.m_ext)
             return;
         if (m_activity && ((m_num_add % 1000) == 0)) 
             dump_activity();
@@ -91,6 +91,13 @@ namespace sat {
         
         unsigned len = 0;
         switch (st) {
+        case status::asserted:
+            buffer[0] = 'c';
+            buffer[1] = ' ';
+            buffer[2] = 'a';
+            buffer[3] = ' ';
+            len = 4;
+            break;
         case status::deleted:
             buffer[0] = 'd';
             buffer[1] = ' ';
@@ -121,6 +128,7 @@ namespace sat {
             unsigned v = lit.var();            
             if (lit.sign()) buffer[len++] = '-';
             char* d = lastd;
+            SASSERT(v > 0);
             while (v > 0) {                
                 d--;
                 *d = (v % 10) + '0';
@@ -260,12 +268,12 @@ namespace sat {
 
     void drat::bool_def(bool_var v, unsigned n) {
         if (m_out)
-            (*m_out) << "bool " << v << " := " << n << "\n";
+            (*m_out) << "c b " << v << " := " << n << " 0\n";
     }
 
     void drat::def_begin(unsigned n, symbol const& name) {
         if (m_out) 
-            (*m_out) << "def " << n << " := " << name;
+            (*m_out) << "c n " << n << " := " << name;
     }
 
     void drat::def_add_arg(unsigned arg) {
@@ -275,7 +283,12 @@ namespace sat {
 
     void drat::def_end() {
         if (m_out) 
-            (*m_out) << "\n";
+            (*m_out) << " 0\n";
+    }
+
+    void drat::log_adhoc(std::function<void(std::ostream&)>& fn) {
+        if (m_out)
+            fn(*m_out);
     }
 
 
@@ -506,7 +519,7 @@ namespace sat {
         } 
         if (!is_drup(n, c) && !is_drat(n, c)) {
             literal_vector lits(n, c);
-            std::cout << "Verification of " << lits << " failed\n";
+            IF_VERBOSE(0, verbose_stream() << "Verification of " << lits << " failed\n");
             // s.display(std::cout);
             std::string line;
             std::getline(std::cin, line);                
@@ -753,6 +766,8 @@ namespace sat {
             }
             }
         }              
+        if (m_out) 
+            dump(lits.size(), lits.c_ptr(), th);
     }
     void drat::add(literal_vector const& c) {
         ++m_num_add;

src/sat/sat_drat.h

@@ -15,6 +15,29 @@ Author:
 
 Notes:
 
+    For DIMACS input it produces DRAT proofs.
+
+    For SMT extensions are as follows:
+
+    Input assertion (trusted modulo internalizer):
+      c a <literal>* 0
+
+    Bridge from ast-node to boolean variable:
+      c b <bool-var-id> := <ast-node-id> 0
+
+    Definition of an ast node:
+      c n <ast-node-id> := <name> <ast-node-id>* 0
+
+    Theory lemma
+      c <theory-id> <literal>* 0
+
+    Available theories are:
+      - euf   The theory lemma should be a consequence of congruence closure.
+      - ba    TBD (need to also log cardinality and pb constraints)
+
+    Life times of theory lemmas is TBD. When they are used for conflict resolution
+    they are only used for the next lemma.
+
 --*/
 #pragma once
 
@@ -91,6 +114,9 @@ namespace sat {
         void def_add_arg(unsigned arg);
         void def_end();
 
+        // ad-hoc logging until a format is developed
+        void log_adhoc(std::function<void(std::ostream&)>& fn);
+
         bool is_cleaned(clause& c) const;        
         void del(literal l);
         void del(literal l1, literal l2);

src/sat/sat_justification.h

@@ -54,6 +54,7 @@ namespace sat {
         
         bool is_ext_justification() const { return m_val2 == EXT_JUSTIFICATION; }
         ext_justification_idx get_ext_justification_idx() const { return m_val1; }
+
     };
 
     inline std::ostream & operator<<(std::ostream & out, justification const & j) {
@@ -77,5 +78,6 @@ namespace sat {
         out << " @" << j.level();
         return out;
     }
+
 };
 

src/sat/sat_params.pyg

@@ -57,7 +57,7 @@ def_module_params('sat',
                           ('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
                           ('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
                           ('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),
-                          ('euf', BOOL, False, 'enable euf solver'),
+                          ('euf', BOOL, False, 'enable euf solver (this feature is preliminary and not ready for general consumption)'),
                           ('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'),
                           ('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'),
                           ('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'),

src/sat/sat_solver.cpp

@@ -86,6 +86,7 @@ namespace sat {
         m_cuber                   = nullptr;
         m_local_search            = nullptr;
         m_mc.set_solver(this);
+        mk_var(false, false);  // reserve var 0 to internal.
     }
 
     solver::~solver() {
@@ -2603,6 +2604,13 @@ namespace sat {
         if (m_step_size > m_config.m_step_size_min) {
             m_step_size -= m_config.m_step_size_dec;
         }
+        struct reset_cache {
+            solver& s;
+            bool active;
+            reset_cache(solver& s) :s(s), active(true) {}
+            ~reset_cache() { if (active) s.m_cached_antecedent_js = 0; }
+        };
+        reset_cache _reset(*this);
         bool unique_max;
         m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);        
         justification js = m_conflict;
@@ -2614,6 +2622,8 @@ namespace sat {
         }
 
         if (m_conflict_lvl == 0) {
+            if (m_config.m_drat && m_ext) 
+                resolve_conflict_for_unsat_core();                
             TRACE("sat", tout << "conflict level is 0\n";);
             return l_false;
         }
@@ -2627,6 +2637,7 @@ namespace sat {
             pop_reinit(m_scope_lvl - m_conflict_lvl + 1);
             m_force_conflict_analysis = true;
             ++m_stats.m_backtracks;
+            _reset.active = false;
             return l_undef;
         }
         m_force_conflict_analysis = false;
@@ -2737,6 +2748,7 @@ namespace sat {
 
         m_lemma[0] = ~consequent;
         learn_lemma_and_backjump();
+
         return l_undef;
     }
 
@@ -3050,8 +3062,13 @@ namespace sat {
     void solver::fill_ext_antecedents(literal consequent, justification js) {
         SASSERT(js.is_ext_justification());
         SASSERT(m_ext);
+        auto idx = js.get_ext_justification_idx();
+        if (consequent == m_cached_antecedent_consequent && idx == m_cached_antecedent_js)
+            return;
         m_ext_antecedents.reset();
-        m_ext->get_antecedents(consequent, js.get_ext_justification_idx(), m_ext_antecedents);
+        m_ext->get_antecedents(consequent, idx, m_ext_antecedents);
+        m_cached_antecedent_consequent = consequent;
+        m_cached_antecedent_js = idx;
     }
 
     bool solver::is_two_phase() const {

src/sat/sat_solver.h

@@ -565,6 +565,8 @@ namespace sat {
         unsigned       m_conflict_lvl;
         literal_vector m_lemma;
         literal_vector m_ext_antecedents;
+        literal        m_cached_antecedent_consequent;
+        ext_justification_idx m_cached_antecedent_js { 0 };
         bool use_backjumping(unsigned num_scopes);
         bool resolve_conflict();
         lbool resolve_conflict_core();

src/sat/smt/ba_solver.cpp

@@ -1783,6 +1783,12 @@ namespace sat {
             watch_literal(~lit, *c);
         }        
         SASSERT(c->well_formed());
+        if (m_solver && m_solver->get_config().m_drat) {
+            std::function<void(std::ostream& out)> fn = [&](std::ostream& out) {
+                out << "c ba constraint " << *c << " 0\n";
+            };
+            m_solver->get_drat().log_adhoc(fn);
+        }
     }
 
 

src/sat/smt/euf_solver.cpp

@@ -26,7 +26,7 @@ namespace euf {
 
     void solver::updt_params(params_ref const& p) {
         m_config.updt_params(p);
-        m_drat = s().get_config().m_drat;
+        m_drat = m_solver && m_solver->get_config().m_drat;
     }
 
     /**
@@ -98,7 +98,6 @@ namespace euf {
     }
 
     bool solver::propagate(literal l, ext_constraint_idx idx) { 
-        force_push();
         auto* ext = sat::constraint_base::to_extension(idx);
         SASSERT(ext != this);
         return ext->propagate(l, idx);
@@ -225,7 +224,6 @@ namespace euf {
     }
 
     sat::check_result solver::check() { 
-        force_push();
         bool give_up = false;
         bool cont = false;
         for (auto* e : m_solvers)
@@ -358,7 +356,6 @@ namespace euf {
     }
 
     void solver::pop_reinit() {
-        force_push();
         for (auto* e : m_solvers)
             e->pop_reinit();
     }

src/sat/smt/euf_solver.h

@@ -176,7 +176,7 @@ namespace euf {
        };
 
         void updt_params(params_ref const& p);
-        void set_solver(sat::solver* s) override { m_solver = s; }
+        void set_solver(sat::solver* s) override { m_solver = s; m_drat = s->get_config().m_drat; }
         void set_lookahead(sat::lookahead* s) override { m_lookahead = s; }
         void init_search() override;
         double get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;

src/sat/tactic/goal2sat.cpp

@@ -33,14 +33,15 @@ Notes:
 #include "ast/pb_decl_plugin.h"
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
-#include "sat/tactic/goal2sat.h"
-#include "sat/sat_cut_simplifier.h"
-#include "sat/smt/ba_solver.h"
-#include "sat/smt/euf_solver.h"
 #include "model/model_evaluator.h"
 #include "model/model_v2_pp.h"
 #include "tactic/tactic.h"
 #include "tactic/generic_model_converter.h"
+#include "sat/sat_cut_simplifier.h"
+#include "sat/tactic/goal2sat.h"
+#include "sat/smt/ba_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/sat_params.hpp"
 #include<sstream>
 
 struct goal2sat::imp : public sat::sat_internalizer {
@@ -91,10 +92,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
     ~imp() override {}
         
     void updt_params(params_ref const & p) {
+        sat_params sp(p);
         m_ite_extra  = p.get_bool("ite_extra", true);
         m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
         m_xor_solver = p.get_bool("xor_solver", false);
-        m_euf = false;
+        m_euf = sp.euf();
     }
 
     void throw_op_not_handled(std::string const& s) {