diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index cb1f63881..89588ee0e 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -386,9 +386,31 @@ public: bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); } 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); } + bool is_redand(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDAND); } + bool is_redor(expr const* e) const { return is_app_of(e, get_fid(), OP_BREDOR); } + bool is_comp(expr const* e) const { return is_app_of(e, get_fid(), OP_BCOMP); } + bool is_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_LEFT); } + bool is_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_ROTATE_RIGHT); } + bool is_ext_rotate_left(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_LEFT); } + bool is_ext_rotate_right(expr const* e) const { return is_app_of(e, get_fid(), OP_EXT_ROTATE_RIGHT); } + + bool is_rotate_left(expr const* e, unsigned& n, expr*& x) const { + return is_rotate_left(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true); + } + bool is_rotate_right(expr const* e, unsigned& n, expr*& x) const { + return is_rotate_right(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true); + } + bool is_int2bv(expr const* e, unsigned& n, expr*& x) const { + return is_int2bv(e) && (n = to_app(e)->get_parameter(0).get_int(), x = to_app(e)->get_arg(0), true); + } MATCH_UNARY(is_bv_not); + MATCH_UNARY(is_redand); + MATCH_UNARY(is_redor); + MATCH_BINARY(is_ext_rotate_left); + MATCH_BINARY(is_ext_rotate_right); + MATCH_BINARY(is_comp); MATCH_BINARY(is_bv_add); MATCH_BINARY(is_bv_sub); MATCH_BINARY(is_bv_mul); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 716a8effe..a1b88bed1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -879,7 +879,6 @@ namespace sat { m_conflict = c; m_not_l = not_l; TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n")); - TRACE("sat", display_watches(tout)); } void solver::assign_core(literal l, justification j) { @@ -1720,6 +1719,9 @@ namespace sat { if (next == null_bool_var) return false; } + else { + SASSERT(value(next) == l_undef); + } push(); m_stats.m_decision++; @@ -1729,11 +1731,14 @@ namespace sat { phase = guess(next) ? l_true: l_false; literal next_lit(next, false); + SASSERT(value(next_lit) == l_undef); if (m_ext && m_ext->decide(next, phase)) { + if (used_queue) m_case_split_queue.unassign_var_eh(next); next_lit = literal(next, false); + SASSERT(value(next_lit) == l_undef); } if (phase == l_undef) @@ -2553,7 +2558,8 @@ namespace sat { } SASSERT(lvl(c_var) < m_conflict_lvl); } - CTRACE("sat", idx == 0, + CTRACE("sat", idx == 0, + tout << "conflict level " << m_conflict_lvl << "\n"; for (literal lit : m_trail) if (is_marked(lit.var())) tout << "missed " << lit << "@" << lvl(lit) << "\n";); @@ -2808,8 +2814,9 @@ namespace sat { unsigned level = 0; if (not_l != null_literal) { - level = lvl(not_l); + level = lvl(not_l); } + TRACE("sat", tout << "level " << not_l << " is " << level << " " << js << "\n"); switch (js.get_kind()) { case justification::NONE: @@ -3484,11 +3491,10 @@ namespace sat { // // ----------------------- void solver::push() { + SASSERT(!m_ext || !m_ext->can_propagate()); SASSERT(!inconsistent()); TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";); SASSERT(m_qhead == m_trail.size()); - if (m_ext) - m_ext->unit_propagate(); m_scopes.push_back(scope()); scope & s = m_scopes.back(); m_scope_lvl++; diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 0150824b2..09db74f75 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -250,7 +250,6 @@ namespace arith { add_clause(~bitof(n, i), bitof(y, i)); else continue; - verbose_stream() << "added b-and clause\n"; return false; } return true; diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 943d0b324..f750f186d 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -106,7 +106,6 @@ namespace euf { attach_node(mk_enode(e, 0, nullptr)); return true; } - bool solver::post_visit(expr* e, bool sign, bool root) { unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0; m_args.reset(); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 68e5e4cc6..b2302a22d 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -145,18 +145,21 @@ namespace polysat { case OP_BSMOD_I: case OP_BSDIV: case OP_BSDIV_I: - expr2pdd(a); - m_delayed_axioms.push_back(a); - ctx.push(push_back_vector(m_delayed_axioms)); - break; - - case OP_BREDAND: // x == 2^K - 1 unary, return single bit, 1 if all input bits are set. case OP_BREDOR: // x > 0 unary, return single bit, 1 if at least one input bit is set. + case OP_BREDAND: // x == 2^K - 1 unary, return single bit, 1 if all input bits are set. case OP_BCOMP: // x == y ? 1 : 0 binary, return single bit, 1 if the arguments are equal. case OP_ROTATE_LEFT: case OP_ROTATE_RIGHT: case OP_EXT_ROTATE_LEFT: case OP_EXT_ROTATE_RIGHT: + case OP_INT2BV: + case OP_BV2INT: + if (bv.is_bv(a)) + expr2pdd(a); + m_delayed_axioms.push_back(a); + ctx.push(push_back_vector(m_delayed_axioms)); + break; + default: IF_VERBOSE(0, verbose_stream() << mk_pp(a, m) << "\n"); NOT_IMPLEMENTED_YET(); @@ -276,6 +279,7 @@ namespace polysat { for (; m_delayed_axioms_qhead < m_delayed_axioms.size() && !inconsistent(); ++m_delayed_axioms_qhead) { app* e = m_delayed_axioms[m_delayed_axioms_qhead]; expr* x, *y; + unsigned n = 0; if (bv.is_bv_sdiv(e, x, y)) axiomatize_sdiv(e, x, y); else if (bv.is_bv_sdivi(e, x, y)) @@ -288,12 +292,92 @@ namespace polysat { axiomatize_smod(e, x, y); else if (bv.is_bv_smodi(e, x, y)) axiomatize_smod(e, x, y); + else if (bv.is_redand(e, x)) + axiomatize_redand(e, x); + else if (bv.is_redor(e, x)) + axiomatize_redor(e, x); + else if (bv.is_comp(e, x, y)) + axiomatize_comp(e, x, y); + else if (bv.is_rotate_left(e, n, x)) + axiomatize_rotate_left(e, n, x); + else if (bv.is_rotate_right(e, n, x)) + axiomatize_rotate_right(e, n, x); + else if (bv.is_ext_rotate_left(e, x, y)) + axiomatize_ext_rotate_left(e, x, y); + else if (bv.is_ext_rotate_right(e, x, y)) + axiomatize_ext_rotate_right(e, x, y); + else if (bv.is_bv2int(e, x)) + axiomatize_bv2int(e, x); + else if (bv.is_int2bv(e, n, x)) + axiomatize_int2bv(e, n, x); else UNREACHABLE(); } return true; } + void solver::axiomatize_int2bv(app* e, unsigned & sz, expr* x) { + NOT_IMPLEMENTED_YET(); + + } + + void solver::axiomatize_bv2int(app* e, expr* x) { + NOT_IMPLEMENTED_YET(); + } + + + expr* solver::rotate_left(app* e, unsigned n, expr* x) { + unsigned sz = bv.get_bv_size(x); + n = n % sz; + if (n == 0 || sz == 1) + return x; + else + return bv.mk_concat(bv.mk_extract(n, 0, x), bv.mk_extract(sz - 1, sz - n - 1, x)); + } + + void solver::axiomatize_rotate_left(app* e, unsigned n, expr* x) { + // e = x[n : 0] ++ x[sz - 1, sz - n - 1] + add_unit(eq_internalize(e, rotate_left(e, n, x))); + } + + void solver::axiomatize_rotate_right(app* e, unsigned n, expr* x) { + unsigned sz = bv.get_bv_size(x); + axiomatize_rotate_left(e, sz - n, x); + } + + void solver::axiomatize_ext_rotate_left(app* e, expr* x, expr* y) { + unsigned sz = bv.get_bv_size(x); + for (unsigned i = 0; i < sz; ++i) + add_clause(~eq_internalize(bv.mk_numeral(i, sz), y), eq_internalize(e, rotate_left(e, i, x))); + add_clause(~mk_literal(bv.mk_ule(bv.mk_numeral(sz, sz), y)), eq_internalize(e, bv.mk_zero(sz))); + } + + void solver::axiomatize_ext_rotate_right(app* e, expr* x, expr* y) { + unsigned sz = bv.get_bv_size(x); + for (unsigned i = 0; i < sz; ++i) + add_clause(~eq_internalize(bv.mk_numeral(i, sz), y), eq_internalize(e, rotate_left(e, sz - i, x))); + add_clause(~mk_literal(bv.mk_ule(bv.mk_numeral(sz, sz), y)), eq_internalize(e, bv.mk_zero(sz))); + } + + // x = N - 1 + void solver::axiomatize_redand(app* e, expr* x) { + unsigned sz = bv.get_bv_size(x); + rational N = rational::power_of_two(sz); + add_equiv(expr2literal(e), eq_internalize(x, bv.mk_numeral(N - 1, sz))); + } + + void solver::axiomatize_redor(app* e, expr* x) { + unsigned sz = bv.get_bv_size(x); + add_equiv(expr2literal(e), ~eq_internalize(x, bv.mk_zero(sz))); + } + + void solver::axiomatize_comp(app* e, expr* x, expr* y) { + unsigned sz = bv.get_bv_size(x); + auto eq = eq_internalize(x, y); + add_clause(~eq, eq_internalize(e, bv.mk_numeral(1, sz))); + add_clause(eq, eq_internalize(e, bv.mk_numeral(0, sz))); + } + // y = 0 -> x // else x - sdiv(x, y) * y void solver::axiomatize_srem(app* e, expr* x, expr* y) { diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index c8d9e314d..8038cc4bb 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -133,6 +133,16 @@ namespace polysat { void axiomatize_srem(app* e, expr* x, expr* y); void axiomatize_smod(app* e, expr* x, expr* y); void axiomatize_sdiv(app* e, expr* x, expr* y); + void axiomatize_redand(app* e, expr* x); + void axiomatize_redor(app* e, expr* x); + void axiomatize_comp(app* e, expr* x, expr* y); + void axiomatize_rotate_left(app* e, unsigned n, expr* x); + void axiomatize_rotate_right(app* e, unsigned n, expr* x); + void axiomatize_ext_rotate_left(app* e, expr* x, expr* y); + void axiomatize_ext_rotate_right(app* e, expr* x, expr* y); + void axiomatize_int2bv(app* e, unsigned & sz, expr* x); + void axiomatize_bv2int(app* e, expr* x); + expr* rotate_left(app* e, unsigned n, expr* x); unsigned m_delayed_axioms_qhead = 0; ptr_vector m_delayed_axioms; bool propagate_delayed_axioms();