adding simplifiers layer

simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.

- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.

The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.

scripts/mk_project.py

@@ -31,10 +31,11 @@ def init_project_def():
     add_lib('nlsat', ['polynomial', 'sat'])
     add_lib('lp', ['util', 'nlsat', 'grobner', 'interval', 'smt_params'], 'math/lp')
     add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter')
+    add_lib('simplifiers', ['euf', 'rewriter'], 'ast/simplifiers')
     add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
     add_lib('model', ['rewriter', 'macros'])
-    add_lib('tactic', ['ast', 'model'])
+    add_lib('tactic', ['ast', 'model', 'simplifiers'])
     add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution')
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')

src/CMakeLists.txt

@@ -49,9 +49,10 @@ add_subdirectory(ast/rewriter)
 add_subdirectory(ast/normal_forms)
 add_subdirectory(ast/macros)
 add_subdirectory(model)
+add_subdirectory(ast/euf)
+add_subdirectory(ast/simplifiers)
 add_subdirectory(tactic)
 add_subdirectory(ast/substitution)
-add_subdirectory(ast/euf)
 add_subdirectory(smt/params)
 add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)

src/ast/simplifiers/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(simplifiers
+  SOURCES
+    euf_completion.cpp
+    bv_slice.cpp
+  COMPONENT_DEPENDENCIES
+    euf
+    rewriter
+)

src/ast/simplifiers/bv_slice.cpp

