mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-21 16:00:13 -07:00
parent 6f93ed8dc2
commit 9173306adc
4 changed files with 20 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,49 +34,9 @@ namespace polysat {
return *m_pdd[sz]; return *m_pdd[sz];
} }
#if 0
dd::fdd const& solver::sz2bits(unsigned sz) {
m_bits.reserve(sz + 1);
auto* bits = m_bits[sz];
if (!bits) {
m_bits.set(sz, alloc(dd::fdd, m_bdd, sz));
bits = m_bits[sz];
}
return *bits;
}
bool solver::has_viable(pvar v) {
return !m_viable[v].is_false();
}
bool solver::is_viable(pvar v, rational const& val) {
return var2bits(v).contains(m_viable[v], val);
}
void solver::add_non_viable(pvar v, rational const& val) {
LOG("pvar " << v << " /= " << val);
SASSERT(is_viable(v, val));
auto const& bits = var2bits(v);
intersect_viable(v, bits.var() != val);
}
void solver::intersect_viable(pvar v, bdd vals) {
push_viable(v);
m_viable[v] &= vals;
if (m_viable[v].is_false())
set_conflict(v);
}
dd::find_t solver::find_viable(pvar v, rational & val) {
return var2bits(v).find_hint(m_viable[v], m_value[v], val);
}
#endif
solver::solver(reslimit& lim): solver::solver(reslimit& lim):
m_lim(lim), m_lim(lim),
m_vble(*this), m_vble(*this),
// m_bdd(1000),
m_dm(m_value_manager, m_alloc), m_dm(m_value_manager, m_alloc),
m_linear_solver(*this), m_linear_solver(*this),
m_free_vars(m_activity), m_free_vars(m_activity),

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

@ -74,24 +74,13 @@ namespace polysat {
d = q.lo().val(); d = q.lo().val();
} }
if (v != null_var) { if (v != null_var) {
bddv const& x = s.m_vble.var2bits(v).var();
s.push_cjust(v, this); s.push_cjust(v, this);
// hacky special case
if (a == 1 && b == 0 && c == 0 && d == 0) s.m_vble.intersect_ule(v, a, b, c, d, is_positive());
// x <= 0
s.m_vble.intersect_viable(v, is_positive() ? x.all0() : !x.all0());
else {
IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << (is_positive() ? " <= " : " > ") << c << "*x + " << d << "\n");
bddv l = a * x + b;
bddv r = c * x + d;
bdd xs = is_positive() ? (l <= r) : (l > r);
s.m_vble.intersect_viable(v, xs);
}
rational val; rational val;
if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) { if (s.m_vble.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, *this); s.propagate(v, val, *this);
}
return; return;
} }

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

@ -46,6 +46,21 @@ namespace polysat {
} }
} }
void viable::intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) {
bddv const& x = var2bits(v).var();
// hacky special case
if (a == 1 && b == 0 && c == 0 && d == 0)
// x <= 0
intersect_viable(v, is_positive ? x.all0() : !x.all0());
else {
IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << (is_positive ? " <= " : " > ") << c << "*x + " << d << "\n");
bddv l = a * x + b;
bddv r = c * x + d;
bdd xs = is_positive ? (l <= r) : (l > r);
intersect_viable(v, xs);
}
}
bool viable::has_viable(pvar v) { bool viable::has_viable(pvar v) {
return !m_viable[v].is_false(); return !m_viable[v].is_false();
} }

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

@ -42,6 +42,8 @@ namespace polysat {
void intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive); void intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive);
void intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive);
/** /**
* Check whether variable v has any viable values left according to m_viable. * Check whether variable v has any viable values left according to m_viable.
*/ */