From 135da9b824b1d9a33be4acdd8bd6d9413d31e36d Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Wed, 15 Mar 2023 16:22:58 +0100 Subject: [PATCH] Log also last conflict --- src/math/polysat/constraint_manager.cpp | 5 +- src/math/polysat/constraint_manager.h | 3 + src/math/polysat/solver.cpp | 100 ++++++++++++------------ src/math/polysat/solver.h | 6 +- 4 files changed, 63 insertions(+), 51 deletions(-) diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index d508f4083..a9aa194a5 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -338,11 +338,14 @@ namespace polysat { signed_constraint constraint_manager::elem(pdd const& t, interval const& i) { if (i.is_full()) - return eq(t.manager().zero()); + return this->t(); else return elem(t, i.lo(), i.hi()); } + signed_constraint constraint_manager::t() { return eq(s.sz2pdd(1).mk_val(0)); } + signed_constraint constraint_manager::f() { return ~t(); } + /** unsigned quotient/remainder */ std::pair constraint_manager::quot_rem(pdd const& a, pdd const& b) { auto& m = a.manager(); diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h index bb59b9c79..d115fe72e 100644 --- a/src/math/polysat/constraint_manager.h +++ b/src/math/polysat/constraint_manager.h @@ -128,6 +128,9 @@ namespace polysat { signed_constraint elem(pdd const& t, pdd const& lo, pdd const& hi); signed_constraint elem(pdd const& t, interval const& i); + signed_constraint t(); + signed_constraint f(); + std::pair quot_rem(pdd const& a, pdd const& b); pdd bnot(pdd const& p); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 28b13c55b..f6246d6a3 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -83,7 +83,7 @@ namespace polysat { if (is_conflict()) LOG("Conflict: " << m_conflict); IF_LOGGING(m_viable.log()); SASSERT(var_queue_invariant()); - if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; } + if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); log_lemma_smt2(*m_conflict.build_lemma()); return l_false; } else if (is_conflict()) resolve_conflict(); else if (can_repropagate_units()) repropagate_units(); else if (should_add_pwatch()) add_pwatch(); @@ -1352,53 +1352,7 @@ namespace polysat { LOG(" " << lit_pp(*this, lit)); } -#if ENABLE_LEMMA_VALIDITY_CHECK - // Write lemma validity check into an *.smt2 file for soundness debugging. - if (clause.is_redundant()) { - namespace fs = std::filesystem; - static unsigned num_lemma = 0; - fs::path filename = std::string("dbg-lemmas/lemma-") + std::to_string(++num_lemma) + ".smt2"; - if (fs::is_directory(filename.parent_path())) { - verbose_stream() << "Writing clause validity check to " << filename << "\n"; - std::stringstream description; - description << " Name: " << clause.name() << "\n"; - description << " Literals:\n"; - uint_set vars; - for (sat::literal lit : clause) { - description << " " << lit_pp(*this, lit) << "\n"; - for (pvar v : lit2cnstr(lit).vars()) - vars.insert(v); - } - bool op_header = false; - for (pvar v : vars) { - signed_constraint c = m_constraints.find_op_by_result_var(v); - if (c && !op_header) { - description << " Relevant op_constraints:\n"; - op_header = true; - } - if (c) - description << " " << c << "\n"; - } - polysat_ast pa(*this); - pa.set_status(l_false); - pa.set_description(description.str()); - pa.add(pa.mk_not(pa.mk_clause(clause))); - if (pa.is_ok()) { - std::ofstream file(filename); - file << pa; - } - else { - filename.replace_extension("txt"); - std::ofstream file(filename); - file << "Not yet implemented in polysat_ast.cpp:\n\n" << description.str(); - } - } - // if (num_lemma == 7) - // std::exit(0); - // if (num_lemma == 161) - // std::exit(0); - } -#endif + log_lemma_smt2(clause); SASSERT(!clause.empty()); m_constraints.store(&clause); @@ -1664,6 +1618,56 @@ namespace polysat { st.update("polysat viable fallback", m_stats.m_num_viable_fallback); } + void solver::log_lemma_smt2(clause& clause) { +#if ENABLE_LEMMA_VALIDITY_CHECK + // Write lemma validity check into an *.smt2 file for soundness debugging. + if (clause.is_redundant()) { + namespace fs = std::filesystem; + static unsigned num_lemma = 0; + fs::path filename = std::string("dbg-lemmas/lemma-") + std::to_string(++num_lemma) + ".smt2"; + if (fs::is_directory(filename.parent_path())) { + verbose_stream() << "Writing clause validity check to " << filename << "\n"; + std::stringstream description; + description << " Name: " << clause.name() << "\n"; + description << " Literals:\n"; + uint_set vars; + for (sat::literal lit : clause) { + description << " " << lit_pp(*this, lit) << "\n"; + for (pvar v : lit2cnstr(lit).vars()) + vars.insert(v); + } + bool op_header = false; + for (pvar v : vars) { + signed_constraint c = m_constraints.find_op_by_result_var(v); + if (c && !op_header) { + description << " Relevant op_constraints:\n"; + op_header = true; + } + if (c) + description << " " << c << "\n"; + } + polysat_ast pa(*this); + pa.set_status(l_false); + pa.set_description(description.str()); + pa.add(pa.mk_not(pa.mk_clause(clause))); + if (pa.is_ok()) { + std::ofstream file(filename); + file << pa; + } + else { + filename.replace_extension("txt"); + std::ofstream file(filename); + file << "Not yet implemented in polysat_ast.cpp:\n\n" << description.str(); + } + } + // if (num_lemma == 7) + // std::exit(0); + // if (num_lemma == 161) + // std::exit(0); + } +#endif + } + bool solver::invariant() { return true; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 9365e7200..3ace14a98 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -324,6 +324,8 @@ namespace polysat { bool inc() { return m_lim.inc(); } + void log_lemma_smt2(clause& clause); + bool invariant(); static bool invariant(signed_constraints const& cs); bool wlist_invariant() const; @@ -532,8 +534,8 @@ namespace polysat { signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); } signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } - signed_constraint t() { return eq(sz2pdd(1).mk_val(0)); } - signed_constraint f() { return ~t(); } + signed_constraint t() { return m_constraints.t(); } + signed_constraint f() { return m_constraints.f(); } /** Create and activate constraints */ void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); }