@@ -0,0 +1,207 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_slice.cpp
+
+Abstract:
+
+    simplifier for extracting bit-vector ranges
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/simplifiers/bv_slice.h"
+
+namespace bv {
+
+    void slice::reduce() {
+        process_eqs();
+        apply_subst();
+        advance_qhead(m_fmls.size());
+    }
+
+    void slice::process_eqs() {
+        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+            auto const [f, d] = m_fmls[i]();
+            process_eq(f);
+        }  
+    }
+
+    void slice::process_eq(expr* e) {
+        expr* x, * y;
+        if (!m.is_eq(e, x, y))
+            return;
+        if (!m_bv.is_bv(x))
+            return;
+        m_xs.reset();
+        m_ys.reset();
+        get_concats(x, m_xs);
+        get_concats(y, m_ys);
+        slice_eq();
+    }
+
+    void slice::slice_eq() {
+        unsigned i = m_xs.size(), j = m_ys.size();
+        unsigned offx = 0, offy = 0;
+        while (0 < i) {
+            SASSERT(0 < j);
+            expr* x = m_xs[i - 1]; // least significant bits are last 
+            expr* y = m_ys[j - 1];
+            SASSERT(offx == 0 || offy == 0);
+            unsigned szx = m_bv.get_bv_size(x);
+            unsigned szy = m_bv.get_bv_size(y);
+            SASSERT(offx < szx);
+            SASSERT(offy < szy);
+            if (szx - offx == szy - offy) {
+                register_slice(offx, szx - 1, x);
+                register_slice(offy, szy - 1, y);
+                --i;
+                --j;
+                offx = 0;
+                offy = 0;
+            }
+            else if (szx - offx < szy - offy) {
+                register_slice(offx, szx - 1, x);
+                register_slice(offy, offy + szx - offx - 1, y);
+                offy += szx - offx;
+                offx = 0;
+                --i;
+            }
+            else {
+                register_slice(offy, szy - 1, y);
+                register_slice(offx, offx + szy - offy - 1, x);
+                offx += szy - offy;
+                offy = 0;
+                --j;
+            }
+        }
+    }
+
+    void slice::register_slice(unsigned lo, unsigned hi, expr* x) {
+        SASSERT(lo <= hi && hi < m_bv.get_bv_size(x));
+        unsigned l, h;
+        while (m_bv.is_extract(x, l, h, x)) {
+            // x[l:h][lo:hi] = x[l+lo:l+hi]
+            hi += l;
+            lo += l;
+            SASSERT(lo <= hi && hi < m_bv.get_bv_size(x));
+        }
+        unsigned sz = m_bv.get_bv_size(x);
+        if (hi - lo + 1 == sz)
+            return;
+        SASSERT(0 < lo || hi + 1 < sz);
+        auto& b = m_boundaries.insert_if_not_there(x, uint_set());
+
+        struct remove_set : public trail {
+            uint_set& b;
+            unsigned i;
+            remove_set(uint_set& b, unsigned i) :b(b), i(i) {}
+            void undo() override {
+                b.remove(i);
+            }
+        };
+        if (lo > 0 && !b.contains(lo)) {
+            b.insert(lo); 
+            if (m_num_scopes > 0)
+                m_trail.push(remove_set(b, lo));
+        }
+        if (hi + 1 < sz && !b.contains(hi + 1)) {
+            b.insert(hi + 1); 
+            if (m_num_scopes > 0)
+                m_trail.push(remove_set(b, hi+ 1));
+        }
+    }
+
+    expr* slice::mk_extract(unsigned hi, unsigned lo, expr* x) {
+        unsigned l, h;
+        while (m_bv.is_extract(x, l, h, x)) {
+            lo += l;
+            hi += l;
+        }
+        if (lo == 0 && hi + 1 == m_bv.get_bv_size(x))
+            return x;
+        else
+            return m_bv.mk_extract(hi, lo, x);
+    }
+
+    void slice::apply_subst() {
+        if (m_boundaries.empty())
+            return;            
+        expr_ref_vector cache(m), pin(m);
+        ptr_vector<expr> todo, args;
+        expr* c;
+        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+            auto const [f, d] = m_fmls[i]();
+            todo.push_back(f);
+            pin.push_back(f);
+            while (!todo.empty()) {
+                expr* e = todo.back();
+                c = cache.get(e->get_id(), nullptr);
+                if (c) {
+                    todo.pop_back();
+                    continue;
+                }
+                if (!is_app(e)) {
+                    cache.setx(e->get_id(), e);
+                    todo.pop_back();
+                    continue;
+                }
+                args.reset();
+                unsigned sz = todo.size();
+                bool change = false;
+                for (expr* arg : *to_app(e)) {
+                    c = cache.get(arg->get_id(), nullptr);
+                    if (c) {
+                        args.push_back(c);
+                        change |= c != arg;
+                        SASSERT(c->get_sort() == arg->get_sort());
+                    }
+                    else
+                        todo.push_back(arg);
+                }
+                if (sz == todo.size()) {
+                    todo.pop_back();
+                    if (change)
+                        cache.setx(e->get_id(), m_rewriter.mk_app(to_app(e)->get_decl(), args));
+                    else
+                        cache.setx(e->get_id(), e);
+                    SASSERT(e->get_sort() == cache.get(e->get_id())->get_sort());
+                    uint_set b;
+                    if (m_boundaries.find(e, b)) {
+                        expr* r = cache.get(e->get_id());
+                        expr_ref_vector xs(m);
+                        unsigned lo = 0;
+                        for (unsigned hi : b) {
+                            xs.push_back(mk_extract(hi - 1, lo, r));
+                            lo = hi;
+                        }
+                        xs.push_back(mk_extract(m_bv.get_bv_size(r) - 1, lo, r));
+                        xs.reverse();
+                        expr_ref xc(m_bv.mk_concat(xs), m);
+                        cache.setx(e->get_id(), xc);    
+                        SASSERT(e->get_sort() == xc->get_sort());
+                    }
+                }
+            }
+            c = cache.get(f->get_id());
+            if (c != f)                 
+                m_fmls.update(i, dependent_expr(m, c, d));            
+        }
+    }
+
+    void slice::get_concats(expr* x, ptr_vector<expr>& xs) {
+        while (m_bv.is_concat(x)) {
+            xs.append(to_app(x)->get_num_args(), to_app(x)->get_args()); 
+            x = xs.back();
+            xs.pop_back();
+        }
+        xs.push_back(x);
+    }
+}

src/ast/simplifiers/bv_slice.h

