mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

more proof hint information

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-27 22:48:11 -08:00
parent 20958f1468
commit c0da732cea
6 changed files with 59 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/sat/smt/polysat/core.cpp
View file

@ -177,12 +177,11 @@ namespace polysat {
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
TRACE("bv", tout << "check-conflict v" << m_var << "\n");
s.set_conflict(m_viable.explain());
// propagate_unsat_core();
s.set_conflict(m_viable.explain(), "viable-conflict");
return sat::check_result::CR_CONTINUE;
case find_t::singleton: {
TRACE("bv", tout << "check-propagate v" << m_var << " := " << m_value << "\n");
auto d = s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
auto d = s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain(), "viable-propagate");
propagate_assignment(m_var, m_value, d);
return sat::check_result::CR_CONTINUE;
}
@ -244,7 +243,7 @@ namespace polysat {
// If no saturation propagation was possible, explain the conflict using the variable assignment.
m_unsat_core = explain_eval(get_constraint(conflict_idx));
m_unsat_core.push_back(get_dependency(conflict_idx));
propagate_unsat_core();
s.set_conflict(m_unsat_core, "polysat-bail-out-conflict");
return sat::check_result::CR_CONTINUE;
}
@ -365,10 +364,10 @@ namespace polysat {
return;
switch (eval(sc)) {
case l_false:
s.propagate(d, true, explain_eval(sc));
s.propagate(d, true, explain_eval(sc), "eval-propagate");
break;
case l_true:
s.propagate(d, false, explain_eval(sc));
s.propagate(d, false, explain_eval(sc), "eval-propagate");
break;
default:
break;
@ -382,25 +381,16 @@ namespace polysat {
return d;
}
#if 0
dependency_vector core::get_dependencies(constraint_id_vector const& ids) const {
dependency_vector result;
for (auto id : ids)
result.push_back(get_dependency(id));
return result;
}
#endif
void core::propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d) {
lbool eval_value = eval(sc);
if (eval_value == l_undef)
sc.propagate(*this, value, d);
else if (value == l_undef)
s.propagate(d, eval_value != l_true, explain_eval(sc));
s.propagate(d, eval_value != l_true, explain_eval(sc), "constraint-propagate");
else if (value != eval_value) {
m_unsat_core = explain_eval(sc);
m_unsat_core.push_back(m_constraint_index[id.id].d);
propagate_unsat_core();
s.set_conflict(m_unsat_core, "polysat-constraint-core");
}
}
@ -420,12 +410,6 @@ namespace polysat {
return s.inconsistent();
}
void core::propagate_unsat_core() {
// default is to use unsat core:
// if core is based on viable, use s.set_lemma();
s.set_conflict(m_unsat_core);
}
void core::assign_eh(constraint_id index, bool sign, unsigned level) {
struct unassign : public trail {
core& c;

3
src/sat/smt/polysat/core.h
View file

@ -81,7 +81,6 @@ namespace polysat {
void propagate_assignment(constraint_id idx);
void propagate_eval(constraint_id idx);
void propagate_assignment(pvar v, rational const& value, dependency dep);
void propagate_unsat_core();
void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
void add_watch(unsigned idx, unsigned var);
@ -157,7 +156,7 @@ namespace polysat {
dependency get_dependency(constraint_id idx) const;
// dependency_vector get_dependencies(constraint_id_vector const& ids) const;
lbool eval(constraint_id id);
dependency propagate(signed_constraint const& sc, dependency_vector const& deps) { return s.propagate(sc, deps); }
dependency propagate(signed_constraint const& sc, dependency_vector const& deps) { return s.propagate(sc, deps, nullptr); }
lbool eval(signed_constraint const& sc);
dependency_vector explain_eval(signed_constraint const& sc);
bool inconsistent() const;

6
src/sat/smt/polysat/types.h
View file

@ -136,9 +136,9 @@ namespace polysat {
virtual ~solver_interface() {}
virtual lbool add_eq_literal(pvar v, rational const& val, dependency& d) = 0;
virtual bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) = 0;
virtual void set_conflict(dependency_vector const& core) = 0;
virtual dependency propagate(signed_constraint sc, dependency_vector const& deps) = 0;
virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps) = 0;
virtual void set_conflict(dependency_vector const& core, char const* hint) = 0;
virtual dependency propagate(signed_constraint sc, dependency_vector const& deps, char const* hint) = 0;
virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps, char const* hint) = 0;
virtual trail_stack& trail() = 0;
virtual bool inconsistent() const = 0;
virtual void get_bitvector_suffixes(pvar v, offset_slices& out) = 0;

44
src/sat/smt/polysat_internalize.cpp
View file

@ -386,8 +386,11 @@ namespace polysat {
void solver::axiomatize_comp(app* e, expr* x, expr* y) {
unsigned sz = bv.get_bv_size(x);
auto eq = eq_internalize(x, y);
add_clause(~eq, eq_internalize(e, bv.mk_numeral(1, sz)));
add_clause(eq, eq_internalize(e, bv.mk_numeral(0, sz)));
polysat_proof* hint = nullptr;
if (ctx.use_drat())
hint = mk_proof_hint("[axiom] bv-comp");
add_clause(~eq, eq_internalize(e, bv.mk_numeral(1, sz)), hint);
add_clause(eq, eq_internalize(e, bv.mk_numeral(0, sz)), hint);
}
// y = 0 -> x
@ -395,8 +398,11 @@ namespace polysat {
void solver::axiomatize_srem(app* e, expr* x, expr* y) {
unsigned sz = bv.get_bv_size(x);
sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
add_clause(~y_eq0, eq_internalize(e, x));
add_clause(y_eq0, eq_internalize(e, bv.mk_bv_mul(bv.mk_bv_sdiv(x, y), y)));
polysat_proof* hint = nullptr;
if (ctx.use_drat())
hint = mk_proof_hint("[axiom] srem");
add_clause(~y_eq0, eq_internalize(e, x), hint);
add_clause(y_eq0, eq_internalize(e, bv.mk_bv_mul(bv.mk_bv_sdiv(x, y), y)), hint);
}
// u := umod(x, y)
@ -416,12 +422,15 @@ namespace polysat {
sat::literal lsigny = mk_literal(signy);
sat::literal u_eq0 = eq_internalize(u, bv.mk_zero(sz));
sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
add_clause(~u_eq0, eq_internalize(e, bv.mk_zero(sz)));
add_clause(u_eq0, ~y_eq0, eq_internalize(e, x));
add_clause(~lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(u)));
add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_sub(y, u)));
add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_add(y, u)));
add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, u));
polysat_proof* hint = nullptr;
if (ctx.use_drat())
hint = mk_proof_hint("[axiom] smod");
add_clause(~u_eq0, eq_internalize(e, bv.mk_zero(sz)), hint);
add_clause(u_eq0, ~y_eq0, eq_internalize(e, x), hint);
add_clause(~lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(u)), hint);
add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_sub(y, u)), hint);
add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_add(y, u)), hint);
add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, u), hint);
}
@ -444,12 +453,15 @@ namespace polysat {
sat::literal lsignx = mk_literal(signx);
sat::literal lsigny = mk_literal(signy);
sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
add_clause(~y_eq0, ~lsignx, eq_internalize(e, bv.mk_numeral(1, sz)));
add_clause(~y_eq0, lsignx, eq_internalize(e, bv.mk_numeral(N-1, sz)));
add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(d)));
add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_neg(d)));
add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, d));
add_clause(y_eq0, ~lsignx, ~lsigny, eq_internalize(e, d));
polysat_proof* hint = nullptr;
if (ctx.use_drat())
hint = mk_proof_hint("[axiom] sdiv");
add_clause(~y_eq0, ~lsignx, eq_internalize(e, bv.mk_numeral(1, sz)), hint);
add_clause(~y_eq0, lsignx, eq_internalize(e, bv.mk_numeral(N-1, sz)), hint);
add_clause(y_eq0, lsignx, ~lsigny, eq_internalize(e, bv.mk_bv_neg(d)), hint);
add_clause(y_eq0, ~lsignx, lsigny, eq_internalize(e, bv.mk_bv_neg(d)), hint);
add_clause(y_eq0, lsignx, lsigny, eq_internalize(e, d), hint);
add_clause(y_eq0, ~lsignx, ~lsigny, eq_internalize(e, d), hint);
}
void solver::internalize_urem_i(app* rem) {

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

@ -107,9 +107,13 @@ namespace polysat {
m_core.assign_eh(a->m_index, l.sign(), s().lvl(l));
}
void solver::set_conflict(dependency_vector const& deps) {
void solver::set_conflict(dependency_vector const& deps, char const* hint_info) {
auto [lits, eqs] = explain_deps(deps);
auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
polysat_proof* hint = nullptr;
if (ctx.use_drat() && hint_info)
hint = mk_proof_hint(hint_info);
auto ex = euf::th_explain::conflict(*this, lits, eqs, hint);
ctx.set_conflict(ex);
}
@ -215,13 +219,16 @@ namespace polysat {
// The polysat::solver takes care of translating signed constraints into expressions, which translate into literals.
// Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions.
dependency solver::propagate(signed_constraint sc, dependency_vector const& deps) {
dependency solver::propagate(signed_constraint sc, dependency_vector const& deps, char const* hint_info) {
TRACE("bv", sc.display(tout << "propagate ") << "\n");
sat::literal lit = ctx.mk_literal(constraint2expr(sc));
if (s().value(lit) == l_true)
return dependency(lit.var());
auto [core, eqs] = explain_deps(deps);
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
polysat_proof* hint = nullptr;
if (ctx.use_drat() && hint_info)
hint = mk_proof_hint(hint_info);
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint);
ctx.propagate(lit, ex);
return dependency(lit.var());
}
@ -268,16 +275,19 @@ namespace polysat {
}
}
void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) {
void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps, char const* hint_info) {
TRACE("bv", tout << "propagate " << d << " " << sign << "\n");
auto [core, eqs] = explain_deps(deps);
SASSERT(d.is_bool_var() || d.is_eq());
polysat_proof* hint = nullptr;
if (ctx.use_drat() && hint_info)
hint = mk_proof_hint(hint_info);
if (d.is_bool_var()) {
auto bv = d.bool_var();
auto lit = sat::literal(bv, sign);
if (s().value(lit) == l_true)
return;
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, hint);
ctx.propagate(lit, ex);
}
else if (sign) {
@ -286,7 +296,7 @@ namespace polysat {
auto n1 = var2enode(v1);
auto n2 = var2enode(v2);
eqs.push_back({ n1, n2 });
auto ex = euf::th_explain::conflict(*this, core, eqs, nullptr);
auto ex = euf::th_explain::conflict(*this, core, eqs, hint);
ctx.set_conflict(ex);
}
}

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

@ -176,10 +176,10 @@ namespace polysat {
// callbacks from core
lbool add_eq_literal(pvar v, rational const& val, dependency& d) override;
void set_conflict(dependency_vector const& core) override;
void set_conflict(dependency_vector const& core, char const* hint) override;
bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) override;
dependency propagate(signed_constraint sc, dependency_vector const& deps) override;
void propagate(dependency const& d, bool sign, dependency_vector const& deps) override;
dependency propagate(signed_constraint sc, dependency_vector const& deps, char const* hint) override;
void propagate(dependency const& d, bool sign, dependency_vector const& deps, char const* hint) override;
trail_stack& trail() override;
bool inconsistent() const override;
void get_bitvector_sub_slices(pvar v, offset_slices& out) override;