mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 23:33:41 +00:00
Code Activity

elim pointer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-22 08:15:32 -07:00
parent 2d78bc9282
commit 0013ae5089
2 changed files with 20 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/math/polysat/conflict.cpp
View file

@ -25,7 +25,7 @@ Notes:
and therefore not a current Boolean literal on the search stack. and therefore not a current Boolean literal on the search stack.
TODO: revert(pvar v) is too weak. TODO: revert(pvar v) is too weak.
It should apply saturation rules currently only available for for propagated values. It should apply saturation rules currently only available for propagated values.
TODO: dependency tracking for constraints evaluating to false should be minimized. TODO: dependency tracking for constraints evaluating to false should be minimized.
--*/ --*/
@ -42,8 +42,7 @@ Notes:
namespace polysat { namespace polysat {
conflict::conflict(solver& s) { conflict::conflict(solver& s):s(s) {
m_solver = &s;
ex_engines.push_back(alloc(ex_polynomial_superposition)); ex_engines.push_back(alloc(ex_polynomial_superposition));
for (auto* engine : ex_engines) for (auto* engine : ex_engines)
engine->set_solver(s); engine->set_solver(s);
@ -55,7 +54,7 @@ namespace polysat {
conflict::~conflict() {} conflict::~conflict() {}
constraint_manager& conflict::cm() const { return s().m_constraints; } constraint_manager& conflict::cm() const { return s.m_constraints; }
std::ostream& conflict::display(std::ostream& out) const { std::ostream& conflict::display(std::ostream& out) const {
char const* sep = ""; char const* sep = "";
@ -104,7 +103,7 @@ namespace polysat {
LOG("Conflict: v" << v); LOG("Conflict: v" << v);
SASSERT(empty()); SASSERT(empty());
m_conflict_var = v; m_conflict_var = v;
for (auto c : s().m_cjust[v]) { for (auto c : s.m_cjust[v]) {
c->set_var_dependent(); c->set_var_dependent();
insert(c); insert(c);
} }
@ -115,7 +114,7 @@ namespace polysat {
LOG("Conflict: " << cl); LOG("Conflict: " << cl);
SASSERT(empty()); SASSERT(empty());
for (auto lit : cl) { for (auto lit : cl) {
auto c = s().lit2cnstr(lit); auto c = s.lit2cnstr(lit);
c->set_var_dependent(); c->set_var_dependent();
insert(~c); insert(~c);
} }
@ -160,7 +159,7 @@ namespace polysat {
void conflict::set_bailout() { void conflict::set_bailout() {
SASSERT(!is_bailout()); SASSERT(!is_bailout());
m_bailout = true; m_bailout = true;
s().m_stats.m_num_bailouts++; s.m_stats.m_num_bailouts++;
} }
void conflict::resolve(constraint_manager const& m, sat::literal lit, clause const& cl) { void conflict::resolve(constraint_manager const& m, sat::literal lit, clause const& cl) {
@ -198,26 +197,26 @@ namespace polysat {
if (it == m_saturation_premises.end()) if (it == m_saturation_premises.end())
return; return;
auto& premises = it->m_value; auto& premises = it->m_value;
clause_builder c_lemma(s()); clause_builder c_lemma(s);
for (auto premise : premises) { for (auto premise : premises) {
LOG_H3("premise: " << premise); LOG_H3("premise: " << premise);
keep(premise); keep(premise);
SASSERT(premise->has_bvar()); SASSERT(premise->has_bvar());
SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true); SASSERT(premise.is_currently_true(s) || premise.bvalue(s) == l_true);
// otherwise the propagation doesn't make sense // otherwise the propagation doesn't make sense
c_lemma.push(~premise.blit()); c_lemma.push(~premise.blit());
} }
c_lemma.push(c.blit()); c_lemma.push(c.blit());
clause_ref lemma = c_lemma.build(); clause_ref lemma = c_lemma.build();
cm().store(lemma.get(), s()); cm().store(lemma.get(), s);
if (s().m_bvars.value(c.blit()) == l_undef) if (s.m_bvars.value(c.blit()) == l_undef)
s().assign_bool(s().level(*lemma), c.blit(), lemma.get(), nullptr); s.assign_bool(s.level(*lemma), c.blit(), lemma.get(), nullptr);
} }
clause_builder conflict::build_lemma() { clause_builder conflict::build_lemma() {
LOG_H3("Build lemma from core"); LOG_H3("Build lemma from core");
LOG("core: " << *this); LOG("core: " << *this);
clause_builder lemma(s()); clause_builder lemma(s);
while (!m_constraints.empty()) { while (!m_constraints.empty()) {
signed_constraint c = m_constraints.back(); signed_constraint c = m_constraints.back();
@ -231,10 +230,10 @@ namespace polysat {
for (unsigned v : m_vars) { for (unsigned v : m_vars) {
if (!is_pmarked(v)) if (!is_pmarked(v))
continue; continue;
SASSERT(s().is_assigned(v)); // note that we may have added too many variables: e.g., y disappears in x*y if x=0 SASSERT(s.is_assigned(v)); // note that we may have added too many variables: e.g., y disappears in x*y if x=0
if (!s().is_assigned(v)) if (!s.is_assigned(v))
continue; continue;
auto diseq = ~s().eq(s().var(v), s().get_value(v)); auto diseq = ~s.eq(s.var(v), s.get_value(v));
cm().ensure_bvar(diseq.get()); cm().ensure_bvar(diseq.get());
lemma.push(diseq); lemma.push(diseq);
} }
@ -254,7 +253,7 @@ namespace polysat {
if (conflict_var() == v) { if (conflict_var() == v) {
forbidden_intervals fi; forbidden_intervals fi;
if (fi.perform(s(), v, cjust_v, *this)) if (fi.perform(s, v, cjust_v, *this))
return true; return true;
} }
@ -268,7 +267,7 @@ namespace polysat {
return true; return true;
// No value resolution method was successful => fall back to saturation and variable elimination // No value resolution method was successful => fall back to saturation and variable elimination
while (s().inc()) { while (s.inc()) {
// TODO: as a last resort, substitute v by m_value[v]? // TODO: as a last resort, substitute v by m_value[v]?
if (try_eliminate(v)) if (try_eliminate(v))
return true; return true;
@ -287,7 +286,7 @@ namespace polysat {
if (!has_v) if (!has_v)
return true; return true;
for (auto* engine : ve_engines) for (auto* engine : ve_engines)
if (engine->perform(s(), v, *this)) if (engine->perform(s, v, *this))
return true; return true;
return false; return false;
} }
@ -307,7 +306,7 @@ namespace polysat {
set_bmark(c->bvar()); set_bmark(c->bvar());
if (c->is_var_dependent()) { if (c->is_var_dependent()) {
for (auto v : c->vars()) { for (auto v : c->vars()) {
if (s().is_assigned(v)) if (s.is_assigned(v))
m_vars.insert(v); m_vars.insert(v);
inc_pref(v); inc_pref(v);
} }

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

@ -26,6 +26,7 @@ namespace polysat {
/** Conflict state, represented as core (~negation of clause). */ /** Conflict state, represented as core (~negation of clause). */
class conflict { class conflict {
solver& s;
signed_constraints m_constraints; // new constraints used as premises signed_constraints m_constraints; // new constraints used as premises
indexed_uint_set m_literals; // set of boolean literals in the conflict indexed_uint_set m_literals; // set of boolean literals in the conflict
uint_set m_vars; // variable assignments used as premises uint_set m_vars; // variable assignments used as premises
@ -52,8 +53,6 @@ namespace polysat {
/** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution. */ /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution. */
bool m_bailout = false; bool m_bailout = false;
solver* m_solver = nullptr;
solver& s() const { return *m_solver; }
constraint_manager& cm() const; constraint_manager& cm() const;
scoped_ptr_vector<explainer> ex_engines; scoped_ptr_vector<explainer> ex_engines;
scoped_ptr_vector<variable_elimination_engine> ve_engines; scoped_ptr_vector<variable_elimination_engine> ve_engines;