@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_slice.h
+
+Abstract:
+
+    simplifier for extracting bit-vector ranges
+    It rewrites a state using bit-vector slices. 
+    Slices are extracted from bit-vector equality assertions 
+    in the style of (but not fully implementing a full slicing) 
+    Bjorner & Pichora, TACAS 1998 and Brutomesso et al 2008.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#pragma once
+
+#include "util/uint_set.h"
+#include "ast/bv_decl_plugin.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/th_rewriter.h"
+
+
+namespace bv {
+
+    class slice : public dependent_expr_simplifier {
+        bv_util                 m_bv;
+        th_rewriter             m_rewriter;
+        obj_map<expr, uint_set> m_boundaries;
+        ptr_vector<expr>        m_xs, m_ys;
+        
+        expr* mk_extract(unsigned hi, unsigned lo, expr* x);
+        void process_eqs();
+        void process_eq(expr* e);
+        void slice_eq();
+        void register_slice(unsigned lo, unsigned hi, expr* x);     
+        void apply_subst();
+        void get_concats(expr* x, ptr_vector<expr>& xs);
+        
+    public:
+
+        slice(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_bv(m), m_rewriter(m) {}
+
+        void push() override { dependent_expr_simplifier::push(); }
+        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); }
+        void reduce() override;
+    };
+}

src/ast/simplifiers/dependent_expr.h

@@ -0,0 +1,75 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    dependent_expr.h
+
+Abstract:
+
+    Container class for dependent expressions.
+    They represent how assertions are tracked in goals.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+#pragma once
+
+#include "ast/ast.h"
+
+class dependent_expr {
+    ast_manager& m;
+    expr*            m_fml;
+    expr_dependency* m_dep;
+public:
+    dependent_expr(ast_manager& m, expr* fml, expr_dependency* d):
+        m(m),
+        m_fml(fml),
+        m_dep(d) {
+        SASSERT(fml);
+        m.inc_ref(fml);
+        m.inc_ref(d);
+    }
+    
+    dependent_expr& operator=(dependent_expr const& other) {
+        SASSERT(&m == &other.m);
+        if (this != &other) {
+            m.inc_ref(other.m_fml);
+            m.inc_ref(other.m_dep);
+            m.dec_ref(m_fml);
+            m.dec_ref(m_dep);
+            m_fml = other.m_fml;
+            m_dep = other.m_dep;
+        }
+        return *this;
+    }
+    
+    dependent_expr(dependent_expr const& other):
+        m(other.m),
+        m_fml(other.m_fml),
+        m_dep(other.m_dep) {
+        m.inc_ref(m_fml);
+        m.inc_ref(m_dep);
+    }
+
+    dependent_expr(dependent_expr && other) noexcept :
+        m(other.m),
+        m_fml(nullptr),
+        m_dep(nullptr) {
+        std::swap(m_fml, other.m_fml);
+        std::swap(m_dep, other.m_dep);
+    }
+
+    ~dependent_expr() {
+        m.dec_ref(m_fml);
+        m.dec_ref(m_dep);
+        m_fml = nullptr;
+        m_dep = nullptr;
+    }
+    
+    std::tuple<expr*, expr_dependency*> operator()() const { 
+        return { m_fml, m_dep }; 
+    }
+};

src/ast/simplifiers/dependent_expr_state.h

