mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

update dep

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-13 17:35:36 +02:00
parent 9e6fd7cb70
commit c082ea4357
5 changed files with 26 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -206,7 +206,7 @@ namespace polysat {
for (auto premise : premises) {
keep(premise);
SASSERT(premise->has_bvar());
SASSERT(s().m_bvars.value(premise.blit()) == l_true); // otherwise the propagation doesn't make sense
SASSERT(premise.bvalue(s()) == l_true); // otherwise the propagation doesn't make sense
c_lemma.push(~premise.blit());
active_level = std::max(active_level, s().m_bvars.level(premise.blit()));
}
@ -315,7 +315,7 @@ namespace polysat {
void conflict_core::set_mark(signed_constraint c) {
if (c->is_marked())
return;
bool bool_propagated = c->has_bvar() && s().m_bvars.value(c.blit()) == l_true;
bool bool_propagated = c->has_bvar() && c.bvalue(s()) == l_true;
c->set_mark();
if (c->has_bvar())
set_bmark(c->bvar());

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

@ -251,4 +251,8 @@ namespace polysat {
if (!cl || !m_unit_clause || m_unit_clause->level() > cl->level())
m_unit_clause = cl;
}
lbool signed_constraint::bvalue(solver& s) const {
return s.m_bvars.value(blit());
}
}

2
src/math/polysat/constraint.h
View file

@ -216,6 +216,7 @@ namespace polysat {
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_true(solver& s) const { return get()->is_currently_true(s, is_positive()); }
lbool bvalue(solver& s) const;
void narrow(solver& s) { get()->narrow(s, is_positive()); }
inequality as_inequality() const { return get()->as_inequality(is_positive()); }
@ -229,6 +230,7 @@ namespace polysat {
constraint& operator*() { return *m_constraint; }
constraint const& operator*() const { return *m_constraint; }
signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
unsigned hash() const {

19
src/math/polysat/saturation.cpp
View file

@ -60,11 +60,26 @@ namespace polysat {
bool inf_saturate::propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints) {
bool crit1_false = crit1.as_signed_constraint().is_currently_false(s());
bool crit2_false = crit2.as_signed_constraint().is_currently_false(s());
if ((crit1_false || crit2_false) && c.is_currently_true(s())) // TODO: check filter
if (!crit1_false && !crit2_false)
return false;
bool is_bool_false = c.bvalue(s()) == l_false;
bool is_model_false = c.is_currently_false(s());
if (!is_bool_false && !is_model_false)
return false;
// refresh dependencies for crit1, crit2
// this is called before core.set, which
// rehashes the variable dependencies
core.keep(crit1.as_signed_constraint());
core.keep(crit2.as_signed_constraint());
if (is_bool_false)
core.insert(~c);
else
core.set(c);
// add fresh constraints
for (auto d : new_constraints)
core.insert(d);
core.insert(c);
return true;
}

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

@ -48,9 +48,8 @@ namespace polysat {
};
friend class constraint;
friend class eq_constraint;
friend class var_constraint;
friend class ule_constraint;
friend class signed_constraint;
friend class clause;
friend class clause_builder;
friend class conflict_core;