mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Encode 2^k*x as (bvshl x k) in the fallback solver

Browse source
This commit is contained in:
Jakob Rath 2022-12-15 14:03:42 +01:00
parent 06a999e219
commit 37536425f4
2 changed files with 36 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -64,7 +64,8 @@ namespace polysat {
return bv->mk_numeral(r, bit_width);
}
// [d,c,b,a] ==> ((a*x + b)*x + c)*x + d
#if 0
// [d,c,b,a] --> ((a*x + b)*x + c)*x + d
expr* mk_poly(univariate const& p) const {
if (p.empty()) {
return mk_numeral(rational::zero());
@ -79,6 +80,38 @@ namespace polysat {
return e;
}
}
#else
// TODO: shouldn't the simplification step of the underlying solver already support this transformation? how to enable?
// 2^k*x --> x << k
// n*x --> n * x
expr* mk_poly_term(rational const& coeff, expr* xpow) const {
unsigned pow;
if (coeff.is_power_of_two(pow))
return bv->mk_bv_shl(xpow, mk_numeral(rational(pow)));
else
return bv->mk_bv_mul(mk_numeral(coeff), xpow);
}
// [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x)
expr* mk_poly(univariate const& p) const {
if (p.empty()) {
return mk_numeral(rational::zero());
}
else {
expr* e = mk_numeral(p.back());
expr* xpow = x;
for (unsigned i = p.size() - 1; i-- > 0; ) {
if (!p[i].is_zero()) {
expr* t = mk_poly_term(p[i], xpow);
e = bv->mk_bv_add(e, t);
}
if (i)
xpow = bv->mk_bv_mul(xpow, x);
}
return e;
}
}
#endif
void add(expr* e, bool sign, dep_t dep) {
if (sign)

3
src/test/polysat.cpp
View file

@ -1661,7 +1661,8 @@ void tst_polysat() {
// test_polysat::test_parity1b();
// test_polysat::test_parity2();
// test_polysat::test_parity3();
test_polysat::test_parity4();
// test_polysat::test_parity4();
// test_polysat::test_parity4(32);
test_polysat::test_parity4(256);
// test_polysat::test_ineq2();
// test_polysat::test_ineq_non_axiom4(32, 3); // stuck in viable refinement loop