@@ -0,0 +1,86 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    dependent_expr_state.h
+
+Abstract:
+
+    abstraction for simplification of depenent expression states.
+    A dependent_expr_state is an interface to a set of dependent expressions.
+    Dependent expressions are formulas together with a set of dependencies that are coarse grained 
+    proof hints or justifications for them. Input assumptions can be self-justified.
+
+    The dependent_expr_simplifier implements main services:
+    - push, pop - that scope the local state
+    - reduce - to process formulas in a dependent_expr_state between the current value of m_qhead and the size() 
+      of the depdenent_expr_state
+
+    A dependent expr_simplifier can be used to:
+    - to build a tactic
+    - for incremental pre-processing
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+    
+--*/
+
+#pragma once
+
+#include "util/trail.h"
+#include "util/statistics.h"
+#include "util/params.h"
+#include "ast/simplifiers/dependent_expr.h"
+
+/**
+   abstract interface to state updated by simplifiers.
+ */
+class dependent_expr_state {
+public:
+    virtual unsigned size() const = 0;
+    virtual dependent_expr const& operator[](unsigned i) = 0;
+    virtual void update(unsigned i, dependent_expr const& j) = 0;
+    virtual bool inconsistent() = 0;
+};
+
+/**
+   Shared interface of simplifiers. 
+ */
+class dependent_expr_simplifier {
+protected:
+    ast_manager&          m;
+    dependent_expr_state& m_fmls;
+    unsigned       m_qhead = 0;          // pointer into last processed formula in m_fmls
+    unsigned       m_num_scopes = 0;
+    trail_stack    m_trail;    
+    void advance_qhead(unsigned sz) { if (m_num_scopes > 0) m_trail.push(value_trail(m_qhead)); m_qhead = sz; }
+public:
+    dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s) {}
+    virtual ~dependent_expr_simplifier() {}
+    virtual void push() { m_num_scopes++; m_trail.push_scope(); }
+    virtual void pop(unsigned n) { m_num_scopes -= n; m_trail.pop_scope(n); }
+    virtual void reduce() = 0;
+    virtual void collect_statistics(statistics& st) const {}
+    virtual void reset_statistics() {}
+    virtual void updt_params(params_ref const& p) {}
+};
+
+/**
+   Factory interface for creating simplifiers. 
+   The use of a factory allows delaying the creation of the dependent_expr_state
+   argument until the point where the expression simplifier is created.
+   This is used in tactics where the dependent_expr_state is a reference to the
+   new tactic. 
+
+   Alternatively have a clone method on dependent_expr_simplifier.
+ */
+class dependent_expr_simplifier_factory {
+    unsigned m_ref = 0;
+public:
+    virtual dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) = 0;
+    virtual ~dependent_expr_simplifier_factory() {}
+    void inc_ref() { ++m_ref; }
+    void dec_ref() { if (--m_ref == 0) dealloc(this); }
+};

src/ast/simplifiers/euf_completion.cpp

