adding euf

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/ast.h

@@ -311,7 +311,7 @@ class sort_size {
     uint64_t m_size; // It is only meaningful if m_kind == SS_FINITE
     sort_size(kind_t k, uint64_t r):m_kind(k), m_size(r) {}
 public:
-    sort_size():m_kind(SS_INFINITE) {}
+    sort_size():m_kind(SS_INFINITE), m_size(0) {}
     sort_size(uint64_t const & sz):m_kind(SS_FINITE), m_size(sz) {}
     explicit sort_size(rational const& r) {
         if (r.is_uint64()) {

src/ast/euf/euf_egraph.cpp

@@ -203,7 +203,6 @@ namespace euf {
         SASSERT(m_num_scopes == 0 || m_worklist.empty());
         unsigned head = 0, tail = m_worklist.size();
         while (head < tail && m.limit().inc() && !inconsistent()) {
-            TRACE("euf", tout << "iterate: " << head << " " << tail << "\n";);
             for (unsigned i = head; i < tail && !inconsistent(); ++i) {
                 enode* n = m_worklist[i]->get_root();
                 if (!n->is_marked1()) {
@@ -349,7 +348,8 @@ namespace euf {
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
         out << std::setw(5)
             << n->get_owner_id() << " := ";
-        out << n->get_root()->get_owner_id() << " ";
+        if (!n->is_root()) 
+            out << "[" << n->get_root()->get_owner_id() << "] ";
         expr* f = n->get_owner();
         if (is_app(f))
             out << to_app(f)->get_decl()->get_name() << " ";
@@ -373,10 +373,8 @@ namespace euf {
         unsigned max_args = 0;
         for (enode* n : m_nodes)
             max_args = std::max(max_args, n->num_args());
-
-        for (enode* n : m_nodes) {
+        for (enode* n : m_nodes) 
             display(out, max_args, n);          
-        }
         return out;
     }
 
@@ -397,9 +395,8 @@ namespace euf {
             enode* n1 = src.m_nodes[i];
             expr* e1 = src.m_exprs[i];
             args.reset();
-            for (unsigned j = 0; j < n1->num_args(); ++j) {
+            for (unsigned j = 0; j < n1->num_args(); ++j) 
                 args.push_back(old_expr2new_enode[n1->get_arg(j)->get_owner_id()]);
-            }
             expr*  e2 = tr(e1);
             enode* n2 = mk(e2, args.size(), args.c_ptr());
             old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
@@ -412,9 +409,8 @@ namespace euf {
             SASSERT(!n1t || n2t);
             SASSERT(!n1t || src.m.get_sort(n1->get_owner()) == src.m.get_sort(n1t->get_owner()));
             SASSERT(!n1t || m.get_sort(n2->get_owner()) == m.get_sort(n2t->get_owner()));
-            if (n1t && n2->get_root() != n2t->get_root()) {
+            if (n1t && n2->get_root() != n2t->get_root()) 
                 merge(n2, n2t, n1->m_justification.copy(copy_justification));
-            }
         }
         propagate();
     }

src/sat/sat_ddfw.h

@@ -90,11 +90,11 @@ namespace sat {
         indexed_uint_set m_unsat;
         indexed_uint_set m_unsat_vars;  // set of variables that are in unsat clauses
         random_gen       m_rand;
-        unsigned         m_num_non_binary_clauses;
-        unsigned         m_restart_count, m_reinit_count, m_parsync_count;
-        uint64_t         m_restart_next,  m_reinit_next,  m_parsync_next;
-        uint64_t         m_flips, m_last_flips, m_shifts;
-        unsigned         m_min_sz;
+        unsigned         m_num_non_binary_clauses{ 0 };
+        unsigned         m_restart_count{ 0 }, m_reinit_count{ 0 }, m_parsync_count{ 0 };
+        uint64_t         m_restart_next{ 0 }, m_reinit_next{ 0 }, m_parsync_next{ 0 };
+        uint64_t         m_flips{ 0 }, m_last_flips{ 0 }, m_shifts{ 0 };
+        unsigned         m_min_sz{ 0 };
         hashtable<unsigned, unsigned_hash, default_eq<unsigned>> m_models;
         stopwatch        m_stopwatch;
 

src/sat/sat_drat.cpp

@@ -73,28 +73,48 @@ namespace sat {
         case drat::status::learned:  return out << "l";
         case drat::status::asserted: return out << "a";
         case drat::status::deleted:  return out << "d";
-        case drat::status::external: return out << "e";
+        case drat::status::ba:       return out << "c ba";
+        case drat::status::euf:      return out << "c euf";
         default: return out;
         }
     }
 
     void drat::dump(unsigned n, literal const* c, status st) {
-        if (st == status::asserted || st == status::external) {
+        if (st == status::asserted)
             return;
-        }
-        if (m_activity && ((m_num_add % 1000) == 0)) {
+        if (m_activity && ((m_num_add % 1000) == 0)) 
             dump_activity();
-        }
 
         char buffer[10000];
         char digits[20];     // enough for storing unsigned
         char* lastd = digits + sizeof(digits);
 
         unsigned len = 0;
-        if (st == status::deleted) {
+        switch (st) {
+        case status::deleted:
             buffer[0] = 'd';
             buffer[1] = ' ';
             len = 2;
+            break;
+        case status::euf:
+            buffer[0] = 'c';
+            buffer[1] = ' ';
+            buffer[2] = 'e';
+            buffer[3] = 'u';
+            buffer[4] = 'f';
+            buffer[5] = ' ';
+            len = 6;
+            break;
+        case status::ba:
+            buffer[0] = 'c';
+            buffer[1] = ' ';
+            buffer[2] = 'b';
+            buffer[3] = 'a';
+            buffer[4] = ' ';
+            len = 5;
+            break;
+        default:
+            break;
         }
         for (unsigned i = 0; i < n; ++i) {
             literal lit = c[i];
@@ -133,7 +153,8 @@ namespace sat {
         unsigned char ch = 0;
         switch (st) {
         case status::asserted: return;
-        case status::external: return; 
+        case status::ba: return; 
+        case status::euf: return; 
         case status::learned: ch = 'a'; break;
         case status::deleted: ch = 'd'; break;
         default: UNREACHABLE(); break;
@@ -237,6 +258,27 @@ namespace sat {
         }
     }
 
+    void drat::bool_def(bool_var v, unsigned n) {
+        if (m_out)
+            (*m_out) << "bool " << v << " := " << n << "\n";
+    }
+
+    void drat::def_begin(unsigned n, symbol const& name) {
+        if (m_out) 
+            (*m_out) << "def " << n << " := " << name;
+    }
+
+    void drat::def_add_arg(unsigned arg) {
+        if (m_out) 
+            (*m_out) << " " << arg;
+    }
+
+    void drat::def_end() {
+        if (m_out) 
+            (*m_out) << "\n";
+    }
+
+
 #if 0
     // debugging code
     bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status st2) {
@@ -439,7 +481,7 @@ namespace sat {
         SASSERT(lits.size() == n);
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             status st = m_status[i];
-            if (m_proof[i] && m_proof[i]->size() > 1 && (st == status::asserted || st == status::external)) {
+            if (m_proof[i] && m_proof[i]->size() > 1 && st == status::asserted) {
                 clause& c = *m_proof[i];
                 unsigned j = 0;
                 for (; j < c.size() && c[j] != ~l; ++j) {}
@@ -698,15 +740,15 @@ namespace sat {
             append(*cl, get_status(learned));
         }
     }
-    void drat::add(literal_vector const& lits, svector<premise> const& premises) {
+    void drat::add(literal_vector const& lits, status th) {
         ++m_num_add;
         if (m_check) {
             switch (lits.size()) {
             case 0: add(); break;
-            case 1: append(lits[0], status::external); break;
+            case 1: append(lits[0], th); break;
             default: {
                 clause* c = m_alloc.mk_clause(lits.size(), lits.c_ptr(), true);
-                append(*c, status::external);
+                append(*c, th);
                 break;
             }
             }
@@ -724,7 +766,7 @@ namespace sat {
             default: {
                 verify(c.size(), c.begin());
                 clause* cl = m_alloc.mk_clause(c.size(), c.c_ptr(), true);
-                append(*cl, status::external);                
+                append(*cl, status::ba);                
                 break;
             }
             }

src/sat/sat_drat.h

@@ -21,20 +21,8 @@ Module Name:
 namespace sat {
     class drat {
     public:
-        struct s_ext {};
-        struct s_unit {};
-        struct premise {
-            enum { t_clause, t_unit, t_ext } m_type;
-            union {
-                clause* m_clause;
-                unsigned m_literal;                
-            };
-            premise(s_ext, literal l): m_type(t_ext), m_literal(l.index()) {}
-            premise(s_unit, literal l): m_type(t_unit), m_literal(l.index()) {}
-            premise(clause* c): m_type(t_clause), m_clause(c) {}
-        };
+        enum status { asserted, learned, deleted, ba, euf };
     private:
-        enum status { asserted, learned, deleted, external };
         struct watched_clause {
             clause* m_clause;
             literal m_l1, m_l2;
@@ -91,9 +79,18 @@ namespace sat {
         void add(literal l, bool learned);
         void add(literal l1, literal l2, bool learned);
         void add(clause& c, bool learned);
-        void add(literal_vector const& c, svector<premise> const& premises);
+        void add(literal_vector const& c, status st);
         void add(literal_vector const& c); // add learned clause
 
+        // support for SMT - connect Boolean variables with AST nodes
+        // associate AST node id with Boolean variable v
+        void bool_def(bool_var v, unsigned n);
+
+        // declare AST node n with 'name' and arguments arg
+        void def_begin(unsigned n, symbol const& name);
+        void def_add_arg(unsigned arg);
+        void def_end();
+
         bool is_cleaned(clause& c) const;        
         void del(literal l);
         void del(literal l1, literal l2);

src/sat/sat_extension.h

@@ -45,6 +45,12 @@ namespace sat {
         ext_constraint_list & get(literal l) { return m_use_list[l.index()]; }
         ext_constraint_list const & get(literal l) const { return m_use_list[l.index()]; }
         void finalize() { m_use_list.finalize(); }
+        bool contains(bool_var v) const {
+            if (m_use_list.size() <= 2*v)
+                return false;
+            literal lit(v, false);
+            return !get(lit).empty() || !get(~lit).empty();
+        }
     };
 
     class extension {
@@ -53,7 +59,9 @@ namespace sat {
         virtual unsigned get_id() const { return 0; }
         virtual void set_solver(solver* s) = 0;
         virtual void set_lookahead(lookahead* s) = 0;
+        virtual void init_search() {}
         virtual bool propagate(literal l, ext_constraint_idx idx) = 0;
+        virtual bool is_external(bool_var v) = 0;
         virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0;
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
         virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) = 0;

src/sat/sat_lookahead.h

@@ -524,7 +524,7 @@ namespace sat {
         void update_lookahead_reward(literal l, unsigned level);
         bool dl_enabled(literal l) const { return m_lits[l.index()].m_double_lookahead != m_istamp_id; }
         void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; }
-        bool dl_no_overflow(unsigned base) const { return base + 2 * m_lookahead.size() * static_cast<uint64_t>(m_config.m_dl_max_iterations + 1) < c_fixed_truth; }
+        bool dl_no_overflow(unsigned base) const { return base + static_cast < uint64_t>(2 * m_lookahead.size()) * static_cast <uint64_t>(m_config.m_dl_max_iterations + 1) < c_fixed_truth; }
 
         unsigned do_double(literal l, unsigned& base);
         unsigned double_look(literal l, unsigned& base);

src/sat/sat_prob.h

@@ -59,7 +59,7 @@ namespace sat {
         clause_vector    m_clause_db;     
         svector<clause_info> m_clauses;
         bool_vector    m_values, m_best_values;
-        unsigned         m_best_min_unsat;
+        unsigned         m_best_min_unsat{ 0 };
         vector<unsigned_vector> m_use_list;
         unsigned_vector  m_flat_use_list;
         unsigned_vector  m_use_list_index;
@@ -68,9 +68,9 @@ namespace sat {
         indexed_uint_set m_unsat;
         random_gen       m_rand;
         unsigned_vector  m_breaks;
-        uint64_t         m_flips;
-        uint64_t         m_next_restart;
-        unsigned         m_restart_count;
+        uint64_t         m_flips{ 0 };
+        uint64_t         m_next_restart{ 0 };
+        unsigned         m_restart_count{ 0 };
         stopwatch        m_stopwatch;
         model            m_model;
 

src/sat/sat_simplifier.cpp

@@ -76,12 +76,17 @@ namespace sat {
     watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); }
 
     bool simplifier::is_external(bool_var v) const { 
-        return 
-            s.is_assumption(v) ||
-            (s.is_external(v) && s.is_incremental()) ||
-            (s.is_external(v) && s.m_ext &&
-             (!m_ext_use_list.get(literal(v, false)).empty() ||
-              !m_ext_use_list.get(literal(v, true)).empty()));
+        if (!s.is_external(v))
+            return s.is_assumption(v);
+        if (s.is_incremental())
+            return true;
+        if (!s.m_ext)
+            return false;
+        if (s.m_ext->is_external(v))
+            return true;
+        if (m_ext_use_list.contains(v))
+            return true;
+        return false;
     }
 
     inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); }

src/sat/sat_solver.cpp

@@ -1843,6 +1843,8 @@ namespace sat {
         m_min_core.reset();
         m_simplifier.init_search();
         m_mc.init_search(*this);
+        if (m_ext)
+            m_ext->init_search();
         TRACE("sat", display(tout););
     }
 
@@ -2983,16 +2985,15 @@ namespace sat {
             level = update_max_level(js.get_literal2(), level, unique_max);
             return level;
         case justification::CLAUSE: 
-            for (literal l : get_clause(js)) {
+            for (literal l : get_clause(js)) 
                 level = update_max_level(l, level, unique_max);
-            }
             return level;
-        case justification::EXT_JUSTIFICATION: 
-            SASSERT(not_l != null_literal);
-            fill_ext_antecedents(~not_l, js);
-            for (literal l : m_ext_antecedents) {
+        case justification::EXT_JUSTIFICATION:
+            if (not_l != null_literal) 
+                not_l.neg();
+            fill_ext_antecedents(not_l, js);
+            for (literal l : m_ext_antecedents) 
                 level = update_max_level(l, level, unique_max);
-            }
             return level;
         default:
             UNREACHABLE();

src/sat/sat_solver.h

@@ -397,6 +397,7 @@ namespace sat {
         void set_par(parallel* p, unsigned id);
         bool canceled() { return !m_rlimit.inc(); }
         config const& get_config() const { return m_config; }
+        drat& get_drat() { return m_drat; }
         void set_incremental(bool b) { m_config.m_incremental = b; }
         bool is_incremental() const { return m_config.m_incremental; }
         extension* get_extension() const override { return m_ext.get(); }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -973,6 +973,7 @@ class inc_sat_solver : public solver {
         if (m_sat_mc) {
             (*m_sat_mc)(mdl);
         }
+        m_goal2sat.update_model(mdl);
         if (m_mcs.back()) {      
             TRACE("sat", m_mcs.back()->display(tout););
             (*m_mcs.back())(mdl);

src/sat/smt/CMakeLists.txt

@@ -1,13 +1,14 @@
 z3_add_component(sat_smt
   SOURCES
     atom2bool_var.cpp
+    ba_internalize.cpp
     ba_solver.cpp
     xor_solver.cpp
-    ba_internalize.cpp
     euf_ackerman.cpp
     euf_internalize.cpp
-    euf_solver.cpp
     euf_model.cpp
+    euf_proof.cpp
+    euf_solver.cpp
   COMPONENT_DEPENDENCIES
     sat
     ast