mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 11:20:26 +00:00
Code Activity

pass along lemma name

Browse source
This commit is contained in:
Jakob Rath 2024-02-26 10:51:01 +01:00
parent b561795214
commit 94e2e0c3e6
5 changed files with 24 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/intblast_solver.cpp
View file

@ -182,20 +182,20 @@ namespace intblast {
translate_expr(e); translate_expr(e);
} }
lbool solver::check_axiom(sat::literal_vector const& lits) { lbool solver::check_axiom(char const* name, sat::literal_vector const& lits) {
sat::literal_vector core; sat::literal_vector core;
for (auto lit : lits) for (auto lit : lits)
core.push_back(~lit); core.push_back(~lit);
return check_core(core, {}); return check_core(name, core, {});
} }
lbool solver::check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) { lbool solver::check_propagation(char const* name, sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
sat::literal_vector core; sat::literal_vector core;
core.append(lits); core.append(lits);
core.push_back(~lit); core.push_back(~lit);
return check_core(core, eqs); return check_core(name, core, eqs);
} }
lbool solver::check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) { lbool solver::check_core(char const* name, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
m_core.reset(); m_core.reset();
m_vars.reset(); m_vars.reset();
m_is_plugin = false; m_is_plugin = false;

6
src/sat/smt/intblast_solver.h
View file

@ -105,9 +105,9 @@ namespace intblast {
~solver() override {} ~solver() override {}
lbool check_axiom(sat::literal_vector const& lits); lbool check_axiom(char const* name, sat::literal_vector const& lits);
lbool check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs); lbool check_core(char const* name, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
lbool check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs); lbool check_propagation(char const* name, sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
lbool check_solver_state(); lbool check_solver_state();

12
src/sat/smt/polysat_model.cpp
View file

@ -97,24 +97,24 @@ namespace polysat {
return out; return out;
} }
void solver::validate_propagate(sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) { void solver::validate_propagate(char const* name, sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
if (!ctx.get_config().m_core_validate) if (!ctx.get_config().m_core_validate)
return; return;
auto r = m_intblast.check_propagation(lit, core, eqs); auto r = m_intblast.check_propagation(name, lit, core, eqs);
VERIFY (r != l_true); VERIFY (r != l_true);
} }
void solver::validate_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) { void solver::validate_conflict(char const* name, sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
if (!ctx.get_config().m_core_validate) if (!ctx.get_config().m_core_validate)
return; return;
auto r = m_intblast.check_core(core, eqs); auto r = m_intblast.check_core(name, core, eqs);
VERIFY (r != l_true); VERIFY (r != l_true);
} }
void solver::validate_axiom(sat::literal_vector const& clause) { void solver::validate_axiom(char const* name, sat::literal_vector const& clause) {
if (!ctx.get_config().m_core_validate) if (!ctx.get_config().m_core_validate)
return; return;
auto r = m_intblast.check_axiom(clause); auto r = m_intblast.check_axiom(name, clause);
VERIFY (r != l_true); VERIFY (r != l_true);
} }

14
src/sat/smt/polysat_solver.cpp
View file

@ -130,7 +130,7 @@ namespace polysat {
TRACE("bv", tout << "conflict: " << lits << " "; TRACE("bv", tout << "conflict: " << lits << " ";
for (auto [a, b] : eqs) tout << ctx.bpp(a) << " == " << ctx.bpp(b) << " "; for (auto [a, b] : eqs) tout << ctx.bpp(a) << " == " << ctx.bpp(b) << " ";
tout << "\n"; s().display(tout)); tout << "\n"; s().display(tout));
validate_conflict(lits, eqs); validate_conflict(hint_info, lits, eqs);
ctx.set_conflict(ex); ctx.set_conflict(ex);
} }
@ -264,7 +264,7 @@ namespace polysat {
verbose_stream() << "contradictory propagation " << sc << " <- " << deps << "\n"; verbose_stream() << "contradictory propagation " << sc << " <- " << deps << "\n";
} }
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint); auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint);
validate_propagate(lit, core, eqs); validate_propagate(hint_info, lit, core, eqs);
ctx.propagate(lit, ex); ctx.propagate(lit, ex);
return dependency(lit.var()); return dependency(lit.var());
} }
@ -313,7 +313,7 @@ namespace polysat {
if (ctx.use_drat() && hint_info) if (ctx.use_drat() && hint_info)
hint = mk_proof_hint(hint_info, core, eqs); hint = mk_proof_hint(hint_info, core, eqs);
auto ex = euf::th_explain::conflict(*this, core, eqs, hint); auto ex = euf::th_explain::conflict(*this, core, eqs, hint);
validate_conflict(core, eqs); validate_conflict(hint_info, core, eqs);
ctx.set_conflict(ex); ctx.set_conflict(ex);
} }
} }
@ -328,7 +328,7 @@ namespace polysat {
core.pop_back(); core.pop_back();
} }
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint); auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint);
validate_propagate(lit, core, eqs); validate_propagate(hint_info, lit, core, eqs);
ctx.propagate(lit, ex); ctx.propagate(lit, ex);
} }
else if (sign) { else if (sign) {
@ -341,7 +341,7 @@ namespace polysat {
if (ctx.use_drat() && hint_info) if (ctx.use_drat() && hint_info)
hint = mk_proof_hint(hint_info, core, eqs); hint = mk_proof_hint(hint_info, core, eqs);
auto ex = euf::th_explain::conflict(*this, core, eqs, hint); auto ex = euf::th_explain::conflict(*this, core, eqs, hint);
validate_conflict(core, eqs); validate_conflict(hint_info, core, eqs);
ctx.set_conflict(ex); ctx.set_conflict(ex);
} }
} }
@ -385,7 +385,7 @@ namespace polysat {
} }
TRACE("bv", display_clause(name, tout, lits)); TRACE("bv", display_clause(name, tout, lits));
IF_VERBOSE(1, display_clause(name, verbose_stream(), lits)); IF_VERBOSE(1, display_clause(name, verbose_stream(), lits));
validate_axiom(lits); validate_axiom(name, lits);
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint)); s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
return true; return true;
} }
@ -393,7 +393,7 @@ namespace polysat {
void solver::add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant) { void solver::add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant) {
++m_stats.m_num_axioms; ++m_stats.m_num_axioms;
sat::literal_vector lits; sat::literal_vector lits;
validate_axiom(sat::literal_vector(static_cast<unsigned>(end - begin), begin)); validate_axiom(name, sat::literal_vector(static_cast<unsigned>(end - begin), begin));
for (auto it = begin; it != end; ++it) { for (auto it = begin; it != end; ++it) {
auto lit = *it; auto lit = *it;
if (s().value(lit) == l_true && s().lvl(lit) == 0) if (s().value(lit) == l_true && s().lvl(lit) == 0)

6
src/sat/smt/polysat_solver.h
View file

@ -239,9 +239,9 @@ namespace polysat {
void add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant); void add_axiom(char const* name, sat::literal const* begin, sat::literal const* end, bool is_redundant);
void equiv_axiom(char const* name, sat::literal a, sat::literal b); void equiv_axiom(char const* name, sat::literal a, sat::literal b);
void validate_propagate(sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs); void validate_propagate(char const* name, sat::literal lit, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
void validate_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs); void validate_conflict(char const* name, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
void validate_axiom(sat::literal_vector const& clause); void validate_axiom(char const* name, sat::literal_vector const& clause);
std::ostream& display_clause(char const * name, std::ostream& out, sat::literal_vector const& lits) const; std::ostream& display_clause(char const * name, std::ostream& out, sat::literal_vector const& lits) const;