3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00

update todos, working on assignment minimization

This commit is contained in:
Nikolaj Bjorner 2021-09-22 13:29:36 -07:00
parent 3447d80310
commit c82bbaad7d
8 changed files with 51 additions and 55 deletions

View file

@ -12,21 +12,12 @@ Author:
Notes: Notes:
TODO: constraints containing v could be tracked incrementally when constraints are added/removed using an index.
TODO: try a final core reduction step or other core minimization TODO: try a final core reduction step or other core minimization
TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core. TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
(works currently if x is unassigned; for other cases we would need extra info from constraint::is_currently_false) (works currently if x is unassigned; for other cases we would need extra info from constraint::is_currently_false)
TODO: build_lemma:
note that we may have added too many variables: e.g., y disappears in x*y if x=0 note that we may have added too many variables: e.g., y disappears in x*y if x=0
TODO: keep is buggy. The assert
SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true);
does not necessarily hold. A saturation premise could be inserted that is a resolvent that evaluates to false
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 propagated values. It should apply saturation rules currently only available for propagated values.
@ -46,9 +37,7 @@ Notes:
namespace polysat { namespace polysat {
conflict::conflict(solver& s):s(s) { conflict::conflict(solver& s):s(s) {
ex_engines.push_back(alloc(ex_polynomial_superposition)); ex_engines.push_back(alloc(ex_polynomial_superposition, s));
for (auto* engine : ex_engines)
engine->set_solver(s);
ve_engines.push_back(alloc(ve_reduction)); ve_engines.push_back(alloc(ve_reduction));
inf_engines.push_back(alloc(inf_saturate)); inf_engines.push_back(alloc(inf_saturate));
for (auto* engine : inf_engines) for (auto* engine : inf_engines)
@ -77,7 +66,6 @@ namespace polysat {
m_literals.reset(); m_literals.reset();
m_vars.reset(); m_vars.reset();
m_conflict_var = null_var; m_conflict_var = null_var;
m_saturation_premises.reset();
m_bailout = false; m_bailout = false;
SASSERT(empty()); SASSERT(empty());
} }
@ -146,16 +134,17 @@ namespace polysat {
m_constraints.push_back(c); m_constraints.push_back(c);
} }
// NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
// Ensure that c is assigned and justified
void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) { void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
insert(c); insert(c);
// NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
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.bvalue(s) == l_true); SASSERT(premise.bvalue(s) == l_true);
// 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());
@ -210,12 +199,12 @@ namespace polysat {
* insert it (and recursively, its premises) into \Gamma * insert it (and recursively, its premises) into \Gamma
*/ */
void conflict::keep(signed_constraint c) { void conflict::keep(signed_constraint c) {
if (!c->has_bvar()) { if (c->has_bvar())
remove(c); return;
cm().ensure_bvar(c.get());
insert(c);
}
LOG_H3("keeping: " << c); LOG_H3("keeping: " << c);
remove(c);
cm().ensure_bvar(c.get());
insert(c);
} }
clause_builder conflict::build_lemma() { clause_builder conflict::build_lemma() {

View file

@ -58,8 +58,6 @@ namespace polysat {
scoped_ptr_vector<variable_elimination_engine> ve_engines; scoped_ptr_vector<variable_elimination_engine> ve_engines;
scoped_ptr_vector<inference_engine> inf_engines; scoped_ptr_vector<inference_engine> inf_engines;
// ptr_addr_map<constraint, vector<signed_constraint>> m_saturation_premises;
map<signed_constraint, vector<signed_constraint>, obj_hash<signed_constraint>, default_eq<signed_constraint>> m_saturation_premises;
public: public:
conflict(solver& s); conflict(solver& s);
~conflict(); ~conflict();

View file

@ -121,6 +121,14 @@ namespace polysat {
return {lookup(lit.var()), lit}; return {lookup(lit.var()), lit};
} }
bool signed_constraint::is_currently_false(solver& s) const {
return get()->is_currently_false(s.assignment(), is_positive());
}
bool signed_constraint::is_currently_true(solver& s) const {
return get()->is_currently_true(s.assignment(), is_positive());
}
/** Look up constraint among stored constraints. */ /** Look up constraint among stored constraints. */
constraint* constraint_manager::dedup(constraint* c1) { constraint* constraint_manager::dedup(constraint* c1) {
constraint* c2 = nullptr; constraint* c2 = nullptr;

View file

@ -16,6 +16,7 @@ Author:
#include "math/polysat/clause.h" #include "math/polysat/clause.h"
#include "math/polysat/types.h" #include "math/polysat/types.h"
#include "math/polysat/interval.h" #include "math/polysat/interval.h"
#include "math/polysat/search_state.h"
namespace polysat { namespace polysat {
@ -161,8 +162,8 @@ namespace polysat {
bool propagate(solver& s, bool is_positive, pvar v); bool propagate(solver& s, bool is_positive, pvar v);
virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v); virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v);
virtual bool is_always_false(bool is_positive) const = 0; virtual bool is_always_false(bool is_positive) const = 0;
virtual bool is_currently_false(solver& s, bool is_positive) const = 0; virtual bool is_currently_false(assignment_t const& a, bool is_positive) const = 0;
virtual bool is_currently_true(solver& s, bool is_positive) const = 0; virtual bool is_currently_true(assignment_t const& a, bool is_positive) const = 0;
virtual void narrow(solver& s, bool is_positive) = 0; virtual void narrow(solver& s, bool is_positive) = 0;
virtual inequality as_inequality(bool is_positive) const = 0; virtual inequality as_inequality(bool is_positive) const = 0;
@ -220,9 +221,9 @@ namespace polysat {
bool propagate(solver& s, pvar v) { return get()->propagate(s, is_positive(), v); } bool propagate(solver& s, pvar v) { return get()->propagate(s, is_positive(), v); }
void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); } void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); }
bool is_always_false() const { return get()->is_always_false(is_positive()); } bool is_always_false() const { return get()->is_always_false(is_positive()); }
bool is_always_true() const { return get()->is_always_false(is_negative()); } bool is_always_true() const { return get()->is_always_false(is_negative()); }
bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); } bool is_currently_false(solver& s) const;
bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); } bool is_currently_true(solver& s) const;
lbool bvalue(solver& s) const; lbool bvalue(solver& s) const;
unsigned level(solver& s) const { return get()->level(s); } unsigned level(solver& s) const { return get()->level(s); }
void narrow(solver& s) { get()->narrow(s, is_positive()); } void narrow(solver& s) { get()->narrow(s, is_positive()); }