@@ -0,0 +1,330 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    euf_completion.cpp
+
+Abstract:
+
+    Ground completion for equalities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+Notes:
+
+Create a congruence closure of E.
+Select _simplest_ term in each equivalence class. A term is _simplest_
+if it is smallest in a well-order, such as a ground Knuth-Bendix order.
+A basic approach is terms that are of smallest depth, are values can be chosen as simplest.
+Ties between equal-depth terms can be resolved arbitrarily.
+
+
+Algorithm for extracting canonical form from an E-graph:
+
+* Compute function canon(t) that maps every term in E to a canonical, least with respect to well-order relative to the congruence closure.
+  That is, terms that are equal modulo the congruence closure have the same canonical representative.
+
+* Each f(t) = g(s) in E:
+  * add f(canon(t)) = canon(f(t)), g(canon(s)) = canon(g(s)) where canon(f(t)) = canon(g(s)) by construction.
+  
+* Each other g(t) in E:
+  * add g(canon(t)) to E.
+  * Note that canon(g(t)) = true because g(t) = true is added to congruence closure of E.
+* We claim the new formula is equivalent.
+* The dependencies for each rewrite can be computed by following the equality justification data-structure.
+
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
+#include "ast/euf/euf_egraph.h"
+#include "ast/simplifiers/euf_completion.h"
+
+namespace euf {
+
+    completion::completion(ast_manager& m, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls),
+        m_egraph(m),
+        m_canonical(m),
+        m_eargs(m),
+        m_deps(m),
+        m_rewriter(m) {
+        m_tt = m_egraph.mk(m.mk_true(), 0, 0, nullptr);
+        m_ff = m_egraph.mk(m.mk_false(), 0, 0, nullptr);
+    }
+
+    void completion::reduce() {
+        ++m_epoch;
+        add_egraph();
+        map_canonical();
+        read_egraph();
+    }
+
+    void completion::add_egraph() {
+        m_nodes.reset();
+        unsigned sz = m_fmls.size();
+        expr* x, *y;
+        for (unsigned i = m_qhead; i < sz; ++i) {
+            auto [f,d] = m_fmls[i]();
+            auto* n = mk_enode(f);
+            if (m.is_eq(f, x, y)) 
+                m_egraph.merge(n->get_arg(0), n->get_arg(1), d);
+            if (m.is_not(f, x)) 
+                m_egraph.merge(n->get_arg(0), m_ff, d);
+            else 
+                m_egraph.merge(n, m_tt, d);
+        }
+        m_egraph.propagate();
+    }
+
+    void completion::read_egraph() {
+
+        if (m_egraph.inconsistent()) {
+            auto* d = explain_conflict();
+            dependent_expr de(m, m.mk_false(), d);
+            m_fmls.update(0, de);
+            return;
+        }
+
+        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+            auto [f, d] = m_fmls[i]();
+            auto* n = m_egraph.find(f);
+            SASSERT(n);
+            
+            expr_dependency_ref dep(d, m);
+            expr_ref g = canonize_fml(f, dep);
+            if (g != f) {
+                m_fmls.update(i, dependent_expr(m, g, dep));
+                m_stats.m_num_rewrites++;
+                IF_VERBOSE(10, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
+            }
+            CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
+        }
+        advance_qhead(m_fmls.size());
+    }
+
+    enode* completion::mk_enode(expr* e) {
+        m_todo.push_back(e);
+        enode* n;
+        while (!m_todo.empty()) {
+            e = m_todo.back();
+            if (m_egraph.find(e)) {
+                m_todo.pop_back();
+                continue;
+            }
+            if (!is_app(e)) {
+                m_nodes.push_back(m_egraph.mk(e, 0, 0, nullptr));
+                m_todo.pop_back();
+                continue;
+            }
+            m_args.reset();
+            unsigned sz = m_todo.size();
+            for (expr* arg : *to_app(e)) {
+                n = m_egraph.find(arg);
+                if (n)
+                    m_args.push_back(n);
+                else 
+                    m_todo.push_back(arg);
+            }
+            if (sz == m_todo.size()) {
+                m_nodes.push_back(m_egraph.mk(e, 0, m_args.size(), m_args.data()));
+                m_todo.pop_back();
+            }
+        }
+        return m_egraph.find(e);
+    }
+
+    expr_ref completion::canonize_fml(expr* f, expr_dependency_ref& d) {
+
+        expr* x, * y;
+        if (m.is_eq(f, x, y)) {
+            expr_ref x1 = canonize(x, d);
+            expr_ref y1 = canonize(y, d);
+
+            if (x == x1 && y == y1)
+                return expr_ref(f, m);
+            if (x1 == y1)
+                return expr_ref(m.mk_true(), m);
+            else {
+                expr* c = get_canonical(x, d);
+                if (c == x1)
+                    return expr_ref(m.mk_eq(y1, c), m);
+                else if (c == y1)
+                    return expr_ref(m.mk_eq(x1, c), m);
+                else
+                    return expr_ref(m.mk_and(m.mk_eq(x1, c), m.mk_eq(y1, c)), m);
+            }
+        }
+
+        if (m.is_not(f, x)) {
+            expr_ref x1 = canonize(x, d);
+            return expr_ref(mk_not(m, x1), m);
+        }
+
+        return canonize(f, d);
+    }
+
+    expr_ref completion::canonize(expr* f, expr_dependency_ref& d) {
+        if (!is_app(f))
+            return expr_ref(f, m); // todo could normalize ground expressions under quantifiers
+
+        m_eargs.reset();
+        bool change = false;
+        for (expr* arg : *to_app(f)) {
+            m_eargs.push_back(get_canonical(arg, d));
+            change = arg != m_eargs.back();
+        }
+
+        if (!change) 
+            return expr_ref(f, m);        
+        else
+            return expr_ref(m_rewriter.mk_app(to_app(f)->get_decl(), m_eargs.size(), m_eargs.data()), m);
+    }
+
+    expr* completion::get_canonical(expr* f, expr_dependency_ref& d) {
+        enode* n = m_egraph.find(f);
+        enode* r = n->get_root();
+        d = m.mk_join(d, explain_eq(n, r));
+        d = m.mk_join(d, m_deps.get(r->get_id(), nullptr));        
+        return m_canonical.get(r->get_id());
+    }
+    
+    expr* completion::get_canonical(enode* n) {
+        if (m_epochs.get(n->get_id(), 0) == m_epoch)
+            return m_canonical.get(n->get_id());
+        else
+            return nullptr;
+    }
+
+    void completion::set_canonical(enode* n, expr* e) {
+        class vtrail : public trail {
+            expr_ref_vector& c;
+            unsigned idx;
+            expr_ref old_value;
+        public:
+            vtrail(expr_ref_vector& c, unsigned idx) : 
+                c(c), idx(idx), old_value(c.get(idx), c.m()) {
+            }
+        
+            void undo() override {
+                c[idx] = old_value;
+                old_value = nullptr;
+            }
+        };
+        if (m_num_scopes > 0)
+            m_trail.push(vtrail(m_canonical, n->get_id()));
+        m_canonical.setx(n->get_id(), e);
+        m_epochs.setx(n->get_id(), m_epoch, 0);
+    }
+
+    expr_dependency* completion::explain_eq(enode* a, enode* b) {
+        if (a == b)
+            return nullptr;
+        ptr_vector<expr_dependency> just;
+        m_egraph.begin_explain();
+        m_egraph.explain_eq(just, nullptr, a, b);
+        m_egraph.end_explain();
+        expr_dependency* d = nullptr;
+        for (expr_dependency* d2 : just)
+            d = m.mk_join(d, d2);
+        return d;
+    }
+
+    expr_dependency* completion::explain_conflict() {
+        ptr_vector<expr_dependency> just;
+        m_egraph.begin_explain();
+        m_egraph.explain(just, nullptr);
+        m_egraph.end_explain();
+        expr_dependency* d = nullptr;
+        for (expr_dependency* d2 : just)
+            d = m.mk_join(d, d2);
+        return d;
+    }
+
+    void completion::collect_statistics(statistics& st) const {
+        st.update("euf-completion-rewrites", m_stats.m_num_rewrites);        
+    }
+
+    void completion::map_canonical() {
+        m_todo.reset();
+        enode_vector roots;
+        for (unsigned i = 0; i < m_nodes.size(); ++i) {
+            enode* n = m_nodes[i]->get_root();
+            if (n->is_marked1())
+                continue;
+            n->mark1();
+            roots.push_back(n);
+            enode* rep = nullptr;
+            for (enode* k : enode_class(n)) 
+                if (!rep || m.is_value(k->get_expr()) || get_depth(rep->get_expr()) > get_depth(k->get_expr()))
+                    rep = k;
+            m_reps.setx(n->get_id(), rep, nullptr);
+
+            TRACE("euf_completion", tout << "rep " << m_egraph.bpp(n) << " -> " << m_egraph.bpp(rep) << "\n";
+                         for (enode* k : enode_class(n)) tout << m_egraph.bpp(k) << "\n";);
+            m_todo.push_back(n->get_expr());
+            for (enode* arg : enode_args(n)) {
+                arg = arg->get_root();
+                if (!arg->is_marked1())
+                    m_nodes.push_back(arg);
+            }
+        }
+        for (enode* r : roots)
+            r->unmark1();
+
+        // explain dependencies when no nodes are marked.
+        // explain_eq uses both mark1 and mark2 on e-nodes so 
+        // we cannot call it inside the previous loop where mark1 is used
+        // to track which roots have been processed.
+        for (enode* r : roots) {
+            enode* rep = m_reps[r->get_id()];
+            auto* d = explain_eq(r, rep);
+            m_deps.setx(r->get_id(), d);
+        }
+        expr_ref new_expr(m);
+        while (!m_todo.empty()) {
+            expr* e = m_todo.back();
+            enode* n = m_egraph.find(e);
+            SASSERT(n->is_root());
+            enode* rep = m_reps[n->get_id()];
+            if (get_canonical(n)) 
+                m_todo.pop_back();
+            else if (get_depth(rep->get_expr()) == 0 || !is_app(rep->get_expr())) {
+                set_canonical(n, rep->get_expr());
+                m_todo.pop_back();
+            }
+            else {
+                m_eargs.reset();
+                unsigned sz = m_todo.size();
+                bool new_arg = false;
+                expr_dependency* d = m_deps.get(n->get_id(), nullptr);
+                for (enode* arg : enode_args(rep)) {
+                    enode* rarg = arg->get_root();
+                    expr* c = get_canonical(rarg);
+                    if (c) {
+                        m_eargs.push_back(c);
+                        new_arg |= c != arg->get_expr();
+                        d = m.mk_join(d, m_deps.get(rarg->get_id(), nullptr));
+                    }
+                    else
+                        m_todo.push_back(rarg->get_expr());
+                }
+                if (sz == m_todo.size()) {
+                    m_todo.pop_back();
+                    if (new_arg) 
+                        new_expr = m_rewriter.mk_app(to_app(rep->get_expr())->get_decl(), m_eargs.size(), m_eargs.data());                    
+                    else
+                        new_expr = rep->get_expr();                        
+                    set_canonical(n, new_expr);
+                    m_deps.setx(n->get_id(), d);
+                }
+            }
+        }
+    }        
+}
+
+

