mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

interval

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-25 18:46:43 +01:00
parent adf41c5d02
commit a4e29ecd7e
4 changed files with 35 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/saturation.h
View file

@ -38,9 +38,7 @@ namespace polysat {
vector<signed_constraint> m_new_constraints;
char const* m_rule = nullptr;
void set_rule(char const* r) { m_rule = r; }
bool find_upper_bound(pvar x, signed_constraint& c, rational& bound);
void set_rule(char const* r) { m_rule = r; }
void push_omega(pdd const& x, pdd const& y);
void push_omega_bisect(pdd const& x, rational x_max, pdd const& y, rational y_max);

30
src/math/polysat/ule_constraint.cpp
View file

@ -134,20 +134,22 @@ namespace polysat {
v = p.var();
else if (q.is_unilinear())
v = q.var();
if (v != null_var) {
signed_constraint sc(this, is_positive);
s.m_viable.intersect(v, sc);
rational val;
switch (s.m_viable.find_viable(v, val)) {
case dd::find_t::singleton:
s.propagate(v, val, sc);
break;
case dd::find_t::empty:
s.set_conflict(v);
break;
default:
break;
}
else
return;
signed_constraint sc(this, is_positive);
if (!s.m_viable.intersect(v, sc))
return;
rational val;
switch (s.m_viable.find_viable(v, val)) {
case dd::find_t::singleton:
s.propagate(v, val, sc); // TBD why is sc used as justification? It should be all of viable
break;
case dd::find_t::empty:
s.set_conflict(v);
break;
default:
break;
}
}

29
src/math/polysat/viable.cpp
View file

@ -64,25 +64,29 @@ namespace polysat {
m_trail.pop_back();
}
void viable::intersect(pvar v, signed_constraint const& c) {
bool viable::intersect(pvar v, signed_constraint const& c) {
auto& fi = s.m_forbidden_intervals;
entry* ne = alloc_entry();
if (!fi.get_interval(c, v, ne->interval, ne->side_cond) || ne->interval.is_currently_empty())
if (!fi.get_interval(c, v, ne->interval, ne->side_cond) || ne->interval.is_currently_empty()) {
m_alloc.push_back(ne);
return false;
}
else {
ne->src = c;
intersect(v, ne);
return intersect(v, ne);
}
}
void viable::intersect(pvar v, entry* ne) {
bool viable::intersect(pvar v, entry* ne) {
entry* e = m_viable[v];
if (e && e->interval.is_full())
return;
if (e && e->interval.is_full()) {
m_alloc.push_back(ne);
return false;
}
if (ne->interval.is_currently_empty()) {
m_alloc.push_back(ne);
return;
return false;
}
auto create_entry = [&]() {
@ -98,8 +102,6 @@ namespace polysat {
e->remove_from(m_viable[v], e);
};
//LOG("intersect " << ne->interval);
if (!e)
m_viable[v] = create_entry();
else {
@ -107,14 +109,14 @@ namespace polysat {
do {
if (e->interval.contains(ne->interval)) {
m_alloc.push_back(ne);
return;
return false;
}
while (ne->interval.contains(e->interval)) {
entry* n = e->next();
remove_entry(e);
if (!m_viable[v]) {
m_viable[v] = create_entry();
return;
return true;
}
if (e == first)
first = n;
@ -124,13 +126,13 @@ namespace polysat {
if (e->interval.lo_val() > ne->interval.lo_val()) {
if (first->prev()->interval.contains(ne->interval)) {
m_alloc.push_back(ne);
return;
return false;
}
e->insert_before(create_entry());
if (e == first)
m_viable[v] = e->prev();
SASSERT(well_formed(m_viable[v]));
return;
return true;
}
e = e->next();
}
@ -139,6 +141,7 @@ namespace polysat {
first->insert_before(create_entry());
}
SASSERT(well_formed(m_viable[v]));
return true;
}
bool viable::has_viable(pvar v) {

4
src/math/polysat/viable.h
View file

@ -44,7 +44,7 @@ namespace polysat {
entry* alloc_entry();
void intersect(pvar v, entry* e);
bool intersect(pvar v, entry* e);
public:
viable(solver& s);
@ -64,7 +64,7 @@ namespace polysat {
* update state of viable for pvar v
* based on affine constraints
*/
void intersect(pvar v, signed_constraint const& c);
bool intersect(pvar v, signed_constraint const& c);
/**
* Check whether variable v has any viable values left according to m_viable.