diff --git a/src/ast/ast.h b/src/ast/ast.h index 0a3e90941..add305694 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2193,6 +2193,9 @@ public: app * mk_xor(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_XOR, lhs, rhs); } app * mk_ite(expr * c, expr * t, expr * e) { return mk_app(m_basic_family_id, OP_ITE, c, t, e); } app * mk_xor(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_XOR, num_args, args); } + app * mk_xor(ptr_buffer const& args) { return mk_xor(args.size(), args.c_ptr()); } + app * mk_xor(ptr_vector const& args) { return mk_xor(args.size(), args.c_ptr()); } + app * mk_xor(ref_buffer const& args) { return mk_xor(args.size(), args.c_ptr()); } app * mk_or(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_OR, num_args, args); } app * mk_and(unsigned num_args, expr * const * args) { return mk_app(m_basic_family_id, OP_AND, num_args, args); } app * mk_or(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2); } diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 62f7d246c..cf1ef1cdd 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -352,6 +352,8 @@ public: bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); } bool is_bv_umul_no_ovfl(expr const* e) const { return is_app_of(e, get_fid(), OP_BUMUL_NO_OVFL); } + MATCH_UNARY(is_bv_not); + MATCH_BINARY(is_bv_add); MATCH_BINARY(is_bv_mul); MATCH_BINARY(is_bv_sle); diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 86a0f3894..1f9395c63 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2293,16 +2293,15 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { return BR_DONE; } - if (m().is_ite(lhs)) { - result = m().mk_ite(to_app(lhs)->get_arg(0), - m().mk_eq(to_app(lhs)->get_arg(1), rhs), - m().mk_eq(to_app(lhs)->get_arg(2), rhs)); + expr* a = nullptr, *b = nullptr, *c = nullptr; + if (m().is_ite(lhs, a, b, c)) { + result = m().mk_ite(a, m().mk_eq(b, rhs), m().mk_eq(c, rhs)); return BR_REWRITE2; } - - if (m_util.is_bv_not(lhs)) { + + if (m_util.is_bv_not(lhs, a)) { SASSERT(v.is_one() || v.is_zero()); - result = m().mk_eq(to_app(lhs)->get_arg(0), mk_numeral(numeral(1) - v, 1)); + result = m().mk_eq(a, mk_numeral(numeral(1) - v, 1)); return BR_REWRITE1; } @@ -2313,11 +2312,9 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { if (m_util.is_bv_or(lhs)) { ptr_buffer new_args; - unsigned num = to_app(lhs)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - new_args.push_back(m().mk_eq(to_app(lhs)->get_arg(i), bit1)); - } - result = m().mk_or(new_args.size(), new_args.c_ptr()); + for (expr* arg : *to_app(lhs)) + new_args.push_back(m().mk_eq(arg, bit1)); + result = m().mk_or(new_args); if (is_one) { return BR_REWRITE2; } @@ -2330,12 +2327,10 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { if (m_util.is_bv_xor(lhs)) { ptr_buffer new_args; - unsigned num = to_app(lhs)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - new_args.push_back(m().mk_eq(to_app(lhs)->get_arg(i), bit1)); - } + for (expr* arg : *to_app(lhs)) + new_args.push_back(m().mk_eq(arg, bit1)); // TODO: bool xor is not flat_assoc... must fix that. - result = m().mk_xor(new_args.size(), new_args.c_ptr()); + result = m().mk_xor(new_args); if (is_one) { return BR_REWRITE2; } @@ -2372,7 +2367,7 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu mk_numeral(bit0 ? 0 : 1, 1))); div(v, two, v); } - result = m().mk_and(new_args.size(), new_args.c_ptr()); + result = m().mk_and(new_args); return BR_REWRITE3; } @@ -2438,7 +2433,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { } SASSERT(i1 == 0 && i2 == 0); SASSERT(new_eqs.size() >= 1); - result = m().mk_and(new_eqs.size(), new_eqs.c_ptr()); + result = m().mk_and(new_eqs); return BR_REWRITE3; } diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index c515b5886..3b87d65f3 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -110,14 +110,16 @@ namespace array { struct hash { solver& s; hash(solver& s) :s(s) {} + unsigned hash_select(axiom_record const& r) const { + unsigned h = mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select->get_arg(1)->get_expr_id()); + for (unsigned i = 2; i < r.select->num_args(); ++i) + h = mk_mix(h, h, r.select->get_arg(i)->get_expr_id()); + return h; + } unsigned operator()(unsigned idx) const { auto const& r = s.m_axiom_trail[idx]; - if (r.m_kind == kind_t::is_select) { - unsigned h = mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select->get_arg(1)->get_expr_id()); - for (unsigned i = 2; i < r.select->num_args(); ++i) - h = mk_mix(h, 1, r.select->get_arg(i)->get_expr_id()); - return h; - } + if (r.m_kind == kind_t::is_select) + return hash_select(r); return mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select ? r.select->get_expr_id() : 1); } }; @@ -125,17 +127,20 @@ namespace array { struct eq { solver& s; eq(solver& s) :s(s) {} - unsigned operator()(unsigned a, unsigned b) const { - auto const& p = s.m_axiom_trail[a]; - auto const& r = s.m_axiom_trail[b]; + bool eq_select(axiom_record const& p, axiom_record const& r) const { if (p.m_kind != r.m_kind || p.n != r.n) return false; - if (p.m_kind != kind_t::is_select) - return p.select == r.select; for (unsigned i = p.select->num_args(); i-- > 1; ) if (p.select->get_arg(i) != r.select->get_arg(i)) return false; - return true; + return true; + } + unsigned operator()(unsigned a, unsigned b) const { + auto const& p = s.m_axiom_trail[a]; + auto const& r = s.m_axiom_trail[b]; + if (p.m_kind == kind_t::is_select) + return eq_select(p, r); + return p.m_kind == r.m_kind && p.n == r.n && p.select == r.select; } }; }; diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp index fbb96d9d6..264399e7d 100644 --- a/src/sat/smt/recfun_solver.cpp +++ b/src/sat/smt/recfun_solver.cpp @@ -312,6 +312,8 @@ namespace recfun { } if (found) { ++m_num_rounds; + if (!to_delete && !m_disabled_guards.empty()) + to_delete = m_disabled_guards.back(); if (to_delete) { m_disabled_guards.erase(to_delete); m_enabled_guards.push_back(to_delete); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 7f8a6dd0c..0a30202e1 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -436,13 +436,15 @@ namespace smt { } if (found) { m_num_rounds++; + if (!to_delete && !m_disabled_guards.empty()) + to_delete = m_disabled_guards.back(); if (to_delete) { m_disabled_guards.erase(to_delete); m_enabled_guards.push_back(to_delete); IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n"); } else { - IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n"); + IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round " << m_num_rounds << ")\n"); } for (expr* g : m_enabled_guards) push_guard(g);