src/ast/simplifiers/euf_completion.h

@@ -0,0 +1,63 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    euf_completion.h
+
+Abstract:
+
+    Ground completion for equalities
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/euf/euf_egraph.h"
+#include "ast/rewriter/th_rewriter.h"
+
+namespace euf {
+
+    class completion : public dependent_expr_simplifier {
+
+        struct stats {
+            unsigned m_num_rewrites = 0;
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
+        egraph                 m_egraph;
+        enode*                 m_tt, *m_ff;
+        ptr_vector<expr>       m_todo;
+        enode_vector           m_args, m_reps, m_nodes;
+        expr_ref_vector        m_canonical, m_eargs;
+        expr_dependency_ref_vector m_deps;
+        unsigned               m_epoch = 0;
+        unsigned_vector        m_epochs;
+        th_rewriter            m_rewriter;
+        stats                  m_stats;
+
+        enode* mk_enode(expr* e);
+        void add_egraph();
+        void map_canonical();
+        void read_egraph();
+        expr_ref canonize(expr* f, expr_dependency_ref& dep);
+        expr_ref canonize_fml(expr* f, expr_dependency_ref& dep);
+        expr* get_canonical(expr* f, expr_dependency_ref& d);
+        expr* get_canonical(enode* n);
+        void set_canonical(enode* n, expr* e);
+        expr_dependency* explain_eq(enode* a, enode* b);
+        expr_dependency* explain_conflict();
+    public:
+        completion(ast_manager& m, dependent_expr_state& fmls);
+        void push() override { m_egraph.push(); dependent_expr_simplifier::push(); }
+        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); }
+        void reduce() override;
+        void collect_statistics(statistics& st) const override;
+        void reset_statistics() override { m_stats.reset(); }
+    };
+}

