diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 6034d8428..c8605b297 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -904,6 +904,10 @@ template void euf::egraph::explain_todo(ptr_vector& justifications, cc_j template void euf::egraph::explain_eq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); template unsigned euf::egraph::explain_diseq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); +template void euf::egraph::explain(ptr_vector& justifications, cc_justification*); +template void euf::egraph::explain_todo(ptr_vector& justifications, cc_justification*); +template void euf::egraph::explain_eq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); +template unsigned euf::egraph::explain_diseq(ptr_vector& justifications, cc_justification*, enode* a, enode* b); #if 0 diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index cfc99e4a0..e007297ef 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/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(GET_TAG(t))) { diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h index 786061065..a599ff5a1 100644 --- a/src/ast/justified_expr.h +++ b/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_proof = nullptr; + m_fml = nullptr; + m_proof = nullptr; } expr* get_fml() const { return m_fml; } + proof* get_proof() const { return m_proof; } }; diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 80495853a..1964e6528 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/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; } diff --git a/src/ast/rewriter/mk_extract_proc.cpp b/src/ast/rewriter/mk_extract_proc.cpp index be61047a4..cc18ae176 100644 --- a/src/ast/rewriter/mk_extract_proc.cpp +++ b/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 diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 271500551..e432678a4 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/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 const& args) { return mk_app(f, args.size(), args.data()); } bool reduce_quantifier(quantifier * old_q, expr * new_body, diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index a7b206d5b..5a076aa0f 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/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) { - if (r == nullptr) - 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)); +tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true)); } diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h index d986b0dbf..d65a33046 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/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)") diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 9aa4c9448..e94e83679 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/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()); } };