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

minor univariate tweak

Browse source
This commit is contained in:
Jakob Rath 2022-12-19 14:04:14 +01:00
parent ac0e9ebe5f
commit 59592754d8
3 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -120,15 +120,16 @@ namespace polysat {
}
}
#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;
SASSERT(!coeff.is_zero());
if (coeff.is_one())
return xpow;
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);
return bv->mk_bv_mul(mk_numeral(coeff), xpow);
}
// [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x)
@ -321,7 +322,7 @@ namespace polysat {
return true;
}
bool find_two(rational& out1, rational& out2) {
bool find_two(rational& out1, rational& out2) override {
out1 = model();
bool ok = true;
push();

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

@ -344,7 +344,7 @@ namespace polysat {
}
};
do {
LOG("refine-equal-lin for src: " << e->src);
LOG("refine-equal-lin for src: " << lit_pp(s, e->src));
rational coeff_val = mod(e->coeff * val, mod_value);
if (e->interval.currently_contains(coeff_val)) {

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

@ -190,7 +190,7 @@ namespace polysat {
find_t find_viable(pvar v, rational& out_val);
/**
* Find a next viable value for variable by determining currently viable lower and upper bounds.
* Find a next viable value for variable. Attempts to find two different values, to distinguish propagation/decision.
* @return l_true on success, l_false on conflict, l_undef on resource limit
*/
lbool find_viable(pvar v, rational& out_lo, rational& out_hi);