src/tactic/CMakeLists.txt

@@ -17,6 +17,7 @@ z3_add_component(tactic
   COMPONENT_DEPENDENCIES
     ast
     model
+    simplifiers
   TACTIC_HEADERS
     probe.h
     tactic.h

src/tactic/bv/CMakeLists.txt

@@ -8,6 +8,7 @@ z3_add_component(bv_tactics
     bv_bound_chk_tactic.cpp
     bv_bounds_tactic.cpp
     bv_size_reduction_tactic.cpp
+    bv_slice_tactic.cpp
     dt2bv_tactic.cpp
     elim_small_bv_tactic.cpp
     max_bv_sharing_tactic.cpp
@@ -21,6 +22,7 @@ z3_add_component(bv_tactics
     bv_bound_chk_tactic.h
     bv_bounds_tactic.h
     bv_size_reduction_tactic.h
+    bv_slice_tactic.h
     bvarray2uf_tactic.h
     dt2bv_tactic.h
     elim_small_bv_tactic.h

src/tactic/bv/bv_slice_tactic.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bv_slice_tactic.h
+
+Abstract:
+
+    Tactic for simplifying with bit-vector slices
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+#pragma once
+
+#include "util/params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_bv_slice_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+  ADD_TACTIC("bv-slice", "simplify using bit-vector slices.", "mk_bv_slice_tactic(m, p)")
+*/
+
+

src/tactic/core/CMakeLists.txt

@@ -10,6 +10,7 @@ z3_add_component(core_tactics
     dom_simplify_tactic.cpp
     elim_term_ite_tactic.cpp
     elim_uncnstr_tactic.cpp
+    euf_completion_tactic.cpp
     injectivity_tactic.cpp
     nnf_tactic.cpp
     occf_tactic.cpp
@@ -38,6 +39,7 @@ z3_add_component(core_tactics
     dom_simplify_tactic.h
     elim_term_ite_tactic.h
     elim_uncnstr_tactic.h
+    euf_completion_tactic.h
     injectivity_tactic.h
     nnf_tactic.h
     occf_tactic.h

src/tactic/core/euf_completion_tactic.cpp

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    euf_completion_tactic.cpp
+
+Abstract:
+
+    Tactic for simplifying with equations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/euf_completion.h"
+#include "tactic/core/euf_completion_tactic.h"
+
+class euf_completion_tactic_factory : public dependent_expr_simplifier_factory {
+public:
+    dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
+        return alloc(euf::completion, m, s);
+    }
+};
+
+tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(euf_completion_tactic_factory), "euf-completion");
+}

src/tactic/core/euf_completion_tactic.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    euf_completion_tactic.h
+
+Abstract:
+
+    Tactic for simplifying with equations.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+#pragma once
+
+#include "util/params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_euf_completion_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+  ADD_TACTIC("euf-completion", "simplify using equalities.", "mk_euf_completion_tactic(m, p)")
+*/
+
+

src/tactic/dependent_expr_state_tactic.h

@@ -0,0 +1,101 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    dependent_expr_state_tactic.h
+
+Abstract:
+
+    The dependent_expr_state_tactic creates a tactic from a dependent_expr_simplifier.
+    It relies on a factory for building simplifiers.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+#include "tactic/tactic.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+
+class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
+    ast_manager&    m;
+    params_ref      m_params;
+    std::string     m_name;
+    ref<dependent_expr_simplifier_factory>  m_factory;
+    scoped_ptr<dependent_expr_simplifier>   m_simp;
+    goal_ref        m_goal;
+    dependent_expr  m_dep;
+
+    void init() {
+        if (!m_simp)
+            m_simp = m_factory->mk(m, m_params, *this);
+    }
+
+public:
+
+    dependent_expr_state_tactic(ast_manager& m, params_ref const& p, dependent_expr_simplifier_factory* f, char const* name):
+        m(m),
+        m_params(p),
+        m_name(name),
+        m_factory(f),
+        m_simp(f->mk(m, p, *this)),
+        m_dep(m, m.mk_true(), nullptr)
+    {}
+
+    /**
+    * size(), [](), update() and inconsisent() implement the abstract interface of dependent_expr_state
+    */
+    unsigned size() const override { return m_goal->size(); }
+
+    dependent_expr const& operator[](unsigned i) override {
+        m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i));
+        return m_dep;
+    }
+    void update(unsigned i, dependent_expr const& j) override {
+        auto [f, d] = j();
+        m_goal->update(i, f, nullptr, d);
+    }
+
+    bool inconsistent() override {
+        return m_goal->inconsistent();
+    }
+        
+    char const* name() const override { return m_name.c_str(); }
+
+    void updt_params(params_ref const & p) override {
+        m_params.append(p);
+        init();
+        m_simp->updt_params(m_params);
+    }
+
+    tactic * translate(ast_manager & m) override {
+        return alloc(dependent_expr_state_tactic, m, m_params, m_factory.get(), name());
+    }
+
+    void operator()(goal_ref const & in, 
+                    goal_ref_buffer & result) override {
+        if (in->proofs_enabled())
+            throw tactic_exception("tactic does not support low level proofs");
+        init();
+        tactic_report report(name(), *in);
+        m_goal = in.get();
+        m_simp->reduce();
+        m_goal->inc_depth();
+        result.push_back(in.get());        
+    }
+
+    void cleanup() override {
+    }
+
+    void collect_statistics(statistics & st) const override {
+        if (m_simp)
+            m_simp->collect_statistics(st);
+    }
+    
+    void reset_statistics() override {
+        if (m_simp)
+            m_simp->reset_statistics();
+    }
+};
+