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

Polysat (#5187)

Browse source 
* test_l2 works now

* Linear propagation: test whether a is odd

* Linear propagation with even coefficients (wip)
This commit is contained in:
Jakob Rath 2021-04-15 17:37:14 +02:00 • committed by GitHub
parent feb31045f5
commit cb9dda19dd
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 77 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,6 +36,7 @@ namespace polysat {
}
void solver::add_non_viable(pvar v, rational const& val) {
LOG("pvar " << v << " /= " << val);
TRACE("polysat", tout << "v" << v << " /= " << val << "\n";);
bdd value = m_bdd.mk_true();
for (unsigned k = size(v); k-- > 0; )
@ -270,7 +271,7 @@ namespace polysat {
rational a = p.hi().val();
rational b = p.lo().val();
rational inv_a;
if (p.lo().val().is_odd()) {
if (a.is_odd()) {
// v1 = -b * inverse(a)
unsigned sz = p.power_of_2();
VERIFY(a.mult_inverse(sz, inv_a));
@ -280,9 +281,50 @@ namespace polysat {
return false;
}
SASSERT(!b.is_odd()); // otherwise p.is_never_zero() would have been true above
// TBD
// constrain viable using condition on x
// 2*x + 2 == 0 mod 4 => x is odd
//
// We have:
// 2^j*a'*x + 2^j*b' == 0 mod m, where a' is odd (but not necessarily b')
// <=> 2^j*(a'*x + b') == 0 mod m
// <=> a'*x + b' == 0 mod (m-j)
// <=> x == -b' * inverse_{m-j}(a') mod (m-j)
// ( <=> 2^j*x == 2^j * -b' * inverse_{m-j}(a') mod m )
//
// x == c mod (m-j)
// Which x in 2^m satisfy this?
// => x \in { c + k * 2^(m-j) | k = 0, ..., 2^j - 1 }
unsigned rank_a = a.trailing_zeros(); // j
SASSERT(b == 0 || rank_a <= b.trailing_zeros());
rational aa = a / rational::power_of_two(rank_a); // a'
rational bb = b / rational::power_of_two(rank_a); // b'
rational inv_aa;
unsigned small_sz = p.power_of_2() - rank_a; // m - j
VERIFY(aa.mult_inverse(small_sz, inv_aa));
rational cc = mod(inv_aa * -bb, rational::power_of_two(small_sz));
LOG(m_vars[other_var] << " = " << cc << " + k * 2^" << small_sz);
// TODO: better way to update the BDD, e.g. construct new one (only if rank_a is small?)
vector<rational> viable;
for (rational k = rational::zero(); k < rational::power_of_two(rank_a); k += 1) {
rational val = cc + k * rational::power_of_two(small_sz);
viable.push_back(val);
}
LOG_V("still viable: " << viable);
unsigned i = 0;
for (rational r = rational::zero(); r < rational::power_of_two(p.power_of_2()); r += 1) {
while (i < viable.size() && viable[i] < r)
++i;
if (i < viable.size() && viable[i] == r)
continue;
if (is_viable(other_var, r)) {
add_non_viable(other_var, r);
}
}
LOG("TODO");
return false;
}

37
src/test/polysat.cpp
View file

@ -35,11 +35,9 @@ namespace polysat {
auto a = s.var(s.add_var(2));
s.add_eq(a + 1);
s.check();
// Expected result: SAT with a = 3
}
// TBD: we get the wrong result / conflicts.
// it claims that v1 + 2*v0 + 1 with v0 replaced by 0 is 1.
// it should be v1 + 1
static void test_l2() {
scoped_solver s;
auto a = s.var(s.add_var(2));
@ -47,6 +45,36 @@ namespace polysat {
s.add_eq(2*a + b + 1);
s.add_eq(2*b + a);
s.check();
// Expected result: SAT with a = 2, b = 3
}
static void test_l3() {
scoped_solver s;
auto a = s.var(s.add_var(2));
auto b = s.var(s.add_var(2));
s.add_eq(3*b + a + 2);
s.check();
// Expected result: SAT
}
static void test_l4() {
scoped_solver s;
auto a = s.var(s.add_var(3));
// auto b = s.var(s.add_var(3));
s.add_eq(4*a + 2);
s.check();
// Expected result: UNSAT
}
// Goal: test propagate_eq in case of 2*a*x + 2*b == 0
static void test_l5() {
scoped_solver s;
auto a = s.var(s.add_var(3));
auto b = s.var(s.add_var(3));
s.add_eq(a + 2*b + 4);
s.add_eq(a + 4*b + 4);
s.check();
// Expected result: UNSAT
}
@ -125,6 +153,9 @@ namespace polysat {
void tst_polysat() {
polysat::test_l1();
polysat::test_l2();
polysat::test_l3();
polysat::test_l4();
polysat::test_l5();
#if 0
// worry about this later
polysat::test_p1();