initial working version

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

src/cmd_context/extra_cmds/dbg_cmds.cpp

@@ -503,4 +503,5 @@ void install_dbg_cmds(cmd_context & ctx) {
     ctx.insert(alloc(set_next_id));
     ctx.insert(alloc(mbp_cmd));
     ctx.insert(alloc(mbi_cmd));
+    ctx.insert(alloc(euf_project_cmd));
 }

src/qe/qe_term_graph.cpp

@@ -26,83 +26,80 @@ Notes:
 
 namespace qe {
 
-class term {
+    class term {
-    // -- an app represented by this term
+        // -- an app represented by this term
-    expr* m_app; // NSB: to make usable with exprs
+        expr* m_app; // NSB: to make usable with exprs
-    // -- root of the equivalence class
+        // -- root of the equivalence class
-    term* m_root;
+        term* m_root;
-    // -- next element in the equivalence class (cyclic linked list)
+        // -- next element in the equivalence class (cyclic linked list)
-    term* m_next;
+        term* m_next;
-    // -- eq class size
+        // -- eq class size
-    unsigned m_class_size;
+        unsigned m_class_size;
-
+        
-    // -- general purpose mark
+        // -- general purpose mark
-    unsigned m_mark:1;
+        unsigned m_mark:1;
-    // -- general purpose second mark
+        // -- general purpose second mark
-    unsigned m_mark2:1;
+        unsigned m_mark2:1;
-    // -- is an interpreted constant
+        // -- is an interpreted constant
-    unsigned m_interpreted:1;
+        unsigned m_interpreted:1;
-
+        
-    // -- terms that contain this term as a child
+        // -- terms that contain this term as a child
-    ptr_vector<term> m_parents;
+        ptr_vector<term> m_parents;
-
+        
-    // arguments of term.
+        // arguments of term.
-    ptr_vector<term> m_children;
+        ptr_vector<term> m_children;
-
+        
-public:
+    public:
-    term(expr* a, u_map<term*>& app2term) : 
+        term(expr* a, u_map<term*>& app2term) : 
-        m_app(a), 
+            m_app(a), 
-        m_root(this), 
+            m_root(this), 
-        m_next(this),
+            m_next(this),
-        m_class_size(1), 
+            m_class_size(1), 
-        m_mark(false), 
+            m_mark(false), 
-        m_mark2(false),
+            m_mark2(false),
-        m_interpreted(false) {
+            m_interpreted(false) {
-        if (!is_app(a)) return;
+            if (!is_app(a)) return;
-        for (expr* e : *to_app(a)) {
+            for (expr* e : *to_app(a)) {
-            term* t = app2term[e->get_id()];
+                term* t = app2term[e->get_id()];
-            t->m_parents.push_back(this);
+                t->m_parents.push_back(this);
-            m_children.push_back(t);
+                m_children.push_back(t);
+            }
         }
-    }
+        
-
+        ~term() {}
-    ~term() {}
+        
-
+        class parents {
-    class parents {
+            term const& t;
+        public:
+            parents(term const& _t):t(_t) {}
+            parents(term const* _t):t(*_t) {}
+            ptr_vector<term>::const_iterator begin() const { return t.m_parents.begin(); }
+            ptr_vector<term>::const_iterator end() const { return t.m_parents.end(); }
+        };
+        
+        class children {
         term const& t;
-    public:
+        public:
-        parents(term const& _t):t(_t) {}
+            children(term const& _t):t(_t) {}
-        parents(term const* _t):t(*_t) {}
+            children(term const* _t):t(*_t) {}
-        ptr_vector<term>::const_iterator begin() const { return t.m_parents.begin(); }
+            ptr_vector<term>::const_iterator begin() const { return t.m_children.begin(); }
-        ptr_vector<term>::const_iterator end() const { return t.m_parents.end(); }
+            ptr_vector<term>::const_iterator end() const { return t.m_children.end(); }
-    };
+        };
-
+        
-    class children {
+        // Congruence table hash function is based on
-        term const& t;
+        // roots of children and function declaration.
-    public:
+        
-        children(term const& _t):t(_t) {}
+        unsigned get_hash() const {
-        children(term const* _t):t(*_t) {}
-        ptr_vector<term>::const_iterator begin() const { return t.m_children.begin(); }
-        ptr_vector<term>::const_iterator end() const { return t.m_children.end(); }
-    };
-
-    // Congruence table hash function is based on
-    // roots of children and function declaration.
-
-    struct cg_hash {
-        unsigned operator()(term const* t) const { 
             unsigned a, b, c;
-            a = b = c = t->get_decl_id(); 
+            a = b = c = get_decl_id(); 
-            for (term * ch : children(t)) {
+            for (term * ch : children(this)) {
                 a = ch->get_root().get_id();
                 mix(a, b, c);
             }
             return c;
         }
-    };
+        
-
+        static bool cg_eq(term const * t1, term const * t2) {
-    struct cg_eq {
-        bool operator()(term * t1, term * t2) const {
             if (t1->get_decl_id() != t2->get_decl_id()) return false;
             if (t1->m_children.size() != t2->m_children.size()) return false;
             for (unsigned i = 0, sz = t1->m_children.size(); i < sz; ++ i) {
@@ -110,348 +107,378 @@ public:
             }
             return true;
         }
+        
+        unsigned get_id() const { return m_app->get_id();}
+        
+        unsigned get_decl_id() const { return is_app(m_app) ? to_app(m_app)->get_decl()->get_id() : m_app->get_id(); }
+        
+        bool is_marked() const {return m_mark;}
+        void set_mark(bool v){m_mark = v;}
+        bool is_marked2() const {return m_mark2;} // NSB: where is this used?
+        void set_mark2(bool v){m_mark2 = v;}      // NSB: where is this used?
+        
+        bool is_interpreted() const {return m_interpreted;}
+        void mark_as_interpreted() {m_interpreted=true;}
+        expr* get_app() const {return m_app;}
+        unsigned get_num_args() const { return is_app(m_app) ? to_app(m_app)->get_num_args() : 0; }
+        
+        term &get_root() const {return *m_root;}
+        bool is_root() const {return m_root == this;}
+        void set_root(term &r) {m_root = &r;}
+        term &get_next() const {return *m_next;}
+        void add_parent(term* p) { m_parents.push_back(p); }
+        
+        unsigned get_class_size() const {return m_class_size;}
+        
+        void merge_eq_class(term &b) {
+            std::swap(this->m_next, b.m_next);
+            m_class_size += b.get_class_size();
+            // -- reset (useful for debugging)
+            b.m_class_size = 0;
+        }
+        
+        // -- make this term the root of its equivalence class
+        void mk_root() {
+            if (is_root()) return;
+            
+            term *curr = this;
+            do {
+                if (curr->is_root()) {
+                    // found previous root
+                    SASSERT(curr != this);
+                    m_class_size = curr->get_class_size();
+                    curr->m_class_size = 0;
+                }
+                curr->set_root(*this);
+                curr = &curr->get_next();
+            }
+            while (curr != this);
+        }
+    };
+    
+
+
+    class arith_term_graph_plugin : public term_graph_plugin {
+        term_graph &m_g;
+        ast_manager &m;
+        arith_util m_arith;
+        
+    public:
+        arith_term_graph_plugin(term_graph &g) :
+            term_graph_plugin (g.get_ast_manager().mk_family_id("arith")),
+            m_g(g), m(g.get_ast_manager()), m_arith(m) {(void)m_g;}
+        
+        virtual ~arith_term_graph_plugin() {}
+        
+        bool mk_eq_core (expr *_e1, expr *_e2, app_ref &res) {
+            expr *e1, *e2;
+            e1 = _e1;
+            e2 = _e2;
+            
+            if (m_arith.is_zero(e1)) {
+                std::swap(e1, e2);
+            }
+            // y + -1*x == 0  --> y = x
+            expr *a0 = 0, *a1 = 0, *x = 0;
+            if (m_arith.is_zero(e2) && m_arith.is_add(e1, a0, a1)) {
+                if (m_arith.is_times_minus_one(a1, x)) {
+                    e1 = a0;
+                    e2 = x;
+                }
+                else if (m_arith.is_times_minus_one(a0, x)) {
+                    e1 = a1;
+                    e2 = x;
+                }
+            }
+            res = m.mk_eq(e1, e2);
+            return true;
+        }
+        
+        app* mk_le_zero(expr *arg) {
+            expr *e1, *e2, *e3;
+            // XXX currently disabled
+            if (m_arith.is_add(arg, e1, e2)) {
+                // e1-e2<=0 --> e1<=e2
+                if (m_arith.is_times_minus_one(e2, e3)) {
+                    return m_arith.mk_le(e1, e3);
+                }
+                // -e1+e2<=0 --> e2<=e1
+                else if (m_arith.is_times_minus_one(e1, e3)) {
+                    return m_arith.mk_le(e2, e3);
+                }
+            }
+            return m_arith.mk_le(arg, mk_zero());
+        }
+
+        app* mk_ge_zero(expr *arg) {
+            expr *e1, *e2, *e3;
+            // XXX currently disabled
+            if (m_arith.is_add(arg, e1, e2)) {
+                // e1-e2>=0 --> e1>=e2
+                if (m_arith.is_times_minus_one(e2, e3)) {
+                    return m_arith.mk_ge(e1, e3);
+                }
+                // -e1+e2>=0 --> e2>=e1
+                else if (m_arith.is_times_minus_one(e1, e3)) {
+                    return m_arith.mk_ge(e2, e3);
+                }
+            }
+            return m_arith.mk_ge(arg, mk_zero());
+        }
+        
+        bool mk_le_core (expr *arg1, expr * arg2, app_ref &result) {
+            // t <= -1  ==> t < 0 ==> ! (t >= 0)
+            rational n;
+            if (m_arith.is_int (arg1) && m_arith.is_minus_one (arg2)) {
+                result = m.mk_not (mk_ge_zero (arg1));
+                return true;
+            }
+            else if (m_arith.is_zero(arg2)) {
+                result = mk_le_zero(arg1);
+                return true;
+            }
+            else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n < 0) {
+                // t <= n ==> t < n + 1 ==> ! (t >= n + 1)
+                result = m.mk_not(m_arith.mk_ge(arg1, m_arith.mk_numeral(n+1, true)));
+                return true;
+            }
+            return false;
+        }
+        
+        expr * mk_zero () {return m_arith.mk_numeral (rational (0), true);}
+        bool is_one (expr const * n) const {
+            rational val;
+            return m_arith.is_numeral (n, val) && val.is_one ();
+        }
+        
+        bool mk_ge_core (expr * arg1, expr * arg2, app_ref &result) {
+            // t >= 1 ==> t > 0 ==> ! (t <= 0)
+            rational n;
+            if (m_arith.is_int (arg1) && is_one (arg2)) {
+                result = m.mk_not (mk_le_zero (arg1));
+                return true;
+            }
+            else if (m_arith.is_zero(arg2)) {
+                result = mk_ge_zero(arg1);
+                return true;
+            }
+            else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n > 0) {
+                // t >= n ==> t > n - 1 ==> ! (t <= n - 1)
+                result = m.mk_not(m_arith.mk_le(arg1, m_arith.mk_numeral(n-1, true)));
+                return true;
+            }
+            return false;
+        }
+        
+        virtual app_ref process_lit (app *_lit) {
+            app *lit = _lit;
+            expr *e1, *e2;
+            
+            // strip negation
+            bool is_neg = m.is_not(lit);
+            if (is_neg) {
+                lit = to_app(to_app(lit)->get_arg(0));
+            }
+            
+            app_ref res(m);
+            res = lit;
+            if (m.is_eq (lit, e1, e2)) {
+                mk_eq_core(e1, e2, res);
+            }
+            else if (m_arith.is_le(lit, e1, e2)) {
+                mk_le_core(e1, e2, res);
+            }
+            else if (m_arith.is_ge(lit, e1, e2)) {
+                mk_ge_core(e1, e2, res);
+            }
+            
+            // restore negation
+            if (is_neg) {
+                res = m.mk_not(res);
+            }
+            
+        return res;
+        }
     };
 
-    unsigned get_id() const { return m_app->get_id();}
+    unsigned term_graph::term_hash::operator()(term const* t) const { return t->get_hash(); }
 
-    unsigned get_decl_id() const { return is_app(m_app) ? to_app(m_app)->get_decl()->get_id() : m_app->get_id(); }
+    bool term_graph::term_eq::operator()(term const* a, term const* b) const { return term::cg_eq(a, b); }
 
-    bool is_marked() const {return m_mark;}
+    term_graph::term_graph(ast_manager &man) : m(man), m_lits(m), m_pinned(m) {
-    void set_mark(bool v){m_mark = v;}
+        m_plugins.register_plugin (alloc(arith_term_graph_plugin, *this));
-    bool is_marked2() const {return m_mark2;} // NSB: where is this used?
-    void set_mark2(bool v){m_mark2 = v;}      // NSB: where is this used?
-
-    bool is_interpreted() const {return m_interpreted;}
-    void mark_as_interpreted() {m_interpreted=true;}
-    expr* get_app() const {return m_app;}
-    unsigned get_num_args() const { return is_app(m_app) ? to_app(m_app)->get_num_args() : 0; }
-
-    term &get_root() const {return *m_root;}
-    bool is_root() const {return m_root == this;}
-    void set_root(term &r) {m_root = &r;}
-    term &get_next() const {return *m_next;}
-
-    unsigned get_class_size() const {return m_class_size;}
-
-    void merge_eq_class(term &b) {
-        std::swap(this->m_next, b.m_next);
-        m_class_size += b.get_class_size();
-        // -- reset (useful for debugging)
-        b.m_class_size = 0;
     }
-
-    // -- make this term the root of its equivalence class
-    void mk_root() {
-        if (is_root()) return;
-
-        term *curr = this;
-        do {
-            if (curr->is_root()) {
-                // found previous root
-                SASSERT(curr != this);
-                m_class_size = curr->get_class_size();
-                curr->m_class_size = 0;
-            }
-            curr->set_root(*this);
-            curr = &curr->get_next();
-        }
-        while (curr != this);
-    }
-};
-
-
-
-class arith_term_graph_plugin : public term_graph_plugin {
-    term_graph &m_g;
-    ast_manager &m;
-    arith_util m_arith;
-
-public:
-    arith_term_graph_plugin(term_graph &g) :
-        term_graph_plugin (g.get_ast_manager().mk_family_id("arith")),
-        m_g(g), m(g.get_ast_manager()), m_arith(m) {(void)m_g;}
-
-    virtual ~arith_term_graph_plugin() {}
-
-    bool mk_eq_core (expr *_e1, expr *_e2, app_ref &res) {
-        expr *e1, *e2;
-        e1 = _e1;
-        e2 = _e2;
-
-        if (m_arith.is_zero(e1)) {
-            std::swap(e1, e2);
-        }
-        // y + -1*x == 0  --> y = x
-        expr *a0 = 0, *a1 = 0, *x = 0;
-        if (m_arith.is_zero(e2) && m_arith.is_add(e1, a0, a1)) {
-            if (m_arith.is_times_minus_one(a1, x)) {
-                e1 = a0;
-                e2 = x;
-            }
-            else if (m_arith.is_times_minus_one(a0, x)) {
-                e1 = a1;
-                e2 = x;
-            }
-        }
-        res = m.mk_eq(e1, e2);
-        return true;
-    }
-
-    app* mk_le_zero(expr *arg) {
-        expr *e1, *e2, *e3;
-        // XXX currently disabled
-        if (m_arith.is_add(arg, e1, e2)) {
-            // e1-e2<=0 --> e1<=e2
-            if (m_arith.is_times_minus_one(e2, e3)) {
-                return m_arith.mk_le(e1, e3);
-            }
-            // -e1+e2<=0 --> e2<=e1
-            else if (m_arith.is_times_minus_one(e1, e3)) {
-                return m_arith.mk_le(e2, e3);
-            }
-        }
-        return m_arith.mk_le(arg, mk_zero());
-    }
-
-    app* mk_ge_zero(expr *arg) {
-        expr *e1, *e2, *e3;
-        // XXX currently disabled
-        if (m_arith.is_add(arg, e1, e2)) {
-            // e1-e2>=0 --> e1>=e2
-            if (m_arith.is_times_minus_one(e2, e3)) {
-                return m_arith.mk_ge(e1, e3);
-            }
-            // -e1+e2>=0 --> e2>=e1
-            else if (m_arith.is_times_minus_one(e1, e3)) {
-                return m_arith.mk_ge(e2, e3);
-            }
-        }
-        return m_arith.mk_ge(arg, mk_zero());
-    }
-
-    bool mk_le_core (expr *arg1, expr * arg2, app_ref &result) {
-        // t <= -1  ==> t < 0 ==> ! (t >= 0)
-        rational n;
-        if (m_arith.is_int (arg1) && m_arith.is_minus_one (arg2)) {
-            result = m.mk_not (mk_ge_zero (arg1));
-            return true;
-        }
-        else if (m_arith.is_zero(arg2)) {
-            result = mk_le_zero(arg1);
-            return true;
-        }
-        else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n < 0) {
-            // t <= n ==> t < n + 1 ==> ! (t >= n + 1)
-            result = m.mk_not(m_arith.mk_ge(arg1, m_arith.mk_numeral(n+1, true)));
-            return true;
-        }
-        return false;
-    }
-
-    expr * mk_zero () {return m_arith.mk_numeral (rational (0), true);}
-    bool is_one (expr const * n) const {
-        rational val;
-        return m_arith.is_numeral (n, val) && val.is_one ();
-    }
-
-    bool mk_ge_core (expr * arg1, expr * arg2, app_ref &result) {
-        // t >= 1 ==> t > 0 ==> ! (t <= 0)
-        rational n;
-        if (m_arith.is_int (arg1) && is_one (arg2)) {
-            result = m.mk_not (mk_le_zero (arg1));
-            return true;
-        }
-        else if (m_arith.is_zero(arg2)) {
-            result = mk_ge_zero(arg1);
-            return true;
-        }
-        else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n > 0) {
-            // t >= n ==> t > n - 1 ==> ! (t <= n - 1)
-            result = m.mk_not(m_arith.mk_le(arg1, m_arith.mk_numeral(n-1, true)));
-            return true;
-        }
-        return false;
-    }
-
-    virtual app_ref process_lit (app *_lit) {
-        app *lit = _lit;
-        expr *e1, *e2;
-
-        // strip negation
-        bool is_neg = m.is_not(lit);
-        if (is_neg) {
-            lit = to_app(to_app(lit)->get_arg(0));
-        }
-
-        app_ref res(m);
-        res = lit;
-        if (m.is_eq (lit, e1, e2)) {
-            mk_eq_core(e1, e2, res);
-        }
-        else if (m_arith.is_le(lit, e1, e2)) {
-            mk_le_core(e1, e2, res);
-        }
-        else if (m_arith.is_ge(lit, e1, e2)) {
-            mk_ge_core(e1, e2, res);
-        }
-
-        // restore negation
-        if (is_neg) {
-            res = m.mk_not(res);
-        }
-
-        return res;
-    }
-};
-
-term_graph::term_graph(ast_manager &man) : m(man), m_lits(m), m_pinned(m) {
-    m_plugins.register_plugin (alloc(arith_term_graph_plugin, *this));
-}
-
-term_graph::~term_graph() {
-    reset();
-}
-
-static family_id get_family_id(ast_manager &m, app *lit) {
-    family_id fid = null_family_id;
-
-    expr *e1 = nullptr, *e2 = nullptr, *e3 = nullptr;
-    // strip negation
-    if (!m.is_not (lit, e1)) { e1 = lit; }
-
-    // deal with equality using sort of range
-    if (m.is_eq (e1, e2, e3)) {
-        fid = get_sort (e2)->get_family_id();
-    }
-    // extract family_id of top level app
-    else {
-        fid = to_app(e1)->get_decl()->get_family_id();
-    }
-
-    return fid;
-}
-
-void term_graph::add_lit(app *l) {
-    app_ref lit(m);
-
-    family_id fid = get_family_id (m, l);
-    term_graph_plugin *pin = m_plugins.get_plugin(fid);
-    if (pin) {
-        lit = pin->process_lit(l);
-    } else {
-        lit = l;
-    }
-    m_lits.push_back(lit);
-    internalize_lit(lit);
-}
-
-bool term_graph::is_internalized(expr *a) {
-    return m_app2term.contains(a->get_id());
-}
-
-term* term_graph::get_term(expr *a) {
-    term *res;
-    return m_app2term.find (a->get_id(), res) ? res : nullptr;
-}
-
-term *term_graph::mk_term(expr *a) {
-    term * t = alloc(term, a, m_app2term);
-    if (t->get_num_args() == 0 && m.is_unique_value(a)){
-        t->mark_as_interpreted();
-    }
-
-    m_terms.push_back(t);
-    m_app2term.insert(a->get_id(), t);
-    return t;
-}
-
-term* term_graph::internalize_term(expr *t) {
     
-    term* res = get_term(t);
+    term_graph::~term_graph() {
-    if (res) return res;
+        reset();
-    ptr_buffer<expr> todo;
+    }
-    todo.push_back(t);
+
-    while (!todo.empty()) {
+    static family_id get_family_id(ast_manager &m, app *lit) {
+        family_id fid = null_family_id;
+        
+        expr *e1 = nullptr, *e2 = nullptr, *e3 = nullptr;
+        // strip negation
+        if (!m.is_not (lit, e1)) { e1 = lit; }
+        
+        // deal with equality using sort of range
+        if (m.is_eq (e1, e2, e3)) {
+            fid = get_sort (e2)->get_family_id();
+        }
+        // extract family_id of top level app
+        else {
+            fid = to_app(e1)->get_decl()->get_family_id();
+        }
+        
+        return fid;
+    }
+    
+    void term_graph::add_lit(app *l) {
+        app_ref lit(m);
+        
+        family_id fid = get_family_id (m, l);
+        term_graph_plugin *pin = m_plugins.get_plugin(fid);
+        if (pin) {
+            lit = pin->process_lit(l);
+        } else {
+            lit = l;
+        }
+        m_lits.push_back(lit);
+        internalize_lit(lit);
+    }
+    
+    bool term_graph::is_internalized(expr *a) {
+        return m_app2term.contains(a->get_id());
+    }
+    
+    term* term_graph::get_term(expr *a) {
+        term *res;
+        return m_app2term.find (a->get_id(), res) ? res : nullptr;
+    }
+    
+    term *term_graph::mk_term(expr *a) {
+        term * t = alloc(term, a, m_app2term);
+        if (t->get_num_args() == 0 && m.is_unique_value(a)){
+            t->mark_as_interpreted();
+        }
+
+        m_terms.push_back(t);
+        m_app2term.insert(a->get_id(), t);
+        return t;
+    }
+    
+    term* term_graph::internalize_term(expr *t) {        
         term* res = get_term(t);
-        if (res) {
+        if (res) return res;
-            todo.pop_back();
+        ptr_buffer<expr> todo;
-            continue;
+        todo.push_back(t);
-        }
+        while (!todo.empty()) {
-        unsigned sz = todo.size();
+            res = get_term(t);
-        if (is_app(t)) {
+            if (res) {
-            for (expr * arg : *::to_app(t)) {
+                todo.pop_back();
-                if (!get_term(arg)) 
+                continue;
-                    todo.push_back(arg);
             }
+            unsigned sz = todo.size();
+            if (is_app(t)) {
+                for (expr * arg : *::to_app(t)) {
+                    if (!get_term(arg)) 
+                        todo.push_back(arg);
+                }
+            }
+            if (sz < todo.size()) continue;
+            todo.pop_back();
+            res = mk_term(t);
         }
-        if (sz < todo.size()) continue;
+        SASSERT(res);
-        todo.pop_back();
-        res = mk_term(t);
-    }
-    return res;
-}
-
-void term_graph::internalize_eq(expr *a1, expr* a2) {
-    merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root());
-}
-
-void term_graph::internalize_lit(expr* lit) {
-    expr *e1 = nullptr, *e2 = nullptr;
-    if (m.is_eq (lit, e1, e2)) {        
-        internalize_eq (e1, e2);
-    }
-    else {
-        internalize_term(lit);
-    }
-}
-
-void term_graph::merge (term &t1, term &t2) {
-    SASSERT(t1.is_root());
-    SASSERT(t2.is_root());
-
-    if (&t1 == &t2) return;
-
-    term *a = &t1;
-    term *b = &t2;
-    if (a->get_class_size() > b->get_class_size()) {
-        std::swap(a, b);
-    }
-
-    // make 'a' be the root of the equivalence class of 'b'
-    b->set_root(*a);
-    for (term *it = &b->get_next(); it != b; it = &it->get_next()) {
-        // TBD: remove parents of it from the cg table.
-        it->set_root(*a);
-    }
-
-    // merge equivalence classes
-    a->merge_eq_class(*b);
-
-    // TBD: insert parents of b's old equilvalence class into the cg table
-    // and propagate equalities.
-
-    // -- merge might have invalidated term2map cache
-
-    // NSB: ??? what is ownership model of pinned in m_terms?
-    m_term2app.reset();
-    m_pinned.reset();  
-}
-
-expr* term_graph::mk_app_core (expr *e) {
-    if (is_app(e)) {
-        expr_ref_vector kids(m);   
-        app* a = ::to_app(e);
-        for (expr * arg : *a) {
-            kids.push_back (mk_app(arg));
-        }        
-        app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr());
-        m_pinned.push_back(res);
         return res;
     }
-    else {
+    
-        return e;
+    void term_graph::internalize_eq(expr *a1, expr* a2) {
+        SASSERT(m_merge.empty());
+        merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root());
+        merge_flush();
+        SASSERT(m_merge.empty());
+    }
+
+    void term_graph::internalize_lit(expr* lit) {
+        expr *e1 = nullptr, *e2 = nullptr;
+        if (m.is_eq (lit, e1, e2)) {        
+            internalize_eq (e1, e2);
+        }
+        else {
+            internalize_term(lit);
+        }
+    }
+
+    void term_graph::merge_flush() {
+        while (!m_merge.empty()) {
+            term* t1 = m_merge.back().first;
+            term* t2 = m_merge.back().second;
+            m_merge.pop_back();
+            merge(*t1, *t2);
+        }
+    }
+
+    void term_graph::merge(term &t1, term &t2) {
+        // -- merge might invalidate term2map cache
+        m_term2app.reset();
+        m_pinned.reset();  
+        
+        SASSERT(t1.is_root());
+        SASSERT(t2.is_root());
+        
+        if (&t1 == &t2) return;
+        
+        term *a = &t1;
+        term *b = &t2;
+        if (a->get_class_size() > b->get_class_size()) {
+            std::swap(a, b);
+        }
+        
+        // Remove parents of it from the cg table.
+        for (term* p : term::parents(b)) {
+            if (!p->is_marked()) {
+                p->set_mark(true);
+                m_cg_table.erase(p);
+            }
+        }
+        // make 'a' be the root of the equivalence class of 'b'    
+        b->set_root(*a);
+        for (term *it = &b->get_next(); it != b; it = &it->get_next()) {
+            it->set_root(*a);
+        }
+        
+        // merge equivalence classes
+        a->merge_eq_class(*b);
+        
+        // Insert parents of b's old equilvalence class into the cg table
+        for (term* p : term::parents(a)) {
+            if (p->is_marked()) {
+                term* p_old = m_cg_table.insert_if_not_there(p);
+                p->set_mark(false);
+                a->add_parent(p);
+                // propagate new equalities.
+                if (p->get_root().get_id() != p_old->get_root().get_id()) {
+                    m_merge.push_back(std::make_pair(p, p_old));
+                }
+            }
+        }        
+    }
+    
+    expr* term_graph::mk_app_core (expr *e) {
+        if (is_app(e)) {
+            expr_ref_vector kids(m);   
+            app* a = ::to_app(e);
+            for (expr * arg : *a) {
+                kids.push_back (mk_app(arg));
+            }        
+            app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr());
+            m_pinned.push_back(res);
+            return res;
+        }
+        else {
+            return e;
+        }
     }
-}
 
 expr_ref term_graph::mk_app(term const &r) {
     SASSERT(r.is_root());
@@ -598,6 +625,7 @@ void term_graph::reset() {
     std::for_each(m_terms.begin(), m_terms.end(), delete_proc<term>());
     m_terms.reset();
     m_lits.reset();
+    m_cg_table.reset();
 }
 
 expr_ref term_graph::mk_pure(term& t) {
@@ -631,7 +659,7 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl
         if (t->get_root().is_marked()) continue;
         // if exclude = true,  but t in decls, then skip
         // if exclude = false, but t not in decls, then skip
-        if (exclude != _decls.contains(t->get_decl_id())) {
+        if (exclude == _decls.contains(t->get_decl_id())) {
             continue;
         }
         //
@@ -662,7 +690,7 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl
     // walk each root. Then traverse each term in the equivalence class
     // create pure variant of the terms (if possible)
     // equate t0 (that comes from the root, which can be purified)
-    // with any other t1.
+    // with any other purifiable t1.
     expr_ref_vector result(m);
     m_term2app.reset();
     m_pinned.reset();
@@ -675,7 +703,7 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl
         roots.insert(t0);
         for (term* r = &t->get_next(); r != t; r = &r->get_next()) {
             // main symbol of term must be consistent with what is included/excluded
-            if (exclude != _decls.contains(r->get_decl_id())) {
+            if (exclude == _decls.contains(r->get_decl_id())) {
                 continue;
             }
             expr_ref t1 = mk_pure(*r);

src/qe/qe_term_graph.h

@@ -37,18 +37,23 @@ namespace qe {
         /// Process (and potentially augment) a literal
         virtual app_ref process_lit (app *lit) = 0;
     };
-    
+   
+
     class term_graph {
+        struct term_hash { unsigned operator()(term const* t) const; };
+        struct term_eq { bool operator()(term const* a, term const* b) const; };
         ast_manager &     m;
         ptr_vector<term>  m_terms;
         app_ref_vector    m_lits; // NSB: expr_ref_vector?
         u_map<term* >     m_app2term;        
         ast_ref_vector    m_pinned;
         u_map<expr*>      m_term2app;
-        
         plugin_manager<term_graph_plugin> m_plugins;
+        ptr_hashtable<term, term_hash, term_eq> m_cg_table;
+        vector<std::pair<term*,term*>> m_merge;
         
         void merge(term &t1, term &t2);
+        void merge_flush();
         
         term *mk_term(expr *t);
         term *get_term(expr *t);