running updates to bv_solver (#4674)

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* na

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

* dbg

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

* bv

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

* drat and fresh

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

* move ackerman functionality

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

* na

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

* debugability

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

* towards debugability

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

* missing file

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

* na

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

* na

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

* remove csp

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

src/sat/dimacs.cpp

@@ -20,43 +20,21 @@ Revision History:
 #undef max
 #undef min
 #include "sat/sat_solver.h"
-
-namespace {
-struct lex_error {};
-
-class stream_buffer {
-    std::istream & m_stream;
-    int            m_val;
-    unsigned       m_line;
-public:
-    
-    stream_buffer(std::istream & s):
-        m_stream(s),
-        m_line(0) {
-        m_val = m_stream.get();
-    }
-
-    int  operator *() const { 
-        return m_val;
-    }
-
-    void operator ++() { 
-        m_val = m_stream.get();
-        if (m_val == '\n') ++m_line;
-    }
-
-    unsigned line() const { return m_line; }
-};
+#include "sat/sat_drat.h"
 
 template<typename Buffer>
-void skip_whitespace(Buffer & in) {
-    while ((*in >= 9 && *in <= 13) || *in == 32) {
-        ++in; 
-    }
+static bool is_whitespace(Buffer & in) {
+    return (*in >= 9 && *in <= 13) || *in == 32;
 }
 
 template<typename Buffer>
-void skip_line(Buffer & in) {
+static void skip_whitespace(Buffer & in) {
+    while (is_whitespace(in))
+        ++in; 
+}
+
+template<typename Buffer>
+static void skip_line(Buffer & in) {
     while(true) {
         if (*in == EOF) {
             return;
@@ -70,7 +48,7 @@ void skip_line(Buffer & in) {
 }
 
 template<typename Buffer>
-int parse_int(Buffer & in, std::ostream& err) {
+static int parse_int(Buffer & in, std::ostream& err) {
     int     val = 0;
     bool    neg = false;
     skip_whitespace(in);
@@ -84,8 +62,11 @@ int parse_int(Buffer & in, std::ostream& err) {
     }
 
     if (*in < '0' || *in > '9') {
-        err << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n";
-        throw lex_error();
+        if (20 <= *in && *in < 128) 
+            err << "(error, \"unexpected char: " << ((char)*in) << " line: " << in.line() << "\")\n";
+        else
+            err << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n";
+        throw dimacs::lex_error();
     }
 
     while (*in >= '0' && *in <= '9') {
@@ -97,7 +78,7 @@ int parse_int(Buffer & in, std::ostream& err) {
 }
 
 template<typename Buffer>
-void read_clause(Buffer & in, std::ostream& err, sat::solver & solver, sat::literal_vector & lits) {
+static void read_clause(Buffer & in, std::ostream& err, sat::solver & solver, sat::literal_vector & lits) {
     int     parsed_lit;
     int     var;
     
@@ -116,7 +97,24 @@ void read_clause(Buffer & in, std::ostream& err, sat::solver & solver, sat::lite
 }
 
 template<typename Buffer>
-bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solver) {
+static void read_clause(Buffer & in, std::ostream& err, sat::literal_vector & lits) {
+    int     parsed_lit;
+    int     var;
+    
+    lits.reset();
+
+    while (true) { 
+        parsed_lit = parse_int(in, err);
+        if (parsed_lit == 0)
+            break;
+        var = abs(parsed_lit);
+        SASSERT(var > 0);
+        lits.push_back(sat::literal(var, parsed_lit < 0));
+    }
+}
+
+template<typename Buffer>
+static bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solver) {
     sat::literal_vector lits;
     try {
         while (true) {
@@ -133,15 +131,158 @@ bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solver) {
             }
         }
     }
-    catch (lex_error) {
+    catch (dimacs::lex_error) {
         return false;
     }
     return true;
 }
 
-}
 
 bool parse_dimacs(std::istream & in, std::ostream& err, sat::solver & solver) {
-    stream_buffer _in(in);
+    dimacs::stream_buffer _in(in);
     return parse_dimacs_core(_in, err, solver);
 }
+
+
+namespace dimacs {
+
+    std::ostream& operator<<(std::ostream& out, drat_record const& r) {
+        switch (r.m_tag) {
+        case drat_record::tag_t::is_clause:
+            return out << r.m_status << " " << r.m_lits << "\n";
+        case drat_record::tag_t::is_node:
+            return out << "e " << r.m_node_id << " " << r.m_name << " " << r.m_args << "\n"; 
+        case drat_record::is_bool_def:
+            return out << "b " << r.m_node_id << " " << r.m_args << "\n";
+        }
+        return out;
+    }
+
+    char const* drat_parser::parse_identifier() {
+        m_buffer.reset();
+        while (!is_whitespace(in)) {
+            m_buffer.push_back(*in);
+            ++in;
+        }
+        m_buffer.push_back(0);
+        return m_buffer.c_ptr();
+    }
+
+    char const* drat_parser::parse_sexpr() {
+        m_buffer.reset();
+        unsigned lp = 0;
+        while (!is_whitespace(in) || lp > 0) {
+            m_buffer.push_back(*in);
+            if (*in == '(') 
+                ++lp;
+            else if (*in == ')') {
+                if (lp == 0) { 
+                    throw lex_error(); 
+                } 
+                else --lp;
+            }
+            ++in;
+        }
+        m_buffer.push_back(0);
+        return m_buffer.c_ptr();        
+    }
+
+    int drat_parser::read_theory_id() {
+        skip_whitespace(in);
+        if ('a' <= *in && *in <= 'z') {
+            if (!m_read_theory_id)
+                throw lex_error();
+            return m_read_theory_id(parse_identifier());
+        }
+        else {
+            return -1;
+        }
+    }
+
+    bool drat_parser::next() {
+        int n, b, e, theory_id;
+        try {
+        loop:
+            skip_whitespace(in);
+            switch (*in) {
+            case EOF:
+                return false;
+            case 'c':
+            case 'p':
+                skip_line(in);
+                goto loop;
+            case 'i':
+                ++in;
+                skip_whitespace(in);
+                read_clause(in, err, m_record.m_lits);
+                m_record.m_tag = drat_record::tag_t::is_clause;
+                m_record.m_status = sat::status::input();
+                break;
+            case 'a':
+                ++in;
+                skip_whitespace(in);
+                theory_id = read_theory_id();
+                skip_whitespace(in);
+                read_clause(in, err, m_record.m_lits);
+                m_record.m_tag = drat_record::tag_t::is_clause;
+                m_record.m_status = sat::status::th(false, theory_id);
+                break;
+            case 'e':
+                ++in;
+                skip_whitespace(in);
+                n = parse_int(in, err);                    
+                skip_whitespace(in);
+                m_record.m_name = parse_sexpr();
+                m_record.m_tag = drat_record::tag_t::is_node;
+                m_record.m_node_id = n;
+                m_record.m_args.reset();
+                while (true) {
+                    n = parse_int(in, err);
+                    if (n == 0)
+                        break;
+                    if (n < 0)
+                        throw lex_error();
+                    m_record.m_args.push_back(n);
+                }
+                break;
+            case 'b':
+                ++in;
+                skip_whitespace(in);
+                b = parse_int(in, err);
+                n = parse_int(in, err);
+                e = parse_int(in, err);
+                if (e != 0)
+                    throw lex_error();
+                m_record.m_tag = drat_record::tag_t::is_bool_def;
+                m_record.m_node_id = b;
+                m_record.m_args.reset();
+                m_record.m_args.push_back(n);
+                break;
+            case 'd':
+                ++in;
+                skip_whitespace(in);
+                read_clause(in, err, m_record.m_lits);
+                m_record.m_tag = drat_record::tag_t::is_clause;
+                m_record.m_status = sat::status::deleted();
+                break;
+            case 'r':
+                ++in;
+                skip_whitespace(in);
+                theory_id = read_theory_id();
+                read_clause(in, err, m_record.m_lits);
+                m_record.m_tag = drat_record::tag_t::is_clause;
+                m_record.m_status = sat::status::th(true, theory_id);
+                break;
+            default:
+                read_clause(in, err, m_record.m_lits);
+                m_record.m_tag = drat_record::tag_t::is_clause;
+                m_record.m_status = sat::status::redundant();
+                break;                
+            }    
+            return true;
+        }
+        catch (lex_error) {
+            return false;
+        }
+    }
+}

src/sat/dimacs.h

@@ -15,6 +15,9 @@ Author:
 
 Revision History:
 
+    Nikolaj Bjorner (nbjorner) 2020-09-07
+    Add parser to consume extended DRAT format.
+
 --*/
 #pragma once
 
@@ -22,4 +25,87 @@ Revision History:
 
 bool parse_dimacs(std::istream & s, std::ostream& err, sat::solver & solver);
 
+namespace dimacs {
+    struct lex_error {};
+
+    class stream_buffer {
+        std::istream & m_stream;
+        int            m_val;
+        unsigned       m_line;
+    public:
+        
+    stream_buffer(std::istream & s):
+        m_stream(s),
+            m_line(0) {
+            m_val = m_stream.get();
+        }
+        
+        int  operator *() const { 
+            return m_val;
+        }
+        
+        void operator ++() { 
+            m_val = m_stream.get();
+            if (m_val == '\n') ++m_line;
+        }
+        
+        unsigned line() const { return m_line; }
+    };
+
+    struct drat_record {
+        enum tag_t { is_clause, is_node, is_bool_def };
+        tag_t            m_tag;
+        // a clause populates m_lits and m_status
+        // a node populates m_node_id, m_name, m_args
+        // a bool def populates m_node_id and one element in m_args
+        sat::literal_vector  m_lits;
+        sat::status     m_status;
+        unsigned        m_node_id;
+        std::string     m_name;
+        unsigned_vector m_args;
+        drat_record():
+            m_tag(is_clause),
+            m_status(sat::status::redundant())
+        {}
+    };
+
+    std::ostream& operator<<(std::ostream& out, drat_record const& r);
+
+    class drat_parser {
+        dimacs::stream_buffer      in;
+        std::ostream&      err;
+        drat_record        m_record;
+        std::function<int(char const*)> m_read_theory_id;
+        svector<char>      m_buffer;
+
+        char const* parse_sexpr();
+        char const* parse_identifier();
+        int read_theory_id();
+        bool next();
+
+    public:
+        drat_parser(std::istream & _in, std::ostream& err):
+            in(_in), err(err)
+        {}
+
+        class iterator {
+            drat_parser& p;
+            bool m_eof;
+        public:
+            iterator(drat_parser& p, bool is_eof):p(p), m_eof(is_eof) { if (!m_eof) m_eof = !p.next(); }
+            drat_record const& operator*() { return p.m_record; }
+            iterator& operator++() { if (!p.next()) m_eof = true; return *this;}
+            bool operator==(iterator const& other) const { return m_eof == other.m_eof; }
+            bool operator!=(iterator const& other) const { return m_eof != other.m_eof; }
+        };
+        
+        iterator begin() { return iterator(*this, false); };
+        iterator end() { return iterator(*this, true); }
+
+        void set_read_theory(std::function<int(char const*)>& r) { m_read_theory_id = r; }
+
+    };
+};
+
+
 

src/sat/sat_aig_cuts.h

@@ -69,11 +69,11 @@ namespace sat {
 
         // encodes one of var, and, !and, xor, !xor, ite, !ite.
         class node {
-            bool     m_sign;
-            bool_op  m_op;
-            uint64_t m_lut;
-            unsigned m_size;
-            unsigned m_offset;
+            bool     m_sign{ false };
+            bool_op  m_op{ no_op };
+            uint64_t m_lut{ 0 };
+            unsigned m_size{ 0 };
+            unsigned m_offset{ 0 };
         public:
             node(): 
                 m_sign(false), m_op(no_op), m_size(UINT_MAX), m_offset(UINT_MAX) {}

src/sat/sat_binspr.h

@@ -38,13 +38,13 @@ namespace sat {
 
         solver&                              m_solver;
         scoped_ptr<solver>                   s;
-        unsigned                             m_bin_clauses;
-        unsigned                             m_stopped_at;
+        unsigned                             m_bin_clauses{ 0 };
+        unsigned                             m_stopped_at{ 0 };
         vector<clause_vector>                m_use_list;
-        unsigned                             m_limit1, m_limit2;
+        unsigned                             m_limit1{ 0 }, m_limit2{ 0 };
         bool_vector                        m_mark, m_mark2;
         literal_vector                       m_must_candidates, m_may_candidates;
-        unsigned                             m_state;
+        unsigned                             m_state{ 0 };
 
         void init_g() { m_state = 0x7; }
         void g_add_binary(literal l1, literal l2, bool flip2);

src/sat/sat_drat.cpp

@@ -6,10 +6,10 @@ Module Name:
     sat_drat.cpp
 
 Abstract:
-   
+
     Produce DRAT proofs.
 
-    Check them using a very simple forward checker 
+    Check them using a very simple forward checker
     that interacts with external plugins.
 
 Author:
@@ -24,19 +24,18 @@ Notes:
 
 
 namespace sat {
-    drat::drat(solver& s):
+    drat::drat(solver& s) :
         s(s),
         m_out(nullptr),
         m_bout(nullptr),
         m_inconsistent(false),
-        m_num_add(0), 
-        m_num_del(0),
         m_check_unsat(false),
         m_check_sat(false),
         m_check(false),
         m_activity(false)
     {
-        if (s.get_config().m_drat && s.get_config().m_drat_file != symbol()) {
+        if (s.get_config().m_drat && s.get_config().m_drat_file.is_non_empty_string()) {
+            std::cout << "DRAT " << s.get_config().m_drat_file << "\n";
             auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out;
             m_out = alloc(std::ofstream, s.get_config().m_drat_file.str(), mode);
             if (s.get_config().m_drat_binary) {
@@ -61,7 +60,7 @@ namespace sat {
         m_bout = nullptr;
     }
 
-    void drat::updt_config() {
+    void drat::updt_config() {            
         m_check_unsat = s.get_config().m_drat_check_unsat;
         m_check_sat = s.get_config().m_drat_check_sat;
         m_check = m_check_unsat || m_check_sat;
@@ -75,31 +74,41 @@ namespace sat {
             out << "d";
         else if (st.is_asserted())
             out << "a";
-        
+        else if (st.is_input())
+            out << "i";
+
         if (!st.is_sat())
             out << " " << m_theory[st.get_th()];
-        return out;        
+        return out;
     }
 
     void drat::dump(unsigned n, literal const* c, status st) {
         if (st.is_asserted() && !s.m_ext)
             return;
-        if (m_activity && ((m_num_add % 1000) == 0)) 
+        if (m_activity && ((m_stats.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.is_asserted()) {
             buffer[len++] = 'a';
-            buffer[len++] = ' ';           
+            buffer[len++] = ' ';
         }
         else if (st.is_deleted()) {
             buffer[len++] = 'd';
             buffer[len++] = ' ';
         }
+        else if (st.is_input()) {
+            buffer[len++] = 'i';
+            buffer[len++] = ' ';
+        }
+        else if (st.is_redundant() && !st.is_sat()) {
+            buffer[len++] = 'r';
+            buffer[len++] = ' ';
+        }
 
         if (!st.is_sat()) {
             for (char ch : m_theory[st.get_th()])
@@ -108,28 +117,28 @@ namespace sat {
         }
         for (unsigned i = 0; i < n; ++i) {
             literal lit = c[i];
-            unsigned v = lit.var();            
+            unsigned v = lit.var();
             if (lit.sign()) buffer[len++] = '-';
             char* d = lastd;
             SASSERT(v > 0);
-            while (v > 0) {                
+            while (v > 0) {
                 d--;
                 *d = (v % 10) + '0';
                 v /= 10;
                 SASSERT(d > digits);
             }
-	    SASSERT(len + lastd < sizeof(buffer) + d);
-	    memcpy(buffer + len, d, lastd - d);
-	    len += static_cast<unsigned>(lastd - d);            
-	    buffer[len++] = ' ';
-	    if (len + 50 > sizeof(buffer)) {
-	        m_out->write(buffer, len);
-	        len = 0;
+            SASSERT(len + lastd < sizeof(buffer) + d);
+            memcpy(buffer + len, d, lastd - d);
+            len += static_cast<unsigned>(lastd - d);
+            buffer[len++] = ' ';
+            if (len + 50 > sizeof(buffer)) {
+                m_out->write(buffer, len);
+                len = 0;
             }
-        }        
-	buffer[len++] = '0';
-	buffer[len++] = '\n';
-	m_out->write(buffer, len);               
+        }
+        buffer[len++] = '0';
+        buffer[len++] = '\n';
+        m_out->write(buffer, len);
 
     }
 
@@ -144,9 +153,9 @@ namespace sat {
     void drat::bdump(unsigned n, literal const* c, status st) {
         unsigned char ch = 0;
         if (st.is_redundant())
-            ch = 'a'; 
+            ch = 'a';
         else if (st.is_deleted())
-            ch = 'd'; 
+            ch = 'd';
         else return;
         char buffer[10000];
         int len = 0;
@@ -164,8 +173,7 @@ namespace sat {
                     m_bout->write(buffer, len);
                     len = 0;
                 }
-            }
-            while (v);
+            } while (v);
         }
         buffer[len++] = 0;
         m_bout->write(buffer, len);
@@ -188,7 +196,7 @@ namespace sat {
             if (c[i] != last) {
                 out << c[i] << " ";
                 last = c[i];
-            }            
+            }
         }
         out << "\n";
     }
@@ -198,7 +206,7 @@ namespace sat {
 
         declare(l);
         IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
-        if (st.is_redundant()) {
+        if (st.is_redundant() && st.is_sat()) {
             verify(1, &l);
         }
         if (st.is_deleted()) {
@@ -213,17 +221,17 @@ namespace sat {
 
     void drat::append(literal l1, literal l2, status st) {
         TRACE("sat_drat", pp(tout, st) << " " << l1 << " " << l2 << "\n";);
-        declare(l1); 
+        declare(l1);
         declare(l2);
         literal lits[2] = { l1, l2 };
-        
+
         IF_VERBOSE(20, trace(verbose_stream(), 2, lits, st););
         if (st.is_deleted()) {
             // noop
             // don't record binary as deleted.
         }
         else {
-            if (st.is_redundant()) {
+            if (st.is_redundant() && st.is_sat()) {
                 verify(2, lits);
             }
             clause* c = m_alloc.mk_clause(2, lits, st.is_redundant());
@@ -252,18 +260,18 @@ namespace sat {
             (*m_out) << "b " << v << " " << n << " 0\n";
     }
 
-    void drat::def_begin(unsigned n, symbol const& name) {
-        if (m_out) 
-            (*m_out) << "n " << n << " " << name;
+    void drat::def_begin(unsigned n, std::string const& name) {
+        if (m_out)
+            (*m_out) << "e " << n << " " << name;
     }
 
     void drat::def_add_arg(unsigned arg) {
-        if (m_out) 
+        if (m_out)
             (*m_out) << " " << arg;
     }
 
     void drat::def_end() {
-        if (m_out) 
+        if (m_out)
             (*m_out) << " 0\n";
     }
 
@@ -300,12 +308,12 @@ namespace sat {
         unsigned n = c.size();
         IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
 
-        if (st.is_redundant()) {
+        if (st.is_redundant() && st.is_sat()) {
             verify(c);
         }
-           
+
         m_status.push_back(st);
-        m_proof.push_back(&c); 
+        m_proof.push_back(&c);
         if (st.is_deleted()) {
             if (n > 0) del_watch(c, c[0]);
             if (n > 1) del_watch(c, c[1]);
@@ -327,11 +335,11 @@ namespace sat {
             }
         }
         switch (num_watch) {
-        case 0: 
-            m_inconsistent = true; 
+        case 0:
+            m_inconsistent = true;
             break;
-        case 1: 
-            assign_propagate(l1); 
+        case 1:
+            assign_propagate(l1);
             break;
         default: {
             SASSERT(num_watch == 2);
@@ -345,7 +353,7 @@ namespace sat {
     }
 
     void drat::del_watch(clause& c, literal l) {
-        watch& w = m_watches[(~l).index()];      
+        watch& w = m_watches[(~l).index()];
         for (unsigned i = 0; i < w.size(); ++i) {
             if (m_watched_clauses[w[i]].m_clause == &c) {
                 w[i] = w.back();
@@ -368,7 +376,7 @@ namespace sat {
     bool drat::is_drup(unsigned n, literal const* c) {
         if (m_inconsistent || n == 0) return true;
         unsigned num_units = m_units.size();
-        for (unsigned i = 0; !m_inconsistent && i < n; ++i) {            
+        for (unsigned i = 0; !m_inconsistent && i < n; ++i) {
             assign_propagate(~c[i]);
         }
         if (!m_inconsistent) {
@@ -417,7 +425,7 @@ namespace sat {
             }
             svector<sat::solver::bin_clause> bin;
             s.collect_bin_clauses(bin, true);
-            for (auto & b : bin) {
+            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;
@@ -435,17 +443,16 @@ namespace sat {
         }
         m_units.shrink(num_units);
         bool ok = m_inconsistent;
-        // IF_VERBOSE(9, verbose_stream() << "is-drup " << m_inconsistent << "\n");
         m_inconsistent = false;
-
         return ok;
     }
 
     bool drat::is_drat(unsigned n, literal const* c) {
-        if (m_inconsistent || n == 0) return true;
-        for (unsigned i = 0; i < n; ++i) {
-            if (is_drat(n, c, i)) return true;
-        }
+        if (m_inconsistent || n == 0) 
+            return true;
+        for (unsigned i = 0; i < n; ++i) 
+            if (is_drat(n, c, i)) 
+                return true;
         return false;
     }
 
@@ -482,7 +489,7 @@ namespace sat {
                 if (st.is_sat() && j != c.size()) {
                     lits.append(j, c.begin());
                     lits.append(c.size() - j - 1, c.begin() + j + 1);
-                    if (!is_drup(lits.size(), lits.c_ptr())) 
+                    if (!is_drup(lits.size(), lits.c_ptr()))
                         return false;
                     lits.resize(n);
                 }
@@ -496,26 +503,33 @@ namespace sat {
         if (!m_check_unsat) {
             return;
         }
-        for (unsigned i = 0; i < n; ++i) { 
+        for (unsigned i = 0; i < n; ++i) {
             declare(c[i]);
-        } 
-        if (!is_drup(n, c) && !is_drat(n, c)) {
-            literal_vector lits(n, c);
-            IF_VERBOSE(0, verbose_stream() << "Verification of " << lits << " failed\n");
-            // s.display(std::cout);
-            std::string line;
-            std::getline(std::cin, line);                
-            SASSERT(false);
-            INVOKE_DEBUGGER();
-            exit(0);
-            UNREACHABLE();
-            //display(std::cout);
-            TRACE("sat_drat", 
-                  tout << literal_vector(n, c) << "\n";
-                  display(tout); 
-                  s.display(tout););
-            UNREACHABLE();
         }
+        if (is_drup(n, c)) {
+            ++m_stats.m_num_drup;
+            return;
+        }
+        if (is_drat(n, c)) {
+            ++m_stats.m_num_drat;
+            return;
+        }
+
+        literal_vector lits(n, c);
+        IF_VERBOSE(0, verbose_stream() << "Verification of " << lits << " failed\n");
+        // s.display(std::cout);
+        std::string line;
+        std::getline(std::cin, line);
+        SASSERT(false);
+        INVOKE_DEBUGGER();
+        exit(0);
+        UNREACHABLE();
+        //display(std::cout);
+        TRACE("sat_drat",
+              tout << literal_vector(n, c) << "\n";
+              display(tout);
+              s.display(tout););
+        UNREACHABLE();
     }
 
     bool drat::contains(literal c, justification const& j) {
@@ -529,7 +543,7 @@ namespace sat {
             return contains(c, j.get_literal());
         case justification::TERNARY:
             return contains(c, j.get_literal1(), j.get_literal2());
-        case justification::CLAUSE: 
+        case justification::CLAUSE:
             return contains(s.get_clause(j));
         default:
             return true;
@@ -546,7 +560,7 @@ namespace sat {
             if (match(n, lits, c)) {
                 if (st.is_deleted()) {
                     num_del++;
-                } 
+                }
                 else {
                     num_add++;
                 }
@@ -578,7 +592,7 @@ namespace sat {
     void drat::display(std::ostream& out) const {
         out << "units: " << m_units << "\n";
         for (unsigned i = 0; i < m_assignment.size(); ++i) {
-            lbool v = value(literal(i, false));            
+            lbool v = value(literal(i, false));
             if (v != l_undef) out << i << ": " << v << "\n";
         }
         for (unsigned i = 0; i < m_proof.size(); ++i) {
@@ -599,12 +613,12 @@ namespace sat {
                 if (num_true == 0 && num_undef == 1) {
                     out << "Unit ";
                 }
-                pp(out, m_status[i]) <<  " " << i << ": " << *c << "\n";
+                pp(out, m_status[i]) << " " << i << ": " << *c << "\n";
             }
         }
         for (unsigned i = 0; i < m_assignment.size(); ++i) {
-            watch const& w1 = m_watches[2*i];
-            watch const& w2 = m_watches[2*i + 1];
+            watch const& w1 = m_watches[2 * i];
+            watch const& w2 = m_watches[2 * i + 1];
             if (!w1.empty()) {
                 out << i << " |-> ";
                 for (unsigned i = 0; i < w1.size(); ++i) out << *(m_watched_clauses[w1[i]].m_clause) << " ";
@@ -626,7 +640,7 @@ namespace sat {
     void drat::assign(literal l) {
         lbool new_value = l.sign() ? l_false : l_true;
         lbool old_value = value(l);
-//        TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";);
+        //        TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";);
         switch (old_value) {
         case l_false:
             m_inconsistent = true;
@@ -645,7 +659,7 @@ namespace sat {
         assign(l);
         for (unsigned i = num_units; !m_inconsistent && i < m_units.size(); ++i) {
             propagate(m_units[i]);
-        }        
+        }
     }
 
     void drat::propagate(literal l) {
@@ -676,10 +690,10 @@ namespace sat {
                         wc.m_l2 = lit;
                         m_watches[(~lit).index()].push_back(idx);
                         done = true;
-                    } 
+                    }
                 }
                 if (done) {
-                    continue;                
+                    continue;
                 }
                 else if (value(wc.m_l1) == l_false) {
                     m_inconsistent = true;
@@ -693,19 +707,19 @@ namespace sat {
             }
         }
     end_process_watch:
-        for (; it != end; ++it, ++it2)          
-            *it2 = *it;                         
-        clauses.set_end(it2);                     
+        for (; it != end; ++it, ++it2)
+            *it2 = *it;
+        clauses.set_end(it2);
     }
 
     status drat::get_status(bool learned) const {
         if (learned || s.m_searching)
             return status::redundant();
-        return status::asserted(); 
+        return status::asserted();
     }
 
     void drat::add() {
-        ++m_num_add;
+        ++m_stats.m_num_add;
         if (m_out) (*m_out) << "0\n";
         if (m_bout) bdump(0, nullptr, status::redundant());
         if (m_check_unsat) {
@@ -713,7 +727,7 @@ namespace sat {
         }
     }
     void drat::add(literal l, bool learned) {
-        ++m_num_add;
+        ++m_stats.m_num_add;
         status st = get_status(learned);
         if (m_out) dump(1, &l, st);
         if (m_bout) bdump(1, &l, st);
@@ -721,19 +735,19 @@ namespace sat {
     }
     void drat::add(literal l1, literal l2, status st) {
         if (st.is_deleted())
-            ++m_num_del;
+            ++m_stats.m_num_del;
         else
-            ++m_num_add;
-        literal ls[2] = {l1, l2};
+            ++m_stats.m_num_add;
+        literal ls[2] = { l1, l2 };
         if (m_out) dump(2, ls, st);
         if (m_bout) bdump(2, ls, st);
         if (m_check) append(l1, l2, st);
     }
     void drat::add(clause& c, status st) {
         if (st.is_deleted())
-            ++m_num_del;
+            ++m_stats.m_num_del;
         else
-            ++m_num_add;
+            ++m_stats.m_num_add;
         if (m_out) dump(c.size(), c.begin(), st);
         if (m_bout) bdump(c.size(), c.begin(), st);
         if (m_check) {
@@ -743,9 +757,9 @@ namespace sat {
     }
     void drat::add(literal_vector const& lits, status st) {
         if (st.is_deleted())
-            ++m_num_del;
-        else 
-            ++m_num_add;
+            ++m_stats.m_num_del;
+        else
+            ++m_stats.m_num_add;
         if (m_check) {
             switch (lits.size()) {
             case 0: add(); break;
@@ -756,12 +770,12 @@ namespace sat {
                 break;
             }
             }
-        }              
-        if (m_out) 
+        }
+        if (m_out)
             dump(lits.size(), lits.c_ptr(), st);
     }
     void drat::add(literal_vector const& c) {
-        ++m_num_add;
+        ++m_stats.m_num_add;
         if (m_out) dump(c.size(), c.begin(), status::redundant());
         if (m_bout) bdump(c.size(), c.begin(), status::redundant());
         if (m_check) {
@@ -780,15 +794,15 @@ namespace sat {
     }
 
     void drat::del(literal l) {
-        ++m_num_del;
+        ++m_stats.m_num_del;
         if (m_out) dump(1, &l, status::deleted());
         if (m_bout) bdump(1, &l, status::deleted());
         if (m_check_unsat) append(l, status::deleted());
     }
 
     void drat::del(literal l1, literal l2) {
-        ++m_num_del;
-        literal ls[2] = {l1, l2};
+        ++m_stats.m_num_del;
+        literal ls[2] = { l1, l2 };
         if (m_out) dump(2, ls, status::deleted());
         if (m_bout) bdump(2, ls, status::deleted());
         if (m_check) append(l1, l2, status::deleted());
@@ -806,26 +820,47 @@ namespace sat {
             m_seen[lit.index()] = false;
         }
 #endif
-        ++m_num_del;
+        ++m_stats.m_num_del;
         if (m_out) dump(c.size(), c.begin(), status::deleted());
         if (m_bout) bdump(c.size(), c.begin(), status::deleted());
         if (m_check) {
-            clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), c.is_learned()); 
+            clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), c.is_learned());
             append(*c1, status::deleted());
         }
     }
 
     void drat::del(literal_vector const& c) {
-        ++m_num_del;
+        ++m_stats.m_num_del;
         if (m_out) dump(c.size(), c.begin(), status::deleted());
         if (m_bout) bdump(c.size(), c.begin(), status::deleted());
         if (m_check) {
-            clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), true); 
+            clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), true);
             append(*c1, status::deleted());
         }
     }
-    
-    void drat::check_model(model const& m) {        
+
+    void drat::check_model(model const& m) {
+    }
+
+    std::ostream& operator<<(std::ostream& out, status const& st) {
+        if (st.is_deleted())
+            out << "d";
+        else if (st.is_input())
+            out << "i";
+        else if (st.is_asserted())
+            out << "a";
+        else if (st.is_redundant() && !st.is_sat())
+            out << "r";
+        if (!st.is_sat())
+            out << " th" << st.m_orig;
+        return out;
+    }
+
+    void drat::collect_statistics(statistics& st) const {
+        st.update("num-drup", m_stats.m_num_drup);
+        st.update("num-drat", m_stats.m_num_drat);
+        st.update("num-add", m_stats.m_num_add);
+        st.update("num-del", m_stats.m_num_del);
     }
 
 }

src/sat/sat_drat.h

@@ -19,18 +19,24 @@ Notes:
 
     For SMT extensions are as follows:
 
-    Assertion (trusted modulo internalizer):
+    Input assertion:
+      i <literal>* 0
+
+    Assertion (true modulo a theory):
       a [<theory-id>] <literal>* 0
-    The optional theory id indicates the assertion is irredundant
+    The if no theory id is given, the assertion is a tautology
+    modulo Tseitin converison. Theory ids track whether the
+    tautology is modulo a theory.
+    Assertions are irredundant.
 
     Bridge from ast-node to boolean variable:
       b <bool-var-id> <ast-node-id> 0
 
-    Definition of an ast node:
-      n <ast-node-id> <name> <ast-node-id>* 0
+    Definition of an expression (ast-node):
+      e <ast-node-id> <name> <ast-node-id>* 0
 
-    Theory lemma
-      <theory-id> <literal>* 0
+    Redundant clause (theory lemma if theory id is given)
+      [r [<theory-id>]] <literal>* 0
 
     Available theories are:
       - euf   The theory lemma should be a consequence of congruence closure.
@@ -45,8 +51,16 @@ Notes:
 #include "sat_types.h"
 
 namespace sat {
+    class justification;
+    class clause;
+
     class drat {
-    private:
+        struct stats {
+            unsigned m_num_drup { 0 };
+            unsigned m_num_drat { 0 };
+            unsigned m_num_add { 0 };
+            unsigned m_num_del { 0 };
+        };
         struct watched_clause {
             clause* m_clause;
             literal m_l1, m_l2;
@@ -64,10 +78,10 @@ namespace sat {
         literal_vector          m_units;
         vector<watch>           m_watches;
         svector<lbool>          m_assignment;
-        svector<std::string>    m_theory;
+        vector<std::string>     m_theory;
         bool                    m_inconsistent;
-        unsigned                m_num_add, m_num_del;
         bool                    m_check_unsat, m_check_sat, m_check, m_activity;
+        stats                   m_stats;
 
         void dump_activity();
         void dump(unsigned n, literal const* c, status st);
@@ -96,6 +110,7 @@ namespace sat {
         bool match(unsigned n, literal const* lits, clause const& c) const;
 
     public:
+
         drat(solver& s);
         ~drat();  
 
@@ -114,7 +129,7 @@ namespace sat {
         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_begin(unsigned n, std::string const& name);
         void def_add_arg(unsigned arg);
         void def_end();
 
@@ -139,7 +154,11 @@ namespace sat {
         bool contains(literal c, justification const& j);
 
         void check_model(model const& m);
+
+        void collect_statistics(statistics& st) const;
     };
 
+    std::ostream& operator<<(std::ostream& out, status const& st);
+
 };
 

src/sat/sat_elim_eqs.cpp

@@ -236,7 +236,6 @@ namespace sat {
             if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 if (m_solver.m_config.m_drat && m_solver.m_config.m_drat_file.is_null()) {
-                    std::cout << "DRAT\n";
                     m_solver.m_drat.add(~l, r, sat::status::redundant());
                     m_solver.m_drat.add(l, ~r, sat::status::redundant());
                 }

src/sat/sat_extension.h

@@ -61,9 +61,10 @@ namespace sat {
         virtual void set_lookahead(lookahead* s) = 0;
         virtual void init_search() {}
         virtual bool propagate(literal l, ext_constraint_idx idx) = 0;
+        virtual bool unit_propagate() = 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 void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) = 0;
         virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) = 0;
         virtual void asserted(literal l) = 0;
         virtual check_result check() = 0;

src/sat/sat_simplifier.cpp

@@ -1900,7 +1900,6 @@ namespace sat {
     }
 
     bool simplifier::try_eliminate(bool_var v) {
-        TRACE("sat_simplifier", tout << "processing: " << v << "\n";);
         if (value(v) != l_undef)
             return false;
 
@@ -1963,7 +1962,7 @@ namespace sat {
                 }
             }
         }
-        TRACE("sat_simplifier", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
+        TRACE("sat_simplifier", tout << "eliminate " << v << ", before: " << before_clauses << " after: " << after_clauses << "\n";);
         m_elim_counter -= num_pos * num_neg + before_lits;
 
         m_elim_counter -= num_pos * num_neg + before_lits;

src/sat/sat_solver.cpp

@@ -86,7 +86,7 @@ namespace sat {
         m_cuber                   = nullptr;
         m_local_search            = nullptr;
         m_mc.set_solver(this);
-        //mk_var(false, false);
+        mk_var(false, false);
     }
 
     solver::~solver() {
@@ -138,7 +138,7 @@ namespace sat {
         m_qhead = 0;
         m_trail.reset();
         m_scopes.reset();
-        //mk_var(false, false);
+        mk_var(false, false);
 
         if (src.inconsistent()) {
             set_conflict();
@@ -353,7 +353,7 @@ namespace sat {
     clause * solver::mk_clause_core(unsigned num_lits, literal * lits, sat::status st) {
         bool redundant = st.is_redundant();
         TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << (redundant?" learned":" aux") << "\n";);
-        if (!redundant) {
+        if (!redundant || !st.is_sat()) {
             unsigned old_sz = num_lits;
             bool keep = simplify_clause(num_lits, lits);
             TRACE("sat_mk_clause", tout << "mk_clause (after simp), keep: " << keep << "\n" << mk_lits_pp(num_lits, lits) << "\n";);
@@ -1103,6 +1103,11 @@ namespace sat {
                 }
             }
             wlist.set_end(it2);
+            if (m_ext) {
+                m_ext->unit_propagate();
+                if (inconsistent())
+                    return false;
+            }
         }
         SASSERT(m_qhead == m_trail.size());
         SASSERT(!m_inconsistent);
@@ -1205,9 +1210,9 @@ namespace sat {
         }
         try {
             init_search();
-            if (inconsistent()) return l_false;
+            if (check_inconsistent()) return l_false;
             propagate(false);
-            if (inconsistent()) return l_false;
+            if (check_inconsistent()) return l_false;
             init_assumptions(num_lits, lits);
             propagate(false);
             if (check_inconsistent()) return l_false;
@@ -1644,7 +1649,9 @@ namespace sat {
 
     bool solver::check_inconsistent() {
         if (inconsistent()) {
-            if (tracking_assumptions())
+            if (tracking_assumptions() && at_search_lvl())
+                resolve_conflict();
+            else if (m_config.m_drat && at_base_lvl())
                 resolve_conflict();
             return true;
         }
@@ -2576,13 +2583,6 @@ 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;
@@ -2609,7 +2609,6 @@ 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;
@@ -2685,7 +2684,7 @@ namespace sat {
                 break;
             }
             case justification::EXT_JUSTIFICATION: {
-                fill_ext_antecedents(consequent, js);
+                fill_ext_antecedents(consequent, js, false);
                 for (literal l : m_ext_antecedents) 
                     process_antecedent(l, num_marks);
                 break;
@@ -2786,6 +2785,7 @@ namespace sat {
         if (m_par && lemma) {
             m_par->share_clause(*this, *lemma);
         }
+        m_lemma.reset();
         TRACE("sat_conflict_detail", tout << "consistent " << (!m_inconsistent) << " scopes: " << scope_lvl() << " backtrack: " << backtrack_lvl << " backjump: " << backjump_lvl << "\n";);
         decay_activity();
         updt_phase_counters();
@@ -2847,7 +2847,7 @@ namespace sat {
             break;
         }
         case justification::EXT_JUSTIFICATION: {
-            fill_ext_antecedents(consequent, js);
+            fill_ext_antecedents(consequent, js, true);
             for (literal l : m_ext_antecedents) {
                 process_antecedent_for_unsat_core(l);
             }
@@ -2975,7 +2975,7 @@ namespace sat {
         case justification::EXT_JUSTIFICATION:
             if (not_l != null_literal) 
                 not_l.neg();
-            fill_ext_antecedents(not_l, js);
+            fill_ext_antecedents(not_l, js, true);
             for (literal l : m_ext_antecedents) 
                 level = update_max_level(l, level, unique_max);
             return level;
@@ -3031,16 +3031,12 @@ namespace sat {
     /**
        \brief js is an external justification. Collect its antecedents and store at m_ext_antecedents.
     */
-    void solver::fill_ext_antecedents(literal consequent, justification js) {
+    void solver::fill_ext_antecedents(literal consequent, justification js, bool probing) {
         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, idx, m_ext_antecedents);
-        m_cached_antecedent_consequent = consequent;
-        m_cached_antecedent_js = idx;
+        m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing);
     }
 
     bool solver::is_two_phase() const {
@@ -3354,7 +3350,7 @@ namespace sat {
             }
             case justification::EXT_JUSTIFICATION: {
                 literal consequent(var, value(var) == l_false);
-                fill_ext_antecedents(consequent, js);
+                fill_ext_antecedents(consequent, js, false);
                 for (literal l : m_ext_antecedents) {
                     if (!process_antecedent_for_minimization(l)) {
                         reset_unmark(old_size);
@@ -3496,7 +3492,7 @@ namespace sat {
                 break;
             }
             case justification::EXT_JUSTIFICATION: {
-                fill_ext_antecedents(~m_lemma[i], js);
+                fill_ext_antecedents(~m_lemma[i], js, true);
                 for (literal l : m_ext_antecedents) {
                     update_lrb_reasoned(l);
                 }
@@ -3657,6 +3653,7 @@ namespace sat {
         s.m_trail_lim = m_trail.size();
         s.m_clauses_to_reinit_lim = m_clauses_to_reinit.size();
         s.m_inconsistent = m_inconsistent;
+        // m_vars_lim.push(num_vars());
         if (m_ext)
             m_ext->push();
     }
@@ -3668,11 +3665,46 @@ namespace sat {
         m_stats.m_units = init_trail_size();
     }
 
+    void solver::pop_vars(unsigned num_scopes) {
+        unsigned old_num_vars = m_vars_lim.pop(num_scopes);
+        if (old_num_vars == num_vars()) 
+            return;
+        IF_VERBOSE(0, verbose_stream() << "new variables created under scope\n";);
+        for (unsigned v = old_num_vars; v < num_vars(); ++v) {
+            
+        }
+    }
+
+    void solver::shrink_vars(unsigned v) {
+        for (bool_var i = v; i < m_justification.size(); ++i) {
+            m_case_split_queue.del_var_eh(i);
+            m_probing.reset_cache(literal(i, true));
+            m_probing.reset_cache(literal(i, false));
+        }
+        m_watches.shrink(2*v);
+        m_assignment.shrink(2*v);
+        m_justification.shrink(v);
+        m_decision.shrink(v);
+        m_eliminated.shrink(v);
+        m_external.shrink(v);
+        m_touched.shrink(v);
+        m_activity.shrink(v);
+        m_mark.shrink(v);
+        m_lit_mark.shrink(2*v);
+        m_phase.shrink(v);
+        m_best_phase.shrink(v);
+        m_prev_phase.shrink(v);
+        m_assigned_since_gc.shrink(v);
+        m_simplifier.reset_todos();
+    }
+
     void solver::pop(unsigned num_scopes) {
         if (num_scopes == 0)
             return;
-        if (m_ext)
+        if (m_ext) {
+            // pop_vars(num_scopes);
             m_ext->pop(num_scopes);
+        }
         SASSERT(num_scopes <= scope_lvl());
         unsigned new_lvl = scope_lvl() - num_scopes;
         scope & s        = m_scopes[new_lvl];
@@ -3709,12 +3741,27 @@ namespace sat {
         m_qhead = m_trail.size();
         if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
         for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
-            m_trail.push_back(m_replay_assign[i]);            
+            literal lit = m_replay_assign[i];
+            if (m_ext && m_external[lit.var()])
+                m_ext->asserted(lit);
+            m_trail.push_back(lit);            
         }
         
         m_replay_assign.reset();
     }
 
+    void solver::get_reinit_literals(unsigned n, literal_vector& r) {
+        unsigned new_lvl = scope_lvl() - n;
+        unsigned old_sz = m_scopes[new_lvl].m_clauses_to_reinit_lim;
+        for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) {
+            clause_wrapper cw = m_clauses_to_reinit[i];
+            for (unsigned j = cw.size(); j-- > 0; )
+                r.push_back(cw[j]);
+        }
+        for (literal lit : m_lemma)
+            r.push_back(lit);
+    }
+
     void solver::reinit_clauses(unsigned old_sz) {
         unsigned sz = m_clauses_to_reinit.size();
         SASSERT(old_sz <= sz);
@@ -3834,26 +3881,7 @@ namespace sat {
         
         // v is an index of a variable that does not occur in solver state.
         if (v < m_justification.size()) {
-            for (bool_var i = v; i < m_justification.size(); ++i) {
-                m_case_split_queue.del_var_eh(i);
-                m_probing.reset_cache(literal(i, true));
-                m_probing.reset_cache(literal(i, false));
-            }
-            m_watches.shrink(2*v);
-            m_assignment.shrink(2*v);
-            m_justification.shrink(v);
-            m_decision.shrink(v);
-            m_eliminated.shrink(v);
-            m_external.shrink(v);
-            m_touched.shrink(v);
-            m_activity.shrink(v);
-            m_mark.shrink(v);
-            m_lit_mark.shrink(2*v);
-            m_phase.shrink(v);
-            m_best_phase.shrink(v);
-            m_prev_phase.shrink(v);
-            m_assigned_since_gc.shrink(v);
-            m_simplifier.reset_todos();
+            shrink_vars(v);
         }
     }
 
@@ -4766,7 +4794,7 @@ namespace sat {
             break;
         }
         case justification::EXT_JUSTIFICATION: {
-            fill_ext_antecedents(lit, js);
+            fill_ext_antecedents(lit, js, true);
             for (literal l : m_ext_antecedents) {
                 if (check_domain(lit, l) && all_found) {
                     s |= m_antecedents.find(l.var());

src/sat/sat_solver.h

@@ -45,6 +45,7 @@ Revision History:
 #include "util/trace.h"
 #include "util/rlimit.h"
 #include "util/scoped_ptr_vector.h"
+#include "util/scoped_limit_trail.h"
 
 namespace sat {
 
@@ -172,6 +173,7 @@ namespace sat {
             bool     m_inconsistent;
         };
         svector<scope>          m_scopes;
+        scoped_limit_trail      m_vars_lim;
         stopwatch               m_stopwatch;
         params_ref              m_params;
         scoped_ptr<solver>      m_clone; // for debugging purposes
@@ -399,6 +401,7 @@ namespace sat {
         bool canceled() { return !m_rlimit.inc(); }
         config const& get_config() const { return m_config; }
         drat& get_drat() { return m_drat; }
+        drat* get_drat_ptr() override { 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(); }
@@ -565,8 +568,6 @@ 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();
@@ -582,7 +583,7 @@ namespace sat {
         void resolve_conflict_for_unsat_core();
         void process_antecedent_for_unsat_core(literal antecedent);
         void process_consequent_for_unsat_core(literal consequent, justification const& js);
-        void fill_ext_antecedents(literal consequent, justification js);
+        void fill_ext_antecedents(literal consequent, justification js, bool probing);
         unsigned skip_literals_above_conflict_level();
         void updt_phase_of_vars();
         void updt_phase_counters();
@@ -621,6 +622,8 @@ namespace sat {
         void push();
         void pop(unsigned num_scopes);
         void pop_reinit(unsigned num_scopes);
+        void shrink_vars(unsigned v);
+        void pop_vars(unsigned num_scopes);
 
         void unassign_vars(unsigned old_sz, unsigned new_lvl);
         void reinit_clauses(unsigned old_sz);
@@ -635,6 +638,14 @@ namespace sat {
         bool_var max_var(clause_vector& clauses, bool_var v);
         bool_var max_var(bool learned, bool_var v);
 
+        // -----------------------
+        //
+        // External
+        //
+        // -----------------------
+    public:
+        void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
+        void get_reinit_literals(unsigned num_scopes, literal_vector& r);
     public:
         void user_push() override;
         void user_pop(unsigned num_scopes) override;
@@ -798,4 +809,3 @@ namespace sat {
 
     std::ostream & operator<<(std::ostream & out, mk_stat const & stat);
 };
-

src/sat/sat_solver/inc_sat_solver.cpp

@@ -126,7 +126,7 @@ public:
         auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
         if (ext) {
             auto& si = result->m_goal2sat.si(dst_m, m_params, result->m_solver, result->m_map, result->m_dep2asm, is_incremental());
-            euf::solver::scoped_set_translate st(*ext, dst_m, result->m_map, si);  
+            euf::solver::scoped_set_translate st(*ext, dst_m, si);  
             result->m_solver.copy(m_solver);
         }        
         else {

src/sat/sat_solver_core.h

@@ -25,6 +25,7 @@ namespace sat {
 
     class cut_simplifier;
     class extension;
+    class drat;
 
     class solver_core {
     protected:
@@ -95,6 +96,8 @@ namespace sat {
 
         virtual cut_simplifier* get_cut_simplifier() { return nullptr; }
 
+        virtual drat* get_drat_ptr() { return nullptr;  }
+
 
         // The following methods are used when converting the state from the SAT solver back
         // to a set of assertions. 

src/sat/sat_types.h

@@ -254,19 +254,22 @@ namespace sat {
 
     class status {
     public:
-        enum class st { asserted, redundant, deleted };
+        enum class st { input, asserted, redundant, deleted };
         st m_st;
         int m_orig;
     public:
         status(enum st s, int o) : m_st(s), m_orig(o) {};
         status(status const& s) : m_st(s.m_st), m_orig(s.m_orig) {}
         status(status&& s) noexcept { m_st = st::asserted; m_orig = -1; std::swap(m_st, s.m_st); std::swap(m_orig, s.m_orig); }
+        status& operator=(status const& other) { m_st = other.m_st; m_orig = other.m_orig; return *this; }
         static status redundant() { return status(status::st::redundant, -1); }
         static status asserted() { return status(status::st::asserted, -1); }
         static status deleted() { return status(status::st::deleted, -1); }
+        static status input() { return status(status::st::input, -1); }
 
         static status th(bool redundant, int id) { return status(redundant ? st::redundant : st::asserted, id); }
 
+        bool is_input() const { return st::input == m_st; }
         bool is_redundant() const { return st::redundant == m_st; }
         bool is_asserted() const { return st::asserted == m_st; }
         bool is_deleted() const { return st::deleted == m_st; }
@@ -275,6 +278,5 @@ namespace sat {
         int  get_th() const { return m_orig;  }
     };
 
-
 };
 

src/sat/smt/CMakeLists.txt

@@ -3,10 +3,12 @@ z3_add_component(sat_smt
     atom2bool_var.cpp
     ba_internalize.cpp
     ba_solver.cpp
+    bv_ackerman.cpp
     bv_internalize.cpp
     bv_solver.cpp
     euf_ackerman.cpp
     euf_internalize.cpp
+    euf_invariant.cpp
     euf_model.cpp
     euf_proof.cpp
     euf_solver.cpp

src/sat/smt/ba_internalize.cpp

@@ -21,6 +21,10 @@ Author:
 
 namespace sat {
 
+    void ba_solver::internalize(expr* e, bool redundant) {
+        internalize(e, false, false, redundant);
+    }
+
     literal ba_solver::internalize(expr* e, bool sign, bool root, bool redundant) {
         flet<bool> _redundant(m_is_redundant, redundant);
         if (m_pb.is_pb(e)) 

src/sat/smt/ba_solver.cpp

@@ -2107,8 +2107,8 @@ namespace sat {
     // ----------------------------
     // constraint generic methods
 
-    void ba_solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
-        get_antecedents(l, index2constraint(idx), r);
+    void ba_solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) {
+        get_antecedents(l, index2constraint(idx), r, probing);
     }
 
     bool ba_solver::is_watched(literal lit, constraint const& c) const {
@@ -2128,14 +2128,14 @@ namespace sat {
         get_wlist(~lit).push_back(w);
     }
 
-    void ba_solver::get_antecedents(literal l, constraint const& c, literal_vector& r) {
+    void ba_solver::get_antecedents(literal l, constraint const& c, literal_vector& r, bool probing) {
         switch (c.tag()) {
         case card_t: get_antecedents(l, c.to_card(), r); break;
         case pb_t: get_antecedents(l, c.to_pb(), r); break;
         case xr_t: get_antecedents(l, c.to_xr(), r); break;
         default: UNREACHABLE(); break;            
         }
-        if (get_config().m_drat && m_solver) {
+        if (get_config().m_drat && m_solver && !probing) {
             literal_vector lits;
             for (literal lit : r) 
                 lits.push_back(~lit);

src/sat/smt/ba_solver.h

@@ -361,7 +361,7 @@ namespace sat {
         void set_conflict(constraint& c, literal lit);
         void assign(constraint& c, literal lit);
         bool assigned_above(literal above, literal below);
-        void get_antecedents(literal l, constraint const& c, literal_vector & r);
+        void get_antecedents(literal l, constraint const& c, literal_vector & r, bool probing);
         bool validate_conflict(constraint const& c) const;
         bool validate_unit_propagation(constraint const& c, literal alit) const;
         void validate_eliminated();
@@ -576,8 +576,9 @@ namespace sat {
 
         bool is_external(bool_var v) override;
         bool propagate(literal l, ext_constraint_idx idx) override;
+        bool unit_propagate() override { return false; }
         lbool resolve_conflict() override;
-        void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
+        void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) override;
         void asserted(literal l) override;
         check_result check() override;
         void push() override;
@@ -604,6 +605,7 @@ namespace sat {
         bool check_model(model const& m) const override;
 
         literal internalize(expr* e, bool sign, bool root, bool redundant) override;
+        void internalize(expr* e, bool redundant) override;
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
         euf::th_solver* fresh(solver* s, euf::solver& ctx) override;
 

src/sat/smt/bv_ackerman.cpp

@@ -0,0 +1,153 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv_ackerman.cpp
+
+Abstract:
+
+    Ackerman reduction plugin for bit-vectors
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-28
+
+--*/
+
+#include "sat/smt/bv_solver.h"
+#include "sat/smt/bv_ackerman.h"
+
+namespace bv {
+
+    ackerman::ackerman(solver& s): s(s) {
+        new_tmp();
+        m_propagate_low_watermark = s.get_config().m_dack_threshold;
+    }
+
+    ackerman::~ackerman() {
+        reset();
+        dealloc(m_tmp_vv);
+    }
+
+    void ackerman::reset() {
+        m_table.reset();
+        m_queue = nullptr;        
+    }
+
+    void ackerman::used_eq_eh(euf::theory_var v1, euf::theory_var v2) {
+        if (v1 == v2)
+            return;
+        if (v1 > v2)
+            std::swap(v1, v2);
+        vv* n = m_tmp_vv;
+        n->v1 = v1;
+        n->v2 = v2;
+        vv* other = m_table.insert_if_not_there(n);        
+        other->m_count++;
+        update_glue(*other);
+        if (other->m_count > m_propagate_high_watermark || other->m_glue == 0)
+            s.s().set_should_simplify();
+        vv::push_to_front(m_queue, other);
+        if (other == n) {
+            new_tmp();        
+            gc();
+        }
+    }
+
+    void ackerman::update_glue(vv& v) {
+        unsigned sz = s.m_bits[v.v1].size();
+        m_diff_levels.reserve(s.s().scope_lvl() + 1, false);
+        unsigned glue = 0;
+        unsigned max_glue = v.m_glue;
+        auto const& bitsa = s.m_bits[v.v1];
+        auto const& bitsb = s.m_bits[v.v2];
+        unsigned i = 0;
+        for (; i < sz && i < max_glue; ++i) {
+            sat::literal a = bitsa[i];
+            sat::literal b = bitsb[i];
+            if (a == b)
+                continue;
+            SASSERT(s.s().value(a) != l_undef);
+            SASSERT(s.s().value(b) == s.s().value(a));
+            unsigned lvl_a = s.s().lvl(a);
+            unsigned lvl_b = s.s().lvl(b);
+            if (!m_diff_levels[lvl_a]) {
+                m_diff_levels[lvl_a] = true;
+                ++glue;
+            }
+            if (!m_diff_levels[lvl_b]) {
+                m_diff_levels[lvl_b] = true;
+                ++glue;
+            }            
+        }
+        for (; i-- > 0; ) {
+            sat::literal a = bitsa[i];
+            sat::literal b = bitsb[i];
+            if (a != b) {
+                m_diff_levels[s.s().lvl(a)] = false;
+                m_diff_levels[s.s().lvl(b)] = false;
+            }
+        }
+        
+        if (glue < max_glue) 
+            v.m_glue = glue <= sz ? 0 : glue;
+    }
+
+    void ackerman::remove(vv* p) {
+        vv::remove_from(m_queue, p);
+        m_table.erase(p);
+        dealloc(p);
+    }
+
+    void ackerman::new_tmp() {
+        m_tmp_vv = alloc(vv);
+        m_tmp_vv->init(m_tmp_vv);
+        m_tmp_vv->m_count = 0;
+        m_tmp_vv->m_glue = UINT_MAX;
+    }
+        
+    void ackerman::gc() {
+        m_num_propagations_since_last_gc++;
+        if (m_num_propagations_since_last_gc <= s.get_config().m_dack_gc) 
+            return;
+        m_num_propagations_since_last_gc = 0;
+        
+        while (m_table.size() > m_gc_threshold) 
+            remove(m_queue->prev());     
+
+        m_gc_threshold *= 110;
+        m_gc_threshold /= 100;
+        m_gc_threshold++;
+    }
+
+    void ackerman::propagate() {
+        SASSERT(s.s().at_base_lvl());
+        auto* n = m_queue;
+        vv* k = nullptr;
+        unsigned num_prop = static_cast<unsigned>(s.s().get_stats().m_conflict * s.get_config().m_dack_factor);
+        num_prop = std::min(num_prop, m_table.size());
+        for (unsigned i = 0; i < num_prop; ++i, n = k) {
+            k = n->next();
+            if (n->m_count < m_propagate_low_watermark && n->m_glue != 0)
+                continue;            
+            add_cc(n->v1, n->v2);
+            remove(n);
+        }
+    }
+
+    void ackerman::add_cc(euf::theory_var v1, euf::theory_var v2) {
+        SASSERT(v1 < v2);
+        if (static_cast<unsigned>(v2) >= s.get_num_vars())
+            return;
+        if (!s.var2enode(v1) || !s.var2enode(v2))
+            return;
+        sort* s1 = s.m.get_sort(s.var2expr(v1));
+        sort* s2 = s.m.get_sort(s.var2expr(v2));
+        if (s1 != s2 || !s.bv.is_bv_sort(s1))
+            return;
+        IF_VERBOSE(0, verbose_stream() << "assert ackerman " << v1 << " " << v2 << "\n");
+        s.assert_ackerman(v1, v2);
+    }
+
+}

src/sat/smt/bv_ackerman.h

@@ -0,0 +1,77 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    euf_ackerman.h
+
+Abstract:
+
+    Ackerman reduction plugin for EUF
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+#pragma once
+
+#include "util/dlist.h"
+#include "sat/smt/atom2bool_var.h"
+#include "sat/smt/sat_th.h"
+
+namespace bv {
+
+    class solver;
+
+    class ackerman {
+
+        struct vv : dll_base<vv> {
+            euf::theory_var v1, v2;
+            unsigned   m_count{ 0 };
+            unsigned   m_glue{ UINT_MAX };
+            vv():v1(euf::null_theory_var), v2(euf::null_theory_var) {}
+            vv(euf::theory_var v1, euf::theory_var v2):v1(v1), v2(v2) {}
+        };
+
+        struct vv_eq {
+            bool operator()(vv const* a, vv const* b) const {
+                return a->v1 == b->v1 && a->v2 == b->v2;
+            }
+        };
+        
+        struct vv_hash {
+            unsigned operator()(vv const* a) const {
+                return mk_mix(a->v1, a->v2, 0);
+            }
+        };
+
+        typedef hashtable<vv*, vv_hash, vv_eq> table_t;
+
+        solver&       s;
+        table_t       m_table;
+        vv*           m_queue { nullptr };
+        vv*           m_tmp_vv { nullptr };
+        unsigned      m_gc_threshold { 1 };
+        unsigned      m_propagate_high_watermark { 10000 };
+        unsigned      m_propagate_low_watermark { 10 };
+        unsigned      m_num_propagations_since_last_gc { 0 };
+        bool_vector   m_diff_levels;
+
+        void update_glue(vv& v);
+        void reset();
+        void new_tmp();
+        void remove(vv* inf);
+        void gc();
+        void add_cc(euf::theory_var v1, euf::theory_var v2);
+
+    public:
+        ackerman(solver& s);
+        ~ackerman();
+
+        void used_eq_eh(euf::theory_var v1, euf::theory_var v2);
+
+        void propagate();
+    };
+
+};

src/sat/smt/bv_internalize.cpp

@@ -22,23 +22,33 @@ Author:
 
 namespace bv {
 
-    class add_var_pos_trail : public trail<euf::solver> {
-        solver::bit_atom * m_atom;
+    solver::bit_atom& solver::atom::to_bit() {
+        SASSERT(is_bit());
+        return dynamic_cast<bit_atom&>(*this);
+    }
+
+    solver::def_atom& solver::atom::to_def() {
+        SASSERT(!is_bit());
+        return dynamic_cast<def_atom&>(*this);
+    }
+
+    class solver::add_var_pos_trail : public trail<euf::solver> {
+        solver::bit_atom* m_atom;
     public:
-        add_var_pos_trail(solver::bit_atom * a):m_atom(a) {}
-        void undo(euf::solver & euf) override {
+        add_var_pos_trail(solver::bit_atom* a) :m_atom(a) {}
+        void undo(euf::solver& euf) override {
             SASSERT(m_atom->m_occs);
             m_atom->m_occs = m_atom->m_occs->m_next;
         }
     };
 
-    class mk_atom_trail : public trail<euf::solver> {
+    class solver::mk_atom_trail : public trail<euf::solver> {
         solver& th;
         sat::bool_var m_var;
     public:
-        mk_atom_trail(sat::bool_var v, solver& th):m_var(v), th(th) {}
-        void undo(euf::solver & euf) override {
-            solver::atom * a = th.get_bv2a(m_var);
+        mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {}
+        void undo(euf::solver& euf) override {
+            solver::atom* a = th.get_bv2a(m_var);
             a->~atom();
             th.erase_bv2a(m_var);
         }
@@ -49,162 +59,152 @@ namespace bv {
         m_find.mk_var();
         m_bits.push_back(sat::literal_vector());
         m_wpos.push_back(0);
-        m_zero_one_bits.push_back(zero_one_bits());
+        m_zero_one_bits.push_back(zero_one_bits());       
         ctx.attach_th_var(n, this, r);
+        
+        TRACE("bv", tout << "mk-var: " << r << " " << n->get_owner_id() << " " << mk_pp(n->get_owner(), m) << "\n";);
         return r;
     }
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
-        if (!visit_rec(m, e, sign, root, redundant))
-            return sat::null_literal;
-        return sat::null_literal;
+    void solver::apply_sort_cnstr(euf::enode * n, sort * s) {
+        get_var(n);
     }
 
-    bool solver::visit(expr* e) {
-        if (!bv.is_bv(e)) {
-            ctx.internalize(e, false, false, m_is_redundant);
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        SASSERT(m.is_bool(e));
+        if (!visit_rec(m, e, sign, root, redundant))
+            return sat::null_literal;
+        return expr2literal(e);
+    }
+
+    void solver::internalize(expr* e, bool redundant) {
+        visit_rec(m, e, false, false, redundant);
+    }
+
+    bool solver::visit(expr* e) {      
+        if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
+            ctx.internalize(e, m_is_redundant);
             return true;
         }
-        m_args.reset();
+        m_stack.push_back(sat::eframe(e));
+        return false;
+    }
+
+    bool solver::visited(expr* e) {
+        euf::enode* n = expr2enode(e);
+        return n && n->is_attached_to(get_id());        
+    }
+
+    bool solver::post_visit(expr* e, bool sign, bool root) {
+        euf::enode* n = expr2enode(e);
         app* a = to_app(e);
-        for (expr* arg : *a) {
-            euf::enode* n = get_enode(arg);
-            if (n)
-                m_args.push_back(n);
-            else
-                m_stack.push_back(sat::eframe(arg));
+        
+        SASSERT(!n || !n->is_attached_to(get_id()));
+        if (!n) {
+            m_args.reset();            
+            if (get_config().m_bv_reflect || m.is_considered_uninterpreted(a->get_decl())) {
+                for (expr* arg : *a)
+                    m_args.push_back(expr2enode(arg));
+            }
+            DEBUG_CODE(for (auto* n : m_args) VERIFY(n););
+            n = ctx.mk_enode(e, m_args.size(), m_args.c_ptr());
+            SASSERT(!n->is_attached_to(get_id()));
+            ctx.attach_node(n);
         }
-        if (m_args.size() != a->get_num_args())
-            return false;
-        if (!smt_params().m_bv_reflect)
-            m_args.reset();
-        euf::enode* n = mk_enode(a, m_args);
-        SASSERT(n->interpreted());
-        theory_var v = n->get_th_var(get_id());
+
+        SASSERT(!n->is_attached_to(get_id()));
+        theory_var v = mk_var(n);
+        SASSERT(n->is_attached_to(get_id()));
+
+        std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits)> bin;
+        std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref& bit)> ebin;
+        std::function<void(unsigned sz, expr* const* xs, expr_ref_vector& bits)> un;
+        std::function<void(unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits)> pun;
+#define internalize_bin(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin);
+#define internalize_un(F) un = [&](unsigned sz, expr* const* xs, expr_ref_vector& bits) { m_bb.F(sz, xs, bits);}; internalize_unary(a, un);
+#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin);
+#define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
+#define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
 
         switch (a->get_decl_kind()) {
-        case OP_BV_NUM:         internalize_num(a, v); break;
-        default:                break;
+        case OP_BV_NUM:           internalize_num(a, v); break;
+        case OP_BNOT:             internalize_un(mk_not); break;
+        case OP_BREDAND:          internalize_un(mk_redand); break;
+        case OP_BREDOR:           internalize_un(mk_redor); break;
+        case OP_BSDIV_I:          internalize_bin(mk_sdiv); break;
+        case OP_BUDIV_I:          internalize_bin(mk_udiv); break;
+        case OP_BUREM_I:          internalize_bin(mk_urem); break;
+        case OP_BSREM_I:          internalize_bin(mk_srem); break;
+        case OP_BSMOD_I:          internalize_bin(mk_smod); break;
+        case OP_BSHL:             internalize_bin(mk_shl); break;
+        case OP_BLSHR:            internalize_bin(mk_lshr); break;
+        case OP_BASHR:            internalize_bin(mk_ashr); break;
+        case OP_EXT_ROTATE_LEFT:  internalize_bin(mk_ext_rotate_left); break;
+        case OP_EXT_ROTATE_RIGHT: internalize_bin(mk_ext_rotate_right); break;
+        case OP_BADD:             internalize_ac(mk_adder); break;
+        case OP_BMUL:             internalize_ac(mk_multiplier); break;
+        case OP_BAND:             internalize_ac(mk_and); break;
+        case OP_BOR:              internalize_ac(mk_or); break;
+        case OP_BXOR:             internalize_ac(mk_xor); break;
+        case OP_BNAND:            internalize_bin(mk_nand); break;
+        case OP_BNOR:             internalize_bin(mk_nor); break;
+        case OP_BXNOR:            internalize_bin(mk_xnor); break;
+        case OP_BCOMP:            internalize_bin(mk_comp); break;
+        case OP_SIGN_EXT:         internalize_pun(mk_sign_extend); break;
+        case OP_ZERO_EXT:         internalize_pun(mk_zero_extend); break;
+        case OP_ROTATE_LEFT:      internalize_pun(mk_rotate_left); break;
+        case OP_ROTATE_RIGHT:     internalize_pun(mk_rotate_right); break;
+        case OP_BUMUL_NO_OVFL:    internalize_nfl(mk_umul_no_overflow); break;
+        case OP_BSMUL_NO_OVFL:    internalize_nfl(mk_smul_no_overflow); break;
+        case OP_BSMUL_NO_UDFL:    internalize_nfl(mk_smul_no_underflow); break;
+        case OP_BIT2BOOL:         internalize_bit2bool(a); break;
+        case OP_ULEQ:             internalize_le<false>(a); break;
+        case OP_SLEQ:             internalize_le<true>(a); break;
+        case OP_XOR3:             internalize_xor3(a); break;
+        case OP_CARRY:            internalize_carry(a); break;
+        case OP_BSUB:             internalize_sub(a); break;
+        case OP_CONCAT:           internalize_concat(a); break;
+        case OP_EXTRACT:          internalize_extract(a); break;
+        case OP_MKBV:             internalize_mkbv(a); break;
+        case OP_INT2BV:           internalize_int2bv(a); break;
+        case OP_BV2INT:           internalize_bv2int(a); break;
+        case OP_BSDIV0:           break;
+        case OP_BUDIV0:           break;
+        case OP_BSREM0:           break;
+        case OP_BUREM0:           break;
+        case OP_BSMOD0:           break;
+        default:
+            UNREACHABLE();
+            break;
         }
         return true;
     }
 
-    bool solver::visited(expr* e) {
-        return get_enode(e) != nullptr;
-    }
-
     void solver::mk_bits(theory_var v) {
         TRACE("bv", tout << "v" << v << "\n";);
-        expr* e = get_expr(v);
+        expr* e = var2expr(v);
         unsigned bv_size = get_bv_size(v);
-        literal_vector& bits = m_bits[v];
-        bits.reset();
+        m_bits[v].reset();
         for (unsigned i = 0; i < bv_size; i++) {
-            expr_ref b2b = mk_bit2bool(e, i);
-            bits.push_back(ctx.internalize(b2b, false, false, m_is_redundant));
+            expr_ref b2b(bv.mk_bit2bool(e, i), m);
+            sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant);
+            m_bits[v].push_back(lit);
         }
     }
 
-    expr_ref solver::mk_bit2bool(expr* e, unsigned idx) {
-        parameter p(idx);
-        expr* args[1] = { e };
-        return expr_ref(m.mk_app(get_id(), OP_BIT2BOOL, 1, &p, 1, args), m);
-    }
-
-#if 0
-        SASSERT(!ctx.b_internalized(n));
-
-        TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";);
-        expr* first_arg = n->get_arg(0);
-
-        if (!ctx.e_internalized(first_arg)) {
-            // This may happen if bit2bool(x) is in a conflict
-            // clause that is being reinitialized, and x was not reinitialized
-            // yet.
-            // So, we internalize x (i.e., arg)
-            ctx.internalize(first_arg, false);
-            SASSERT(ctx.e_internalized(first_arg));
-            // In most cases, when x is internalized, its bits are created.
-            // They are created because x is a bit-vector operation or apply_sort_cnstr is invoked.
-            // However, there is an exception. The method apply_sort_cnstr is not invoked for ite-terms.
-            // So, I execute get_var on the enode attached to first_arg. 
-            // This will force a theory variable to be created if it does not already exist.
-            // This will also force the creation of all bits for x.
-            enode* first_arg_enode = ctx.get_enode(first_arg);
-            get_var(first_arg_enode);
-        }
-
-        enode* arg = ctx.get_enode(first_arg);
-        // The argument was already internalized, but it may not have a theory variable associated with it.
-        // For example, for ite-terms the method apply_sort_cnstr is not invoked.
-        // See comment in the then-branch.
-        theory_var v_arg = arg->get_th_var(get_id());
-        if (v_arg == null_theory_var) {
-            // The method get_var will create a theory variable for arg. 
-            // As a side-effect the bits for arg will also be created.
-            get_var(arg);
-            SASSERT(ctx.b_internalized(n));
-        }
-        else if (!ctx.b_internalized(n)) {
-            SASSERT(v_arg != null_theory_var);
-            bool_var bv = ctx.mk_bool_var(n);
-            ctx.set_var_theory(bv, get_id());
-            bit_atom* a = new (get_region()) bit_atom();
-            insert_bv2a(bv, a);
-            m_trail_stack.push(mk_atom_trail(bv));
-            unsigned idx = n->get_decl()->get_parameter(0).get_int();
-            SASSERT(a->m_occs == 0);
-            a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
-            // Fix for #2182, and SPACER bit-vector
-            if (idx < m_bits[v_arg].size()) {
-                ctx.mk_th_axiom(get_id(), m_bits[v_arg][idx], literal(bv, true));
-                ctx.mk_th_axiom(get_id(), ~m_bits[v_arg][idx], literal(bv, false));
-            }
-        }
-        // axiomatize bit2bool on constants.
-        rational val;
-        unsigned sz;
-        if (m_util.is_numeral(first_arg, val, sz)) {
-            rational bit;
-            unsigned idx = n->get_decl()->get_parameter(0).get_int();
-            div(val, rational::power_of_two(idx), bit);
-            mod(bit, rational(2), bit);
-            literal lit = ctx.get_literal(n);
-            if (bit.is_zero()) lit.neg();
-            ctx.mark_as_relevant(lit);
-            ctx.mk_th_axiom(get_id(), 1, &lit);
-        }
-
-    }
-#endif
-
-
-    euf::enode * solver::mk_enode(expr * n, ptr_vector<euf::enode> const& args) {
-        euf::enode * e = ctx.get_enode(n);
-        if (!e) {
-            e = ctx.mk_enode(n, args.size(), args.c_ptr());
-            mk_var(e);
-        }
-        return e;
-    }
-
     euf::theory_var solver::get_var(euf::enode* n) {
         theory_var v = n->get_th_var(get_id());
         if (v == euf::null_theory_var) {
             v = mk_var(n);
-            mk_bits(v);
+            if (bv.is_bv(n->get_owner())) 
+                mk_bits(v);            
         }
         return v;
     }
 
     euf::enode* solver::get_arg(euf::enode* n, unsigned idx) {
-        if (get_config().m_bv_reflect) {
-            return n->get_arg(idx);
-        }
-        else {
-            expr* arg = n->get_arg(idx)->get_owner();
-            return ctx.get_enode(arg);
-        }
+        app* o = to_app(n->get_owner());
+        return ctx.get_enode(o->get_arg(idx));
     }
 
     inline euf::theory_var solver::get_arg_var(euf::enode* n, unsigned idx) {
@@ -212,20 +212,14 @@ namespace bv {
     }
 
     void solver::get_bits(theory_var v, expr_ref_vector& r) {
-        literal_vector& bits = m_bits[v];
-        for (literal lit : bits) {
-            r.push_back(get_expr(lit));
-        }
+        for (literal lit : m_bits[v]) 
+            r.push_back(literal2expr(lit));        
     }
 
     inline void solver::get_bits(euf::enode* n, expr_ref_vector& r) {
         get_bits(get_var(n), r);
     }
 
-    inline void solver::get_arg_bits(euf::enode* n, unsigned idx, expr_ref_vector& r) {
-        get_bits(get_arg_var(n, idx), r);
-    }
-
     inline void solver::get_arg_bits(app* n, unsigned idx, expr_ref_vector& r) {
         app* arg = to_app(n->get_arg(idx));
         get_bits(ctx.get_enode(arg), r);
@@ -234,7 +228,7 @@ namespace bv {
     void solver::register_true_false_bit(theory_var v, unsigned idx) {
         SASSERT(s().value(m_bits[v][idx]) != l_undef);
         bool is_true = (s().value(m_bits[v][idx]) == l_true);
-        zero_one_bits & bits = m_zero_one_bits[v];
+        zero_one_bits& bits = m_zero_one_bits[v];
         bits.push_back(zero_one_bit(v, idx, is_true));
     }
 
@@ -242,18 +236,22 @@ namespace bv {
        \brief Add bit l to the given variable.
     */
     void solver::add_bit(theory_var v, literal l) {
-        literal_vector & bits = m_bits[v];
-        unsigned idx          = bits.size();
-        bits.push_back(l);
-        if (s().value(l) != l_undef && s().lvl(l) == 0) {
+        unsigned idx = m_bits[v].size();
+        m_bits[v].push_back(l);
+        s().set_external(l.var());
+        set_bit_eh(v, l, idx);
+    }
+
+    void solver::set_bit_eh(theory_var v, literal l, unsigned idx) {
+        if (s().value(l) != l_undef && s().lvl(l) == 0) 
             register_true_false_bit(v, idx);
-        }
         else {
-            atom * a = get_bv2a(l.var());
-            SASSERT(!a || a->is_bit());
-            if (a) {
-                bit_atom* b = static_cast<bit_atom*>(a);
-                find_new_diseq_axioms(b->m_occs, v, idx);
+            atom* a = get_bv2a(l.var());
+            if (a && !a->is_bit()) 
+                ;
+            else if (a) {
+                bit_atom* b = &a->to_bit();
+                find_new_diseq_axioms(*b, v, idx);
                 ctx.push(add_var_pos_trail(b));
                 b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
             }
@@ -261,24 +259,23 @@ namespace bv {
                 bit_atom* b = new (get_region()) bit_atom();
                 insert_bv2a(l.var(), b);
                 ctx.push(mk_atom_trail(l.var(), *this));
-                SASSERT(b->m_occs == 0);
+                SASSERT(!b->m_occs);
                 b->m_occs = new (get_region()) var_pos_occ(v, idx);
             }
         }
     }
 
-    void solver::add_unit(sat::literal lit) {
-        s().add_clause(1, &lit, status());
-    }
-
-    void solver::init_bits(euf::enode * n, expr_ref_vector const & bits) {
+    void solver::init_bits(expr* e, expr_ref_vector const& bits) {
+        euf::enode* n = expr2enode(e);
         SASSERT(get_bv_size(n) == bits.size());
         SASSERT(euf::null_theory_var != n->get_th_var(get_id()));
         theory_var v = n->get_th_var(get_id());
-        unsigned sz = bits.size();
         m_bits[v].reset();
+        for (expr* bit : bits) 
+            add_bit(v, ctx.internalize(bit, false, false, m_is_redundant));        
         for (expr* bit : bits)
-            add_bit(v, get_literal(bit));
+            get_var(expr2enode(bit));
+        SASSERT(get_bv_size(n) == bits.size());
         find_wpos(v);
     }
 
@@ -287,22 +284,23 @@ namespace bv {
     }
 
     unsigned solver::get_bv_size(theory_var v) {
-        return get_bv_size(get_enode(v));
+        return get_bv_size(var2enode(v));
     }
 
     void solver::internalize_num(app* n, theory_var v) {
         numeral val;
         unsigned sz = 0;
+        SASSERT(expr2enode(n)->interpreted());
         VERIFY(bv.is_numeral(n, val, sz));
         expr_ref_vector bits(m);
-        m_bb.num2bits(val, sz, bits); 
-        literal_vector & c_bits = m_bits[v];
+        m_bb.num2bits(val, sz, bits);
         SASSERT(bits.size() == sz);
-        SASSERT(c_bits.empty());
+        SASSERT(m_bits[v].empty());
+        sat::literal true_literal = ctx.internalize(m.mk_true(), false, false, false);
         for (unsigned i = 0; i < sz; i++) {
-            expr * l = bits.get(i);
+            expr* l = bits.get(i);
             SASSERT(m.is_true(l) || m.is_false(l));
-            c_bits.push_back(m.is_true(l) ? true_literal : false_literal);
+            m_bits[v].push_back(m.is_true(l) ? true_literal : ~true_literal);
             register_true_false_bit(v, i);
         }
         fixed_var_eh(v);
@@ -310,14 +308,12 @@ namespace bv {
 
     void solver::internalize_mkbv(app* n) {
         expr_ref_vector bits(m);
-        euf::enode * e = mk_enode(n, m_args);
         bits.append(n->get_num_args(), n->get_args());
-        init_bits(e, bits);
+        init_bits(n, bits);
     }
 
     void solver::internalize_bv2int(app* n) {
-        mk_enode(n, m_args);
-        assert_bv2int_axiom(n);        
+        assert_bv2int_axiom(n);
     }
 
     /**
@@ -325,172 +321,270 @@ namespace bv {
      * n = bv2int(k) = ite(bit2bool(k[sz-1],2^{sz-1},0) + ... + ite(bit2bool(k[0],1,0))
      */
 
-    void solver::assert_bv2int_axiom(app * n) {
-        expr* k = nullptr;
-        sort * int_sort = m.get_sort(n);
-        SASSERT(bv.is_bv2int(n, k));
+    void solver::assert_bv2int_axiom(app* n) {
+        expr* k = nullptr;        
+        VERIFY(bv.is_bv2int(n, k));
         SASSERT(bv.is_bv_sort(m.get_sort(k)));
         expr_ref_vector k_bits(m);
-        euf::enode * k_enode = mk_enode(k, m_args);
+        euf::enode* k_enode = expr2enode(k);
         get_bits(k_enode, k_bits);
         unsigned sz = bv.get_bv_size(k);
         expr_ref_vector args(m);
-        expr_ref zero(bv.mk_numeral(numeral(0), int_sort), m);
-        numeral num(1);
-        for (expr* b : k_bits) {
-            expr_ref n(m_autil.mk_numeral(num, int_sort), m);
-            args.push_back(m.mk_ite(b, n, zero));
-            num *= numeral(2);
-        }
+        expr_ref zero(m_autil.mk_int(0), m);
+        unsigned i = 0;        
+        for (expr* b : k_bits) 
+            args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero));        
         expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m);
         expr_ref eq(m.mk_eq(n, sum), m);
         sat::literal lit = ctx.internalize(eq, false, false, m_is_redundant);
         add_unit(lit);
     }
 
-
     void solver::internalize_int2bv(app* n) {
         SASSERT(bv.is_int2bv(n));
-        euf::enode* e = mk_enode(n, m_args);
-        theory_var v = e->get_th_var(get_id());
-        mk_bits(v);
-        assert_int2bv_axiom(n);        
+        euf::enode* e = expr2enode(n);
+        mk_bits(e->get_th_var(get_id()));
+        assert_int2bv_axiom(n);
     }
 
     /**
      * create the axiom:
-     *   bv2int(n) = e mod 2^bit_width 
+     *   bv2int(n) = e mod 2^bit_width
      * where n = int2bv(e)
      *
      * Create the axioms:
      *   bit2bool(i,n) == ((e div 2^i) mod 2 != 0)
      * for i = 0,.., sz-1
      */
-    void solver::assert_int2bv_axiom(app* n) {        
-        SASSERT(bv.is_int2bv(n));
-        expr* e = n->get_arg(0);
-        euf::enode* n_enode = mk_enode(n, m_args);
-        parameter param(m_autil.mk_int());
-        expr* n_expr = n;
+    void solver::assert_int2bv_axiom(app* n) {
+        expr* e = nullptr;
+        VERIFY(bv.is_int2bv(n, e));      
+        euf::enode* n_enode = expr2enode(n);
         expr_ref lhs(m), rhs(m);
-        lhs = m.mk_app(get_id(), OP_BV2INT, 1, &param, 1, &n_expr);
+        lhs = bv.mk_bv2int(n);
         unsigned sz = bv.get_bv_size(n);
         numeral mod = power(numeral(2), sz);
-        rhs = m_autil.mk_mod(e, m_autil.mk_numeral(mod, true));
+        rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
         expr_ref eq(m.mk_eq(lhs, rhs), m);
-        literal l = ctx.internalize(eq, false, false, m_is_redundant);
-        add_unit(l);
-
         TRACE("bv", tout << eq << "\n";);
-
+        add_unit(ctx.internalize(eq, false, false, m_is_redundant));
+       
         expr_ref_vector n_bits(m);
-        
         get_bits(n_enode, n_bits);
 
         for (unsigned i = 0; i < sz; ++i) {
-            numeral div = power(numeral(2), i);
-            mod = numeral(2);
-            rhs = m_autil.mk_idiv(e, m_autil.mk_numeral(div, true));
-            rhs = m_autil.mk_mod(rhs, m_autil.mk_numeral(mod, true));
-            rhs = m.mk_eq(rhs, m_autil.mk_numeral(rational(1), true));
-            lhs = n_bits.get(i);            
+            numeral div = power2(i);
+            rhs = m_autil.mk_idiv(e, m_autil.mk_int(div));
+            rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2));
+            rhs = m.mk_eq(rhs, m_autil.mk_int(1));
+            lhs = n_bits.get(i);
             expr_ref eq(m.mk_eq(lhs, rhs), m);
             TRACE("bv", tout << eq << "\n";);
-            l = ctx.internalize(eq, false, false, m_is_redundant);
-            add_unit(l);
+            add_unit(ctx.internalize(eq, false, false, m_is_redundant));
         }
     }
 
-
-    void solver::internalize_add(app* n) {}
-    void solver::internalize_sub(app* n) {}
-    void solver::internalize_mul(app* n) {}
-    void solver::internalize_udiv(app* n) {}
-    void solver::internalize_sdiv(app* n) {}
-    void solver::internalize_urem(app* n) {}
-    void solver::internalize_srem(app* n) {}
-    void solver::internalize_smod(app* n) {}
-    void solver::internalize_shl(app* n) {}
-    void solver::internalize_lshr(app* n) {}
-    void solver::internalize_ashr(app* n) {}
-    void solver::internalize_ext_rotate_left(app* n) {}
-    void solver::internalize_ext_rotate_right(app* n) {}
-    void solver::internalize_and(app* n) {}
-    void solver::internalize_or(app* n) {}
-    void solver::internalize_not(app* n) {}
-    void solver::internalize_nand(app* n) {}
-    void solver::internalize_nor(app* n) {}
-    void solver::internalize_xor(app* n) {}
-    void solver::internalize_xnor(app* n) {}
-    void solver::internalize_concat(app* n) {}
-    void solver::internalize_sign_extend(app* n) {}
-    void solver::internalize_zero_extend(app* n) {}
-    void solver::internalize_extract(app* n) {}
-    void solver::internalize_redand(app* n) {}
-    void solver::internalize_redor(app* n) {}
-    void solver::internalize_comp(app* n) {}
-    void solver::internalize_rotate_left(app* n) {}
-    void solver::internalize_rotate_right(app* n) {}
-    void solver::internalize_umul_no_overflow(app* n) {}
-    void solver::internalize_smul_no_overflow(app* n) {}
-    void solver::internalize_smul_no_underflow(app* n) {}
-
-}
-
-
-
-#if 0
-
-        case OP_BADD:           internalize_add(term); return true;
-        case OP_BSUB:           internalize_sub(term); return true;
-        case OP_BMUL:           internalize_mul(term); return true;
-        case OP_BSDIV_I:        internalize_sdiv(term); return true;
-        case OP_BUDIV_I:        internalize_udiv(term); return true;
-        case OP_BSREM_I:        internalize_srem(term); return true;
-        case OP_BUREM_I:        internalize_urem(term); return true;
-        case OP_BSMOD_I:        internalize_smod(term); return true;
-        case OP_BAND:           internalize_and(term); return true;
-        case OP_BOR:            internalize_or(term); return true;
-        case OP_BNOT:           internalize_not(term); return true;
-        case OP_BXOR:           internalize_xor(term); return true;
-        case OP_BNAND:          internalize_nand(term); return true;
-        case OP_BNOR:           internalize_nor(term); return true;
-        case OP_BXNOR:          internalize_xnor(term); return true;
-        case OP_CONCAT:         internalize_concat(term); return true;
-        case OP_SIGN_EXT:       internalize_sign_extend(term); return true;
-        case OP_ZERO_EXT:       internalize_zero_extend(term); return true;
-        case OP_EXTRACT:        internalize_extract(term); return true;
-        case OP_BREDOR:         internalize_redor(term); return true;
-        case OP_BREDAND:        internalize_redand(term); return true;
-        case OP_BCOMP:          internalize_comp(term); return true;
-        case OP_BSHL:           internalize_shl(term); return true;
-        case OP_BLSHR:          internalize_lshr(term); return true;
-        case OP_BASHR:          internalize_ashr(term); return true;
-        case OP_ROTATE_LEFT:    internalize_rotate_left(term); return true;
-        case OP_ROTATE_RIGHT:   internalize_rotate_right(term); return true;
-        case OP_EXT_ROTATE_LEFT:  internalize_ext_rotate_left(term); return true;
-        case OP_EXT_ROTATE_RIGHT: internalize_ext_rotate_right(term); return true;
-        case OP_BSDIV0:         return false;
-        case OP_BUDIV0:         return false;
-        case OP_BSREM0:         return false;
-        case OP_BUREM0:         return false;
-        case OP_BSMOD0:         return false;
-        case OP_MKBV:           internalize_mkbv(term); return true;
-        case OP_INT2BV:
-            if (params().m_bv_enable_int2bv2int) {
-                internalize_int2bv(term);
-            }
-            return params().m_bv_enable_int2bv2int;
-        case OP_BV2INT:
-            if (params().m_bv_enable_int2bv2int) {
-                internalize_bv2int(term);
-            }
-            return params().m_bv_enable_int2bv2int;
-        default:
-            TRACE("bv_op", tout << "unsupported operator: " << mk_ll_pp(term, m) << "\n";);
-            UNREACHABLE();
-            return false;
+    template<bool Signed>
+    void solver::internalize_le(app* n) {
+        SASSERT(n->get_num_args() == 2);
+        expr_ref_vector arg1_bits(m), arg2_bits(m);
+        get_arg_bits(n, 0, arg1_bits);
+        get_arg_bits(n, 1, arg2_bits);
+        expr_ref le(m);
+        if (Signed)
+            m_bb.mk_sle(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), le);
+        else
+            m_bb.mk_ule(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), le);
+        literal def = ctx.internalize(le, false, false, m_is_redundant);
+        add_def(def, expr2literal(n));
     }
 
+    void solver::internalize_carry(app* n) {
+        SASSERT(n->get_num_args() == 3);
+        literal r = ctx.get_literal(n);
+        literal l1 = ctx.get_literal(n->get_arg(0));
+        literal l2 = ctx.get_literal(n->get_arg(1));
+        literal l3 = ctx.get_literal(n->get_arg(2));
+        add_clause(~r, l1, l2);
+        add_clause(~r, l1, l3);
+        add_clause(~r, l2, l3);
+        add_clause(r, ~l1, ~l2);
+        add_clause(r, ~l1, ~l3);
+        add_clause(r, ~l2, ~l3);
+    }
+
+    void solver::internalize_xor3(app* n) {
+        SASSERT(n->get_num_args() == 3);
+        literal r = ctx.get_literal(n);
+        literal l1 = expr2literal(n->get_arg(0));
+        literal l2 = expr2literal(n->get_arg(1));
+        literal l3 = expr2literal(n->get_arg(2));
+        add_clause(~r, l1, l2, l3);
+        add_clause(~r, ~l1, ~l2, l3);
+        add_clause(~r, ~l1, l2, ~l3);
+        add_clause(~r, l1, ~l2, ~l3);
+        add_clause(r, ~l1, l2, l3);
+        add_clause(r, l1, ~l2, l3);
+        add_clause(r, l1, l2, ~l3);
+        add_clause(r, ~l1, ~l2, ~l3);
+    }
+
+    void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) {
+        SASSERT(n->get_num_args() == 1);
+        expr_ref_vector arg1_bits(m), bits(m);
+        get_arg_bits(n, 0, arg1_bits);
+        fn(arg1_bits.size(), arg1_bits.c_ptr(), bits);
+        init_bits(n, bits);
+    }
+
+    void solver::internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn) {
+        SASSERT(n->get_num_args() == 1);
+        expr_ref_vector arg1_bits(m), bits(m);
+        get_arg_bits(n, 0, arg1_bits);
+        unsigned param = n->get_decl()->get_parameter(0).get_int();
+        fn(arg1_bits.size(), arg1_bits.c_ptr(), param, bits);
+        init_bits(n, bits);
+    }
+
+    void solver::internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
+        SASSERT(n->get_num_args() == 2);
+        expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
+        get_arg_bits(n, 0, arg1_bits);
+        get_arg_bits(n, 1, arg2_bits);
+        SASSERT(arg1_bits.size() == arg2_bits.size());
+        fn(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits);
+        init_bits(n, bits);
+    }
+
+    void solver::internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
+        SASSERT(n->get_num_args() >= 2);
+        expr_ref_vector bits(m), new_bits(m), arg_bits(m);
+        unsigned i = n->get_num_args() - 1;        
+        get_arg_bits(n, i, bits);
+        for (; i-- > 0; ) {
+            arg_bits.reset();
+            get_arg_bits(n, i, arg_bits);
+            SASSERT(arg_bits.size() == bits.size());
+            new_bits.reset();
+            fn(arg_bits.size(), arg_bits.c_ptr(), bits.c_ptr(), new_bits);
+            bits.swap(new_bits);
+        }
+        init_bits(n, bits);
+        TRACE("bv_verbose", tout << arg_bits << " " << bits << " " << new_bits << "\n";);
+    }
+
+    void solver::internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn) {
+        SASSERT(n->get_num_args() == 2);
+        expr_ref_vector arg1_bits(m), arg2_bits(m);
+        get_arg_bits(n, 0, arg1_bits);
+        get_arg_bits(n, 1, arg2_bits);
+        expr_ref out(m);
+        fn(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), out);
+        sat::literal def = ctx.internalize(out, false, false, m_is_redundant);
+        add_def(def, ctx.get_literal(n));
+    }
+
+    void solver::add_def(sat::literal def, sat::literal l) {        
+        def_atom* a = new (get_region()) def_atom(l, def);
+        insert_bv2a(l.var(), a);
+        ctx.push(mk_atom_trail(l.var(), *this));
+        add_clause(l, ~def);
+        add_clause(def, ~l);
+    }
+
+    void solver::internalize_concat(app* n) {
+        euf::enode* e = expr2enode(n);
+        theory_var v = e->get_th_var(get_id());
+        m_bits[v].reset();
+        for (unsigned i = n->get_num_args(); i-- > 0; ) 
+            for (literal lit : m_bits[get_arg_var(e, i)]) 
+                add_bit(v, lit);                    
+        find_wpos(v);
+    }
+
+    void solver::internalize_sub(app* n) {
+        SASSERT(n->get_num_args() == 2);
+        expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
+        get_arg_bits(n, 0, arg1_bits);
+        get_arg_bits(n, 1, arg2_bits);
+        SASSERT(arg1_bits.size() == arg2_bits.size());
+        expr_ref carry(m);
+        m_bb.mk_subtracter(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits, carry);
+        init_bits(n, bits);
+    }
+
+    void solver::internalize_extract(app* n) {
+        SASSERT(n->get_num_args() == 1);
+        euf::enode* e = expr2enode(n);
+        theory_var v = e->get_th_var(get_id());
+        theory_var arg = get_arg_var(e, 0);
+        unsigned start = n->get_decl()->get_parameter(1).get_int();
+        unsigned end = n->get_decl()->get_parameter(0).get_int();
+        SASSERT(start <= end && end < get_bv_size(v));
+        m_bits[v].reset();
+        for (unsigned i = start; i <= end; ++i)
+            add_bit(v, m_bits[arg][i]);
+        find_wpos(v);
+    }
+
+    void solver::internalize_bit2bool(app* n) {
+        unsigned idx = 0;
+        expr* arg = nullptr;
+        VERIFY(bv.is_bit2bool(n, arg, idx));
+        euf::enode* argn = expr2enode(arg);
+        if (!argn->is_attached_to(get_id())) {
+            mk_var(argn);
+        }        
+        theory_var v_arg = argn->get_th_var(get_id());
+        sat::literal lit = expr2literal(n);
+        sat::bool_var b = lit.var();
+        bit_atom* a = new (get_region()) bit_atom();
+        SASSERT(idx < get_bv_size(v_arg));
+        a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
+        insert_bv2a(b, a);
+        ctx.push(mk_atom_trail(b, *this));           
+        if (idx < m_bits[v_arg].size() && lit != m_bits[v_arg][idx]) {
+            add_clause(m_bits[v_arg][idx], ~lit);
+            add_clause(~m_bits[v_arg][idx], lit);
+        }
+        // axiomatize bit2bool on constants.
+        rational val;
+        unsigned sz;
+        if (bv.is_numeral(arg, val, sz)) {
+            rational bit;
+            div(val, rational::power_of_two(idx), bit);
+            mod(bit, rational(2), bit);
+            if (bit.is_zero()) lit.neg();
+            add_unit(lit);
+        }
+    }
+
+    void solver::assert_ackerman(theory_var v1, theory_var v2) {
+        flet<bool> _red(m_is_redundant, true);
+        ++m_stats.m_ackerman;
+        expr* o1 = var2expr(v1);
+        expr* o2 = var2expr(v2);
+        expr_ref oe(m.mk_eq(o1, o2), m);
+        literal oeq = ctx.internalize(oe, false, false, m_is_redundant);
+        unsigned sz = get_bv_size(v1);
+        TRACE("bv", tout << oe << "\n";);
+        literal_vector eqs;
+        for (unsigned i = 0; i < sz; ++i) {
+            literal l1 = m_bits[v1][i];
+            literal l2 = m_bits[v2][i];
+            expr_ref e1(m), e2(m);
+            e1 = bv.mk_bit2bool(o1, i);
+            e2 = bv.mk_bit2bool(o2, i);
+            expr_ref e(m.mk_eq(e1, e2), m);
+            literal eq = ctx.internalize(e, false, false, m_is_redundant);
+            add_clause(l1, ~l2, ~eq);
+            add_clause(~l1, l2, ~eq);
+            add_clause(l1, l2, eq);
+            add_clause(~l1, ~l2, eq);
+            add_clause(eq, ~oeq);
+            eqs.push_back(~eq);
+        }
+        eqs.push_back(oeq);
+        s().add_clause(eqs.size(), eqs.c_ptr(), sat::status::th(m_is_redundant, get_id()));
+    }
 }
-#endif

src/sat/smt/bv_solver.cpp

@@ -3,18 +3,20 @@ Copyright (c) 2020 Microsoft Corporation
 
 Module Name:
 
-    bv_internalize.cpp
+    bv_solver.cpp
 
 Abstract:
 
-    Internalize utilities for bit-vector solver plugin.
+    Solving utilities for bit-vectors.
 
 Author:
 
     Nikolaj Bjorner (nbjorner) 2020-09-02
+    based on smt/theory_bv
 
 --*/
 
+#include "ast/ast_ll_pp.h"
 #include "sat/smt/bv_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
@@ -22,52 +24,110 @@ Author:
 
 namespace bv {
 
-    void solver::fixed_var_eh(theory_var v) {
-        
+    class solver::bit_trail : public trail<euf::solver> {
+        solver& s;
+        solver::var_pos vp;
+        sat::literal lit;
+    public:
+        bit_trail(solver& s, var_pos vp) : s(s), vp(vp), lit(s.m_bits[vp.first][vp.second]) {}
+
+        virtual void undo(euf::solver& euf) {
+            s.m_bits[vp.first][vp.second] = lit;
+        }
+    };
+
+    solver::solver(euf::solver& ctx, theory_id id) :
+        euf::th_euf_solver(ctx, id),
+        bv(m),
+        m_autil(m),
+        m_ackerman(*this),
+        m_bb(m, get_config()),
+        m_find(*this) {
+    }
+
+    void solver::fixed_var_eh(theory_var v1) {
+        numeral val1, val2;
+        VERIFY(get_fixed_value(v1, val1));
+        unsigned sz = m_bits[v1].size();
+        value_sort_pair key(val1, sz);
+        theory_var v2;
+        bool is_current =
+            m_fixed_var_table.find(key, v2) &&
+            v2 < static_cast<int>(get_num_vars()) &&
+            is_bv(v2) &&
+            get_bv_size(v2) == sz &&
+            get_fixed_value(v2, val2) && val1 == val2;
+
+        if (!is_current)
+            m_fixed_var_table.insert(key, v1);
+        else if (var2enode(v1)->get_root() != var2enode(v2)->get_root()) {
+            SASSERT(get_bv_size(v1) == get_bv_size(v2));
+            TRACE("bv", tout << "detected equality: v" << v1 << " = v" << v2 << "\n" << pp(v1) << pp(v2););
+            m_stats.m_num_th2core_eq++;
+            add_fixed_eq(v1, v2);
+            ctx.propagate(var2enode(v1), var2enode(v2), mk_bit2bv_justification(v1, v2));
+        }
+    }
+
+    void solver::add_fixed_eq(theory_var v1, theory_var v2) {
+        if (!get_config().m_bv_eq_axioms)
+            return;
+        m_ackerman.used_eq_eh(v1, v2);
+    }
+
+    bool solver::get_fixed_value(theory_var v, numeral& result) const {
+        result.reset();
+        unsigned i = 0;
+        for (literal b : m_bits[v]) {
+            switch (ctx.s().value(b)) {
+            case l_false:
+                break;
+            case l_undef:
+                return false;
+            case l_true:
+                result += power2(i);
+                break;
+            }
+            ++i;
+        }
+        return true;
     }
 
     /**
        \brief Find an unassigned bit for m_wpos[v], if such bit cannot be found invoke fixed_var_eh
     */
     void solver::find_wpos(theory_var v) {
-        literal_vector const & bits = m_bits[v];
-        unsigned sz                 = bits.size();
-        unsigned & wpos             = m_wpos[v];
-        unsigned init               = wpos;
-        for (; wpos < sz; wpos++) {
-            TRACE("find_wpos", tout << "curr bit: " << bits[wpos] << "\n";);
-            if (s().value(bits[wpos]) == l_undef) {
-                TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";);
+        literal_vector const& bits = m_bits[v];
+        unsigned sz = bits.size();
+        unsigned& wpos = m_wpos[v];
+        for (unsigned i = 0; i < sz; ++i) {
+            unsigned idx = (i + wpos) % sz;
+            if (s().value(bits[idx]) == l_undef) {
+                wpos = idx;
+                TRACE("bv", tout << "moved wpos of v" << v << " to " << wpos << "\n";);
                 return;
             }
         }
-        wpos = 0;
-        for (; wpos < init; wpos++) {
-            if (s().value(bits[wpos]) == l_undef) {
-                TRACE("find_wpos", tout << "moved wpos of v" << v << " to " << wpos << "\n";);
-                return;
-            }
-        }
-        TRACE("find_wpos", tout << "v" << v << " is a fixed variable.\n";);
+        TRACE("bv", tout << "v" << v << " is a fixed variable.\n";);
         fixed_var_eh(v);
     }
 
     /**
-   \brief v[idx] = ~v'[idx], then v /= v' is a theory axiom.
-*/
-    void solver::find_new_diseq_axioms(var_pos_occ* occs, theory_var v, unsigned idx) {
+     *\brief v[idx] = ~v'[idx], then v /= v' is a theory axiom.
+    */
+    void solver::find_new_diseq_axioms(bit_atom& a, theory_var v, unsigned idx) {
+        if (!get_config().m_bv_eq_axioms)
+            return;
         literal l = m_bits[v][idx];
         l.neg();
-        while (occs) {
-            theory_var v2 = occs->m_var;
-            unsigned   idx2 = occs->m_idx;
+        for (auto vp : a) {
+            theory_var v2 = vp.first;
+            unsigned   idx2 = vp.second;
             if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v))
                 mk_new_diseq_axiom(v, v2, idx);
-            occs = occs->m_next;
         }
     }
 
-
     /**
        \brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom.
     */
@@ -78,60 +138,533 @@ namespace bv {
         // TBD: disabled until new literal creation is supported
         return;
         SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
-        TRACE("bv_solver", tout << "found new diseq axiom\n" << pp(v1) << pp(v2);); 
+        TRACE("bv", tout << "found new diseq axiom\n" << pp(v1) << pp(v2););
         m_stats.m_num_diseq_static++;
-        expr_ref eq(m.mk_eq(get_expr(v1), get_expr(v2)), m);
-        sat::literal neq = ctx.internalize(eq, true, false, m_is_redundant);
-        s().add_clause(1, &neq, sat::status::th(m_is_redundant, get_id()));
+        expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m);
+        add_unit(~ctx.internalize(eq, false, false, m_is_redundant));
     }
 
     std::ostream& solver::display(std::ostream& out, theory_var v) const {
+        expr* e = var2expr(v);
         out << "v";
         out.width(4);
         out << std::left << v;
-        out << " #";
+        out << " ";
         out.width(4);
-        out << get_enode(v)->get_owner_id() << " -> #";
+        out << e->get_id() << " -> ";
         out.width(4);
-#if 0
-        out << get_enode(find(v))->get_owner_id();
-        out << std::right << ", bits:";
-        literal_vector const& bits = m_bits[v];
-        for (literal lit : bits) {
-            out << " " << lit << ":";
-            ctx.display_literal(out, lit);
+        out << var2enode(find(v))->get_owner_id();
+        out << std::right;
+        out.flush();
+        atom* a = nullptr;
+        if (is_bv(v)) {
+            numeral val;
+            if (get_fixed_value(v, val))
+                out << " (= " << val << ")";
+            for (literal lit : m_bits[v]) {
+                out << " " << lit << ":" << mk_bounded_pp(literal2expr(lit), m, 1);
+            }
         }
-        numeral val;
-        if (get_fixed_value(v, val))
-            out << ", value: " << val;
+        else if (m.is_bool(e) && (a = m_bool_var2atom.get(expr2literal(e).var(), nullptr))) {
+            if (a->is_bit()) {
+                for (var_pos vp : a->to_bit())
+                    out << " " << var2enode(vp.first)->get_owner_id() << "[" << vp.second << "]";
+            }
+            else
+                out << "def-atom";
+        }
+        else
+            out << " " << mk_bounded_pp(e, m, 1);
         out << "\n";
-#endif
         return out;
     }
 
+    void solver::new_eq_eh(euf::th_eq const& eq) {
+        TRACE("bv", tout << "new eq " << eq.m_v1 << " == " << eq.m_v2 << "\n";);
+        if (is_bv(eq.m_v1))
+            m_find.merge(eq.m_v1, eq.m_v2);
+    }
+
     double solver::get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const { return 0; }
     bool solver::is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) { return false; }
     bool solver::is_external(bool_var v) { return true; }
     bool solver::propagate(literal l, sat::ext_constraint_idx idx) { return false; }
-    void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r) {}
-    void solver::asserted(literal l) {}
-    sat::check_result solver::check() { return sat::check_result::CR_DONE; }
-    void solver::push() {}
-    void solver::pop(unsigned n) {}
+
+    void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
+        auto& c = bv_justification::from_index(idx);
+        TRACE("bv", display_constraint(tout, idx););
+        switch (c.m_kind) {
+        case bv_justification::kind_t::bv2bit:
+            r.push_back(c.m_antecedent);
+            ctx.add_antecedent(var2enode(c.m_v1), var2enode(c.m_v2));
+            break;
+        case bv_justification::kind_t::bit2bv:
+            SASSERT(m_bits[c.m_v1].size() == m_bits[c.m_v2].size());
+            for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
+                sat::literal a = m_bits[c.m_v1][i];
+                sat::literal b = m_bits[c.m_v2][i];
+                SASSERT(a == b || s().value(a) != l_undef);
+                SASSERT(s().value(a) == s().value(b));
+                if (a == b)
+                    continue;
+                if (s().value(a) == l_false) {
+                    a.neg();
+                    b.neg();
+                }
+                r.push_back(a);
+                r.push_back(b);
+            }
+            break;
+        }
+        if (!probing && ctx.use_drat())
+            log_drat(c);
+    }
+
+    void solver::log_drat(bv_justification const& c) {
+        // this has a side-effect so changes provability:
+        expr_ref eq(m.mk_eq(var2expr(c.m_v1), var2expr(c.m_v2)), m);
+        sat::literal leq = ctx.internalize(eq, false, false, false);
+        sat::literal_vector lits;
+        auto add_bit = [&](sat::literal lit) {
+            if (s().value(lit) == l_true)
+                lit.neg();
+            lits.push_back(lit);
+        };
+        switch (c.m_kind) {
+        case bv_justification::kind_t::bv2bit:
+            lits.push_back(~leq);
+            lits.push_back(~c.m_antecedent);
+            lits.push_back(c.m_consequent);
+            break;
+        case bv_justification::kind_t::bit2bv:
+            lits.push_back(leq);
+            for (unsigned i = m_bits[c.m_v1].size(); i-- > 0; ) {
+                sat::literal a = m_bits[c.m_v1][i];
+                sat::literal b = m_bits[c.m_v2][i];
+                if (a != b) {
+                    add_bit(a);
+                    add_bit(b);
+                }
+            }
+            break;
+        }
+        ctx.get_drat().add(lits, status());
+    }
+
+    void solver::asserted(literal l) {
+        atom* a = get_bv2a(l.var());
+        TRACE("bv", tout << "asserted: " << l << "\n";);
+        if (a->is_bit())
+            for (auto vp : a->to_bit())
+                m_prop_queue.push_back(vp);
+    }
+
+    bool solver::unit_propagate() {
+        if (m_prop_queue_head == m_prop_queue.size())
+            return false;
+        ctx.push(value_trail<euf::solver, unsigned>(m_prop_queue_head));
+        for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head)
+            propagate_bits(m_prop_queue[m_prop_queue_head]);
+        return true;
+    }
+
+    void solver::propagate_bits(var_pos entry) {
+        theory_var v1 = entry.first;
+        unsigned idx = entry.second;
+        SASSERT(idx < m_bits[v1].size());
+        if (m_wpos[v1] == idx)
+            find_wpos(v1);
+
+        literal bit1 = m_bits[v1][idx];
+        lbool   val = s().value(bit1);
+        TRACE("bv", tout << "propagating v" << v1 << " #" << var2enode(v1)->get_owner_id() << "[" << idx << "] = " << val << "\n";);
+        if (val == l_undef)
+            return;
+
+        if (val == l_false)
+            bit1.neg();
+
+        for (theory_var v2 = m_find.next(v1); v2 != v1 && !s().inconsistent(); v2 = m_find.next(v2)) {
+            literal bit2 = m_bits[v2][idx];
+            SASSERT(m_bits[v1][idx] != ~m_bits[v2][idx]);
+            TRACE("bv", tout << "propagating #" << var2enode(v2)->get_owner_id() << "[" << idx << "] = " << s().value(bit2) << "\n";);
+
+            if (val == l_false)
+                bit2.neg();
+            if (l_true != s().value(bit2))
+                assign_bit(bit2, v1, v2, idx, bit1, false);
+        }
+    }
+
+    sat::check_result solver::check() {
+        SASSERT(m_prop_queue.size() == m_prop_queue_head);
+        return sat::check_result::CR_DONE;
+    }
+
+    void solver::push() {
+        th_euf_solver::lazy_push();
+        m_prop_queue_lim.push_back(m_prop_queue.size());
+    }
+
+    void solver::pop(unsigned n) {
+        unsigned old_sz = m_prop_queue_lim.size() - n;
+        m_prop_queue.shrink(m_prop_queue_lim[old_sz]);
+        m_prop_queue_lim.shrink(old_sz);
+        n = lazy_pop(n);
+        if (n > 0) {
+            old_sz = get_num_vars();
+            m_bits.shrink(old_sz);
+            m_wpos.shrink(old_sz);
+            m_zero_one_bits.shrink(old_sz);
+        }
+    }
+
     void solver::pre_simplify() {}
-    void solver::simplify() {}
+
+    void solver::simplify() {
+        m_ackerman.propagate();
+    }
+
+    bool solver::set_root(literal l, literal r) {
+        atom* a = get_bv2a(l.var());
+        if (!a || !a->is_bit())
+            return true;
+        for (auto vp : a->to_bit()) {
+            sat::literal l2 = m_bits[vp.first][vp.second];
+            sat::literal r2 = (l.sign() == l2.sign()) ? r : ~r;
+            SASSERT(l2.var() == l.var());
+            ctx.push(bit_trail(*this, vp));
+            m_bits[vp.first][vp.second] = r2;
+            set_bit_eh(vp.first, r2, vp.second);
+        }
+        return true;
+    }
+
+    /**
+    * Instantiate Ackerman axioms for bit-vectors that have become equal after roots have been added.
+    */
+    void solver::flush_roots() {
+        struct eq {
+            solver& s;
+            eq(solver& s) :s(s) {}
+            bool operator()(theory_var v1, theory_var v2) const {
+                return s.m_bits[v1] == s.m_bits[v2];
+            }
+        };
+        struct hash {
+            solver& s;
+            hash(solver& s) :s(s) {}
+            bool operator()(theory_var v) const {
+                literal_vector const& a = s.m_bits[v];
+                return string_hash(reinterpret_cast<char*>(a.c_ptr()), a.size() * sizeof(sat::literal), 3);
+            }
+        };
+        eq eq_proc(*this);
+        hash hash_proc(*this);
+        map<theory_var, theory_var, hash, eq> table(hash_proc, eq_proc);
+        for (unsigned v = 0; v < get_num_vars(); ++v) {
+            if (!m_bits[v].empty()) {
+                theory_var w = table.insert_if_not_there(v, v);
+                if (v != w && m_find.find(v) != m_find.find(w))
+                    assert_ackerman(v, w);
+            }
+        }    
+        TRACE("bv", tout << "infer new equations for bit-vectors that are now equal\n";);
+    }
+
     void solver::clauses_modifed() {}
     lbool solver::get_phase(bool_var v) { return l_undef; }
-    std::ostream& solver::display(std::ostream& out) const { return out; }
-    std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { return out; }
-    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { return out; }
-    void solver::collect_statistics(statistics& st) const {}
-    sat::extension* solver::copy(sat::solver* s) { return nullptr; }
+    std::ostream& solver::display(std::ostream& out) const {
+        unsigned num_vars = get_num_vars();
+        if (num_vars > 0)
+            out << "bv-solver:\n";
+        for (unsigned v = 0; v < num_vars; v++)
+            out << pp(v);
+        return out;
+    }
+
+    std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const {
+        return display_constraint(out, idx);
+    }
+
+    std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
+        auto& c = bv_justification::from_index(idx);
+        switch (c.m_kind) {
+        case bv_justification::kind_t::bv2bit:
+            return out << c.m_consequent << " <= " << c.m_antecedent << " v" << c.m_v1 << " == v" << c.m_v2 << "\n";
+        case bv_justification::kind_t::bit2bv:
+            return out << m_bits[c.m_v1] << " == " << m_bits[c.m_v2] << " => v" << c.m_v1 << " == v" << c.m_v2 << "\n";
+        default:
+            UNREACHABLE();
+            break;
+        }
+        return out;
+    }
+
+    void solver::collect_statistics(statistics& st) const {
+        st.update("bv conflicts", m_stats.m_num_conflicts);
+        st.update("bv diseqs", m_stats.m_num_diseq_static);
+        st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
+        st.update("bv bit2core", m_stats.m_num_bit2core);
+        st.update("bv->core eq", m_stats.m_num_th2core_eq);
+        st.update("bv ackerman", m_stats.m_ackerman);
+    }
+
+    sat::extension* solver::copy(sat::solver* s) { UNREACHABLE(); return nullptr; }
+
+    euf::th_solver* solver::fresh(sat::solver* s, euf::solver& ctx) {
+        bv::solver* result = alloc(bv::solver, ctx, get_id());
+        ast_translation tr(m, ctx.get_manager());
+        for (unsigned i = 0; i < get_num_vars(); ++i) {
+            expr* e1 = var2expr(i);
+            expr* e2 = tr(e1);
+            euf::enode* n2 = ctx.get_enode(e2);
+            SASSERT(n2);
+            result->mk_var(n2);
+            result->m_bits[i].append(m_bits[i]);
+            result->m_zero_one_bits[i].append(m_zero_one_bits[i]);
+        }
+        for (unsigned i = 0; i < get_num_vars(); ++i)
+            if (find(i) != i)
+                result->m_find.merge(i, find(i));
+        result->m_prop_queue.append(m_prop_queue);
+        for (unsigned i = 0; i < m_bool_var2atom.size(); ++i) {
+            atom* a = m_bool_var2atom[i];
+            if (!a)
+                continue;
+
+            if (a->is_bit()) {
+                bit_atom* new_a = new (result->get_region()) bit_atom();
+                m_bool_var2atom.setx(i, new_a, nullptr);
+                for (auto vp : a->to_bit())
+                    new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs);
+            }
+            else {
+                def_atom* new_a = new (result->get_region()) def_atom(a->to_def().m_var, a->to_def().m_def);
+                m_bool_var2atom.setx(i, new_a, nullptr);
+            }
+        }
+        return result;
+    }
+
     void solver::pop_reinit() {}
     bool solver::validate() { return true; }
     void solver::init_use_list(sat::ext_use_list& ul) {}
     bool solver::is_blocked(literal l, sat::ext_constraint_idx) { return false; }
     bool solver::check_model(sat::model const& m) const { return true; }
-    unsigned solver::max_var(unsigned w) const { return 0;}
- 
+    unsigned solver::max_var(unsigned w) const { return w; }
+
+    void solver::add_value(euf::enode* n, expr_ref_vector& values) {
+        SASSERT(bv.is_bv(n->get_owner()));
+        theory_var v = n->get_th_var(get_id());
+        rational val;
+        unsigned i = 0;
+        for (auto l : m_bits[v]) {
+            switch (s().value(l)) {
+            case l_true:
+                val += power2(i);
+                break;
+            default:
+                break;
+            }
+            ++i;
+        }
+        values[n->get_root_id()] = bv.mk_numeral(val, m_bits[v].size());
+    }
+
+    trail_stack<euf::solver>& solver::get_trail_stack() {
+        return ctx.get_trail_stack();
+    }
+
+    void solver::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
+        TRACE("bv", tout << "merging: v" << v1 << " #" << var2enode(v1)->get_owner_id() << " v" << v2 << " #" << var2enode(v2)->get_owner_id() << "\n";);
+        if (!merge_zero_one_bits(r1, r2)) {
+            TRACE("bv", tout << "conflict detected\n";);
+            return; // conflict was detected
+        }
+        SASSERT(m_bits[v1].size() == m_bits[v2].size());
+        unsigned sz = m_bits[v1].size();
+        for (unsigned idx = 0; !s().inconsistent() && idx < sz; idx++) {
+            literal bit1 = m_bits[v1][idx];
+            literal bit2 = m_bits[v2][idx];
+            CTRACE("bv", bit1 == ~bit2, tout << pp(v1) << pp(v2) << "idx: " << idx << "\n";);
+            SASSERT(bit1 != ~bit2);
+            lbool val1 = s().value(bit1);
+            lbool val2 = s().value(bit2);
+            TRACE("bv", tout << "merge v" << v1 << " " << bit1 << ":= " << val1 << " " << bit2 << ":= " << val2 << "\n";);
+            if (val1 == val2)
+                continue;
+            CTRACE("bv", (val1 != l_undef && val2 != l_undef), tout << "inconsistent "; tout << pp(v1) << pp(v2) << "idx: " << idx << "\n";);
+            if (val1 == l_false)
+                assign_bit(~bit2, v1, v2, idx, ~bit1, true);
+            else if (val1 == l_true)
+                assign_bit(bit2, v1, v2, idx, bit1, true);
+            else if (val2 == l_false)
+                assign_bit(~bit1, v2, v1, idx, ~bit2, true);
+            else if (val2 == l_true)
+                assign_bit(bit1, v2, v1, idx, bit2, true);
+        }
+    }
+
+    sat::justification solver::mk_bv2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) {
+        void* mem = get_region().allocate(bv_justification::get_obj_size());
+        sat::constraint_base::initialize(mem, this);
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2, c, a);
+        return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index());
+    }
+
+    sat::ext_justification_idx solver::mk_bit2bv_justification(theory_var v1, theory_var v2) {
+        void* mem = get_region().allocate(bv_justification::get_obj_size());
+        sat::constraint_base::initialize(mem, this);
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2);
+        return constraint->to_index();
+    }
+
+    void solver::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
+        m_stats.m_num_bit2core++;
+        SASSERT(ctx.s().value(antecedent) == l_true);
+        SASSERT(m_bits[v2][idx].var() == consequent.var());
+        SASSERT(consequent.var() != antecedent.var());
+        s().assign(consequent, mk_bv2bit_justification(v1, v2, consequent, antecedent));
+        if (s().value(consequent) == l_false) {
+            m_stats.m_num_conflicts++;
+            SASSERT(s().inconsistent());
+        }
+        else {
+            if (get_config().m_bv_eq_axioms && false) {
+                // TODO - enable when pop_reinit is available
+                expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m);
+                flet<bool> _is_redundant(m_is_redundant, true);
+                literal eq_lit = ctx.internalize(eq, false, false, m_is_redundant);
+                add_clause(~antecedent, ~eq_lit, consequent);
+                add_clause(antecedent, ~eq_lit, ~consequent);
+            }
+
+            if (m_wpos[v2] == idx)
+                find_wpos(v2);
+            bool_var cv = consequent.var();
+            atom* a = get_bv2a(cv);
+            if (a && a->is_bit())
+                for (auto curr : a->to_bit())
+                    if (propagate_eqc || find(curr.first) != find(v2) || curr.second != idx) 
+                        m_prop_queue.push_back(curr);                    
+        }
+    }
+
+    void solver::unmerge_eh(theory_var v1, theory_var v2) {
+        // v1 was the root of the equivalence class
+        // I must remove the zero_one_bits that are from v2.
+        zero_one_bits& bits = m_zero_one_bits[v1];
+        if (bits.empty())
+            return;
+        for (unsigned j = bits.size(); j-- > 0; ) {
+            zero_one_bit& bit = bits[j];
+            if (find(bit.m_owner) == v1) {
+                bits.shrink(j + 1);
+                return;
+            }
+        }
+        bits.shrink(0);
+    }
+
+    bool solver::merge_zero_one_bits(theory_var r1, theory_var r2) {
+        zero_one_bits& bits2 = m_zero_one_bits[r2];
+        if (bits2.empty())
+            return true;
+        zero_one_bits& bits1 = m_zero_one_bits[r1];
+        unsigned bv_size = get_bv_size(r1);
+        SASSERT(bv_size == get_bv_size(r2));
+        m_merge_aux[0].reserve(bv_size + 1, euf::null_theory_var);
+        m_merge_aux[1].reserve(bv_size + 1, euf::null_theory_var);
+
+        struct scoped_reset {
+            solver& s;
+            zero_one_bits& bits1;
+            scoped_reset(solver& s, zero_one_bits& bits1) :s(s), bits1(bits1) {}
+            ~scoped_reset() {
+                for (auto& zo : bits1)
+                    s.m_merge_aux[zo.m_is_true][zo.m_idx] = euf::null_theory_var;
+            }
+        };
+        scoped_reset _sr(*this, bits1);
+
+        DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) SASSERT(m_merge_aux[0][i] == euf::null_theory_var || m_merge_aux[1][i] == euf::null_theory_var););
+
+        // save info about bits1
+        for (auto& zo : bits1)
+            m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner;
+        // check if bits2 is consistent with bits1, and copy new bits to bits1
+        for (auto& zo : bits2) {
+            theory_var v2 = zo.m_owner;
+            theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx];
+            if (v1 != euf::null_theory_var) {
+                // conflict was detected ... v1 and v2 have complementary bits
+                SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
+                SASSERT(m_bits[v1].size() == m_bits[v2].size());
+                mk_new_diseq_axiom(v1, v2, zo.m_idx);
+                return false;
+            }
+            // copy missing variable to bits1
+            if (m_merge_aux[zo.m_is_true][zo.m_idx] == euf::null_theory_var)
+                bits1.push_back(zo);
+        }
+        // reset m_merge_aux vector
+        DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == euf::null_theory_var || m_merge_aux[1][i] == euf::null_theory_var); });
+        return true;
+    }
+
+    rational const& solver::power2(unsigned i) const {
+        while (m_power2.size() <= i)
+            m_power2.push_back(m_bb.power(m_power2.size()));
+        return m_power2[i];
+    }
+
+    /**
+        \brief Check whether m_zero_one_bits is an accurate summary of the bits in the
+        equivalence class rooted by v.
+        \remark The method does nothing if v is not the root of the equivalence class.
+    */
+    bool solver::check_zero_one_bits(theory_var v) {
+        if (s().inconsistent())
+            return true; // property is only valid if the context is not in a conflict.
+        if (!is_root(v) || !is_bv(v))
+            return true;
+        bool_vector bits[2];
+        unsigned      num_bits = 0;
+        unsigned      bv_sz = get_bv_size(v);
+        bits[0].resize(bv_sz, false);
+        bits[1].resize(bv_sz, false);
+
+        theory_var curr = v;
+        do {
+            literal_vector const& lits = m_bits[curr];
+            for (unsigned i = 0; i < lits.size(); i++) {
+                literal l = lits[i];
+                if (s().value(l) != l_undef) {
+                    unsigned is_true = s().value(l) == l_true;
+                    if (bits[!is_true][i]) {
+                        // expect a conflict later on.
+                        return true;
+                    }
+                    if (!bits[is_true][i]) {
+                        bits[is_true][i] = true;
+                        num_bits++;
+                    }
+                }
+            }
+            curr = m_find.next(curr);
+        } while (curr != v);
+
+        zero_one_bits const& _bits = m_zero_one_bits[v];
+        SASSERT(_bits.size() == num_bits);
+        bool_vector already_found;
+        already_found.resize(bv_sz, false);
+        for (auto& zo : _bits) {
+            SASSERT(find(zo.m_owner) == v);
+            SASSERT(bits[zo.m_is_true][zo.m_idx]);
+            SASSERT(!already_found[zo.m_idx]);
+            already_found[zo.m_idx] = true;
+        }
+        return true;
+    }
 }

src/sat/smt/bv_solver.h

@@ -17,8 +17,13 @@ Author:
 #pragma once
 
 #include "sat/smt/sat_th.h"
+#include "sat/smt/bv_ackerman.h"
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
 
+namespace euf {
+    class solver;
+}
+
 namespace bv {
 
     class solver : public euf::th_euf_solver {
@@ -32,15 +37,42 @@ namespace bv {
         typedef std::pair<numeral, unsigned> value_sort_pair;
         typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
         typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
-        typedef union_find<solver>  th_union_find;
+        typedef union_find<solver, euf::solver>  bv_union_find;
+        typedef std::pair<theory_var, unsigned> var_pos;
+
+        friend class ackerman;
 
         struct stats {
             unsigned   m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
-            unsigned   m_num_eq_dynamic;
+            unsigned   m_ackerman;
             void reset() { memset(this, 0, sizeof(stats)); }
             stats() { reset(); }
         };
 
+        struct bv_justification {
+            enum kind_t { bv2bit, bit2bv };
+            kind_t     m_kind;
+            theory_var m_v1;
+            theory_var m_v2;
+            sat::literal m_consequent;
+            sat::literal m_antecedent;
+            bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
+                m_kind(kind_t::bv2bit), m_v1(v1), m_v2(v2), m_consequent(c), m_antecedent(a) {}
+            bv_justification(theory_var v1, theory_var v2):
+                m_kind(kind_t::bit2bv), m_v1(v1), m_v2(v2) {}
+            sat::ext_constraint_idx to_index() const { 
+                return sat::constraint_base::mem2base(this); 
+            }
+            static bv_justification& from_index(size_t idx) {
+                return *reinterpret_cast<bv_justification*>(sat::constraint_base::from_index(idx)->mem());
+            }
+            static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(bv_justification)); }
+        };
+
+        sat::justification mk_bv2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a);
+        sat::ext_justification_idx mk_bit2bv_justification(theory_var v1, theory_var v2);
+        void log_drat(bv_justification const& c);
+ 
 
         /**
            \brief Structure used to store the position of a bitvector variable that
@@ -66,17 +98,31 @@ namespace bv {
 
         typedef svector<zero_one_bit> zero_one_bits;
 
+        struct bit_atom;
+        struct def_atom;
         class atom {
         public:
             virtual ~atom() {}
             virtual bool is_bit() const = 0;
+            bit_atom& to_bit();
+            def_atom& to_def();
         };
 
         struct var_pos_occ {
-            theory_var    m_var;
-            unsigned      m_idx;
+            var_pos       m_vp;
             var_pos_occ * m_next;
-            var_pos_occ(theory_var v = euf::null_theory_var, unsigned idx = 0, var_pos_occ * next = nullptr):m_var(v), m_idx(idx), m_next(next) {}
+            var_pos_occ(theory_var v = euf::null_theory_var, unsigned idx = 0, var_pos_occ * next = nullptr):m_vp(v, idx), m_next(next) {}
+        };
+
+        class var_pos_it {
+            var_pos_occ* m_first;
+        public:
+            var_pos_it(var_pos_occ* c) : m_first(c) {}
+            var_pos operator*() { return m_first->m_vp; }
+            var_pos_it& operator++() { m_first = m_first->m_next; return *this; }
+            var_pos_it operator++(int) { var_pos_it tmp = *this; ++* this; return tmp; }
+            bool operator==(var_pos_it const& other) const { return m_first == other.m_first; }
+            bool operator!=(var_pos_it const& other) const { return !(*this == other); }
         };
 
         struct bit_atom : public atom {
@@ -84,44 +130,51 @@ namespace bv {
             bit_atom():m_occs(nullptr) {}
             ~bit_atom() override {}
             bool is_bit() const override { return true; }
+            var_pos_it begin() const { return var_pos_it(m_occs); }
+            var_pos_it end() const { return var_pos_it(nullptr); }
         };
 
-        struct le_atom : public atom {
+        struct def_atom : public atom {
             literal    m_var;
             literal    m_def;
-            le_atom(literal v, literal d):m_var(v), m_def(d) {}
-            ~le_atom() override {}
+            def_atom(literal v, literal d):m_var(v), m_def(d) {}
+            ~def_atom() override {}
             bool is_bit() const override { return false; }
         };
 
-        friend class add_var_pos_trail;
-        friend class mk_atom_trail;
+        class bit_trail;
+        class add_var_pos_trail;
+        class mk_atom_trail;
         typedef ptr_vector<atom> bool_var2atom;
 
         bv_util                  bv;
         arith_util               m_autil;
         stats                    m_stats;
+        ackerman                 m_ackerman;
         bit_blaster              m_bb;
-        th_union_find            m_find;
+        bv_union_find            m_find;
         vector<literal_vector>   m_bits;     // per var, the bits of a given variable.
-        ptr_vector<expr>         m_bits_expr;
-        svector<unsigned>        m_wpos;     // per var, watch position for fixed variable detection. 
+        unsigned_vector          m_wpos;     // per var, watch position for fixed variable detection. 
         vector<zero_one_bits>    m_zero_one_bits; // per var, see comment in the struct zero_one_bit
         bool_var2atom            m_bool_var2atom;
+        value2var                m_fixed_var_table;
+        mutable vector<rational> m_power2;
+        literal_vector           m_tmp_literals;
+        svector<var_pos>         m_prop_queue;
+        unsigned_vector          m_prop_queue_lim;
+        unsigned                 m_prop_queue_head { 0 };
+
+
         sat::solver* m_solver;
         sat::solver& s() { return *m_solver;  }
 
-        // internalize:
-
+        // internalize
         void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); }
         void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = 0; }
         atom * get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, 0); }
-
-        sat::literal false_literal;
-        sat::literal true_literal;
         bool visit(expr* e) override;
         bool visited(expr* e) override;
-        bool post_visit(expr* e, bool sign, bool root) override { return true; }
+        bool post_visit(expr* e, bool sign, bool root) override;
         unsigned get_bv_size(euf::enode* n);
         unsigned get_bv_size(theory_var v);
         theory_var get_var(euf::enode* n);
@@ -129,66 +182,55 @@ namespace bv {
         inline theory_var get_arg_var(euf::enode* n, unsigned idx);
         void get_bits(theory_var v, expr_ref_vector& r);
         void get_bits(euf::enode* n, expr_ref_vector& r);
-        void get_arg_bits(euf::enode* n, unsigned idx, expr_ref_vector& r);
         void get_arg_bits(app* n, unsigned idx, expr_ref_vector& r);
-        euf::enode* mk_enode(expr* n, ptr_vector<euf::enode> const& args);
         void fixed_var_eh(theory_var v);
-
+        bool is_bv(theory_var v) const { return bv.is_bv(var2expr(v)); }
         sat::status status() const { return sat::status::th(m_is_redundant, get_id());  }
-        void add_unit(sat::literal lit);
         void register_true_false_bit(theory_var v, unsigned i);
         void add_bit(theory_var v, sat::literal lit);
-        void init_bits(euf::enode * n, expr_ref_vector const & bits);
+        void set_bit_eh(theory_var v, literal l, unsigned idx);
+        void init_bits(expr* e, expr_ref_vector const & bits);
         void mk_bits(theory_var v);
-        expr_ref mk_bit2bool(expr* b, unsigned idx);
-        void internalize_num(app * n, theory_var v);
-        void internalize_add(app * n);
-        void internalize_sub(app * n);
-        void internalize_mul(app * n);
-        void internalize_udiv(app * n);
-        void internalize_sdiv(app * n);
-        void internalize_urem(app * n);
-        void internalize_srem(app * n);
-        void internalize_smod(app * n);
-        void internalize_shl(app * n);
-        void internalize_lshr(app * n);
-        void internalize_ashr(app * n);
-        void internalize_ext_rotate_left(app * n);
-        void internalize_ext_rotate_right(app * n);
-        void internalize_and(app * n);
-        void internalize_or(app * n);
-        void internalize_not(app * n);
-        void internalize_nand(app * n);
-        void internalize_nor(app * n);
-        void internalize_xor(app * n);
-        void internalize_xnor(app * n);
-        void internalize_concat(app * n);
-        void internalize_sign_extend(app * n);
-        void internalize_zero_extend(app * n);
-        void internalize_extract(app * n);
-        void internalize_redand(app * n);
-        void internalize_redor(app * n);
-        void internalize_comp(app * n);
-        void internalize_rotate_left(app * n);
-        void internalize_rotate_right(app * n);
+        void add_def(sat::literal def, sat::literal l);
+        void internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn);
+        void internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
+        void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
+        void internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn);
+        void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
+        void internalize_num(app * n, theory_var v);       
+        void internalize_concat(app * n);        
         void internalize_bv2int(app* n);
         void internalize_int2bv(app* n);
         void internalize_mkbv(app* n);
-        void internalize_umul_no_overflow(app *n);
-        void internalize_smul_no_overflow(app *n);
-        void internalize_smul_no_underflow(app *n);
-
+        void internalize_xor3(app* n);
+        void internalize_carry(app* n);
+        void internalize_sub(app* n);
+        void internalize_extract(app* n);
+        void internalize_bit2bool(app* n);
+        template<bool Signed>
+        void internalize_le(app* n);
         void assert_bv2int_axiom(app * n);
         void assert_int2bv_axiom(app* n);
+        void assert_ackerman(theory_var v1, theory_var v2);
 
         // solving
+        theory_var find(theory_var v) const { return m_find.find(v); }
         void find_wpos(theory_var v);
-        void find_new_diseq_axioms(var_pos_occ* occs, theory_var v, unsigned idx);
+        void find_new_diseq_axioms(bit_atom& a, theory_var v, unsigned idx);
         void mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx);
+        bool get_fixed_value(theory_var v, numeral& result) const;
+        void add_fixed_eq(theory_var v1, theory_var v2);      
+        svector<theory_var>   m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
+        bool merge_zero_one_bits(theory_var r1, theory_var r2);
+        void assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc);
+        void propagate_bits(var_pos entry);
+        numeral const& power2(unsigned i) const;
 
-
+        // invariants
+        bool check_zero_one_bits(theory_var v);
+       
     public:
-        solver(euf::solver& ctx);
+        solver(euf::solver& ctx, theory_id id);
         ~solver() override {}
         void set_solver(sat::solver* s) override { m_solver = s; }
         void set_lookahead(sat::lookahead* s) override { }
@@ -197,19 +239,22 @@ namespace bv {
         bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override;
         bool is_external(bool_var v) override;
         bool propagate(literal l, sat::ext_constraint_idx idx) override;
-        void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r) override;
+        void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override;
         void asserted(literal l) override;
         sat::check_result check() override;
         void push() override;
         void pop(unsigned n) override;
         void pre_simplify() override;        
         void simplify() override;
+        bool set_root(literal l, literal r) override;
+        void flush_roots() override;
         void clauses_modifed() override;
         lbool get_phase(bool_var v) override;
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
         void collect_statistics(statistics& st) const override;
+        euf::th_solver* fresh(sat::solver* s, euf::solver& ctx) override;
         extension* copy(sat::solver* s) override;       
         void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override {}
         void gc() override {}
@@ -220,18 +265,31 @@ namespace bv {
         bool check_model(sat::model const& m) const override;
         unsigned max_var(unsigned w) const override;
 
+        void new_eq_eh(euf::th_eq const& eq) override;
+        bool unit_propagate() override;
+
+        void add_value(euf::enode* n, expr_ref_vector& values) override;
+
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
                         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override { return false; }
 
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override { return false; }
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
+        void internalize(expr* e, bool redundant) override;
         euf::theory_var mk_var(euf::enode* n) override;
+        void apply_sort_cnstr(euf::enode * n, sort * s) override;
 
+        
+        void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
+        void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { SASSERT(check_zero_one_bits(r1)); }
+        void unmerge_eh(theory_var v1, theory_var v2);
+        trail_stack<euf::solver>& get_trail_stack();
 
         // disagnostics
-        std::ostream& display(std::ostream& out, theory_var v) const;
+        std::ostream& display(std::ostream& out, theory_var v) const;        
         typedef std::pair<solver const*, theory_var> pp_var;
         pp_var pp(theory_var v) const { return pp_var(this, v); }
+
     };
 
     inline std::ostream& operator<<(std::ostream& out, solver::pp_var const& p) { return p.first->display(out, p.second); }

src/sat/smt/euf_ackerman.cpp

@@ -58,37 +58,10 @@ namespace euf {
         inf.b = b;
         inf.c = nullptr;
         inf.is_cc = true;
+        inf.m_count = 0;
         insert();
     }
 
-    void ackerman::remove_from_queue(inference* inf) {
-        if (m_queue->m_next == m_queue) {
-            SASSERT(inf == m_queue);
-            m_queue = nullptr;
-            return;
-        }            
-        if (m_queue == inf) 
-            m_queue = inf->m_next;
-        auto* next = inf->m_next;
-        auto* prev = inf->m_prev;
-        prev->m_next = next;
-        next->m_prev = prev;        
-    }
-
-    void ackerman::push_to_front(inference* inf) {
-        if (!m_queue) {
-            m_queue = inf;
-        }
-        else if (m_queue != inf) {
-            auto* next = inf->m_next;
-            auto* prev = inf->m_prev;
-            prev->m_next = next;
-            next->m_prev = prev;
-            inf->m_prev = m_queue->m_prev;
-            inf->m_next = m_queue;
-            m_queue->m_prev = inf;
-        }
-    }
 
     void ackerman::insert() {
         inference* inf = m_tmp_inference;
@@ -97,15 +70,16 @@ namespace euf {
             m.inc_ref(inf->a);
             m.inc_ref(inf->b);
             m.inc_ref(inf->c);
-        }
-        else 
             new_tmp();        
+        }
         other->m_count++;
-        push_to_front(other);
+        if (other->m_count > m_high_watermark) 
+            s.s().set_should_simplify();
+        inference::push_to_front(m_queue, other);
     }
 
     void ackerman::remove(inference* inf) {
-        remove_from_queue(inf);
+        inference::remove_from(m_queue, inf);
         m_table.erase(inf);
         m.dec_ref(inf->a);
         m.dec_ref(inf->b);
@@ -115,13 +89,10 @@ namespace euf {
 
     void ackerman::new_tmp() {
         m_tmp_inference = alloc(inference);
-        m_tmp_inference->m_next = m_tmp_inference->m_prev = m_tmp_inference;
-        m_tmp_inference->m_count = 0;
+        m_tmp_inference->init(m_tmp_inference);
     }
 
     void ackerman::cg_conflict_eh(expr * n1, expr * n2) {
-        if (s.m_config.m_dack != DACK_ROOT)
-            return;
         if (!is_app(n1) || !is_app(n2))
             return;
         app* a = to_app(n1);
@@ -133,8 +104,6 @@ namespace euf {
     }
 
     void ackerman::used_eq_eh(expr* a, expr* b, expr* c) {
-        if (!s.m_config.m_dack_eq)
-            return;
         if (a == b || a == c || b == c)
             return;
         insert(a, b, c);
@@ -142,8 +111,6 @@ namespace euf {
     }
         
     void ackerman::used_cc_eh(app* a, app* b) {
-        if (s.m_config.m_dack != DACK_CR)
-            return;
         SASSERT(a->get_decl() == b->get_decl());
         SASSERT(a->get_num_args() == b->get_num_args());        
         insert(a, b);
@@ -157,8 +124,8 @@ namespace euf {
         m_num_propagations_since_last_gc = 0;
         
         while (m_table.size() > m_gc_threshold) 
-            remove(m_queue->m_prev);     
-
+            remove(m_queue->prev());
+    
         m_gc_threshold *= 110;
         m_gc_threshold /= 100;
         m_gc_threshold++;
@@ -171,13 +138,16 @@ namespace euf {
         unsigned num_prop = static_cast<unsigned>(s.s().get_stats().m_conflict * s.m_config.m_dack_factor);
         num_prop = std::min(num_prop, m_table.size());
         for (unsigned i = 0; i < num_prop; ++i, n = k) {
-            k = n->m_next;
+            k = n->next();
             if (n->m_count < s.m_config.m_dack_threshold) 
                 continue;
+            if (n->m_count >= m_high_watermark && num_prop < m_table.size())
+                ++num_prop;
             if (n->is_cc) 
                 add_cc(n->a, n->b);
             else 
-                add_eq(n->a, n->b, n->c);           
+                add_eq(n->a, n->b, n->c);       
+            ++s.m_stats.m_ackerman;
             remove(n);
         }
     }

src/sat/smt/euf_ackerman.h

@@ -16,6 +16,7 @@ Author:
 --*/
 #pragma once
 
+#include "util/dlist.h"
 #include "ast/euf/euf_egraph.h"
 #include "sat/smt/atom2bool_var.h"
 #include "sat/smt/sat_th.h"
@@ -24,13 +25,12 @@ namespace euf {
 
     class solver;
 
+
     class ackerman {
 
-        struct inference {
+        struct inference : dll_base<inference>{
             bool is_cc;
             expr* a, *b, *c;
-            inference* m_next{ nullptr };
-            inference* m_prev{ nullptr };
             unsigned   m_count{ 0 };
             inference():is_cc(false), a(nullptr), b(nullptr), c(nullptr) {}
             inference(app* a, app* b):is_cc(true), a(a), b(b), c(nullptr) {}
@@ -58,6 +58,7 @@ namespace euf {
         inference*    m_queue { nullptr };
         inference*    m_tmp_inference { nullptr };
         unsigned      m_gc_threshold { 1 };
+        unsigned      m_high_watermark { 1000 };
         unsigned      m_num_propagations_since_last_gc { 0 };
  
         void reset();
@@ -69,8 +70,6 @@ namespace euf {
         void add_cc(expr* a, expr* b);
         void add_eq(expr* a, expr* b, expr* c);        
         void gc();
-        void push_to_front(inference* inf);        
-        void remove_from_queue(inference* inf);
 
     public:
         ackerman(solver& s, ast_manager& m);

src/sat/smt/euf_internalize.cpp

@@ -21,17 +21,27 @@ Author:
 
 namespace euf {
 
-    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+    void solver::internalize(expr* e, bool redundant) {
         if (si.is_bool_op(e))
-            return si.internalize(e, redundant);
-        auto* ext = get_solver(e);
-        if (ext)
-            return ext->internalize(e, sign, root, redundant);
+            attach_lit(si.internalize(e, redundant), e);        
+        else if (auto* ext = get_solver(e))
+            ext->internalize(e, redundant);
+        else
+            visit_rec(m, e, false, false, redundant);
+        SASSERT(m_egraph.find(e));
+    }
 
+    sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
+        if (si.is_bool_op(e)) 
+            return attach_lit(si.internalize(e, redundant), e);        
+        if (auto* ext = get_solver(e))
+            return ext->internalize(e, sign, root, redundant);
         if (!visit_rec(m, e, sign, root, redundant))
             return sat::null_literal;
         SASSERT(m_egraph.find(e));
-        return literal(m_expr2var.to_bool_var(e), sign);
+        if (m.is_bool(e))
+            return literal(si.to_bool_var(e), sign);
+        return sat::null_literal;
     }
 
     bool solver::visit(expr* e) {
@@ -39,15 +49,7 @@ namespace euf {
         if (n)
             return true;
         if (si.is_bool_op(e)) {
-            sat::literal lit = si.internalize(e, m_is_redundant);
-            n = m_var2node.get(lit.var(), nullptr);
-            if (n && !lit.sign())
-                return n;
-            
-            n = m_egraph.mk(e, 0, nullptr);
-            attach_lit(lit, n);
-            if (!m.is_true(e) && !m.is_false(e)) 
-                s().set_external(lit.var());
+            attach_lit(si.internalize(e, m_is_redundant), e);
             return true;
         }
         if (is_app(e) && to_app(e)->get_num_args() > 0) {
@@ -64,8 +66,12 @@ namespace euf {
         m_args.reset();
         for (unsigned i = 0; i < num; ++i)
             m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
-        if (root && internalize_root(to_app(e), sign))
+        if (root && internalize_root(to_app(e), sign, m_args))
             return false;
+        if (auto* s = get_solver(e)) {
+            s->internalize(e, m_is_redundant);
+            return true;
+        }
         enode* n = m_egraph.mk(e, num, m_args.c_ptr());
         attach_node(n);
         return true;
@@ -77,33 +83,45 @@ namespace euf {
 
     void solver::attach_node(euf::enode* n) {
         expr* e = n->get_owner();
-        log_node(n);
-        if (m.is_bool(e)) {
-            sat::bool_var v = si.add_bool_var(e);
-            log_bool_var(v, n);
-            attach_lit(literal(v, false),  n);
+        if (!m.is_bool(e))
+            log_node(e);
+        else 
+            attach_lit(literal(si.add_bool_var(e), false),  e);        
+
+        if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
+            auto* e_ext = get_solver(e);
+            auto* s_ext = get_solver(m.get_sort(e));
+            if (s_ext && s_ext != e_ext)
+                s_ext->apply_sort_cnstr(n, m.get_sort(e));
         }
         axiomatize_basic(n);
     }
 
-    void solver::attach_lit(literal lit, euf::enode* n) {
+    sat::literal solver::attach_lit(literal lit, expr* e) {
         if (lit.sign()) {
-            sat::bool_var v = si.add_bool_var(n->get_owner());
+            sat::bool_var v = si.add_bool_var(e);
+            s().set_external(v);
             sat::literal lit2 = literal(v, false);
-            s().mk_clause(~lit, lit2, sat::status::th(false, m.get_basic_family_id()));
-            s().mk_clause(lit, ~lit2, sat::status::th(false, m.get_basic_family_id()));
+            s().mk_clause(~lit, lit2, sat::status::asserted());
+            s().mk_clause(lit, ~lit2, sat::status::asserted());
             lit = lit2;
         }
         sat::bool_var v = lit.var();
-        m_var2node.reserve(v + 1, nullptr);
-        SASSERT(m_var2node[v] == nullptr);
-        m_var2node[v] = n;
+        m_var2expr.reserve(v + 1, nullptr);
+        SASSERT(m_var2expr[v] == nullptr);
+        m_var2expr[v] = e;
         m_var_trail.push_back(v);
+        s().set_external(v);
+        if (!m_egraph.find(e)) {
+            enode* n = m_egraph.mk(e, 0, nullptr);
+            m_egraph.set_merge_enabled(n, false);
+        }
+        return lit;
     }
 
-    bool solver::internalize_root(app* e, bool sign) {
+    bool solver::internalize_root(app* e, bool sign, enode_vector const& args) {
         if (m.is_distinct(e)) {
-            enode_vector _args(m_args);
+            enode_vector _args(args);
             if (sign)
                 add_not_distinct_axiom(e, _args.c_ptr());
             else
@@ -202,7 +220,7 @@ namespace euf {
             expr* c = a->get_arg(0);
             expr* th = a->get_arg(1);
             expr* el = a->get_arg(2);
-            sat::bool_var v = m_expr2var.to_bool_var(c);
+            sat::bool_var v = si.to_bool_var(c);
             SASSERT(v != sat::null_bool_var);
             SASSERT(!m.is_bool(e));
             expr_ref eq_th(m.mk_eq(a, th), m);
@@ -224,7 +242,7 @@ namespace euf {
                 }
             }
             expr_ref fml(m.mk_or(eqs), m);
-            sat::literal dist(m_expr2var.to_bool_var(e), false);
+            sat::literal dist(si.to_bool_var(e), false);
             sat::literal some_eq = si.internalize(fml, m_is_redundant);
             sat::literal lits1[2] = { ~dist, ~some_eq };
             sat::literal lits2[2] = { dist, some_eq };

src/sat/smt/euf_invariant.cpp

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    euf_invariant.cpp
+
+Abstract:
+
+    Check invariants for EUF solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-07
+
+--*/
+
+#include "sat/smt/euf_solver.h"
+
+namespace euf {
+
+    /**
+       \brief Check if expressions attached to bool_variables and enodes have a consistent assignment.
+       For all a, b.  root(a) == root(b) ==> get_assignment(a) == get_assignment(b)
+    */
+
+    void solver::check_eqc_bool_assignment() const {
+        for (enode* n : m_egraph.nodes()) {
+            VERIFY(!m.is_bool(n->get_owner()) || 
+                   s().value(get_literal(n)) == s().value(get_literal(n->get_root())));        
+        }
+    }
+
+    void solver::check_missing_bool_enode_propagation() const {
+        for (enode* n : m_egraph.nodes()) 
+            if (m.is_bool(n->get_owner()) && l_undef == s().value(get_literal(n))) {
+                if (!n->is_root()) {
+                    VERIFY(l_undef == s().value(get_literal(n->get_root())));
+                }
+                else
+                    for (enode* o : enode_class(n)) {
+                        VERIFY(l_undef == s().value(get_literal(o)));
+                    }
+            }
+    }
+
+
+}

src/sat/smt/euf_model.cpp

@@ -16,6 +16,7 @@ Author:
 --*/
 
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "sat/smt/euf_solver.h"
 #include "model/value_factory.h"
 
@@ -79,7 +80,7 @@ namespace euf {
                 }
                 if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
                     continue;
-                sat::bool_var v = m_expr2var.to_bool_var(e);
+                sat::bool_var v = si.to_bool_var(e);
                 SASSERT(v != sat::null_bool_var);
                 switch (s().value(v)) {
                 case l_true:
@@ -100,6 +101,8 @@ namespace euf {
                 expr* v = user_sort.get_fresh_value(m.get_sort(e));
                 values.set(id, v);
             }
+            else if ((mb = get_solver(m.get_sort(e))))
+                mb->add_value(n, values);
             else {
                 IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
             }                
@@ -119,6 +122,9 @@ namespace euf {
             if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f))
                 continue;
             expr* v = values.get(n->get_root_id());
+            CTRACE("euf", !v, tout << "no value for " << mk_pp(e, m) << "\n";);
+            if (!v)
+                continue;
             unsigned arity = f->get_arity();
             if (arity == 0) 
                 mdl->register_decl(f, v);
@@ -129,8 +135,11 @@ namespace euf {
                     mdl->register_decl(f, fi);
                 }
                 args.reset();
-                for (enode* arg : enode_args(n)) 
+                for (enode* arg : enode_args(n)) {
                     args.push_back(values.get(arg->get_root_id()));
+                    SASSERT(args.back());
+                }
+                SASSERT(args.size() == arity);
                 if (!fi->get_entry(args.c_ptr()))
                     fi->insert_new_entry(args.c_ptr(), v);
             }

src/sat/smt/euf_proof.cpp

@@ -19,53 +19,60 @@ Author:
 
 namespace euf {
 
-    void solver::log_node(enode* n) {
-        if (m_drat) {
-            expr* e = n->get_owner();
-            if (is_app(e)) {
-                symbol const& name = to_app(e)->get_name();
-                s().get_drat().def_begin(n->get_owner_id(), name);
-                for (enode* arg : enode_args(n)) {
-                    s().get_drat().def_add_arg(arg->get_owner_id());
-                }
-                s().get_drat().def_end();
-            }
-            else {
-                IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
-            }
-        }
-    }
-
-    void solver::log_bool_var(sat::bool_var v, enode* n) {
-        if (m_drat) {
-            s().get_drat().bool_def(v, n->get_owner_id());
+    void solver::init_drat() {
+        if (!m_drat_initialized)
+            get_drat().add_theory(m.get_basic_family_id(), symbol("euf"));
+        m_drat_initialized = true;
+    }
+
+    void solver::log_node(expr* e) {
+        if (!use_drat())
+            return;
+        if (is_app(e)) {
+            std::stringstream strm;
+            strm << mk_ismt2_func(to_app(e)->get_decl(), m);
+            get_drat().def_begin(e->get_id(), strm.str());
+            for (expr* arg : *to_app(e))
+                get_drat().def_add_arg(arg->get_id());
+            get_drat().def_end();
+        }
+        else {
+            IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
         }
     }
 
+    /**
+     * \brief logs antecedents to a proof trail.
+     *
+     * NB with theories, this is not a pure EUF justification,
+     * It is true modulo EUF and previously logged certificates
+     * so it isn't necessarily an axiom over EUF,
+     * We will here leave it to the EUF checker to perform resolution steps.
+     */
     void solver::log_antecedents(literal l, literal_vector const& r) {
         TRACE("euf", log_antecedents(tout, l, r););
-        if (m_drat) {
-            literal_vector lits;
-            for (literal lit : r) lits.push_back(~lit);
-            if (l != sat::null_literal)
-                lits.push_back(l);
-            s().get_drat().add(lits, sat::status::th(true, m.get_basic_family_id()));
-        }
+        if (!use_drat())
+            return;
+        literal_vector lits;
+        for (literal lit : r) lits.push_back(~lit);
+        if (l != sat::null_literal)
+            lits.push_back(l);
+        get_drat().add(lits, sat::status::th(true, m.get_basic_family_id()));
     }
 
     void solver::log_antecedents(std::ostream& out, literal l, literal_vector const& r) {
         for (sat::literal l : r) {
-            enode* n = m_var2node[l.var()];
+            expr* n = m_var2expr[l.var()];
             out << ~l << ": ";
             if (!l.sign()) out << "! ";
-            out << mk_pp(n->get_owner(), m) << "\n";
+            out << mk_pp(n, m) << "\n";
             SASSERT(s().value(l) == l_true);
         }
         if (l != sat::null_literal) {
             out << l << ": ";
             if (l.sign()) out << "! ";
-            enode* n = m_var2node[l.var()];
-            out << mk_pp(n->get_owner(), m) << "\n";            
+            expr* n = m_var2expr[l.var()];
+            out << mk_pp(n, m) << "\n";
         }
     }
 

src/sat/smt/euf_solver.cpp

@@ -20,27 +20,25 @@ Author:
 #include "sat/sat_solver.h"
 #include "sat/smt/sat_smt.h"
 #include "sat/smt/ba_solver.h"
+#include "sat/smt/bv_solver.h"
 #include "sat/smt/euf_solver.h"
 
 namespace euf {
 
     void solver::updt_params(params_ref const& p) {
         m_config.updt_params(p);
-        m_drat = m_solver && m_solver->get_config().m_drat;
-        if (m_drat) 
-            m_solver->get_drat().add_theory(m.get_basic_family_id(), symbol("euf"));
     }
 
     /**
     * retrieve extension that is associated with Boolean variable.
     */
     th_solver* solver::get_solver(sat::bool_var v) {
-        if (v >= m_var2node.size())
+        if (v >= m_var2expr.size())
             return nullptr;
-        euf::enode* n = m_var2node[v];
-        if (!n)
+        expr* e = m_var2expr[v];
+        if (!e)
             return nullptr;
-        return get_solver(n->get_owner());
+        return get_solver(e);
     }
 
     th_solver* solver::get_solver(expr* e) {
@@ -49,8 +47,7 @@ namespace euf {
         return nullptr;
     }
 
-    th_solver* solver::get_solver(func_decl* f) {
-        family_id fid = f->get_family_id();
+    th_solver* solver::get_solver(family_id fid, func_decl* f) {
         if (fid == null_family_id)
             return nullptr;
         auto* ext = m_id2solver.get(fid, nullptr);
@@ -59,19 +56,24 @@ namespace euf {
         if (fid == m.get_basic_family_id())
             return nullptr;
         pb_util pb(m);
+        bv_util bvu(m);
         if (pb.get_family_id() == fid) {
             ext = alloc(sat::ba_solver, *this, fid);
-            if (m_drat)
-                m_solver->get_drat().add_theory(fid, symbol("ba"));
+            if (use_drat())
+                s().get_drat().add_theory(fid, symbol("ba"));
+        }
+        else if (bvu.get_family_id() == fid) {
+            ext = alloc(bv::solver, *this, fid);
+            if (use_drat())
+                s().get_drat().add_theory(fid, symbol("bv"));            
         }
         if (ext) {
             ext->set_solver(m_solver);
             ext->push_scopes(s().num_scopes());
             add_solver(fid, ext);
         }
-        else {
+        else if (f) 
             unhandled_function(f);
-        }
         return ext;
     }
 
@@ -84,7 +86,7 @@ namespace euf {
         if (m_unhandled_functions.contains(f))
             return;
         m_unhandled_functions.push_back(f);
-        m_trail.push_back(new (m_region) push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions));
+        m_trail.push(push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions));
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
     }
 
@@ -93,7 +95,7 @@ namespace euf {
     }
 
     bool solver::is_external(bool_var v) {
-        if (nullptr != m_var2node.get(v, nullptr))
+        if (nullptr != m_var2expr.get(v, nullptr))
             return true;
         for (auto* s : m_solvers)
             if (s->is_external(v))
@@ -107,86 +109,125 @@ namespace euf {
         return ext->propagate(l, idx);
     }
 
-    void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r) {
+    void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) {
+        m_egraph.begin_explain();
+        m_explain.reset();
         auto* ext = sat::constraint_base::to_extension(idx);
         if (ext == this)
-            get_antecedents(l, constraint::from_idx(idx), r);
+            get_antecedents(l, constraint::from_idx(idx), r, probing);
         else
-            ext->get_antecedents(l, idx, r);
+            ext->get_antecedents(l, idx, r, probing);
+        for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
+            size_t* e = m_explain[qhead];
+            if (is_literal(e))
+                r.push_back(get_literal(e));
+            else {
+                size_t idx = get_justification(e);
+                auto* ext = sat::constraint_base::to_extension(idx);
+                SASSERT(ext != this);
+                sat::literal lit = sat::null_literal;
+                ext->get_antecedents(lit, idx, r, probing);
+            }
+        }
+        m_egraph.end_explain();
+        if (!probing)
+            log_antecedents(l, r);
     }
 
-    void solver::get_antecedents(literal l, constraint& j, literal_vector& r) {
-        m_explain.reset();
+    void solver::add_antecedent(enode* a, enode* b) {
+        m_egraph.explain_eq<size_t>(m_explain, a, b);
+    }
+
+    void solver::propagate(enode* a, enode* b, ext_justification_idx idx) {
+        m_egraph.merge(a, b, to_ptr(idx));
+    }
+
+
+    void solver::get_antecedents(literal l, constraint& j, literal_vector& r, bool probing) {
+        expr* e = nullptr;
         euf::enode* n = nullptr;
 
-        // init_ackerman();
+        init_ackerman();
 
         switch (j.kind()) {
         case constraint::kind_t::conflict:
             SASSERT(m_egraph.inconsistent());
-            m_egraph.explain<unsigned>(m_explain);
+            m_egraph.explain<size_t>(m_explain);
             break;
         case constraint::kind_t::eq:
-            n = m_var2node[l.var()];
+            e = m_var2expr[l.var()];
+            n = m_egraph.find(e);
             SASSERT(n);
             SASSERT(m_egraph.is_equality(n));
             SASSERT(!l.sign());
-            m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1));
+            m_egraph.explain_eq<size_t>(m_explain, n->get_arg(0), n->get_arg(1));
             break;
         case constraint::kind_t::lit:
-            n = m_var2node[l.var()];
+            e = m_var2expr[l.var()];
+            n = m_egraph.find(e);
             SASSERT(n);
             SASSERT(m.is_bool(n->get_owner()));
-            m_egraph.explain_eq<unsigned>(m_explain, n, (l.sign() ? mk_false() : mk_true()));
+            m_egraph.explain_eq<size_t>(m_explain, n, (l.sign() ? mk_false() : mk_true()));
             break;
         default:
             IF_VERBOSE(0, verbose_stream() << (unsigned)j.kind() << "\n");
             UNREACHABLE();
         }
-        for (unsigned* idx : m_explain) 
-            r.push_back(sat::to_literal((unsigned)(idx - base_ptr())));
-
-        log_antecedents(l, r);
     }
 
     void solver::asserted(literal l) {
-        auto* ext = get_solver(l.var());
-        if (ext) {
-            ext->asserted(l);
+        expr* e = m_var2expr.get(l.var(), nullptr);
+        if (!e) {
             return;
         }
 
-        bool sign = l.sign();
-        auto n = m_var2node.get(l.var(), nullptr);
+        bool sign = l.sign();        
+        TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " " << (sign ? "not ": " ") << e->get_id()  << "\n";);
+        euf::enode* n = m_egraph.find(e);
         if (!n)
             return;
-        
-        expr* e = n->get_owner();
-        if (m.is_eq(e) && !sign) {
+        for (auto th : enode_th_vars(n))           
+            m_id2solver[th.get_id()]->asserted(l);
+        if (!n->merge_enabled())
+            return;
+        size_t* c = to_ptr(l);
+        SASSERT(is_literal(c));
+        SASSERT(l == get_literal(c));
+        if (m.is_eq(e) && !sign && n->num_args() == 2) {
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
-            TRACE("euf", tout << mk_pp(e, m) << "\n";);
-            m_egraph.merge(na, nb, base_ptr() + l.index());
+            m_egraph.merge(na, nb, c);
         }
         else {            
             euf::enode* nb = sign ? mk_false() : mk_true();
-            TRACE("euf", tout << (sign ? "not ": " ") << mk_pp(n->get_owner(), m)  << "\n";);
-            m_egraph.merge(n, nb, base_ptr() + l.index());
+            m_egraph.merge(n, nb, c);
         }
-        // TBD: delay propagation?
-        propagate();
     }
 
-    void solver::propagate() {  
-        while (m_egraph.propagate() && !s().inconsistent()) {
+    bool solver::unit_propagate() {
+        bool propagated = false;
+        while (!s().inconsistent()) {
             if (m_egraph.inconsistent()) {  
                 unsigned lvl = s().scope_lvl();
                 s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index()));
-                return;
+                return true;
             }
-            propagate_literals();
-            propagate_th_eqs();
+            bool propagated1 = false;
+            if (m_egraph.propagate()) {
+                propagate_literals();
+                propagate_th_eqs();
+                propagated1 = true;
+            }
+
+            for (auto* s : m_solvers) {
+                if (s->unit_propagate())
+                    propagated1 = true;
+            }
+            if (!propagated1)
+                break;
+            propagated = true;             
         }
+        return propagated;
     }
 
     void solver::propagate_literals() {
@@ -196,7 +237,7 @@ namespace euf {
             bool is_eq = p.second;
             expr* e = n->get_owner();
             expr* a = nullptr, *b = nullptr;
-            bool_var v = m_expr2var.to_bool_var(e);
+            bool_var v = si.to_bool_var(e);
             SASSERT(m.is_bool(e));
             size_t cnstr;
             literal lit;
@@ -207,7 +248,7 @@ namespace euf {
             }
             else {
                 a = e, b = n->get_root()->get_owner();
-                SASSERT(m.is_true(a) || m.is_false(b));
+                SASSERT(m.is_true(b) || m.is_false(b));
                 cnstr = lit_constraint().to_index();
                 lit = literal(v, m.is_false(b));
             }
@@ -222,7 +263,7 @@ namespace euf {
     void solver::propagate_th_eqs() {
         for (; m_egraph.has_th_eq() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_th_eq()) {
             th_eq eq = m_egraph.get_th_eq();
-            m_id2solver[eq.m_id]->new_eq_eh(eq);
+            m_id2solver[eq.m_id]->new_eq_eh(eq);            
         }
     }
 
@@ -246,6 +287,7 @@ namespace euf {
     }
 
     sat::check_result solver::check() { 
+        TRACE("euf", s().display(tout););
         bool give_up = false;
         bool cont = false;
         for (auto* e : m_solvers)
@@ -262,37 +304,52 @@ namespace euf {
     }
 
     void solver::push() {
+        si.push();
         scope s;
         s.m_var_lim = m_var_trail.size();
-        s.m_trail_lim = m_trail.size();
         m_scopes.push_back(s);
-        m_region.push_scope();
+        m_trail.push_scope();
         for (auto* e : m_solvers)
             e->push();
         m_egraph.push();
     }
 
-    void solver::force_push() {
-        for (; m_num_scopes > 0; --m_num_scopes) {
-
-        }
-    }
-
     void solver::pop(unsigned n) {
         m_egraph.pop(n);
         for (auto* e : m_solvers)
             e->pop(n);
-
         scope const & s = m_scopes[m_scopes.size() - n];
-
         for (unsigned i = m_var_trail.size(); i-- > s.m_var_lim; )
-            m_var2node[m_var_trail[i]] = nullptr;
-        m_var_trail.shrink(s.m_var_lim);
-        
-        undo_trail_stack(*this, m_trail, s.m_trail_lim);
-
-        m_region.pop_scope(n);
+            m_var2expr[m_var_trail[i]] = nullptr;
+        m_var_trail.shrink(s.m_var_lim);        
+        m_trail.pop_scope(n);
         m_scopes.shrink(m_scopes.size() - n);
+        si.pop(n);
+    }
+
+    void solver::start_reinit(unsigned n) {
+        sat::literal_vector lits;
+        m_reinit_vars.reset();
+        m_reinit_exprs.reset();
+        s().get_reinit_literals(n, lits);
+        for (sat::literal lit : lits) {
+            sat::bool_var v = lit.var();
+            expr* e = bool_var2expr(v);
+            if (m_reinit_vars.contains(v) || !e)
+                continue;
+            m_reinit_vars.push_back(v);
+            m_reinit_exprs.push_back(e);
+        }
+    }
+
+    void solver::finish_reinit() {
+        unsigned sz = m_reinit_vars.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            euf::enode* n = get_enode(m_reinit_exprs.get(i));
+            if (n)
+                continue;
+
+        }
     }
 
     void solver::pre_simplify() {
@@ -319,13 +376,33 @@ namespace euf {
         return l_undef; 
     }
 
+    bool solver::set_root(literal l, literal r) {
+        bool ok = true;
+        for (auto* s : m_solvers)
+            if (!s->set_root(l, r))
+                ok = false;
+        expr* e = bool_var2expr(l.var());
+        if (e) {
+            if (m.is_eq(e) && !m.is_iff(e))
+                ok = false;
+            euf::enode* n = get_enode(e);
+            if (n && n->merge_enabled())
+                ok = false;
+        }
+        return ok;
+    }
+
+    void solver::flush_roots() {
+        for (auto* s : m_solvers)
+            s->flush_roots();
+    }
+
     std::ostream& solver::display(std::ostream& out) const {
         m_egraph.display(out);
-
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
-            euf::enode* n = m_var2node[v];
-            out << v << ": " << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m, 1) << "\n";        
+            expr* e = m_var2expr[v];
+            out << v << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
         }
         for (auto* e : m_solvers)
             e->display(out);
@@ -350,13 +427,19 @@ namespace euf {
         m_egraph.collect_statistics(st);
         for (auto* e : m_solvers)
             e->collect_statistics(st);
-        st.update("euf dynack", m_stats.m_num_dynack);
+        st.update("euf ackerman", m_stats.m_ackerman);
     }
 
     sat::extension* solver::copy(sat::solver* s) { 
-        auto* r = alloc(solver, *m_to_m, *m_to_expr2var, *m_to_si);
+        auto* r = alloc(solver, *m_to_m, *m_to_si);
         r->m_config = m_config;
-        std::function<void* (void*)> copy_justification = [&](void* x) { return (void*)(r->base_ptr() + ((unsigned*)x - base_ptr())); };
+        sat::literal true_lit = sat::null_literal;
+        if (s->init_trail_size() > 0)
+            true_lit = s->trail_literal(0); 
+        std::function<void* (void*)> copy_justification = [&](void* x) { 
+            SASSERT(true_lit != sat::null_literal); 
+            return (void*)(r->to_ptr(true_lit)); 
+        };
         r->m_egraph.copy_from(m_egraph, copy_justification);        
         r->set_solver(s);
         for (unsigned i = 0; i < m_id2solver.size(); ++i) {
@@ -386,6 +469,9 @@ namespace euf {
         for (auto* e : m_solvers)
             if (!e->validate())
                 return false;
+        check_eqc_bool_assignment();
+        check_missing_bool_enode_propagation();
+        m_egraph.invariant();
         return true; 
     }
 
@@ -411,9 +497,9 @@ namespace euf {
     unsigned solver::max_var(unsigned w) const { 
         for (auto* e : m_solvers)
             w = e->max_var(w);
-        for (unsigned sz = m_var2node.size(); sz-- > 0; ) {
-            euf::enode* n = m_var2node[sz];
-            if (n && m.is_bool(n->get_owner())) {
+        for (unsigned sz = m_var2expr.size(); sz-- > 0; ) {
+            expr* n = m_var2expr[sz];
+            if (n && m.is_bool(n)) {
                 w = std::max(w, sz);
                 break;
             }           
@@ -422,21 +508,15 @@ namespace euf {
     }
 
     double solver::get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const {
-        double r = 0;
-        for (auto* e : m_solvers) {
-            r = e->get_reward(l, idx, occs);
-            if (r != 0)
-                return r;
-        }
-        return r;
+        auto* ext = sat::constraint_base::to_extension(idx);
+        SASSERT(ext);        
+        return (ext == this) ? 0 : ext->get_reward(l, idx, occs);        
     }
 
     bool solver::is_extended_binary(ext_justification_idx idx, literal_vector& r) {
-        for (auto* e : m_solvers) {
-            if (e->is_extended_binary(idx, r))
-                return true;
-        }
-        return false;
+        auto* ext = sat::constraint_base::to_extension(idx);
+        SASSERT(ext);        
+        return (ext != this) && ext->is_extended_binary(idx, r);
     }
 
     void solver::init_ackerman() {

src/sat/smt/euf_solver.h

@@ -48,41 +48,52 @@ namespace euf {
         size_t to_index() const { return sat::constraint_base::mem2base(this); }
     };
 
+
+
     class solver : public sat::extension, public th_internalizer, public th_decompile {
         typedef top_sort<euf::enode> deps_t;
         friend class ackerman;
         // friend class sat::ba_solver;
         struct stats {
-            unsigned m_num_dynack;
+            unsigned m_ackerman;
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
         struct scope {
             unsigned m_var_lim;
-            unsigned m_trail_lim;
         };
-        typedef ptr_vector<trail<solver> > trail_stack;
+        typedef trail_stack<solver> euf_trail_stack;
+
+
+        size_t* to_ptr(sat::literal l) { return TAG(size_t*, reinterpret_cast<size_t*>((size_t)(l.index() << 4)), 1); }
+        size_t* to_ptr(size_t jst) { return TAG(size_t*, reinterpret_cast<size_t*>(jst), 2); }
+        bool is_literal(size_t* p) const { return GET_TAG(p) == 1; }
+        bool is_justification(size_t* p) const { return GET_TAG(p) == 2; }
+        sat::literal get_literal(size_t* p) {
+            unsigned idx = static_cast<unsigned>(reinterpret_cast<size_t>(UNTAG(size_t*, p)));
+            return sat::to_literal(idx >> 4);
+        }
+        size_t get_justification(size_t* p) const {
+            return reinterpret_cast<size_t>(UNTAG(size_t*, p));
+        }
 
         ast_manager&          m;
-        atom2bool_var&        m_expr2var;
         sat::sat_internalizer& si;
         smt_params            m_config;
-        bool                  m_drat { false };
         euf::egraph           m_egraph;
+        euf_trail_stack       m_trail;
         stats                 m_stats;
-        region                m_region;
         func_decl_ref_vector  m_unhandled_functions;
-        trail_stack           m_trail;
+        
 
         sat::solver*           m_solver { nullptr };
         sat::lookahead*        m_lookahead { nullptr };
         ast_manager*           m_to_m;
-        atom2bool_var*         m_to_expr2var;
         sat::sat_internalizer* m_to_si;
         scoped_ptr<euf::ackerman>   m_ackerman;
 
-        ptr_vector<euf::enode>                          m_var2node;
-        ptr_vector<unsigned>                            m_explain;
+        ptr_vector<expr>                                m_var2expr;
+        ptr_vector<size_t>                              m_explain;
         unsigned                                        m_num_scopes { 0 };
         unsigned_vector                                 m_var_trail;
         svector<scope>                                  m_scopes;
@@ -93,26 +104,29 @@ namespace euf {
         constraint* m_eq       { nullptr };
         constraint* m_lit      { nullptr };
 
-        sat::solver& s() { return *m_solver; }
-        unsigned * base_ptr() { return reinterpret_cast<unsigned*>(this); }
-
         // internalization
-
         bool visit(expr* e) override;
         bool visited(expr* e) override;
-        bool post_visit(expr* e, bool sign, bool root) override;
-        void attach_node(euf::enode* n);
-        void attach_lit(sat::literal lit, euf::enode* n);
+        bool post_visit(expr* e, bool sign, bool root) override;        
+        sat::literal attach_lit(sat::literal lit, expr* e);
         void add_distinct_axiom(app* e, euf::enode* const* args);
         void add_not_distinct_axiom(app* e, euf::enode* const* args);
         void axiomatize_basic(enode* n);
-        bool internalize_root(app* e, bool sign);
+        bool internalize_root(app* e, bool sign, ptr_vector<enode> const& args);
         euf::enode* mk_true();
         euf::enode* mk_false();
+
+        // replay
+        expr_ref_vector      m_reinit_exprs;
+        sat::bool_var_vector m_reinit_vars;
         
+        void start_reinit(unsigned num_scopes);
+        void finish_reinit();
 
         // extensions
-        th_solver* get_solver(func_decl* f);
+        th_solver* get_solver(family_id fid, func_decl* f);
+        th_solver* get_solver(sort* s) { return get_solver(s->get_family_id(), nullptr); }
+        th_solver* get_solver(func_decl* f) { return get_solver(f->get_family_id(), f); }
         th_solver* get_solver(expr* e);
         th_solver* get_solver(sat::bool_var v);
         void add_solver(family_id fid, th_solver* th);
@@ -127,15 +141,20 @@ namespace euf {
         void values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl);
 
         // solving
-        void propagate();
         void propagate_literals();
         void propagate_th_eqs();
-        void get_antecedents(literal l, constraint& j, literal_vector& r);
-        void force_push();
+        void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
+
+        // proofs
         void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
         void log_antecedents(literal l, literal_vector const& r);
-        void log_node(enode* n);
-        void log_bool_var(sat::bool_var v, enode* n);
+        void log_node(expr* n);
+        bool m_drat_initialized{ false };
+        void init_drat();
+
+        // invariant
+        void check_eqc_bool_assignment() const;
+        void check_missing_bool_enode_propagation() const;        
 
         constraint& mk_constraint(constraint*& c, constraint::kind_t k);
         constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
@@ -143,17 +162,17 @@ namespace euf {
         constraint& lit_constraint() { return mk_constraint(m_lit, constraint::kind_t::lit); }
 
     public:
-       solver(ast_manager& m, atom2bool_var& expr2var, sat::sat_internalizer& si, params_ref const& p = params_ref()):
+       solver(ast_manager& m, sat::sat_internalizer& si, params_ref const& p = params_ref()):
             m(m),
-            m_expr2var(expr2var),
             si(si),
             m_egraph(m),
+            m_trail(*this),
             m_unhandled_functions(m),
             m_solver(nullptr),
             m_lookahead(nullptr),
             m_to_m(&m),
-            m_to_expr2var(&expr2var),
-            m_to_si(&si)
+            m_to_si(&si),
+            m_reinit_exprs(m)
         {
             updt_params(p);
         }
@@ -166,37 +185,45 @@ namespace euf {
 
        struct scoped_set_translate {
            solver& s;
-           scoped_set_translate(solver& s, ast_manager& m, atom2bool_var& a2b, sat::sat_internalizer& si) :
+           scoped_set_translate(solver& s, ast_manager& m, sat::sat_internalizer& si) :
                s(s) {
                s.m_to_m = &m;
-               s.m_to_expr2var = &a2b;
                s.m_to_si = &si;
            }
            ~scoped_set_translate() {
                s.m_to_m = &s.m;
-               s.m_to_expr2var = &s.m_expr2var;
                s.m_to_si = &s.si;
            }
        };
 
+        sat::solver& s() { return *m_solver; }
+        sat::solver const& s() const { return *m_solver; }
         sat::sat_internalizer& get_si() { return si; }
         ast_manager& get_manager() { return m; }
         enode* get_enode(expr* e) { return m_egraph.find(e); }
-        sat::literal get_literal(expr* e) { return literal(m_expr2var.to_bool_var(e), false); }
+        sat::literal get_literal(expr* e) const { return literal(si.to_bool_var(e), false); }
+        sat::literal get_literal(enode* e) const { return get_literal(e->get_owner()); }
         smt_params const& get_config() { return m_config; }
-        region& get_region() { return m_region; }
+        region& get_region() { return m_trail.get_region(); }
         template <typename C>
-        void push(C const& c) { m_trail.push_back(new (m_region) C(c));  }
+        void push(C const& c) { m_trail.push(c);  }
+        euf_trail_stack& get_trail_stack() { return m_trail; }
 
         void updt_params(params_ref const& p);
-        void set_solver(sat::solver* s) override { m_solver = s; m_drat = s->get_config().m_drat; }
+        void set_solver(sat::solver* s) override { m_solver = s; }
         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;
         bool is_extended_binary(ext_justification_idx idx, literal_vector& r) override;
         bool is_external(bool_var v) override;
         bool propagate(literal l, ext_constraint_idx idx) override;
-        void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
+        bool unit_propagate() override;
+        void propagate(enode* a, enode* b, ext_justification_idx);
+        bool set_root(literal l, literal r) override;
+        void flush_roots() override;
+
+        void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) override;
+        void add_antecedent(enode* a, enode* b);
         void asserted(literal l) override;
         sat::check_result check() override;
         void push() override;
@@ -220,6 +247,9 @@ namespace euf {
         bool check_model(sat::model const& m) const override;
         unsigned max_var(unsigned w) const override;
 
+        bool use_drat() { return s().get_config().m_drat && (init_drat(), true);  }
+        sat::drat& get_drat() { return s().get_drat(); }
+
         // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
                         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
@@ -228,11 +258,18 @@ namespace euf {
 
         // internalize
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
+        void internalize(expr* e, bool learned) override;
         void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); }
+        void attach_node(euf::enode* n);
         euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); }
+        expr* bool_var2expr(sat::bool_var v) { return m_var2expr.get(v, nullptr); }
 
         void update_model(model_ref& mdl);
 
         func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }       
-    };
+    };    
 };
+
+inline std::ostream& operator<<(std::ostream& out, euf::solver const& s) {
+    return s.display(out);
+}

src/sat/smt/sat_smt.h

@@ -39,8 +39,11 @@ namespace sat {
         virtual ~sat_internalizer() {}
         virtual bool is_bool_op(expr* e) const = 0;
         virtual literal internalize(expr* e, bool learned) = 0;
+        virtual bool_var to_bool_var(expr* e) = 0;
         virtual bool_var add_bool_var(expr* e)  = 0;
         virtual void cache(app* t, literal l) = 0;
+        virtual void push() = 0;
+        virtual void pop(unsigned n) = 0;
     };
     
     class constraint_base {

src/sat/smt/sat_th.cpp

@@ -65,15 +65,24 @@ namespace euf {
         return ctx.get_region();
     }
 
-    enode* th_euf_solver::get_enode(expr* e) const { 
+    trail_stack<euf::solver>& th_euf_solver::get_trail_stack() {
+        return ctx.get_trail_stack();
+    }
+
+    enode* th_euf_solver::expr2enode(expr* e) const { 
         return ctx.get_enode(e); 
     }
 
-    sat::literal th_euf_solver::get_literal(expr* e) const {
+    sat::literal th_euf_solver::expr2literal(expr* e) const {
         return ctx.get_literal(e);
     }
 
+    expr* th_euf_solver::bool_var2expr(sat::bool_var v) const {
+        return ctx.bool_var2expr(v);
+    }
+
     theory_var th_euf_solver::mk_var(enode * n) {
+        force_push();
         SASSERT(!is_attached_to_var(n));
         euf::theory_var v = m_var2enode.size();
         m_var2enode.push_back(n);
@@ -82,7 +91,7 @@ namespace euf {
 
     bool th_euf_solver::is_attached_to_var(enode* n) const {
         theory_var v = n->get_th_var(get_id());
-        return v != null_theory_var && get_enode(v) == n;
+        return v != null_theory_var && var2enode(v) == n;
     }
 
     theory_var th_euf_solver::get_th_var(expr* e) const {
@@ -99,4 +108,35 @@ namespace euf {
         m_var2enode_lim.shrink(new_lvl);
     }
 
+    unsigned th_euf_solver::lazy_pop(unsigned n) {
+        if (n <= m_num_scopes) {
+            m_num_scopes -= n;
+            return 0;
+        }
+        else {
+            n -= m_num_scopes;
+            pop(n);
+            return n;
+        }
+    }
+
+    void th_euf_solver::add_unit(sat::literal lit) {
+        ctx.s().add_clause(1, &lit, sat::status::th(m_is_redundant, get_id())); 
+    }
+
+    void th_euf_solver::add_clause(sat::literal a, sat::literal b) {
+        sat::literal lits[2] = { a, b };
+        ctx.s().add_clause(2, lits, sat::status::th(m_is_redundant, get_id()));
+    }
+
+    void th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {
+        sat::literal lits[3] = { a, b, c };
+        ctx.s().add_clause(3, lits, sat::status::th(m_is_redundant, get_id()));
+    }
+
+    void th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
+        sat::literal lits[4] = { a, b, c, d };
+        ctx.s().add_clause(4, lits, sat::status::th(m_is_redundant, get_id()));
+    }
+
 }

src/sat/smt/sat_th.h

@@ -36,11 +36,14 @@ namespace euf {
         virtual bool visit(expr* e) { return false; }
         virtual bool visited(expr* e) { return false; }
         virtual bool post_visit(expr* e, bool sign, bool root) { return false; }
+
     public:
         virtual ~th_internalizer() {}
 
         virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0;
 
+        virtual void internalize(expr* e, bool redundant) = 0;
+
         /**
            \brief Apply (interpreted) sort constraints on the given enode.
         */
@@ -69,7 +72,7 @@ namespace euf {
         /**
            \brief compute dependencies for node n
          */
-        virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) {}
+        virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) { dep.insert(n, nullptr);  }
 
         /**
            \brief should function be included in model.
@@ -102,24 +105,39 @@ namespace euf {
         solver &            ctx;
         euf::enode_vector   m_var2enode;
         unsigned_vector     m_var2enode_lim;
+        unsigned            m_num_scopes{ 0 };
 
         smt_params const& get_config() const;
-        sat::literal get_literal(expr* e) const;
+        sat::literal expr2literal(expr* e) const;
         region& get_region();
+        
+
+        void add_unit(sat::literal lit);
+        void add_clause(sat::literal a, sat::literal b);
+        void add_clause(sat::literal a, sat::literal b, sat::literal c);
+        void add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d);
+
     public:
         th_euf_solver(euf::solver& ctx, euf::theory_id id);
         virtual ~th_euf_solver() {}
         virtual theory_var mk_var(enode * n);
         unsigned get_num_vars() const { return m_var2enode.size();}
-        enode* get_enode(expr* e) const; 
-        enode* get_enode(theory_var v) const { return m_var2enode[v]; }
-        expr* get_expr(theory_var v) const { return get_enode(v)->get_owner(); }
-        expr_ref get_expr(sat::literal lit) const { expr* e = get_expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
+        enode* expr2enode(expr* e) const; 
+        enode* var2enode(theory_var v) const { return m_var2enode[v]; }
+        expr* var2expr(theory_var v) const { return var2enode(v)->get_owner(); }
+        expr* bool_var2expr(sat::bool_var v) const;
+        expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); }
         theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
         theory_var get_th_var(expr* e) const;
+        trail_stack<euf::solver> & get_trail_stack();
         bool is_attached_to_var(enode* n) const;
+        bool is_root(theory_var v) const { return var2enode(v)->is_root(); }
         void push() override;
         void pop(unsigned n) override;
+
+        void lazy_push() { ++m_num_scopes; }
+        void force_push() { for (; m_num_scopes > 0; --m_num_scopes) push(); }
+        unsigned lazy_pop(unsigned n);
     };
 
 

src/sat/tactic/goal2sat.cpp

@@ -29,6 +29,7 @@ Notes:
 #include "util/ref_util.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/ast_util.h"
@@ -38,6 +39,7 @@ Notes:
 #include "tactic/tactic.h"
 #include "tactic/generic_model_converter.h"
 #include "sat/sat_cut_simplifier.h"
+#include "sat/sat_drat.h"
 #include "sat/tactic/goal2sat.h"
 #include "sat/smt/ba_solver.h"
 #include "sat/smt/euf_solver.h"
@@ -72,6 +74,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     bool                        m_default_external;
     bool                        m_xor_solver;
     bool                        m_euf;
+    bool                        m_drat;
     bool                        m_is_redundant { false };
     sat::literal_vector         aig_lits;
     
@@ -98,6 +101,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
         m_xor_solver = p.get_bool("xor_solver", false);
         m_euf = sp.euf();
+        m_drat = sp.drat_file() != symbol();
     }
 
     void throw_op_not_handled(std::string const& s) {
@@ -125,19 +129,71 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_solver.add_clause(num, lits, m_is_redundant ? sat::status::redundant() : sat::status::asserted());
     }
 
+    void mk_root_clause(sat::literal l) {
+        TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
+        m_solver.add_clause(1, &l, m_is_redundant ? sat::status::redundant() : sat::status::input());
+    }
+
+    void mk_root_clause(sat::literal l1, sat::literal l2) {
+        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
+        m_solver.add_clause(l1, l2, m_is_redundant ? sat::status::redundant() : sat::status::input());
+    }
+
+    void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
+        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
+        m_solver.add_clause(l1, l2, l3, m_is_redundant ? sat::status::redundant() : sat::status::input());
+    }
+
+    void mk_root_clause(unsigned num, sat::literal * lits) {
+        TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
+        m_solver.add_clause(num, lits, m_is_redundant ? sat::status::redundant() : sat::status::input());
+    }
+
+    sat::bool_var add_var(bool is_ext, expr* n) {
+        auto v = m_solver.add_var(is_ext);
+        log_node(v, n);
+        return v;
+    }
+
+    void log_node(sat::bool_var v, expr* n) {
+        if (m_drat && m_solver.get_drat_ptr()) {
+            sat::drat* drat = m_solver.get_drat_ptr();
+            if (is_app(n)) {
+                app* a = to_app(n);
+                std::stringstream strm;
+                strm << mk_ismt2_func(a->get_decl(), m);
+                drat->def_begin(n->get_id(), strm.str());
+                for (expr* arg : *a)
+                    drat->def_add_arg(arg->get_id());
+                drat->def_end();
+            }
+            else {
+                IF_VERBOSE(0, verbose_stream() << "skipping DRAT of non-app\n");
+            }
+            drat->bool_def(v, n->get_id());
+        }
+    }
+
+
+
     sat::literal mk_true() {
         if (m_true == sat::null_literal) {
             // create fake variable to represent true;
-            m_true = sat::literal(m_solver.add_var(false), false);
+            m_true = sat::literal(add_var(false, m.mk_true()), false);
             mk_clause(m_true); // v is true
         }
         return m_true;
     }
 
+    sat::bool_var to_bool_var(expr* e) override {
+        return m_map.to_bool_var(e);
+    }
+
     sat::bool_var add_bool_var(expr* t) override {
         sat::bool_var v = m_map.to_bool_var(t);
         if (v == sat::null_bool_var) {
-            v = m_solver.add_var(true);
+            v = add_var(true, t);
+            force_push();
             m_map.insert(t, v);
         }
         else {
@@ -146,6 +202,28 @@ struct goal2sat::imp : public sat::sat_internalizer {
         return v;
     }
 
+    unsigned m_num_scopes{ 0 };
+
+    void force_push() {
+        for (; m_num_scopes > 0; --m_num_scopes)
+            m_map.push();
+    }
+
+    void push() override {
+        ++m_num_scopes;
+    }
+
+    void pop(unsigned n) override {
+        if (n <= m_num_scopes) {
+            m_num_scopes -= n;
+            return;
+        }
+        n -= m_num_scopes;
+        m_num_scopes = 0;
+        m_cache.reset();
+        m_map.pop(n);
+    }
+
     void cache(app* t, sat::literal l) override {
         m_cache.insert(t, l);
     }
@@ -166,12 +244,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 strm << mk_ismt2_pp(t, m);
                 throw_op_not_handled(strm.str());
             }
-            else {
-                bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
-                v = m_solver.add_var(ext);
-                m_map.insert(t, v);
-                l = sat::literal(v, sign);
-                TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
+            else {                
                 if (!is_uninterp_const(t)) {
                     if (m_euf) {
                         convert_euf(t, root, sign);                        
@@ -180,6 +253,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
                     else
                         m_unhandled_funs.push_back(to_app(t)->get_decl());
                 }
+                bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
+                v = add_var(ext, t);
+                force_push();
+                m_map.insert(t, v);
+                l = sat::literal(v, sign);
+                TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
             }
         }
         else {
@@ -191,7 +270,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             m_result_stack.reset();
         SASSERT(l != sat::null_literal);
         if (root)
-            mk_clause(l);
+            mk_root_clause(l);
         else
             m_result_stack.push_back(l);
     }
@@ -213,7 +292,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             if (sign)
                 l.neg();
             if (root)
-                mk_clause(l);
+                mk_root_clause(l);
             else
                 m_result_stack.push_back(l);
             return true;
@@ -275,17 +354,17 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 for (unsigned i = 0; i < num; i++) {
                     sat::literal l = m_result_stack[i];
                     l.neg();
-                    mk_clause(l);
+                    mk_root_clause(l);
                 }
             }
             else {
-                mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
+                mk_root_clause(m_result_stack.size(), m_result_stack.c_ptr());
             }
             m_result_stack.reset();
         }
         else {
             SASSERT(num <= m_result_stack.size());
-            sat::bool_var k = m_solver.add_var(false);
+            sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
             m_cache.insert(t, l);
             sat::literal * lits = m_result_stack.end() - num;           
@@ -321,18 +400,18 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 for (unsigned i = 0; i < num; ++i) {
                     m_result_stack[i].neg();
                 }                
-                mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
+                mk_root_clause(m_result_stack.size(), m_result_stack.c_ptr());
             }
             else {
                 for (unsigned i = 0; i < num; ++i) {
-                    mk_clause(m_result_stack[i]);
+                    mk_root_clause(m_result_stack[i]);
                 }
             }
             m_result_stack.reset();
         }
         else {
             SASSERT(num <= m_result_stack.size());
-            sat::bool_var k = m_solver.add_var(false);
+            sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
             m_cache.insert(t, l);
             sat::literal * lits = m_result_stack.end() - num;
@@ -373,17 +452,17 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (root) {
             SASSERT(sz == 3);
             if (sign) {
-                mk_clause(~c, ~t);
-                mk_clause(c,  ~e);
+                mk_root_clause(~c, ~t);
+                mk_root_clause(c,  ~e);
             }
             else {
-                mk_clause(~c, t);
-                mk_clause(c, e);
+                mk_root_clause(~c, t);
+                mk_root_clause(c, e);
             }
             m_result_stack.reset();
         }
         else {
-            sat::bool_var k = m_solver.add_var(false);
+            sat::bool_var k = add_var(false, n);
             sat::literal  l(k, false);
             m_cache.insert(n, l);
             mk_clause(~l, ~c, t);
@@ -411,16 +490,16 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (root) {
             SASSERT(sz == 2);
             if (sign) {
-                mk_clause(l1);
-                mk_clause(~l2);
+                mk_root_clause(l1);
+                mk_root_clause(~l2);
             }
             else {
-                mk_clause(~l1, l2);
+                mk_root_clause(~l1, l2);
             }
             m_result_stack.reset();
         }
         else {
-            sat::bool_var k = m_solver.add_var(false);
+            sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
             m_cache.insert(t, l);
             // l <=> (l1 => l2)
@@ -443,17 +522,17 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (root) {
             SASSERT(sz == 2);
             if (sign) {
-                mk_clause(l1, l2);
-                mk_clause(~l1, ~l2);
+                mk_root_clause(l1, l2);
+                mk_root_clause(~l1, ~l2);
             }
             else {
-                mk_clause(l1, ~l2);
-                mk_clause(~l1, l2);
+                mk_root_clause(l1, ~l2);
+                mk_root_clause(~l1, l2);
             }
             m_result_stack.reset();
         }
         else {
-            sat::bool_var k = m_solver.add_var(false);
+            sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
             m_cache.insert(t, l);
             mk_clause(~l, l1, ~l2);
@@ -486,7 +565,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat::extension* ext = m_solver.get_extension();
         euf::solver* euf = nullptr;
         if (!ext) {
-            euf = alloc(euf::solver, m, m_map, *this);
+            euf = alloc(euf::solver, m, *this);
             m_solver.set_extension(euf);
             for (unsigned i = m_solver.num_scopes(); i-- > 0; )
                 euf->push();
@@ -502,7 +581,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (lit == sat::null_literal)
             return;
         if (root)
-            mk_clause(lit);
+            mk_root_clause(lit);
         else
             m_result_stack.push_back(lit);
     }
@@ -528,7 +607,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (lit == sat::null_literal)
             return;
         if (root) 
-            mk_clause(lit);        
+            mk_root_clause(lit);        
         else 
             m_result_stack.push_back(lit);      
     }
@@ -643,6 +722,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     sat::literal internalize(expr* n, bool redundant) override {
         unsigned sz = m_result_stack.size();
+        (void)sz;
         process(n, false, redundant);
         SASSERT(m_result_stack.size() == sz + 1);
         sat::literal result = m_result_stack.back();

src/sat/tactic/sat_tactic.cpp

@@ -64,7 +64,8 @@ class sat_tactic : public tactic {
             TRACE("sat_dimacs", m_solver->display_dimacs(tout););
             dep2assumptions(dep2asm, assumptions);
             lbool r = m_solver->check(assumptions.size(), assumptions.c_ptr());
-            TRACE("sat", tout << "result of checking: " << r << " " << m_solver->get_reason_unknown() << "\n";);
+            TRACE("sat", tout << "result of checking: " << r << " "; 
+                  if (r == l_undef) tout << m_solver->get_reason_unknown(); tout << "\n";);
             if (r == l_false) {
                 expr_dependency * lcore = nullptr;
                 if (produce_core) {
@@ -88,13 +89,18 @@ class sat_tactic : public tactic {
                     for (auto const& kv : map) {
                         expr * n   = kv.m_key;
                         sat::bool_var v = kv.m_value;
+                        if (!is_app(n))
+                            continue;
+                        app* a = to_app(n);
+                        if (!is_uninterp_const(a))
+                            continue;
                         TRACE("sat_tactic", tout << "extracting value of " << mk_ismt2_pp(n, m) << "\nvar: " << v << "\n";);
                         switch (sat::value_at(v, ll_m)) {
                         case l_true: 
-                            md->register_decl(to_app(n)->get_decl(), m.mk_true()); 
+                            md->register_decl(a->get_decl(), m.mk_true()); 
                             break;
                         case l_false:
-                            md->register_decl(to_app(n)->get_decl(), m.mk_false());
+                            md->register_decl(a->get_decl(), m.mk_false());
                             break;
                         default:
                             break;