mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

build_lemma returns clause_builder; adjust reason in revert_bool_decision

Browse source
This commit is contained in:
Jakob Rath 2021-09-07 15:02:29 +02:00
parent 733c21bb20
commit 24f96acf4f
8 changed files with 83 additions and 75 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/math/polysat/clause_builder.cpp
View file

@ -23,7 +23,6 @@ namespace polysat {
void clause_builder::reset() {
m_literals.reset();
m_new_constraints.reset();
m_level = 0;
m_dep = nullptr;
SASSERT(empty());
@ -42,23 +41,27 @@ namespace polysat {
}
void clause_builder::push_literal(sat::literal lit) {
constraint* c = m_solver.m_constraints.lookup(lit.var());
push(m_solver.m_constraints.lookup(lit));
}
void clause_builder::push(signed_constraint c) {
SASSERT(c);
SASSERT(c->has_bvar());
if (c->unit_clause()) {
add_dependency(c->unit_clause()->dep());
add_dependency(c->unit_dep());
return;
}
m_level = std::max(m_level, c->level());
m_literals.push_back(lit);
m_literals.push_back(c.blit());
}
void clause_builder::push_new_constraint(signed_constraint c) {
SASSERT(c);
if (c.is_always_false())
return;
m_level = std::max(m_level, c->level());
m_literals.push_back(c.blit());
m_new_constraints.push_back(c.get());
}
// void clause_builder::push_new_constraint(signed_constraint c) {
// SASSERT(c);
// if (c.is_always_false())
// return;
// m_level = std::max(m_level, c->level());
// m_literals.push_back(c.blit());
// m_new_constraints.push_back(c.get());
// }
}

13
src/math/polysat/clause_builder.h
View file

@ -27,16 +27,17 @@ namespace polysat {
class clause_builder {
solver& m_solver;
sat::literal_vector m_literals;
scoped_ptr_vector<constraint> m_new_constraints;
p_dependency_ref m_dep;
unsigned m_level = 0;
public:
clause_builder(solver& s);
bool empty() const { return m_literals.empty() && m_new_constraints.empty() && m_dep == nullptr && m_level == 0; }
bool empty() const { return m_literals.empty() && m_dep == nullptr && m_level == 0; }
void reset();
unsigned level() const { return m_level; }
/// Build the clause. This will reset the clause builder so it can be reused.
clause_ref build();
@ -45,9 +46,15 @@ namespace polysat {
/// Add a literal to the clause.
/// Intended to be used for literals representing a constraint that already exists.
void push_literal(sat::literal lit);
void push(signed_constraint c);
/// Add a constraint to the clause that does not yet exist in the solver so far.
void push_new_constraint(signed_constraint c);
// void push_new_constraint(signed_constraint c);
using const_iterator = decltype(m_literals)::const_iterator;
const_iterator begin() const { return m_literals.begin(); }
const_iterator end() const { return m_literals.end(); }
};
}

52
src/math/polysat/conflict_core.cpp
View file

@ -130,11 +130,35 @@ namespace polysat {
m_solver->activate_constraint(c);
}
clause_ref conflict_core::build_lemma(unsigned model_level) {
/** Create fallback lemma that excludes the current search state */
clause_builder conflict_core::build_fallback_lemma(unsigned lvl) {
LOG_H3("Creating fallback lemma for level " << lvl);
LOG_V("m_search: " << m_solver->m_search);
clause_builder lemma(*m_solver);
unsigned todo = lvl;
unsigned i = 0;
while (todo > 0) {
auto const& item = m_solver->m_search[i++];
if (!m_solver->is_decision(item))
continue;
LOG_V("Adding: " << item);
if (item.is_assignment()) {
pvar v = item.var();
auto c = ~cm().eq(0, m_solver->var(v) - m_solver->m_value[v]);
cm().ensure_bvar(c.get());
lemma.push_literal(c.blit());
} else {
sat::literal lit = item.lit();
lemma.push_literal(~lit);
}
--todo;
}
return lemma;
}
clause_builder conflict_core::build_core_lemma(unsigned model_level) {
LOG_H3("build lemma from core");
sat::literal_vector literals;
p_dependency_ref dep = m_solver->mk_dep_ref(null_dependency);
unsigned lvl = 0;
clause_builder lemma(*m_solver);
// TODO: try a final core reduction step?
@ -146,12 +170,7 @@ namespace polysat {
// Insert the temporary constraint from saturation into \Gamma.
handle_saturation_premises(c);
}
if (c->unit_clause()) {
dep = m_solver->m_dm.mk_join(dep, c->unit_dep());
continue;
}
lvl = std::max(lvl, c->level());
literals.push_back(~c.blit());
lemma.push(c);
}
if (m_needs_model) {
@ -166,13 +185,20 @@ namespace polysat {
// SASSERT(!m_solver->m_justification[v].is_unassigned()); // TODO: why does this trigger????
if (m_solver->m_justification[v].level() > model_level)
continue;
auto diseq = ~cm().eq(lvl, m_solver->var(v) - m_solver->m_value[v]);
auto diseq = ~cm().eq(lemma.level(), m_solver->var(v) - m_solver->m_value[v]);
cm().ensure_bvar(diseq.get());
literals.push_back(diseq.blit());
lemma.push(diseq);
}
}
return clause::from_literals(lvl, std::move(dep), std::move(literals));
return lemma;
}
clause_builder conflict_core::build_lemma(unsigned reverted_level) {
if (is_bailout())
return build_fallback_lemma(reverted_level);
else
return build_core_lemma(reverted_level - 1);
}
bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {

5
src/math/polysat/conflict_core.h
View file

@ -13,6 +13,7 @@ Author:
--*/
#pragma once
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
namespace polysat {
@ -89,7 +90,9 @@ namespace polysat {
bool resolve_value(pvar v, vector<signed_constraint> const& cjust_v);
/** Convert the core into a lemma to be learned. */
clause_ref build_lemma(unsigned model_level);
clause_builder build_lemma(unsigned reverted_level);
clause_builder build_core_lemma(unsigned model_level);
clause_builder build_fallback_lemma(unsigned lvl);
bool try_eliminate(pvar v);
bool try_saturate(pvar v);

3
src/math/polysat/explain.cpp
View file

@ -54,6 +54,7 @@ namespace polysat {
if (!c2.is_currently_false(s()))
continue;
// TODO: separate method for this; then try_explain1 and try_explain* for multi-steps; replace the false constraint in the core.
// c1 is true, c2 is false
LOG("c1: " << c1);
LOG("c2: " << c2);
@ -71,7 +72,7 @@ namespace polysat {
premises.push_back(c1);
premises.push_back(c2);
if (!c->contains_var(v)) {
core.reset();
core.reset(); // TODO: doesn't work; this removes the premises as well... / instead: remove the false one.
core.insert(c, std::move(premises));
return true;
} else {

4
src/math/polysat/forbidden_intervals.cpp
View file

@ -66,6 +66,9 @@ namespace polysat {
bool forbidden_intervals::explain(solver& s, vector<signed_constraint> const& conflict, pvar v, clause_ref& out_lemma) {
return false;
#if 0
// Extract forbidden intervals from conflicting constraints
vector<fi_record> records;
bool has_full = false;
@ -171,6 +174,7 @@ namespace polysat {
}
out_lemma = clause.build();
return true;
#endif
}
}

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

@ -636,11 +636,7 @@ namespace polysat {
SASSERT(m_justification[v].is_decision());
unsigned const lvl = m_justification[v].level();
clause_ref lemma;
if (m_conflict.is_bailout())
lemma = mk_fallback_lemma(lvl); // must call this before backjump
else
lemma = m_conflict.build_lemma(lvl - 1);
clause_ref lemma = m_conflict.build_lemma(lvl).build();
m_conflict.reset();
backjump(lvl - 1);
@ -678,38 +674,11 @@ namespace polysat {
return m_bvars.is_decision(item.lit().var());
}
/** Create fallback lemma that excludes the current search state */
clause_ref solver::mk_fallback_lemma(unsigned lvl) {
LOG_H3("Creating fallback lemma for level " << lvl);
LOG_V("m_search: " << m_search);
clause_builder lemma(*this);
unsigned todo = lvl;
unsigned i = 0;
while (todo > 0) {
auto const& item = m_search[i++];
if (!is_decision(item))
continue;
LOG_V("Adding: " << item);
if (item.is_assignment()) {
pvar v = item.var();
auto c = ~m_constraints.eq(0, var(v) - m_value[v]);
m_constraints.ensure_bvar(c.get());
lemma.push_literal(c.blit());
} else {
sat::literal lit = item.lit();
lemma.push_literal(~lit);
}
--todo;
}
return lemma.build();
}
void solver::revert_bool_decision(sat::literal lit) {
sat::bool_var const var = lit.var();
LOG_H3("Reverting boolean decision: " << lit);
SASSERT(m_bvars.is_decision(var));
// TODO:
// Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core.
//
// In a CDCL solver, this means ~L is in the lemma (actually, as the asserting literal). We drop the decision and replace it by the propagation (~L)^lemma.
@ -728,18 +697,14 @@ namespace polysat {
// again L is in core, unless we core-reduced it away
unsigned const lvl = m_bvars.level(var);
clause_ref reason;
if (m_conflict.is_bailout())
reason = mk_fallback_lemma(lvl);
else
reason = m_conflict.build_lemma(lvl - 1);
clause_builder reason_builder = m_conflict.build_lemma(lvl);
m_conflict.reset();
bool contains_lit = std::any_of(reason->begin(), reason->end(), [lit](auto reason_lit) { return reason_lit == ~lit; });
bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
// bool contains_lit = std::any_of(reason_builder->begin(), reason_builder->end(), [lit](auto reason_lit) { return reason_lit == ~lit; });
if (!contains_lit) {
// Problem:
// a(x), b(x) => c(y) [ i.e., a(x) no longer in the core ]
// but now what to do with decision a(x)^?
// At this point, we do not have ~lit in the reason.
// For now, we simply add it (thus weakening the reason)
//
// Alternative (to be considered later):
// - 'reason' itself (without ~L) would already be an explanation for ~L
@ -747,10 +712,10 @@ namespace polysat {
// - would need to check what we can gain by relaxing that invariant
// - drawback: might have to bail out at boolean resolution
// Also: maybe we can skip ~L in some cases? but in that case it shouldn't be marked.
SASSERT(false); // debugging: just to find a case when this happens.
// lemma does not contain ~L, so we add it (thus weakening the lemma)
NOT_IMPLEMENTED_YET(); // should add it to the core before calling build_lemma.
//
reason_builder.push_literal(~lit);
}
clause_ref reason = reason_builder.build();
// The lemma where 'lit' comes from.
// Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma.

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

@ -218,7 +218,6 @@ namespace polysat {
void resolve_bool(sat::literal lit);
void revert_decision(pvar v);
void revert_bool_decision(sat::literal lit);
clause_ref mk_fallback_lemma(unsigned lvl);
void report_unsat();
void learn_lemma(pvar v, clause_ref lemma);