minor fixes

- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.

src/ast/euf/euf_egraph.cpp

@@ -904,6 +904,10 @@ template void euf::egraph::explain_todo(ptr_vector<size_t>& justifications, cc_j
 template void euf::egraph::explain_eq(ptr_vector<size_t>& justifications, cc_justification*, enode* a, enode* b);
 template unsigned euf::egraph::explain_diseq(ptr_vector<size_t>& justifications, cc_justification*, enode* a, enode* b);
 
+template void euf::egraph::explain(ptr_vector<expr_dependency>& justifications, cc_justification*);
+template void euf::egraph::explain_todo(ptr_vector<expr_dependency>& justifications, cc_justification*);
+template void euf::egraph::explain_eq(ptr_vector<expr_dependency>& justifications, cc_justification*, enode* a, enode* b);
+template unsigned euf::egraph::explain_diseq(ptr_vector<expr_dependency>& justifications, cc_justification*, enode* a, enode* b);
 
 
 #if 0

src/ast/euf/euf_etable.cpp

@@ -201,8 +201,6 @@ namespace euf {
     enode_bool_pair etable::insert(enode * n) {
         // it doesn't make sense to insert a constant.
         SASSERT(n->num_args() > 0);
-        SASSERT(!m_manager.is_and(n->get_expr()));
-        SASSERT(!m_manager.is_or(n->get_expr()));
         enode * n_prime;
         void * t = get_table(n); 
         switch (static_cast<table_kind>(GET_TAG(t))) {

src/ast/justified_expr.h

@@ -33,8 +33,7 @@ public:
     justified_expr(justified_expr const& other):
         m(other.m),
         m_fml(other.m_fml),
-        m_proof(other.m_proof)
+        m_proof(other.m_proof) {
-    {
         m.inc_ref(m_fml);
         m.inc_ref(m_proof);
     }
@@ -42,8 +41,7 @@ public:
     justified_expr(justified_expr && other) noexcept :
         m(other.m),
         m_fml(nullptr),
-        m_proof(nullptr)
+        m_proof(nullptr) {
-    {
         std::swap(m_fml, other.m_fml);
         std::swap(m_proof, other.m_proof);
     }
@@ -51,10 +49,11 @@ public:
     ~justified_expr() {
         m.dec_ref(m_fml);
         m.dec_ref(m_proof);
-		m_fml = nullptr;
+        m_fml = nullptr;
-		m_proof = nullptr;
+        m_proof = nullptr;
     }
     
     expr* get_fml() const { return m_fml; }
+
     proof* get_proof() const { return m_proof; }        
 };

src/ast/rewriter/bool_rewriter.cpp

@@ -290,7 +290,7 @@ br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args,
                 ast_lt lt;
                 std::sort(flat_args.begin(), flat_args.end(), lt);
             }
-            result = m().mk_or(flat_args);
+            result = mk_or_app(flat_args.size(), flat_args.data());
         }
         return BR_DONE;
     }

src/ast/rewriter/mk_extract_proc.cpp

@@ -32,8 +32,15 @@ mk_extract_proc::~mk_extract_proc() {
 }
 
 app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
+    unsigned l, h;
+    while (m_util.is_extract(arg, l, h, arg)) {
+        low += l;
+        high += l;
+    }
     ast_manager & m = m_util.get_manager();
     sort * s = arg->get_sort();
+    if (low == 0 && high + 1 == m_util.get_bv_size(arg) && is_app(arg))
+        return to_app(arg);
     if (m_low == low && m_high == high && m_domain == s)
         return m.mk_app(m_f_cached, arg);
     // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain

src/ast/rewriter/th_rewriter.h

@@ -47,6 +47,7 @@ public:
     expr_ref operator()(expr * n, unsigned num_bindings, expr * const * bindings);
 
     expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args);
+    expr_ref mk_app(func_decl* f, ptr_vector<expr> const& args) { return mk_app(f, args.size(), args.data()); }
 
     bool reduce_quantifier(quantifier * old_q, 
                            expr * new_body, 

src/tactic/core/solve_eqs_tactic.cpp

@@ -1141,9 +1141,6 @@ public:
     
 };
 
-tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r) {
+tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p) {
-    if (r == nullptr)
+    return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true));
-        return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true));
-    else
-        return clean(alloc(solve_eqs_tactic, m, p, r, false));
 }

src/tactic/core/solve_eqs_tactic.h

@@ -21,9 +21,8 @@ Revision History:
 #include "util/params.h"
 class ast_manager;
 class tactic;
-class expr_replacer;
 
-tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref(), expr_replacer * r = nullptr);
+tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref());
 
 /*
   ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs_tactic(m, p)")

src/tactic/core/symmetry_reduce_tactic.cpp

@@ -25,6 +25,7 @@ Notes:
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_util.h"
 
 class symmetry_reduce_tactic : public tactic {
     class imp;
@@ -608,12 +609,12 @@ private:
         return (j == A.size())?0:A[j];
     }
 
-    app* mk_member(app* t, term_set const& C) {
+    expr* mk_member(app* t, term_set const& C) {
         expr_ref_vector eqs(m());
         for (unsigned i = 0; i < C.size(); ++i) {
             eqs.push_back(m().mk_eq(t, C[i]));
         }
-        return m().mk_or(eqs.size(), eqs.data());
+        return mk_or(m(), eqs.size(), eqs.data());
     }
 };