mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

compile

Browse source
This commit is contained in:
Jakob Rath 2023-07-27 15:49:39 +02:00
parent c09859fe63
commit 8b9d9db77e
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/test/viable.cpp
View file

@ -318,6 +318,8 @@ namespace polysat {
} }
public: public:
using entry = viable::entry;
static bool check_one(unsigned a1, unsigned b1, unsigned a2, unsigned b2, unsigned val, unsigned bw) { static bool check_one(unsigned a1, unsigned b1, unsigned a2, unsigned b2, unsigned val, unsigned bw) {
return check_one(rational(a1), rational(b1), rational(a2), rational(b2), rational(val), bw); return check_one(rational(a1), rational(b1), rational(a2), rational(b2), rational(val), bw);
} }
@ -348,14 +350,14 @@ namespace polysat {
v.intersect(x.var(), c); v.intersect(x.var(), c);
// Trigger forbidden interval refinement // Trigger forbidden interval refinement
v.is_viable(x.var(), val); v.is_viable(x.var(), val);
auto* e = v.m_units[x.var()]; entry* e = v.m_units[x.var()].get_entries(s.size(x.var())); // TODO: take other widths into account
if (!e) { if (!e) {
std::cout << "test_fi: no interval for a1=" << a1 << " b1=" << b1 << " a2=" << a2 << " b2=" << b2 << " val=" << val << " neg=" << negated << std::endl; std::cout << "test_fi: no interval for a1=" << a1 << " b1=" << b1 << " a2=" << a2 << " b2=" << b2 << " val=" << val << " neg=" << negated << std::endl;
VERIFY(false); VERIFY(false);
return false; return false;
} }
VERIFY(e); VERIFY(e);
auto* first = e; entry* first = e;
SASSERT(e->next() == e); // the result is expected to be a single interval (although for this check it doesn't really matter if there's more...) SASSERT(e->next() == e); // the result is expected to be a single interval (although for this check it doesn't really matter if there's more...)
auto check_is_violated = [&](rational const& x, bool expect_violated) -> bool { auto check_is_violated = [&](rational const& x, bool expect_violated) -> bool {