mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-24 21:26:59 +00:00
Code Activity

Add constraints::fixed

Browse source
This commit is contained in:
Jakob Rath 2024-05-14 15:03:30 +02:00
parent cc799bbfc1
commit 764ccebcbf
2 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/sat/smt/polysat/constraints.cpp
View file

@ -115,12 +115,23 @@ namespace polysat {
return ult(p, rational::power_of_two(k)); return ult(p, rational::power_of_two(k));
} }
// 2^{N-i-1}* p >= 2^{N-1} // 2^{N-i-1} p >= 2^{N-1}
signed_constraint constraints::bit(pdd const& p, unsigned i) { signed_constraint constraints::bit(pdd const& p, unsigned i) {
unsigned N = p.manager().power_of_2(); unsigned N = p.manager().power_of_2();
return uge(p * rational::power_of_two(N - i - 1), rational::power_of_two(N - 1)); return uge(p * rational::power_of_two(N - i - 1), rational::power_of_two(N - 1));
} }
// 2^k p - 2^{k+lo} val < 2^{k+lo}
// where k = N - hi - 1
signed_constraint constraints::fixed(pdd const& p, unsigned hi, unsigned lo, rational const& val) {
unsigned const N = p.manager().power_of_2();
SASSERT(lo <= hi && hi < N);
unsigned const k = N - hi - 1;
rational const& ttk = rational::power_of_two(k);
rational const& ttkl = rational::power_of_two(k + lo);
return ult(ttk * p - ttkl * val, ttkl);
}
bool signed_constraint::is_eq(pvar& v, rational& val) { bool signed_constraint::is_eq(pvar& v, rational& val) {
if (m_sign) if (m_sign)
return false; return false;

3
src/sat/smt/polysat/constraints.h
View file

@ -184,6 +184,9 @@ namespace polysat {
signed_constraint band(pdd const& a, pdd const& b, pdd const& r); signed_constraint band(pdd const& a, pdd const& b, pdd const& r);
signed_constraint bor(pdd const& a, pdd const& b, pdd const& r); signed_constraint bor(pdd const& a, pdd const& b, pdd const& r);
// p[hi:lo] = val, represented as inequality
signed_constraint fixed(pdd const& p, unsigned hi, unsigned lo, rational const& val);
//signed_constraint even(pdd const& p) { return parity_at_least(p, 1); } //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
//signed_constraint odd(pdd const& p) { return ~even(p); } //signed_constraint odd(pdd const& p) { return ~even(p); }
}; };