From ab8fe199c59ac7721c0a8fe03c79af7aa77dd8a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Oct 2023 18:41:23 +0900 Subject: [PATCH] fix case for 0 multiplier in monomial_bounds disabled in master - it violates invariants in the lra solver. --- src/math/lp/monomial_bounds.cpp | 7 ++++++- src/sat/smt/euf_proof_checker.cpp | 6 ++---- src/smt/smt_clause_proof.cpp | 22 +++++++++++++++------- src/smt/smt_clause_proof.h | 6 +++--- src/smt/smt_internalizer.cpp | 6 +++--- src/smt/theory_lra.cpp | 13 +++++++++---- 6 files changed, 38 insertions(+), 22 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index e3b14d1b7..9bc49fc43 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -276,7 +276,7 @@ namespace nla { rational k = fixed_var_product(m); lpvar w = non_fixed_var(m); - if (w == null_lpvar) + if (w == null_lpvar || k == 0) propagate_fixed(m, k); else propagate_nonfixed(m, k, w); @@ -293,6 +293,10 @@ namespace nla { void monomial_bounds::propagate_fixed(monic const& m, rational const& k) { auto* dep = explain_fixed(m, k); + if (!c().lra.is_base(m.var())) { + lp::impq val(k); + c().lra.set_value_for_nbasic_column(m.var(), val); + } c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep); // propagate fixed equality auto exp = get_explanation(dep); @@ -300,6 +304,7 @@ namespace nla { } void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) { + VERIFY(k != 0); vector> coeffs; coeffs.push_back(std::make_pair(-k, w)); coeffs.push_back(std::make_pair(rational::one(), m.var())); diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp index a538b2a80..42cda4bfb 100644 --- a/src/sat/smt/euf_proof_checker.cpp +++ b/src/sat/smt/euf_proof_checker.cpp @@ -501,8 +501,9 @@ namespace euf { for (expr* arg : clause) std::cout << "\n " << mk_bounded_pp(arg, m); std::cout << ")\n"; + std::cout.flush(); - if (is_rup(proof_hint)) + if (false && is_rup(proof_hint)) diagnose_rup_failure(clause); add_clause(clause); @@ -527,9 +528,6 @@ namespace euf { for (expr* f : core) std::cout << mk_pp(f, m) << "\n"; } - SASSERT(false); - - exit(0); } void smt_proof_checker::collect_statistics(statistics& st) const { diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index 777961334..bf27777c4 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -90,14 +90,14 @@ namespace smt { return proof_ref(m); } - void clause_proof::add(clause& c) { + void clause_proof::add(clause& c, literal_buffer const* simp_lits) { if (!is_enabled()) return; justification* j = c.get_justification(); auto st = kind2st(c.get_kind()); auto pr = justification2proof(st, j); CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";); - update(c, st, pr); + update(c, st, pr, simp_lits); } void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) { @@ -137,12 +137,15 @@ namespace smt { update(st, m_lits, pr); } - void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) { + void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits) { if (!is_enabled()) return; m_lits.reset(); m_lits.push_back(ctx.literal2expr(lit1)); m_lits.push_back(ctx.literal2expr(lit2)); + if (simp_lits) + for (auto lit : *simp_lits) + m_lits.push_back(ctx.literal2expr(~lit)); auto st = kind2st(k); auto pr = justification2proof(st, j); update(st, m_lits, pr); @@ -160,7 +163,7 @@ namespace smt { } void clause_proof::del(clause& c) { - update(c, status::deleted, justification2proof(status::deleted, nullptr)); + update(c, status::deleted, justification2proof(status::deleted, nullptr), nullptr); } std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) { @@ -190,7 +193,9 @@ namespace smt { if (ctx.get_fparams().m_clause_proof) m_trail.push_back(info(st, v, p)); if (m_on_clause_eh) - m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data()); + m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data()); + static unsigned s_count = 0; + if (m_has_log) { init_pp_out(); auto& out = *m_pp_out; @@ -220,12 +225,15 @@ namespace smt { } } - void clause_proof::update(clause& c, status st, proof* p) { + void clause_proof::update(clause& c, status st, proof* p, literal_buffer const* simp_lits) { if (!is_enabled()) return; m_lits.reset(); for (literal lit : c) - m_lits.push_back(ctx.literal2expr(lit)); + m_lits.push_back(ctx.literal2expr(lit)); + if (simp_lits) + for (auto lit : *simp_lits) + m_lits.push_back(ctx.literal2expr(~lit)); update(st, m_lits, p); } diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h index 1c5931136..d7cc421cf 100644 --- a/src/smt/smt_clause_proof.h +++ b/src/smt/smt_clause_proof.h @@ -68,7 +68,7 @@ namespace smt { void init_pp_out(); void update(status st, expr_ref_vector& v, proof* p); - void update(clause& c, status st, proof* p); + void update(clause& c, status st, proof* p, literal_buffer const* simp_lits); status kind2st(clause_kind k); proof_ref justification2proof(status st, justification* j); void log(status st, proof* p); @@ -79,8 +79,8 @@ namespace smt { clause_proof(context& ctx); void shrink(clause& c, unsigned new_size); void add(literal lit, clause_kind k, justification* j); - void add(literal lit1, literal lit2, clause_kind k, justification* j); - void add(clause& c); + void add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits = nullptr); + void add(clause& c, literal_buffer const* simp_lits = nullptr); void add(unsigned n, literal const* lits, clause_kind k, justification* j); void propagate(literal lit, justification const& j, literal_vector const& ante); void del(clause& c); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 0e9e39996..b6d1e2f2b 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1378,12 +1378,12 @@ namespace smt { clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) { TRACE("mk_clause", display_literals_verbose(tout << "creating clause: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";); m_clause_proof.add(num_lits, lits, k, j); + literal_buffer simp_lits; switch (k) { case CLS_TH_AXIOM: dump_axiom(num_lits, lits); Z3_fallthrough; case CLS_AUX: { - literal_buffer simp_lits; if (m_searching) dump_lemma(num_lits, lits); if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) { @@ -1451,7 +1451,7 @@ namespace smt { else if (get_assignment(l2) == l_false) { assign(l1, b_justification(~l2)); } - m_clause_proof.add(l1, l2, k, j); + m_clause_proof.add(l1, l2, k, j, &simp_lits); m_stats.m_num_mk_bin_clause++; return nullptr; } @@ -1464,7 +1464,7 @@ namespace smt { bool reinit = save_atoms; SASSERT(!lemma || j == 0 || !j->in_region()); clause * cls = clause::mk(m, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.data()); - m_clause_proof.add(*cls); + m_clause_proof.add(*cls, &simp_lits); if (lemma) { cls->set_activity(activity); if (k == CLS_LEARNED) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1a64d4081..96cd3dd47 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2112,7 +2112,8 @@ public: bool propagate_core() { m_model_is_initialized = false; flush_bound_axioms(); - // disabled in master: propagate_nla(); + // disabled in master: + // propagate_nla(); if (!can_propagate_core()) return false; m_new_def = false; @@ -2161,6 +2162,8 @@ public: } void add_equalities() { + if (!propagate_eqs()) + return; for (auto const& [v,k,e] : m_nla->fixed_equalities()) add_equality(v, k, e); for (auto const& [i,j,e] : m_nla->equalities()) @@ -2168,7 +2171,7 @@ public: } void add_equality(lpvar j, rational const& k, lp::explanation const& exp) { - verbose_stream() << "equality " << j << " " << k << "\n"; + //verbose_stream() << "equality " << j << " " << k << "\n"; TRACE("arith", tout << "equality " << j << " " << k << "\n"); theory_var v; if (k == 1) @@ -3174,8 +3177,7 @@ public: std::function fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); }; scoped_trace_stream _sts(th, fn); - - // SASSERT(validate_eq(x, y)); + //VERIFY(validate_eq(x, y)); ctx().assign_eq(x, y, eq_justification(js)); } @@ -3288,6 +3290,7 @@ public: display(tout << "is-conflict: " << is_conflict << "\n");); for (auto ev : m_explanation) set_evidence(ev.ci(), m_core, m_eqs); + // SASSERT(validate_conflict(m_core, m_eqs)); if (is_conflict) { @@ -3543,6 +3546,8 @@ public: lbool r = nctx.check(); if (r == l_true) { nctx.display_asserted_formulas(std::cout); + std::cout.flush(); + std::cout.flush(); } return l_true != r; }