mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Log also last conflict

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-03-15 16:22:58 +01:00
parent 03a6d74c58
commit 135da9b824
4 changed files with 63 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/polysat/constraint_manager.cpp
View file

@ -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<pdd, pdd> constraint_manager::quot_rem(pdd const& a, pdd const& b) {
auto& m = a.manager();

3
src/math/polysat/constraint_manager.h
View file

@ -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<pdd, pdd> quot_rem(pdd const& a, pdd const& b);
pdd bnot(pdd const& p);

100
src/math/polysat/solver.cpp
View file

@ -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;
}

6
src/math/polysat/solver.h
View file

@ -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); }