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

guard pdd-AND against wrong semantics

Browse source
This commit is contained in:
Jakob Rath 2023-02-24 13:47:42 +01:00
parent ae8075e22d
commit 133661d81b
2 changed files with 26 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/math/dd/dd_pdd.cpp
View file

@ -109,11 +109,29 @@ namespace dd {
pdd pdd_manager::add(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_add_op), this); }
pdd pdd_manager::zero() { return pdd(zero_pdd, this); }
pdd pdd_manager::one() { return pdd(one_pdd, this); }
pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { return p + q - (p*q); }
pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) { if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; }
pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { pdd q(mk_val(x)); if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; }
pdd pdd_manager::mk_not(pdd const& p) { return 1 - p; }
// NOTE: bit-wise AND cannot be expressed in mod2N_e semantics with the existing operations.
pdd pdd_manager::mk_and(pdd const& p, pdd const& q) {
VERIFY(m_semantics == mod2_e || m_semantics == zero_one_vars_e);
return p * q;
}
pdd pdd_manager::mk_or(pdd const& p, pdd const& q) {
return p + q - mk_and(p, q);
}
pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) {
if (m_semantics == mod2_e)
return p + q;
return p + q - 2*mk_and(p, q);
}
pdd pdd_manager::mk_not(pdd const& p) {
if (m_semantics == mod2N_e)
return -p - 1;
VERIFY(m_semantics == mod2_e || m_semantics == zero_one_vars_e);
return 1 - p;
}
pdd pdd_manager::subst_val(pdd const& p, unsigned v, rational const& val) {
pdd r = mk_var(v) + val;

6
src/math/dd/dd_pdd.h
View file

@ -340,9 +340,9 @@ namespace dd {
pdd mul(rational const& c, pdd const& b);
pdd div(pdd const& a, rational const& c);
bool try_div(pdd const& a, rational const& c, pdd& out_result);
pdd mk_and(pdd const& p, pdd const& q);
pdd mk_or(pdd const& p, pdd const& q);
pdd mk_xor(pdd const& p, pdd const& q);
pdd mk_xor(pdd const& p, unsigned q);
pdd mk_not(pdd const& p);
pdd reduce(pdd const& a, pdd const& b);
pdd subst_val0(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
@ -445,10 +445,10 @@ namespace dd {
pdd operator+(pdd const& other) const { VERIFY_EQ(&m, &other.m); return m.add(*this, other); }
pdd operator-(pdd const& other) const { VERIFY_EQ(&m, &other.m); return m.sub(*this, other); }
pdd operator*(pdd const& other) const { VERIFY_EQ(&m, &other.m); return m.mul(*this, other); }
pdd operator&(pdd const& other) const { VERIFY_EQ(&m, &other.m); VERIFY(m.get_semantics() != pdd_manager::mod2N_e); return m.mul(*this, other); } // ??? TODO: fix for 2^N
pdd operator&(pdd const& other) const { VERIFY_EQ(&m, &other.m); return m.mk_and(*this, other); }
pdd operator|(pdd const& other) const { VERIFY_EQ(&m, &other.m); return m.mk_or(*this, other); }
pdd operator^(pdd const& other) const { VERIFY_EQ(&m, &other.m); return m.mk_xor(*this, other); }
pdd operator^(unsigned other) const { return m.mk_xor(*this, other); }
pdd operator^(unsigned other) const { return m.mk_xor(*this, m.mk_val(other)); }
pdd operator*(rational const& other) const { return m.mul(other, *this); }
pdd operator+(rational const& other) const { return m.add(other, *this); }