View file

@ -19,8 +19,8 @@ namespace polysat {
signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) { signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) {
// c1 is true, c2 is false // c1 is true, c2 is false
SASSERT(c1.is_currently_true(s())); SASSERT(c1.is_currently_true(s));
SASSERT(c2.is_currently_false(s())); SASSERT(c2.is_currently_false(s));
LOG_H3("Resolving upon v" << v); LOG_H3("Resolving upon v" << v);
LOG("c1: " << c1); LOG("c1: " << c1);
LOG("c2: " << c2); LOG("c2: " << c2);
@ -33,9 +33,9 @@ namespace polysat {
// (this condition might be too strict, but we use it for now to prevent looping) // (this condition might be too strict, but we use it for now to prevent looping)
if (b.degree(v) <= r.degree(v)) if (b.degree(v) <= r.degree(v))
return {}; return {};
signed_constraint c = s().eq(r); signed_constraint c = s.eq(r);
LOG("resolved: " << c << " currently false? " << c.is_currently_false(s())); LOG("resolved: " << c << " currently false? " << c.is_currently_false(s));
if (!c.is_currently_false(s())) if (!c.is_currently_false(s))
return {}; return {};
return c; return c;
} }
@ -51,15 +51,15 @@ namespace polysat {
for (auto c1 : core) { for (auto c1 : core) {
if (!is_positive_equality_over(v, c1)) if (!is_positive_equality_over(v, c1))
continue; continue;
if (!c1.is_currently_true(s())) if (!c1.is_currently_true(s))
continue; continue;
signed_constraint c = resolve1(v, c1, c2); signed_constraint c = resolve1(v, c1, c2);
if (!c) if (!c)
continue; continue;
if (!c->has_bvar()) if (!c->has_bvar())
s().m_constraints.ensure_bvar(c.get()); s.m_constraints.ensure_bvar(c.get());
switch (c.bvalue(s())) { switch (c.bvalue(s)) {
case l_false: case l_false:
// new conflict state based on propagation and theory conflict // new conflict state based on propagation and theory conflict
core.reset(); core.reset();
@ -72,8 +72,8 @@ namespace polysat {
premises.push_back(c1); premises.push_back(c1);
premises.push_back(c2); premises.push_back(c2);
core.replace(c2, c, premises); core.replace(c2, c, premises);
SASSERT(l_true == c.bvalue(s())); SASSERT(l_true == c.bvalue(s));
SASSERT(c.is_currently_false(s())); SASSERT(c.is_currently_false(s));
break; break;
default: default:
break; break;
@ -95,7 +95,7 @@ namespace polysat {
for (auto c2 : core) { for (auto c2 : core) {
if (!is_positive_equality_over(v, c2)) if (!is_positive_equality_over(v, c2))
continue; continue;
if (!c2.is_currently_false(s())) if (!c2.is_currently_false(s))
continue; continue;
switch (find_replacement(c2, v, core)) { switch (find_replacement(c2, v, core)) {
case l_undef: case l_undef:
@ -115,7 +115,7 @@ namespace polysat {
while (progress) { while (progress) {
progress = false; progress = false;
for (auto c : core) { for (auto c : core) {
if (is_positive_equality_over(v, c) && c.is_currently_true(s()) && reduce_by(v, c, core)) { if (is_positive_equality_over(v, c) && c.is_currently_true(s) && reduce_by(v, c, core)) {
progress = true; progress = true;
break; break;
} }
@ -130,7 +130,7 @@ namespace polysat {
continue; continue;
if (is_positive_equality_over(v, c)) if (is_positive_equality_over(v, c))
continue; continue;
if (!c.is_currently_false(s())) if (!c.is_currently_false(s))
continue; continue;
if (c->is_ule()) { if (c->is_ule()) {
auto lhs = c->to_ule().lhs(); auto lhs = c->to_ule().lhs();
@ -139,14 +139,14 @@ namespace polysat {
auto b = rhs.reduce(v, p); auto b = rhs.reduce(v, p);
if (a == lhs && b == rhs) if (a == lhs && b == rhs)
continue; continue;
auto c2 = s().ule(a, b); auto c2 = s.ule(a, b);
if (!c.is_positive()) if (!c.is_positive())
c2 = ~c2; c2 = ~c2;
SASSERT(c2.is_currently_false(s())); SASSERT(c2.is_currently_false(s));
if (!c2->has_bvar() || l_undef == c2.bvalue(s())) if (!c2->has_bvar() || l_undef == c2.bvalue(s))
core.keep(c2); // adds propagation of c to the search stack core.keep(c2); // adds propagation of c to the search stack
core.reset(); core.reset();
if (c2.bvalue(s()) == l_false) { if (c2.bvalue(s) == l_false) {
core.insert(eq); core.insert(eq);
core.insert(c); core.insert(c);
core.insert(~c2); core.insert(~c2);

View file

@ -23,11 +23,10 @@ namespace polysat {
class explainer { class explainer {
friend class conflict; friend class conflict;
solver* m_solver = nullptr;
void set_solver(solver& s) { m_solver = &s; }
protected: protected:
solver& s() { return *m_solver; } solver& s;
public: public:
explainer(solver& s) :s(s) {}
virtual ~explainer() {} virtual ~explainer() {}
virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict& core) = 0; virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict& core) = 0;
}; };
@ -41,6 +40,7 @@ namespace polysat {
bool reduce_by(pvar, signed_constraint c, conflict& core); bool reduce_by(pvar, signed_constraint c, conflict& core);
lbool try_explain1(pvar v, conflict& core); lbool try_explain1(pvar v, conflict& core);
public: public:
ex_polynomial_superposition(solver& s) : explainer(s) {}
bool try_explain(pvar v, conflict& core) override; bool try_explain(pvar v, conflict& core) override;
}; };

View file

@ -204,15 +204,15 @@ namespace polysat {
return is_always_false(is_positive, lhs(), rhs()); return is_always_false(is_positive, lhs(), rhs());
} }
bool ule_constraint::is_currently_false(solver& s, bool is_positive) const { bool ule_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
auto p = lhs().subst_val(s.assignment()); auto p = lhs().subst_val(a);
auto q = rhs().subst_val(s.assignment()); auto q = rhs().subst_val(a);
return is_always_false(is_positive, p, q); return is_always_false(is_positive, p, q);
} }
bool ule_constraint::is_currently_true(solver& s, bool is_positive) const { bool ule_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
auto p = lhs().subst_val(s.assignment()); auto p = lhs().subst_val(a);
auto q = rhs().subst_val(s.assignment()); auto q = rhs().subst_val(a);
if (is_positive) { if (is_positive) {
if (p.is_zero()) if (p.is_zero())
return true; return true;

View file

@ -34,8 +34,8 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override; std::ostream& display(std::ostream& out) const override;
bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const; bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const;
bool is_always_false(bool is_positive) const override; bool is_always_false(bool is_positive) const override;
bool is_currently_false(solver& s, bool is_positive) const override; bool is_currently_false(assignment_t const& a, bool is_positive) const override;
bool is_currently_true(solver& s, bool is_positive) const override; bool is_currently_true(assignment_t const& a, bool is_positive) const override;
void narrow(solver& s, bool is_positive) override; void narrow(solver& s, bool is_positive) override;
inequality as_inequality(bool is_positive) const override; inequality as_inequality(bool is_positive) const override;
unsigned hash() const override; unsigned hash() const override;