diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 3ee1e4caf..dfa0c5467 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -514,7 +514,12 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { } if (ProofGen) { quantifier_ref new_q(m().update_quantifier(q, num_pats, new_pats.c_ptr(), num_no_pats, new_no_pats.c_ptr(), new_body), m()); - m_pr = q == new_q ? nullptr : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos)); + m_pr = nullptr; + if (q != new_q) { + m_pr = result_pr_stack().get(fr.m_spos); + m_pr = m().mk_bind_proof(q, m_pr); + m_pr = m().mk_quant_intro(q, new_q, m_pr); + } m_r = new_q; proof_ref pr2(m()); if (m_cfg.reduce_quantifier(new_q, new_body, new_pats.c_ptr(), new_no_pats.c_ptr(), m_r, pr2)) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index eaedd22ba..20e1fb36c 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -69,14 +69,14 @@ static bool is_escape_char(char const *& s, unsigned& result) { } /* 2 octal digits */ if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) && - !is_octal_digit(*(s + 3), d3)) { + !is_octal_digit(*(s + 3), d3)) { result = d1 * 8 + d2; s += 3; return true; } /* 3 octal digits */ if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) && - is_octal_digit(*(s + 3), d3)) { + is_octal_digit(*(s + 3), d3)) { result = d1*64 + d2*8 + d3; s += 4; return true; @@ -296,13 +296,10 @@ bool zstring::operator==(const zstring& other) const { return false; } for (unsigned i = 0; i < length(); ++i) { - unsigned Xi = m_buffer[i]; - unsigned Yi = other[i]; - if (Xi != Yi) { + if (m_buffer[i] != other[i]) { return false; } } - return true; } @@ -325,19 +322,14 @@ bool operator<(const zstring& lhs, const zstring& rhs) { unsigned Ri = rhs[i]; if (Li < Ri) { return true; - } else if (Li > Ri) { + } + else if (Li > Ri) { return false; - } else { - continue; - } + } } // at this point, all compared characters are equal, // so decide based on the relative lengths - if (lhs.length() < rhs.length()) { - return true; - } else { - return false; - } + return lhs.length() < rhs.length(); } @@ -556,7 +548,7 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA); m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT); - m_sigs[OP_STRING_CONST] = 0; + m_sigs[OP_STRING_CONST] = nullptr; m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT); @@ -1063,7 +1055,6 @@ app* seq_util::re::mk_empty(sort* s) { return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, nullptr, 0, nullptr, s); } - bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) { if (is_loop(n)) { app const* a = to_app(n); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 90d1a5481..8a880b1cf 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -523,21 +523,15 @@ namespace smt { SASSERT(pb.is_at_least_k(atom) || pb.is_ge(atom) || pb.is_eq(atom)); } TRACE("pb", display(tout, *c, true);); - //app_ref fml1(m), fml2(m); - //fml1 = c->to_expr(ctx, m); c->unique(); lbool is_true = c->normalize(); c->prune(); c->post_prune(); - //fml2 = c->to_expr(ctx, m); - //expr_ref validate_pb = pb_rewriter(m).mk_validate_rewrite(fml1, fml2); - //pb_rewriter(m).dump_pb_rewrite(validate_pb); literal lit(abv); - TRACE("pb", display(tout, *c); tout << " := " << lit << "\n";); - switch(is_true) { + switch (is_true) { case l_false: lit = ~lit; // fall-through @@ -590,14 +584,11 @@ namespace smt { else { c->m_compilation_threshold = UINT_MAX; } - init_watch_var(*c); + init_watch_ineq(*c); init_watch(abv); m_var_infos[abv].m_ineq = c; m_ineqs_trail.push_back(abv); - - TRACE("pb", display(tout, *c);); - return true; } @@ -699,50 +690,40 @@ namespace smt { } } - void theory_pb::watch_literal(literal lit, ineq* c) { init_watch(lit.var()); ptr_vector* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()]; + TRACE("pb", display(tout << "watch " << lit << " " << (c), *c);); if (ineqs == nullptr) { ineqs = alloc(ptr_vector); m_var_infos[lit.var()].m_lit_watch[lit.sign()] = ineqs; } - ineqs->push_back(c); - } - - - void theory_pb::watch_var(bool_var v, ineq* c) { - init_watch(v); - ptr_vector* ineqs = m_var_infos[v].m_var_watch; - if (ineqs == nullptr) { - ineqs = alloc(ptr_vector); - m_var_infos[v].m_var_watch = ineqs; + for (auto* c1 : *ineqs) { + //if (c1 == c) return; + SASSERT (c1 != c); } ineqs->push_back(c); } - void theory_pb::unwatch_var(bool_var v, ineq* c) { - ptr_vector* ineqs = m_var_infos[v].m_var_watch; - if (ineqs) { - remove(*ineqs, c); - } - } - void theory_pb::unwatch_literal(literal lit, ineq* c) { ptr_vector* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()]; if (ineqs) { + TRACE("pb", display(tout << "unwatch " << lit << " " << (c), *c);); remove(*ineqs, c); } } void theory_pb::remove(ptr_vector& ineqs, ineq* c) { - for (unsigned j = 0; j < ineqs.size(); ++j) { + unsigned sz = ineqs.size(); + for (unsigned j = 0; j < sz; ++j) { if (ineqs[j] == c) { - std::swap(ineqs[j], ineqs[ineqs.size()-1]); + std::swap(ineqs[j], ineqs[sz-1]); ineqs.pop_back(); - break; + TRACE("pb", tout << "removed\n";); + return; } } + TRACE("pb", tout << "not removed\n";); } // ---------------------------- @@ -1042,13 +1023,6 @@ namespace smt { } } } - ineqs = m_var_infos[v].m_var_watch; - if (ineqs != nullptr) { - for (unsigned i = 0; i < ineqs->size(); ++i) { - ineq* c = (*ineqs)[i]; - assign_watch(v, is_true, *c); - } - } ineq* c = m_var_infos[v].m_ineq; if (c != nullptr) { if (c->is_ge()) { @@ -1143,19 +1117,6 @@ namespace smt { return lits; } - class theory_pb::rewatch_vars : public trail { - theory_pb& pb; - ineq& c; - public: - rewatch_vars(theory_pb& p, ineq& c): pb(p), c(c) {} - void undo(context& ctx) override { - for (unsigned i = 0; i < c.size(); ++i) { - pb.watch_var(c.lit(i).var(), &c); - } - } - }; - - class theory_pb::negate_ineq : public trail { ineq& c; public: @@ -1176,7 +1137,6 @@ namespace smt { ctx.push_trail(value_trail(c.m_max_sum)); ctx.push_trail(value_trail(c.m_min_sum)); ctx.push_trail(value_trail(c.m_nfixed)); - ctx.push_trail(rewatch_vars(*this, c)); SASSERT(c.is_ge()); unsigned sz = c.size(); @@ -1227,104 +1187,7 @@ namespace smt { */ void theory_pb::assign_eq(ineq& c, bool is_true) { SASSERT(c.is_eq()); - - } - - /** - Propagation rules: - - nfixed = N & minsum = k -> T - nfixed = N & minsum != k -> F - - minsum > k or maxsum < k -> F - minsum = k & = -> fix 0 variables - nfixed+1 = N & = -> fix unassigned variable or conflict - nfixed+1 = N & != -> maybe forced unassigned to ensure disequal - minsum >= k -> T - maxsum < k -> F - */ - - void theory_pb::assign_watch(bool_var v, bool is_true, ineq& c) { - - context& ctx = get_context(); - unsigned i; - literal l = c.lit(); - lbool asgn = ctx.get_assignment(l); - - if (c.max_sum() < c.mpz_k() && asgn == l_false) { - return; - } - if (c.is_ge() && c.min_sum() >= c.mpz_k() && asgn == l_true) { - return; - } - for (i = 0; i < c.size(); ++i) { - if (c.lit(i).var() == v) { - break; - } - } - - TRACE("pb", display(tout << "assign watch " << literal(v,!is_true) << " ", c, true);); - - SASSERT(i < c.size()); - if (c.lit(i).sign() == is_true) { - ctx.push_trail(value_trail(c.m_max_sum)); - c.m_max_sum -= c.ncoeff(i); - } - else { - ctx.push_trail(value_trail(c.m_min_sum)); - c.m_min_sum += c.ncoeff(i); - } - DEBUG_CODE( - scoped_mpz sum(m_mpz_mgr); - scoped_mpz maxs(m_mpz_mgr); - for (unsigned i = 0; i < c.size(); ++i) { - if (ctx.get_assignment(c.lit(i)) == l_true) sum += c.ncoeff(i); - if (ctx.get_assignment(c.lit(i)) != l_false) maxs += c.ncoeff(i); - } - CTRACE("pb", (maxs > c.max_sum()), display(tout, c, true);); - SASSERT(c.min_sum() <= sum); - SASSERT(sum <= maxs); - SASSERT(maxs <= c.max_sum()); - ); - SASSERT(c.min_sum() <= c.max_sum()); - SASSERT(!m_mpz_mgr.is_neg(c.min_sum())); - ctx.push_trail(value_trail(c.m_nfixed)); - ++c.m_nfixed; - SASSERT(c.nfixed() <= c.size()); - if (c.is_ge() && c.min_sum() >= c.mpz_k() && asgn != l_true) { - TRACE("pb", display(tout << "Set " << l << "\n", c, true);); - add_assign(c, get_helpful_literals(c, false), l); - } - else if (c.max_sum() < c.mpz_k() && asgn != l_false) { - TRACE("pb", display(tout << "Set " << ~l << "\n", c, true);); - add_assign(c, get_unhelpful_literals(c, true), ~l); - } - else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() == c.mpz_k() && asgn != l_true) { - TRACE("pb", display(tout << "Set " << l << "\n", c, true);); - add_assign(c, get_all_literals(c, false), l); - } - else if (c.is_eq() && c.nfixed() == c.size() && c.min_sum() != c.mpz_k() && asgn != l_false) { - TRACE("pb", display(tout << "Set " << ~l << "\n", c, true);); - add_assign(c, get_all_literals(c, false), ~l); - } -#if 0 - else if (c.is_eq() && c.min_sum() > c.mpz_k() && asgn != l_false) { - TRACE("pb", display(tout << "Set " << ~l << "\n", c, true);); - add_assign(c, get_all_literals(c, false), ~l); - } - else if (c.is_eq() && asgn == l_true && c.min_sum() == c.mpz_k() && c.max_sum() > c.mpz_k()) { - literal_vector& lits = get_all_literals(c, false); - lits.push_back(c.lit()); - for (unsigned i = 0; i < c.size(); ++i) { - if (ctx.get_assignment(c.lit(i)) == l_undef) { - add_assign(c, lits, ~c.lit(i)); - } - } - } -#endif - else { - IF_VERBOSE(14, display(verbose_stream() << "no propagation ", c, true);); - } + UNREACHABLE(); } @@ -1682,7 +1545,6 @@ namespace smt { void theory_pb::clear_watch(ineq& c) { for (unsigned i = 0; i < c.size(); ++i) { literal w = c.lit(i); - unwatch_var(w.var(), &c); unwatch_literal(w, &c); } c.m_watch_sum.reset(); @@ -1728,7 +1590,7 @@ namespace smt { ctx.push_trail(unwatch_ge(*this, c)); } - void theory_pb::init_watch_var(ineq& c) { + void theory_pb::init_watch_ineq(ineq& c) { c.m_min_sum.reset(); c.m_max_sum.reset(); c.m_nfixed = 0; @@ -1736,7 +1598,6 @@ namespace smt { c.m_max_watch.reset(); c.m_watch_sz = 0; for (unsigned i = 0; i < c.size(); ++i) { - watch_var(c.lit(i).var(), &c); c.m_max_sum += c.ncoeff(i); } } @@ -2757,16 +2618,6 @@ namespace smt { display_watch(out, vi, false); display_watch(out, vi, true); } - for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { - ineq_watch const* w = m_var_infos[vi].m_var_watch; - if (!w) continue; - out << "watch (v): " << literal(vi) << " |-> "; - ineq_watch const& wl = *w; - for (unsigned i = 0; i < wl.size(); ++i) { - out << wl[i]->lit() << " "; - } - out << "\n"; - } for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { ineq* c = m_var_infos[vi].m_ineq; if (c) { diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index c20683d73..e7b95bf94 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -252,13 +252,12 @@ namespace smt { struct var_info { ineq_watch* m_lit_watch[2]; - ineq_watch* m_var_watch; ineq* m_ineq; card_watch* m_lit_cwatch[2]; card* m_card; - var_info(): m_var_watch(nullptr), m_ineq(nullptr), m_card(nullptr) + var_info(): m_ineq(nullptr), m_card(nullptr) { m_lit_watch[0] = nullptr; m_lit_watch[1] = nullptr; @@ -269,7 +268,6 @@ namespace smt { void reset() { dealloc(m_lit_watch[0]); dealloc(m_lit_watch[1]); - dealloc(m_var_watch); dealloc(m_ineq); dealloc(m_lit_cwatch[0]); dealloc(m_lit_cwatch[1]); @@ -305,16 +303,13 @@ namespace smt { void add_watch(ineq& c, unsigned index); void del_watch(ineq_watch& watch, unsigned index, ineq& c, unsigned ineq_index); void init_watch_literal(ineq& c); - void init_watch_var(ineq& c); + void init_watch_ineq(ineq& c); void clear_watch(ineq& c); void watch_literal(literal lit, ineq* c); - void watch_var(bool_var v, ineq* c); void unwatch_literal(literal w, ineq* c); - void unwatch_var(bool_var v, ineq* c); void remove(ptr_vector& ineqs, ineq* c); bool assign_watch_ge(bool_var v, bool is_true, ineq_watch& watch, unsigned index); - void assign_watch(bool_var v, bool is_true, ineq& c); void assign_ineq(ineq& c, bool is_true); void assign_eq(ineq& c, bool is_true);