From 133661d81bc60eb3fdefa4444647519492b2494c Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 24 Feb 2023 13:47:42 +0100 Subject: [PATCH] guard pdd-AND against wrong semantics --- src/math/dd/dd_pdd.cpp | 28 +++++++++++++++++++++++----- src/math/dd/dd_pdd.h | 6 +++--- 2 files changed, 26 insertions(+), 8 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index d6e1b547e..89dd2a12e 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -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; diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index ca2628154..efb684532 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -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> 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); }