diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/Makefile.am | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 2729 | ||||
-rw-r--r-- | src/theory/quantifiers/bv_inverter_utils.cpp | 2592 | ||||
-rw-r--r-- | src/theory/quantifiers/bv_inverter_utils.h | 72 |
5 files changed, 2729 insertions, 2668 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index afc8c0f1b..f6c66b743 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -424,6 +424,8 @@ libcvc4_add_sources( theory/quantifiers/anti_skolem.h theory/quantifiers/bv_inverter.cpp theory/quantifiers/bv_inverter.h + theory/quantifiers/bv_inverter_utils.cpp + theory/quantifiers/bv_inverter_utils.h theory/quantifiers/candidate_rewrite_database.cpp theory/quantifiers/candidate_rewrite_database.h theory/quantifiers/candidate_rewrite_filter.cpp diff --git a/src/Makefile.am b/src/Makefile.am index 0a32cb645..7856d7f29 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -436,6 +436,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/anti_skolem.h \ theory/quantifiers/bv_inverter.cpp \ theory/quantifiers/bv_inverter.h \ + theory/quantifiers/bv_inverter_utils.cpp \ + theory/quantifiers/bv_inverter_utils.h \ theory/quantifiers/candidate_rewrite_database.cpp \ theory/quantifiers/candidate_rewrite_database.h \ theory/quantifiers/candidate_rewrite_filter.cpp \ diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 3ff27366b..2525f5d18 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -15,13 +15,12 @@ #include "theory/quantifiers/bv_inverter.h" #include <algorithm> -#include <stack> #include "options/quantifiers_options.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/quantifiers/bv_inverter_utils.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -#include "theory/bv/theory_bv_utils.h" - using namespace CVC4::kind; @@ -56,9 +55,9 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) Node new_cond = Rewriter::rewrite(cond); if (new_cond != cond) { - Trace("cegqi-bv-skvinv-debug") << "Condition " << cond - << " was rewritten to " << new_cond - << std::endl; + Trace("cegqi-bv-skvinv-debug") + << "Condition " << cond << " was rewritten to " << new_cond + << std::endl; } // optimization : if condition is ( x = solve_var ) should just return // solve_var and not introduce a Skolem this can happen when we ask for @@ -71,9 +70,9 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) if (new_cond[i] == solve_var) { c = new_cond[1 - i]; - Trace("cegqi-bv-skvinv") << "SKVINV : " << c - << " is trivially associated with conditon " - << new_cond << std::endl; + Trace("cegqi-bv-skvinv") + << "SKVINV : " << c << " is trivially associated with conditon " + << new_cond << std::endl; break; } } @@ -106,25 +105,13 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) static bool isInvertible(Kind k, unsigned index) { - return k == NOT - || k == EQUAL - || k == BITVECTOR_ULT - || k == BITVECTOR_SLT - || k == BITVECTOR_COMP - || k == BITVECTOR_NOT - || k == BITVECTOR_NEG - || k == BITVECTOR_CONCAT - || k == BITVECTOR_SIGN_EXTEND - || k == BITVECTOR_PLUS - || k == BITVECTOR_MULT - || k == BITVECTOR_UREM_TOTAL - || k == BITVECTOR_UDIV_TOTAL - || k == BITVECTOR_AND - || k == BITVECTOR_OR - || k == BITVECTOR_XOR - || k == BITVECTOR_LSHR - || k == BITVECTOR_ASHR - || k == BITVECTOR_SHL; + return k == NOT || k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT + || k == BITVECTOR_COMP || k == BITVECTOR_NOT || k == BITVECTOR_NEG + || k == BITVECTOR_CONCAT || k == BITVECTOR_SIGN_EXTEND + || k == BITVECTOR_PLUS || k == BITVECTOR_MULT + || k == BITVECTOR_UREM_TOTAL || k == BITVECTOR_UDIV_TOTAL + || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR + || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR || k == BITVECTOR_SHL; } Node BvInverter::getPathToPv( @@ -144,9 +131,9 @@ Node BvInverter::getPathToPv( else { unsigned rmod = 0; // TODO : randomize? - for (unsigned i = 0; i < lit.getNumChildren(); i++) + for (size_t i = 0, num = lit.getNumChildren(); i < num; i++) { - unsigned ii = (i + rmod) % lit.getNumChildren(); + size_t ii = (i + rmod) % lit.getNumChildren(); // only recurse if the kind is invertible // this allows us to avoid paths that go through skolem functions if (!isInvertible(lit.getKind(), ii)) @@ -163,7 +150,7 @@ Node BvInverter::getPathToPv( { children.push_back(lit.getOperator()); } - for (unsigned j = 0; j < lit.getNumChildren(); j++) + for (size_t j = 0, num = lit.getNumChildren(); j < num; j++) { children.push_back(j == ii ? litc : lit[j]); } @@ -225,2607 +212,6 @@ static Node dropChild(Node n, unsigned index) return nb.getNumChildren() == 1 ? nb[0] : nb.constructNode(); } -static Node getScBvUltUgt(bool pol, Kind k, Node x, Node t) -{ - Assert(k == BITVECTOR_ULT || k == BITVECTOR_UGT); - - NodeManager* nm = NodeManager::currentNM(); - unsigned w = bv::utils::getSize(t); - Node sc; - - if (k == BITVECTOR_ULT) - { - if (pol == true) - { - /* x < t - * with invertibility condition: - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkZero(w)); - Node scr = nm->mkNode(k, x, t); - sc = nm->mkNode(IMPLIES, scl, scr); - } - else - { - /* x >= t - * with invertibility condition: - * true (no invertibility condition) */ - sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); - } - } - else - { - Assert(k == BITVECTOR_UGT); - if (pol == true) - { - /* x > t - * with invertibility condition: - * (distinct t ones) - * where - * ones = ~0 with getSize(ones) = w */ - Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w)); - Node scr = nm->mkNode(k, x, t); - sc = nm->mkNode(IMPLIES, scl, scr); - } - else - { - /* x <= t - * with invertibility condition: - * true (no invertibility condition) */ - sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); - } - } - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t) -{ - Assert(k == BITVECTOR_SLT || k == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - unsigned w = bv::utils::getSize(t); - Node sc; - - if (k == BITVECTOR_SLT) - { - if (pol == true) - { - /* x < t - * with invertibility condition: - * (distinct t min) - * where - * min is the minimum signed value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node scl = nm->mkNode(DISTINCT, min, t); - Node scr = nm->mkNode(k, x, t); - sc = nm->mkNode(IMPLIES, scl, scr); - } - else - { - /* x >= t - * with invertibility condition: - * true (no invertibility condition) */ - sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); - } - } - else - { - Assert(k == BITVECTOR_SGT); - if (pol == true) - { - /* x > t - * with invertibility condition: - * (distinct t max) - * where - * max is the signed maximum value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node scl = nm->mkNode(DISTINCT, t, max); - Node scr = nm->mkNode(k, x, t); - sc = nm->mkNode(IMPLIES, scl, scr); - } - else - { - /* x <= t - * with invertibility condition: - * true (no invertibility condition) */ - sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); - } - } - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvMult(bool pol, - Kind litk, - Kind k, - unsigned idx, - Node x, - Node s, - Node t) -{ - Assert(k == BITVECTOR_MULT); - Assert (litk == EQUAL - || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - Node scl; - unsigned w = bv::utils::getSize(s); - Assert (w == bv::utils::getSize(t)); - - if (litk == EQUAL) - { - Node z = bv::utils::mkZero(w); - - if (pol) - { - /* x * s = t - * with invertibility condition (synthesized): - * (= (bvand (bvor (bvneg s) s) t) t) - * - * is equivalent to: - * ctz(t) >= ctz(s) - * -> - * (or - * (= t z) - * (and - * (bvuge (bvand t (bvneg t)) (bvand s (bvneg s))) - * (distinct s z))) - * where - * z = 0 with getSize(z) = w */ - Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); - scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_AND, o, t), t); - } - else - { - /* x * s != t - * with invertibility condition: - * (or (distinct t z) (distinct s z)) - * where - * z = 0 with getSize(z) = w */ - scl = nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()); - } - } - else if (litk == BITVECTOR_ULT) - { - if (pol) - { - /* x * s < t - * with invertibility condition (synthesized): - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = nm->mkNode(DISTINCT, t, z); - } - else - { - /* x * s >= t - * with invertibility condition (synthesized): - * (bvuge (bvor (bvneg s) s) t) */ - Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); - scl = nm->mkNode(BITVECTOR_UGE, o, t); - } - } - else if (litk == BITVECTOR_UGT) - { - if (pol) - { - /* x * s > t - * with invertibility condition (synthesized): - * (bvult t (bvor (bvneg s) s)) */ - Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); - scl = nm->mkNode(BITVECTOR_ULT, t, o); - } - else - { - /* x * s <= t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else if (litk == BITVECTOR_SLT) - { - if (pol) - { - /* x * s < t - * with invertibility condition (synthesized): - * (bvslt (bvand (bvnot (bvneg t)) (bvor (bvneg s) s)) t) */ - Node a1 = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t)); - Node a2 = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); - scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_AND, a1, a2), t); - } - else - { - /* x * s >= t - * with invertibility condition (synthesized): - * (bvsge (bvand (bvor (bvneg s) s) max) t) - * where - * max is the signed maximum value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); - Node a = nm->mkNode(BITVECTOR_AND, o, max); - scl = nm->mkNode(BITVECTOR_SGE, a, t); - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (pol) - { - /* x * s > t - * with invertibility condition (synthesized): - * (bvslt t (bvsub t (bvor (bvor s t) (bvneg s)))) */ - Node o = nm->mkNode(BITVECTOR_OR, - nm->mkNode(BITVECTOR_OR, s, t), nm->mkNode(BITVECTOR_NEG, s)); - Node sub = nm->mkNode(BITVECTOR_SUB, t, o); - scl = nm->mkNode(BITVECTOR_SLT, t, sub); - } - else - { - /* x * s <= t - * with invertibility condition (synthesized): - * (not (and (= s z) (bvslt t s))) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = nm->mkNode(AND, s.eqNode(z), nm->mkNode(BITVECTOR_SLT, t, s)); - scl = scl.notNode(); - } - } - - Node scr = - nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvUrem(bool pol, - Kind litk, - Kind k, - unsigned idx, - Node x, - Node s, - Node t) -{ - Assert(k == BITVECTOR_UREM_TOTAL); - Assert (litk == EQUAL - || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - Node scl; - unsigned w = bv::utils::getSize(s); - Assert (w == bv::utils::getSize(t)); - - if (litk == EQUAL) - { - if (idx == 0) - { - if (pol) - { - /* x % s = t - * with invertibility condition (synthesized): - * (bvuge (bvnot (bvneg s)) t) */ - Node neg = nm->mkNode(BITVECTOR_NEG, s); - scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t); - } - else - { - /* x % s != t - * with invertibility condition: - * (or (distinct s (_ bv1 w)) (distinct t z)) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = nm->mkNode(OR, - s.eqNode(bv::utils::mkOne(w)).notNode(), - t.eqNode(z).notNode()); - } - } - else - { - if (pol) - { - /* s % x = t - * with invertibility condition (synthesized): - * (bvuge (bvand (bvsub (bvadd t t) s) s) t) - * - * is equivalent to: - * (or (= s t) - * (and (bvugt s t) - * (bvugt (bvsub s t) t) - * (or (= t z) (distinct (bvsub s (_ bv1 w)) t)))) - * where - * z = 0 with getSize(z) = w */ - Node add = nm->mkNode(BITVECTOR_PLUS, t, t); - Node sub = nm->mkNode(BITVECTOR_SUB, add, s); - Node a = nm->mkNode(BITVECTOR_AND, sub, s); - scl = nm->mkNode(BITVECTOR_UGE, a, t); - } - else - { - /* s % x != t - * with invertibility condition: - * (or (distinct s z) (distinct t z)) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); - } - } - } - else if (litk == BITVECTOR_ULT) - { - if (idx == 0) - { - if (pol) - { - /* x % s < t - * with invertibility condition: - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = t.eqNode(z).notNode(); - } - else - { - /* x % s >= t - * with invertibility condition (synthesized): - * (bvuge (bvnot (bvneg s)) t) */ - Node neg = nm->mkNode(BITVECTOR_NEG, s); - scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t); - } - } - else - { - if (pol) - { - /* s % x < t - * with invertibility condition: - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = t.eqNode(z).notNode(); - } - else - { - /* s % x >= t - * with invertibility condition (combination of = and >): - * (or - * (bvuge (bvand (bvsub (bvadd t t) s) s) t) ; eq, synthesized - * (bvult t s)) ; ugt, synthesized */ - Node add = nm->mkNode(BITVECTOR_PLUS, t, t); - Node sub = nm->mkNode(BITVECTOR_SUB, add, s); - Node a = nm->mkNode(BITVECTOR_AND, sub, s); - Node sceq = nm->mkNode(BITVECTOR_UGE, a, t); - Node scugt = nm->mkNode(BITVECTOR_ULT, t, s); - scl = nm->mkNode(OR, sceq, scugt); - } - } - } - else if (litk == BITVECTOR_UGT) - { - if (idx == 0) - { - if (pol) - { - /* x % s > t - * with invertibility condition (synthesized): - * (bvult t (bvnot (bvneg s))) */ - Node nt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s)); - scl = nm->mkNode(BITVECTOR_ULT, t, nt); - } - else - { - /* x % s <= t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else - { - if (pol) - { - /* s % x > t - * with invertibility condition (synthesized): - * (bvult t s) */ - scl = nm->mkNode(BITVECTOR_ULT, t, s); - } - else - { - /* s % x <= t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - } - else if (litk == BITVECTOR_SLT) - { - if (idx == 0) - { - if (pol) - { - /* x % s < t - * with invertibility condition (synthesized): - * (bvslt (bvnot t) (bvor (bvneg s) (bvneg t))) */ - Node o1 = nm->mkNode(BITVECTOR_NEG, s); - Node o2 = nm->mkNode(BITVECTOR_NEG, t); - Node o = nm->mkNode(BITVECTOR_OR, o1, o2); - scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_NOT, t), o); - } - else - { - /* x % s >= t - * with invertibility condition (synthesized): - * (or (bvslt t s) (bvsge z s)) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - Node s1 = nm->mkNode(BITVECTOR_SLT, t, s); - Node s2 = nm->mkNode(BITVECTOR_SGE, z, s); - scl = nm->mkNode(OR, s1, s2); - } - } - else - { - Node z = bv::utils::mkZero(w); - - if (pol) - { - /* s % x < t - * with invertibility condition (synthesized): - * (or (bvslt s t) (bvslt z t)) - * where - * z = 0 with getSize(z) = w */ - Node slt1 = nm->mkNode(BITVECTOR_SLT, s, t); - Node slt2 = nm->mkNode(BITVECTOR_SLT, z, t); - scl = nm->mkNode(OR, slt1, slt2); - } - else - { - /* s % x >= t - * with invertibility condition: - * (and - * (=> (bvsge s z) (bvsge s t)) - * (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t))) - * where - * z = 0 with getSize(z) = w */ - Node i1 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGE, s, t)); - Node i2 = nm->mkNode(IMPLIES, - nm->mkNode(AND, - nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, t, z)), - nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t)); - scl = nm->mkNode(AND, i1, i2); - } - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (idx == 0) - { - Node z = bv::utils::mkZero(w); - - if (pol) - { - /* x % s > t - * with invertibility condition: - * - * (and - * (and - * (=> (bvsgt s z) (bvslt t (bvnot (bvneg s)))) - * (=> (bvsle s z) (distinct t max))) - * (or (distinct t z) (distinct s (_ bv1 w)))) - * where - * z = 0 with getSize(z) = w - * and max is the maximum signed value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node nt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s)); - Node i1 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SGT, s, z), nm->mkNode(BITVECTOR_SLT, t, nt)); - Node i2 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SLE, s, z), t.eqNode(max).notNode()); - Node a1 = nm->mkNode(AND, i1, i2); - Node a2 = nm->mkNode(OR, - t.eqNode(z).notNode(), s.eqNode(bv::utils::mkOne(w)).notNode()); - scl = nm->mkNode(AND, a1, a2); - } - else - { - /* x % s <= t - * with invertibility condition (synthesized): - * (bvslt ones (bvand (bvneg s) t)) - * where - * z = 0 with getSize(z) = w - * and ones = ~0 with getSize(ones) = w */ - Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, s), t); - scl = nm->mkNode(BITVECTOR_SLT, bv::utils::mkOnes(w), a); - } - } - else - { - if (pol) - { - /* s % x > t - * with invertibility condition: - * (and - * (=> (bvsge s z) (bvsgt s t)) - * (=> (bvslt s z) - * (bvsgt (bvlshr (bvsub s (_ bv1 w)) (_ bv1 w)) t))) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - Node i1 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGT, s, t)); - Node shr = nm->mkNode(BITVECTOR_LSHR, - bv::utils::mkDec(s), bv::utils::mkOne(w)); - Node i2 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGT, shr, t)); - scl = nm->mkNode(AND, i1, i2); - } - else - { - /* s % x <= t - * with invertibility condition (synthesized): - * (or (bvult t min) (bvsge t s)) - * where - * min is the minimum signed value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node o1 = nm->mkNode(BITVECTOR_ULT, t, min); - Node o2 = nm->mkNode(BITVECTOR_SGE, t, s); - scl = nm->mkNode(OR, o1, o2); - } - } - } - - Node scr = - nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvUdiv(bool pol, - Kind litk, - Kind k, - unsigned idx, - Node x, - Node s, - Node t) -{ - Assert(k == BITVECTOR_UDIV_TOTAL); - Assert(litk == EQUAL - || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - unsigned w = bv::utils::getSize(s); - Assert (w == bv::utils::getSize(t)); - Node scl; - Node z = bv::utils::mkZero(w); - - if (litk == EQUAL) - { - if (idx == 0) - { - if (pol) - { - /* x udiv s = t - * with invertibility condition (synthesized): - * (= (bvudiv (bvmul s t) s) t) - * - * is equivalent to: - * (or - * (and (= t (bvnot z)) - * (or (= s z) (= s (_ bv1 w)))) - * (and (distinct t (bvnot z)) - * (distinct s z) - * (not (umulo s t)))) - * - * where - * umulo(s, t) is true if s * t produces and overflow - * and z = 0 with getSize(z) = w */ - Node mul = nm->mkNode(BITVECTOR_MULT, s, t); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s); - scl = nm->mkNode(EQUAL, div, t); - } - else - { - /* x udiv s != t - * with invertibility condition: - * (or (distinct s z) (distinct t ones)) - * where - * z = 0 with getSize(z) = w - * and ones = ~0 with getSize(ones) = w */ - Node ones = bv::utils::mkOnes(w); - scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(ones).notNode()); - } - } - else - { - if (pol) - { - /* s udiv x = t - * with invertibility condition (synthesized): - * (= (bvudiv s (bvudiv s t)) t) - * - * is equivalent to: - * (or - * (= s t) - * (= t (bvnot z)) - * (and - * (bvuge s t) - * (or - * (= (bvurem s t) z) - * (bvule (bvadd (bvudiv s (bvadd t (_ bv1 w))) (_ bv1 w)) - * (bvudiv s t))) - * (=> (= s (bvnot (_ bv0 8))) (distinct t (_ bv0 8))))) - * - * where - * z = 0 with getSize(z) = w */ - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t); - scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, div), t); - } - else - { - /* s udiv x != t - * with invertibility condition (w > 1): - * true (no invertibility condition) - * - * with invertibility condition (w == 1): - * (= (bvand s t) z) - * - * where - * z = 0 with getSize(z) = w */ - if (w > 1) - { - scl = nm->mkConst<bool>(true); - } - else - { - scl = nm->mkNode(BITVECTOR_AND, s, t).eqNode(z); - } - } - } - } - else if (litk == BITVECTOR_ULT) - { - if (idx == 0) - { - if (pol) - { - /* x udiv s < t - * with invertibility condition (synthesized): - * (and (bvult z s) (bvult z t)) - * where - * z = 0 with getSize(z) = w */ - Node u1 = nm->mkNode(BITVECTOR_ULT, z, s); - Node u2 = nm->mkNode(BITVECTOR_ULT, z, t); - scl = nm->mkNode(AND, u1, u2); - } - else - { - /* x udiv s >= t - * with invertibility condition (synthesized): - * (= (bvand (bvudiv (bvmul s t) t) s) s) */ - Node mul = nm->mkNode(BITVECTOR_MULT, s, t); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, t); - scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_AND, div, s), s); - } - } - else - { - if (pol) - { - /* s udiv x < t - * with invertibility condition (synthesized): - * (and (bvult z (bvnot (bvand (bvneg t) s))) (bvult z t)) - * where - * z = 0 with getSize(z) = w */ - Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, t), s); - Node u1 = nm->mkNode(BITVECTOR_ULT, z, nm->mkNode(BITVECTOR_NOT, a)); - Node u2 = nm->mkNode(BITVECTOR_ULT, z, t); - scl = nm->mkNode(AND, u1, u2); - } - else - { - /* s udiv x >= t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - } - else if (litk == BITVECTOR_UGT) - { - if (idx == 0) - { - if (pol) - { - /* x udiv s > t - * with invertibility condition: - * (bvugt (bvudiv ones s) t) - * where - * ones = ~0 with getSize(ones) = w */ - Node ones = bv::utils::mkOnes(w); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); - scl = nm->mkNode(BITVECTOR_UGT, div, t); - } - else - { - /* x udiv s <= t - * with invertibility condition (synthesized): - * (bvuge (bvor s t) (bvnot (bvneg s))) */ - Node u1 = nm->mkNode(BITVECTOR_OR, s, t); - Node u2 = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s)); - scl = nm->mkNode(BITVECTOR_UGE, u1, u2); - } - } - else - { - if (pol) - { - /* s udiv x > t - * with invertibility condition (synthesized): - * (bvult t ones) - * where - * ones = ~0 with getSize(ones) = w */ - Node ones = bv::utils::mkOnes(w); - scl = nm->mkNode(BITVECTOR_ULT, t, ones); - } - else - { - /* s udiv x <= t - * with invertibility condition (synthesized): - * (bvult z (bvor (bvnot s) t)) - * where - * z = 0 with getSize(z) = w */ - scl = nm->mkNode(BITVECTOR_ULT, - z, nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NOT, s), t)); - } - } - } - else if (litk == BITVECTOR_SLT) - { - if (idx == 0) - { - if (pol) - { - /* x udiv s < t - * with invertibility condition: - * (=> (bvsle t z) (bvslt (bvudiv min s) t)) - * where - * z = 0 with getSize(z) = w - * and min is the minimum signed value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node sle = nm->mkNode(BITVECTOR_SLE, t, z); - Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s); - Node slt = nm->mkNode(BITVECTOR_SLT, div, t); - scl = nm->mkNode(IMPLIES, sle, slt); - } - else - { - /* x udiv s >= t - * with invertibility condition: - * (or - * (bvsge (bvudiv ones s) t) - * (bvsge (bvudiv max s) t)) - * where - * ones = ~0 with getSize(ones) = w - * and max is the maximum signed value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node ones = bv::utils::mkOnes(w); - Node udiv1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); - Node udiv2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, max, s); - Node sge1 = nm->mkNode(BITVECTOR_SGE, udiv1, t); - Node sge2 = nm->mkNode(BITVECTOR_SGE, udiv2, t); - scl = nm->mkNode(OR, sge1, sge2); - } - } - else - { - if (pol) - { - /* s udiv x < t - * with invertibility condition (synthesized): - * (or (bvslt s t) (bvsge t z)) - * where - * z = 0 with getSize(z) = w */ - Node slt = nm->mkNode(BITVECTOR_SLT, s, t); - Node sge = nm->mkNode(BITVECTOR_SGE, t, z); - scl = nm->mkNode(OR, slt, sge); - } - else - { - /* s udiv x >= t - * with invertibility condition (w > 1): - * (and - * (=> (bvsge s z) (bvsge s t)) - * (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t))) - * - * with invertibility condition (w == 1): - * (bvsge s t) - * - * where - * z = 0 with getSize(z) = w */ - - if (w > 1) - { - Node div = nm->mkNode(BITVECTOR_LSHR, s, bv::utils::mkConst(w, 1)); - Node i1 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SGE, s, z), - nm->mkNode(BITVECTOR_SGE, s, t)); - Node i2 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SLT, s, z), - nm->mkNode(BITVECTOR_SGE, div, t)); - scl = nm->mkNode(AND, i1, i2); - } - else - { - scl = nm->mkNode(BITVECTOR_SGE, s, t); - } - } - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (idx == 0) - { - if (pol) - { - /* x udiv s > t - * with invertibility condition: - * (or - * (bvsgt (bvudiv ones s) t) - * (bvsgt (bvudiv max s) t)) - * where - * ones = ~0 with getSize(ones) = w - * and max is the maximum signed value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node ones = bv::utils::mkOnes(w); - Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); - Node sgt1 = nm->mkNode(BITVECTOR_SGT, div1, t); - Node div2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, max, s); - Node sgt2 = nm->mkNode(BITVECTOR_SGT, div2, t); - scl = nm->mkNode(OR, sgt1, sgt2); - } - else - { - /* x udiv s <= t - * with invertibility condition (combination of = and <): - * (or - * (= (bvudiv (bvmul s t) s) t) ; eq, synthesized - * (=> (bvsle t z) (bvslt (bvudiv min s) t))) ; slt - * where - * z = 0 with getSize(z) = w - * and min is the minimum signed value with getSize(min) = w */ - Node mul = nm->mkNode(BITVECTOR_MULT, s, t); - Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s); - Node o1 = nm->mkNode(EQUAL, div1, t); - Node min = bv::utils::mkMinSigned(w); - Node sle = nm->mkNode(BITVECTOR_SLE, t, z); - Node div2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s); - Node slt = nm->mkNode(BITVECTOR_SLT, div2, t); - Node o2 = nm->mkNode(IMPLIES, sle, slt); - scl = nm->mkNode(OR, o1, o2); - } - } - else - { - if (pol) - { - /* s udiv x > t - * with invertibility condition (w > 1): - * (and - * (=> (bvsge s z) (bvsgt s t)) - * (=> (bvslt s z) (bvsgt (bvlshr s (_ bv1 w)) t))) - * - * with invertibility condition (w == 1): - * (bvsgt s t) - * - * where - * z = 0 with getSize(z) = w */ - if (w > 1) - { - Node div = nm->mkNode(BITVECTOR_LSHR, s, bv::utils::mkConst(w, 1)); - Node i1 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SGE, s, z), - nm->mkNode(BITVECTOR_SGT, s, t)); - Node i2 = nm->mkNode(IMPLIES, - nm->mkNode(BITVECTOR_SLT, s, z), - nm->mkNode(BITVECTOR_SGT, div, t)); - scl = nm->mkNode(AND, i1, i2); - } - else - { - scl = nm->mkNode(BITVECTOR_SGT, s, t); - } - } - else - { - /* s udiv x <= t - * with invertibility condition (synthesized): - * (not (and (bvslt t (bvnot #x0)) (bvslt t s))) - * <-> - * (or (bvsge t ones) (bvsge t s)) - * where - * ones = ~0 with getSize(ones) = w */ - Node ones = bv::utils::mkOnes(w); - Node sge1 = nm->mkNode(BITVECTOR_SGE, t, ones); - Node sge2 = nm->mkNode(BITVECTOR_SGE, t, s); - scl = nm->mkNode(OR, sge1, sge2); - } - } - } - - Node scr = - nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvAndOr(bool pol, - Kind litk, - Kind k, - unsigned idx, - Node x, - Node s, - Node t) -{ - Assert (k == BITVECTOR_AND || k == BITVECTOR_OR); - Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - unsigned w = bv::utils::getSize(s); - Assert (w == bv::utils::getSize(t)); - Node scl; - - if (litk == EQUAL) - { - if (pol) - { - /* x & s = t - * x | s = t - * with invertibility condition: - * (= (bvand t s) t) - * (= (bvor t s) t) */ - scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s)); - } - else - { - if (k == BITVECTOR_AND) - { - /* x & s = t - * with invertibility condition: - * (or (distinct s z) (distinct t z)) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); - } - else - { - /* x | s = t - * with invertibility condition: - * (or (distinct s ones) (distinct t ones)) - * where - * ones = ~0 with getSize(ones) = w */ - Node n = bv::utils::mkOnes(w); - scl = nm->mkNode(OR, s.eqNode(n).notNode(), t.eqNode(n).notNode()); - } - } - } - else if (litk == BITVECTOR_ULT) - { - if (pol) - { - if (k == BITVECTOR_AND) - { - /* x & s < t - * with invertibility condition (synthesized): - * (distinct t z) - * where - * z = 0 with getSize(z) = 0 */ - Node z = bv::utils::mkZero(w); - scl = t.eqNode(z).notNode(); - } - else - { - /* x | s < t - * with invertibility condition (synthesized): - * (bvult s t) */ - scl = nm->mkNode(BITVECTOR_ULT, s, t); - } - } - else - { - if (k == BITVECTOR_AND) - { - /* x & s >= t - * with invertibility condition (synthesized): - * (bvuge s t) */ - scl = nm->mkNode(BITVECTOR_UGE, s, t); - } - else - { - /* x | s >= t - * with invertibility condition (synthesized): - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - } - else if (litk == BITVECTOR_UGT) - { - if (pol) - { - if (k == BITVECTOR_AND) - { - /* x & s > t - * with invertibility condition (synthesized): - * (bvult t s) */ - scl = nm->mkNode(BITVECTOR_ULT, t, s); - } - else - { - /* x | s > t - * with invertibility condition (synthesized): - * (bvult t ones) - * where - * ones = ~0 with getSize(ones) = w */ - scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w)); - } - } - else - { - if (k == BITVECTOR_AND) - { - /* x & s <= t - * with invertibility condition (synthesized): - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - else - { - /* x | s <= t - * with invertibility condition (synthesized): - * (bvuge t s) */ - scl = nm->mkNode(BITVECTOR_UGE, t, s); - } - } - } - else if (litk == BITVECTOR_SLT) - { - if (pol) - { - if (k == BITVECTOR_AND) - { - /* x & s < t - * with invertibility condition (synthesized): - * (bvslt (bvand (bvnot (bvneg t)) s) t) */ - Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t)); - scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_AND, nnt, s), t); - } - else - { - /* x | s < t - * with invertibility condition (synthesized): - * (bvslt (bvor (bvnot (bvsub s t)) s) t) */ - Node st = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_SUB, s, t)); - scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_OR, st, s), t); - } - } - else - { - if (k == BITVECTOR_AND) - { - /* x & s >= t - * with invertibility condition (case = combined with synthesized bvsgt): - * (or - * (= (bvand s t) t) - * (bvslt t (bvand (bvsub t s) s))) */ - Node sc_sgt = nm->mkNode( - BITVECTOR_SLT, - t, - nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_SUB, t, s), s)); - Node sc_eq = nm->mkNode(BITVECTOR_AND, s, t).eqNode(t); - scl = sc_eq.orNode(sc_sgt); - } - else - { - /* x | s >= t - * with invertibility condition (synthesized): - * (bvsge s (bvand s t)) */ - scl = nm->mkNode(BITVECTOR_SGE, s, nm->mkNode(BITVECTOR_AND, s, t)); - } - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (pol) - { - /* x & s > t - * x | s > t - * with invertibility condition (synthesized): - * (bvslt t (bvand s max)) - * (bvslt t (bvor s max)) - * where - * max is the signed maximum value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(k, s, max)); - } - else - { - if (k == BITVECTOR_AND) - { - /* x & s <= t - * with invertibility condition (synthesized): - * (bvuge s (bvand t min)) - * where - * min is the signed minimum value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - scl = nm->mkNode(BITVECTOR_UGE, s, nm->mkNode(BITVECTOR_AND, t, min)); - } - else - { - /* x | s <= t - * with invertibility condition (synthesized): - * (bvsge t (bvor s min)) - * where - * min is the signed minimum value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_OR, s, min)); - } - } - } - Node scr = nm->mkNode(litk, nm->mkNode(k, x, s), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node defaultShiftSc(Kind litk, Kind shk, Node s, Node t) -{ - unsigned w; - NodeBuilder<> nb(OR); - NodeManager *nm; - - nm = NodeManager::currentNM(); - - w = bv::utils::getSize(s); - Assert(w == bv::utils::getSize(t)); - - nb << nm->mkNode(litk, s, t); - for (unsigned i = 1; i <= w; i++) - { - Node sw = bv::utils::mkConst(w, i); - nb << nm->mkNode(litk, nm->mkNode(shk, s, sw), t); - } - if (nb.getNumChildren() == 1) - return nb[0]; - return nb.constructNode(); -} - - -static Node getScBvLshr(bool pol, - Kind litk, - Kind k, - unsigned idx, - Node x, - Node s, - Node t) -{ - Assert(k == BITVECTOR_LSHR); - Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - Node scl; - unsigned w = bv::utils::getSize(s); - Assert(w == bv::utils::getSize(t)); - Node z = bv::utils::mkZero(w); - - if (litk == EQUAL) - { - if (idx == 0) - { - Node ww = bv::utils::mkConst(w, w); - - if (pol) - { - /* x >> s = t - * with invertibility condition (synthesized): - * (= (bvlshr (bvshl t s) s) t) */ - Node shl = nm->mkNode(BITVECTOR_SHL, t, s); - Node lshr = nm->mkNode(BITVECTOR_LSHR, shl, s); - scl = lshr.eqNode(t); - } - else - { - /* x >> s != t - * with invertibility condition: - * (or (distinct t z) (bvult s w)) - * where - * z = 0 with getSize(z) = w - * and w = getSize(s) = getSize(t) */ - scl = nm->mkNode(OR, - t.eqNode(z).notNode(), - nm->mkNode(BITVECTOR_ULT, s, ww)); - } - } - else - { - if (pol) - { - /* s >> x = t - * with invertibility condition: - * (or (= (bvlshr s i) t) ...) - * for i in 0..w */ - scl = defaultShiftSc(EQUAL, BITVECTOR_LSHR, s, t); - } - else - { - /* s >> x != t - * with invertibility condition: - * (or (distinct s z) (distinct t z)) - * where - * z = 0 with getSize(z) = w */ - scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); - } - } - } - else if (litk == BITVECTOR_ULT) - { - if (idx == 0) - { - if (pol) - { - /* x >> s < t - * with invertibility condition (synthesized): - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - scl = t.eqNode(z).notNode(); - } - else - { - /* x >> s >= t - * with invertibility condition (synthesized): - * (= (bvlshr (bvshl t s) s) t) */ - Node ts = nm->mkNode(BITVECTOR_SHL, t, s); - scl = nm->mkNode(BITVECTOR_LSHR, ts, s).eqNode(t); - } - } - else - { - if (pol) - { - /* s >> x < t - * with invertibility condition (synthesized): - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - scl = t.eqNode(z).notNode(); - } - else - { - /* s >> x >= t - * with invertibility condition (synthesized): - * (bvuge s t) */ - scl = nm->mkNode(BITVECTOR_UGE, s, t); - } - } - } - else if (litk == BITVECTOR_UGT) - { - if (idx == 0) - { - if (pol) - { - /* x >> s > t - * with invertibility condition (synthesized): - * (bvult t (bvlshr (bvnot s) s)) */ - Node lshr = nm->mkNode(BITVECTOR_LSHR, nm->mkNode(BITVECTOR_NOT, s), s); - scl = nm->mkNode(BITVECTOR_ULT, t, lshr); - } - else - { - /* x >> s <= t - * with invertibility condition: - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else - { - if (pol) - { - /* s >> x > t - * with invertibility condition (synthesized): - * (bvult t s) */ - scl = nm->mkNode(BITVECTOR_ULT, t, s); - } - else - { - /* s >> x <= t - * with invertibility condition: - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - } - else if (litk == BITVECTOR_SLT) - { - if (idx == 0) - { - if (pol) - { - /* x >> s < t - * with invertibility condition (synthesized): - * (bvslt (bvlshr (bvnot (bvneg t)) s) t) */ - Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t)); - Node lshr = nm->mkNode(BITVECTOR_LSHR, nnt, s); - scl = nm->mkNode(BITVECTOR_SLT, lshr, t); - } - else - { - /* x >> s >= t - * with invertibility condition: - * (=> (not (= s z)) (bvsge (bvlshr ones s) t)) - * where - * z = 0 with getSize(z) = w - * and ones = ~0 with getSize(ones) = w */ - Node ones = bv::utils::mkOnes(w); - Node lshr = nm->mkNode(BITVECTOR_LSHR, ones, s); - Node nz = s.eqNode(z).notNode(); - scl = nz.impNode(nm->mkNode(BITVECTOR_SGE, lshr, t)); - } - } - else - { - if (pol) - { - /* s >> x < t - * with invertibility condition (synthesized): - * (or (bvslt s t) (bvslt z t)) - * where - * z = 0 with getSize(z) = w */ - Node st = nm->mkNode(BITVECTOR_SLT, s, t); - Node zt = nm->mkNode(BITVECTOR_SLT, z, t); - scl = st.orNode(zt); - } - else - { - /* s >> x >= t - * with invertibility condition: - * (and - * (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t)) - * (=> (bvsge s z) (bvsge s t))) - * where - * z = 0 with getSize(z) = w */ - Node one = bv::utils::mkConst(w, 1); - Node sz = nm->mkNode(BITVECTOR_SLT, s, z); - Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one); - Node sge1 = nm->mkNode(BITVECTOR_SGE, lshr, t); - Node sge2 = nm->mkNode(BITVECTOR_SGE, s, t); - scl = sz.impNode(sge1).andNode(sz.notNode().impNode(sge2)); - } - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (idx == 0) - { - if (pol) - { - /* x >> s > t - * with invertibility condition (synthesized): - * (bvslt t (bvlshr (bvshl max s) s)) - * where - * max is the signed maximum value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node shl = nm->mkNode(BITVECTOR_SHL, max, s); - Node lshr = nm->mkNode(BITVECTOR_LSHR, shl, s); - scl = nm->mkNode(BITVECTOR_SLT, t, lshr); - } - else - { - /* x >> s <= t - * with invertibility condition (synthesized): - * (bvsge t (bvlshr t s)) */ - scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_LSHR, t, s)); - } - } - else - { - if (pol) - { - /* s >> x > t - * with invertibility condition: - * (and - * (=> (bvslt s z) (bvsgt (bvlshr s one) t)) - * (=> (bvsge s z) (bvsgt s t))) - * where - * z = 0 and getSize(z) = w */ - Node one = bv::utils::mkOne(w); - Node sz = nm->mkNode(BITVECTOR_SLT, s, z); - Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one); - Node sgt1 = nm->mkNode(BITVECTOR_SGT, lshr, t); - Node sgt2 = nm->mkNode(BITVECTOR_SGT, s, t); - scl = sz.impNode(sgt1).andNode(sz.notNode().impNode(sgt2)); - } - else - { - /* s >> x <= t - * with invertibility condition (synthesized): - * (or (bvult t min) (bvsge t s)) - * where - * min is the minimum signed value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node ult = nm->mkNode(BITVECTOR_ULT, t, min); - Node sge = nm->mkNode(BITVECTOR_SGE, t, s); - scl = ult.orNode(sge); - } - } - } - Node scr = - nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvAshr(bool pol, - Kind litk, - Kind k, - unsigned idx, - Node x, - Node s, - Node t) -{ - Assert(k == BITVECTOR_ASHR); - Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - Node scl; - unsigned w = bv::utils::getSize(s); - Assert(w == bv::utils::getSize(t)); - Node z = bv::utils::mkZero(w); - Node n = bv::utils::mkOnes(w); - - if (litk == EQUAL) - { - if (idx == 0) - { - if (pol) - { - /* x >> s = t - * with invertibility condition: - * (and - * (=> (bvult s w) (= (bvashr (bvshl t s) s) t)) - * (=> (bvuge s w) (or (= t ones) (= t z))) - * ) - * where - * z = 0 with getSize(z) = w - * and ones = ~0 with getSize(ones) = w - * and w = getSize(t) = getSize(s) */ - Node ww = bv::utils::mkConst(w, w); - Node shl = nm->mkNode(BITVECTOR_SHL, t, s); - Node ashr = nm->mkNode(BITVECTOR_ASHR, shl, s); - Node ult = nm->mkNode(BITVECTOR_ULT, s, ww); - Node imp1 = ult.impNode(ashr.eqNode(t)); - Node to = t.eqNode(n); - Node tz = t.eqNode(z); - Node imp2 = ult.notNode().impNode(to.orNode(tz)); - scl = imp1.andNode(imp2); - } - else - { - /* x >> s != t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else - { - if (pol) - { - /* s >> x = t - * with invertibility condition: - * (or (= (bvashr s i) t) ...) - * for i in 0..w */ - scl = defaultShiftSc(EQUAL, BITVECTOR_ASHR, s, t); - } - else - { - /* s >> x != t - * with invertibility condition: - * (and - * (or (not (= t z)) (not (= s z))) - * (or (not (= t ones)) (not (= s ones)))) - * where - * z = 0 with getSize(z) = w - * and ones = ~0 with getSize(ones) = w */ - scl = nm->mkNode(AND, - nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()), - nm->mkNode(OR, t.eqNode(n).notNode(), s.eqNode(n).notNode())); - } - } - } - else if (litk == BITVECTOR_ULT) - { - if (idx == 0) - { - if (pol) - { - /* x >> s < t - * with invertibility condition (synthesized): - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - scl = t.eqNode(z).notNode(); - } - else - { - /* x >> s >= t - * with invertibility condition (synthesized): - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else - { - if (pol) - { - /* s >> x < t - * with invertibility condition (synthesized): - * (and (not (and (bvuge s t) (bvslt s z))) (not (= t z))) - * where - * z = 0 with getSize(z) = w */ - Node st = nm->mkNode(BITVECTOR_UGE, s, t); - Node sz = nm->mkNode(BITVECTOR_SLT, s, z); - Node tz = t.eqNode(z).notNode(); - scl = st.andNode(sz).notNode().andNode(tz); - } - else - { - /* s >> x >= t - * with invertibility condition (synthesized): - * (not (and (bvult s (bvnot s)) (bvult s t))) */ - Node ss = nm->mkNode(BITVECTOR_ULT, s, nm->mkNode(BITVECTOR_NOT, s)); - Node st = nm->mkNode(BITVECTOR_ULT, s, t); - scl = ss.andNode(st).notNode(); - } - } - } - else if (litk == BITVECTOR_UGT) - { - if (idx == 0) - { - if (pol) - { - /* x >> s > t - * with invertibility condition (synthesized): - * (bvult t ones) - * where - * ones = ~0 with getSize(ones) = w */ - scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w)); - } - else - { - /* x >> s <= t - * with invertibility condition (synthesized): - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else - { - if (pol) - { - /* s >> x > t - * with invertibility condition (synthesized): - * (or (bvslt s (bvlshr s (bvnot t))) (bvult t s)) */ - Node lshr = nm->mkNode(BITVECTOR_LSHR, s, nm->mkNode(BITVECTOR_NOT, t)); - Node ts = nm->mkNode(BITVECTOR_ULT, t, s); - Node slt = nm->mkNode(BITVECTOR_SLT, s, lshr); - scl = slt.orNode(ts); - } - else - { - /* s >> x <= t - * with invertibility condition (synthesized): - * (or (bvult s min) (bvuge t s)) - * where - * min is the minimum signed value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node ult = nm->mkNode(BITVECTOR_ULT, s, min); - Node uge = nm->mkNode(BITVECTOR_UGE, t, s); - scl = ult.orNode(uge); - } - } - } - else if (litk == BITVECTOR_SLT) - { - if (idx == 0) - { - if (pol) - { - /* x >> s < t - * with invertibility condition: - * (bvslt (bvashr min s) t) - * where - * min is the minimum signed value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_ASHR, min, s), t); - } - else - { - /* x >> s >= t - * with invertibility condition: - * (bvsge (bvlshr max s) t) - * where - * max is the signed maximum value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - scl = nm->mkNode(BITVECTOR_SGE, nm->mkNode(BITVECTOR_LSHR, max, s), t); - } - } - else - { - if (pol) - { - /* s >> x < t - * with invertibility condition (synthesized): - * (or (bvslt s t) (bvslt z t)) - * where - * z = 0 and getSize(z) = w */ - Node st = nm->mkNode(BITVECTOR_SLT, s, t); - Node zt = nm->mkNode(BITVECTOR_SLT, z, t); - scl = st.orNode(zt); - } - else - { - /* s >> x >= t - * with invertibility condition (synthesized): - * (not (and (bvult t (bvnot t)) (bvslt s t))) */ - Node tt = nm->mkNode(BITVECTOR_ULT, t, nm->mkNode(BITVECTOR_NOT, t)); - Node st = nm->mkNode(BITVECTOR_SLT, s, t); - scl = tt.andNode(st).notNode(); - } - } - } - else - { - Assert(litk == BITVECTOR_SGT); - Node max = bv::utils::mkMaxSigned(w); - if (idx == 0) - { - Node lshr = nm->mkNode(BITVECTOR_LSHR, max, s); - if (pol) - { - /* x >> s > t - * with invertibility condition (synthesized): - * (bvslt t (bvlshr max s))) - * where - * max is the signed maximum value with getSize(max) = w */ - scl = nm->mkNode(BITVECTOR_SLT, t, lshr); - } - else - { - /* x >> s <= t - * with invertibility condition (synthesized): - * (bvsge t (bvnot (bvlshr max s))) - * where - * max is the signed maximum value with getSize(max) = w */ - scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, lshr)); - } - } - else - { - if (pol) - { - /* s >> x > t - * with invertibility condition (synthesized): - * (and (bvslt t (bvand s max)) (bvslt t (bvor s max))) - * where - * max is the signed maximum value with getSize(max) = w */ - Node sam = nm->mkNode(BITVECTOR_AND, s, max); - Node som = nm->mkNode(BITVECTOR_OR, s, max); - Node slta = nm->mkNode(BITVECTOR_SLT, t, sam); - Node slto = nm->mkNode(BITVECTOR_SLT, t, som); - scl = slta.andNode(slto); - } - else - { - /* s >> x <= t - * with invertibility condition (synthesized): - * (or (bvsge t z) (bvsge t s)) - * where - * z = 0 and getSize(z) = w */ - Node tz = nm->mkNode(BITVECTOR_SGE, t, z); - Node ts = nm->mkNode(BITVECTOR_SGE, t, s); - scl = tz.orNode(ts); - } - } - } - Node scr = - nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvShl(bool pol, - Kind litk, - Kind k, - unsigned idx, - Node x, - Node s, - Node t) -{ - Assert(k == BITVECTOR_SHL); - Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - Node scl; - unsigned w = bv::utils::getSize(s); - Assert(w == bv::utils::getSize(t)); - Node z = bv::utils::mkZero(w); - - if (litk == EQUAL) - { - if (idx == 0) - { - Node ww = bv::utils::mkConst(w, w); - - if (pol) - { - /* x << s = t - * with invertibility condition (synthesized): - * (= (bvshl (bvlshr t s) s) t) */ - Node lshr = nm->mkNode(BITVECTOR_LSHR, t, s); - Node shl = nm->mkNode(BITVECTOR_SHL, lshr, s); - scl = shl.eqNode(t); - } - else - { - /* x << s != t - * with invertibility condition: - * (or (distinct t z) (bvult s w)) - * with - * w = getSize(s) = getSize(t) - * and z = 0 with getSize(z) = w */ - scl = nm->mkNode(OR, - t.eqNode(z).notNode(), - nm->mkNode(BITVECTOR_ULT, s, ww)); - } - } - else - { - if (pol) - { - /* s << x = t - * with invertibility condition: - * (or (= (bvshl s i) t) ...) - * for i in 0..w */ - scl = defaultShiftSc(EQUAL, BITVECTOR_SHL, s, t); - } - else - { - /* s << x != t - * with invertibility condition: - * (or (distinct s z) (distinct t z)) - * where - * z = 0 with getSize(z) = w */ - scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); - } - } - } - else if (litk == BITVECTOR_ULT) - { - if (idx == 0) - { - if (pol) - { - /* x << s < t - * with invertibility condition (synthesized): - * (not (= t z)) */ - scl = t.eqNode(z).notNode(); - } - else - { - /* x << s >= t - * with invertibility condition (synthesized): - * (bvuge (bvshl ones s) t) */ - Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s); - scl = nm->mkNode(BITVECTOR_UGE, shl, t); - } - } - else - { - if (pol) - { - /* s << x < t - * with invertibility condition (synthesized): - * (not (= t z)) */ - scl = t.eqNode(z).notNode(); - } - else - { - /* s << x >= t - * with invertibility condition: - * (or (bvuge (bvshl s i) t) ...) - * for i in 0..w */ - scl = defaultShiftSc(BITVECTOR_UGE, BITVECTOR_SHL, s, t); - } - } - } - else if (litk == BITVECTOR_UGT) - { - if (idx == 0) - { - if (pol) - { - /* x << s > t - * with invertibility condition (synthesized): - * (bvult t (bvshl ones s)) - * where - * ones = ~0 with getSize(ones) = w */ - Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s); - scl = nm->mkNode(BITVECTOR_ULT, t, shl); - } - else - { - /* x << s <= t - * with invertibility condition: - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else - { - if (pol) - { - /* s << x > t - * with invertibility condition: - * (or (bvugt (bvshl s i) t) ...) - * for i in 0..w */ - scl = defaultShiftSc(BITVECTOR_UGT, BITVECTOR_SHL, s, t); - } - else - { - /* s << x <= t - * with invertibility condition: - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - } - else if (litk == BITVECTOR_SLT) - { - if (idx == 0) - { - if (pol) - { - /* x << s < t - * with invertibility condition (synthesized): - * (bvslt (bvshl (bvlshr min s) s) t) - * where - * min is the signed minimum value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node lshr = nm->mkNode(BITVECTOR_LSHR, min, s); - Node shl = nm->mkNode(BITVECTOR_SHL, lshr, s); - scl = nm->mkNode(BITVECTOR_SLT, shl, t); - } - else - { - /* x << s >= t - * with invertibility condition (synthesized): - * (bvsge (bvand (bvshl max s) max) t) - * where - * max is the signed maximum value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node shl = nm->mkNode(BITVECTOR_SHL, max, s); - scl = nm->mkNode(BITVECTOR_SGE, nm->mkNode(BITVECTOR_AND, shl, max), t); - } - } - else - { - if (pol) - { - /* s << x < t - * with invertibility condition (synthesized): - * (bvult (bvshl min s) (bvadd t min)) - * where - * min is the signed minimum value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node shl = nm->mkNode(BITVECTOR_SHL, min, s); - Node add = nm->mkNode(BITVECTOR_PLUS, t, min); - scl = nm->mkNode(BITVECTOR_ULT, shl, add); - } - else - { - /* s << x >= t - * with invertibility condition: - * (or (bvsge (bvshl s i) t) ...) - * for i in 0..w */ - scl = defaultShiftSc(BITVECTOR_SGE, BITVECTOR_SHL, s, t); - } - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (idx == 0) - { - if (pol) - { - /* x << s > t - * with invertibility condition (synthesized): - * (bvslt t (bvand (bvshl max s) max)) - * where - * max is the signed maximum value with getSize(max) = w */ - Node max = bv::utils::mkMaxSigned(w); - Node shl = nm->mkNode(BITVECTOR_SHL, max, s); - scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(BITVECTOR_AND, shl, max)); - } - else - { - /* x << s <= t - * with invertibility condition (synthesized): - * (bvult (bvlshr t (bvlshr t s)) min) - * where - * min is the signed minimum value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - Node ts = nm->mkNode(BITVECTOR_LSHR, t, s); - scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, ts), min); - } - } - else - { - if (pol) - { - /* s << x > t - * with invertibility condition: - * (or (bvsgt (bvshl s i) t) ...) - * for i in 0..w */ - scl = defaultShiftSc(BITVECTOR_SGT, BITVECTOR_SHL, s, t); - } - else - { - /* s << x <= t - * with invertibility condition (synthesized): - * (bvult (bvlshr t s) min) - * where - * min is the signed minimum value with getSize(min) = w */ - Node min = bv::utils::mkMinSigned(w); - scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, s), min); - } - } - } - Node scr = - nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvConcat(bool pol, - Kind litk, - unsigned idx, - Node x, - Node sv_t, - Node t) -{ - Assert(litk == EQUAL - || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - Kind k = sv_t.getKind(); - Assert(k == BITVECTOR_CONCAT); - NodeManager* nm = NodeManager::currentNM(); - unsigned nchildren = sv_t.getNumChildren(); - unsigned w1 = 0, w2 = 0; - unsigned w = bv::utils::getSize(t), wx = bv::utils::getSize(x); - NodeBuilder<> nbs1(BITVECTOR_CONCAT), nbs2(BITVECTOR_CONCAT); - Node s1, s2; - Node t1, t2, tx; - Node scl, scr; - - if (idx != 0) - { - if (idx == 1) - { - s1 = sv_t[0]; - } - else - { - for (unsigned i = 0; i < idx; ++i) { nbs1 << sv_t[i]; } - s1 = nbs1.constructNode(); - } - w1 = bv::utils::getSize(s1); - t1 = bv::utils::mkExtract(t, w - 1, w - w1); - } - - tx = bv::utils::mkExtract(t, w - w1 - 1 , w - w1 - wx); - - if (idx != nchildren-1) - { - if (idx == nchildren-2) - { - s2 = sv_t[nchildren-1]; - } - else - { - for (unsigned i = idx+1; i < nchildren; ++i) { nbs2 << sv_t[i]; } - s2 = nbs2.constructNode(); - } - w2 = bv::utils::getSize(s2); - Assert(w2 == w - w1 - wx); - t2 = bv::utils::mkExtract(t, w2 - 1, 0); - } - - Assert(!s1.isNull() || t1.isNull()); - Assert(!s2.isNull() || t2.isNull()); - Assert(!s1.isNull() || !s2.isNull()); - Assert(s1.isNull() || w1 == bv::utils::getSize(t1)); - Assert(s2.isNull() || w2 == bv::utils::getSize(t2)); - - if (litk == EQUAL) - { - if (s1.isNull()) - { - if (pol) - { - /* x o s2 = t (interpret t as tx o t2) - * with invertibility condition: - * (= s2 t2) */ - scl = s2.eqNode(t2); - } - else - { - /* x o s2 != t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else if (s2.isNull()) - { - if (pol) - { - /* s1 o x = t (interpret t as t1 o tx) - * with invertibility condition: - * (= s1 t1) */ - scl = s1.eqNode(t1); - } - else - { - /* s1 o x != t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else - { - if (pol) - { - /* s1 o x o s2 = t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and (= s1 t1) (= s2 t2)) */ - scl = nm->mkNode(AND, s1.eqNode(t1), s2.eqNode(t2)); - } - else - { - /* s1 o x o s2 != t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - } - else if (litk == BITVECTOR_ULT) - { - if (s1.isNull()) - { - if (pol) - { - /* x o s2 < t (interpret t as tx o t2) - * with invertibility condition: - * (=> (= tx z) (bvult s2 t2)) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node ult = nm->mkNode(BITVECTOR_ULT, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(z), ult); - } - else - { - /* x o s2 >= t (interpret t as tx o t2) - * (=> (= tx ones) (bvuge s2 t2)) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node uge = nm->mkNode(BITVECTOR_UGE, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(n), uge); - } - } - else if (s2.isNull()) - { - if (pol) - { - /* s1 o x < t (interpret t as t1 o tx) - * with invertibility condition: - * (and (bvule s1 t1) (=> (= s1 t1) (distinct tx z))) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1); - Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode()); - scl = nm->mkNode(AND, ule, imp); - } - else - { - /* s1 o x >= t (interpret t as t1 o tx) - * with invertibility condition: - * (bvuge s1 t1) */ - scl = nm->mkNode(BITVECTOR_UGE, s1, t1); - } - } - else - { - if (pol) - { - /* s1 o x o s2 < t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvule s1 t1) - * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2))) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULT, s2, t2)); - scl = nm->mkNode(AND, ule, imp); - } - else - { - /* s1 o x o s2 >= t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvuge s1 t1) - * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2))) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGE, s2, t2)); - scl = nm->mkNode(AND, uge, imp); - } - } - } - else if (litk == BITVECTOR_UGT) - { - if (s1.isNull()) - { - if (pol) - { - /* x o s2 > t (interpret t as tx o t2) - * with invertibility condition: - * (=> (= tx ones) (bvugt s2 t2)) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node ugt = nm->mkNode(BITVECTOR_UGT, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(n), ugt); - } - else - { - /* x o s2 <= t (interpret t as tx o t2) - * with invertibility condition: - * (=> (= tx z) (bvule s2 t2)) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node ule = nm->mkNode(BITVECTOR_ULE, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(z), ule); - } - } - else if (s2.isNull()) - { - if (pol) - { - /* s1 o x > t (interpret t as t1 o tx) - * with invertibility condition: - * (and (bvuge s1 t1) (=> (= s1 t1) (distinct tx ones))) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1); - Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode()); - scl = nm->mkNode(AND, uge, imp); - } - else - { - /* s1 o x <= t (interpret t as t1 o tx) - * with invertibility condition: - * (bvule s1 t1) */ - scl = nm->mkNode(BITVECTOR_ULE, s1, t1); - } - } - else - { - if (pol) - { - /* s1 o x o s2 > t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvuge s1 t1) - * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2))) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGT, s2, t2)); - scl = nm->mkNode(AND, uge, imp); - } - else - { - /* s1 o x o s2 <= t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvule s1 t1) - * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2))) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULE, s2, t2)); - scl = nm->mkNode(AND, ule, imp); - } - } - } - else if (litk == BITVECTOR_SLT) - { - if (s1.isNull()) - { - if (pol) - { - /* x o s2 < t (interpret t as tx o t2) - * with invertibility condition: - * (=> (= tx min) (bvult s2 t2)) - * where - * min is the signed minimum value with getSize(min) = wx */ - Node min = bv::utils::mkMinSigned(wx); - Node ult = nm->mkNode(BITVECTOR_ULT, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(min), ult); - } - else - { - /* x o s2 >= t (interpret t as tx o t2) - * (=> (= tx max) (bvuge s2 t2)) - * where - * max is the signed maximum value with getSize(max) = wx */ - Node max = bv::utils::mkMaxSigned(wx); - Node uge = nm->mkNode(BITVECTOR_UGE, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(max), uge); - } - } - else if (s2.isNull()) - { - if (pol) - { - /* s1 o x < t (interpret t as t1 o tx) - * with invertibility condition: - * (and (bvsle s1 t1) (=> (= s1 t1) (distinct tx z))) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1); - Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode()); - scl = nm->mkNode(AND, sle, imp); - } - else - { - /* s1 o x >= t (interpret t as t1 o tx) - * with invertibility condition: - * (bvsge s1 t1) */ - scl = nm->mkNode(BITVECTOR_SGE, s1, t1); - } - } - else - { - if (pol) - { - /* s1 o x o s2 < t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvsle s1 t1) - * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2))) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULT, s2, t2)); - scl = nm->mkNode(AND, sle, imp); - } - else - { - /* s1 o x o s2 >= t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvsge s1 t1) - * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2))) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGE, s2, t2)); - scl = nm->mkNode(AND, sge, imp); - } - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (s1.isNull()) - { - if (pol) - { - /* x o s2 > t (interpret t as tx o t2) - * with invertibility condition: - * (=> (= tx max) (bvugt s2 t2)) - * where - * max is the signed maximum value with getSize(max) = wx */ - Node max = bv::utils::mkMaxSigned(wx); - Node ugt = nm->mkNode(BITVECTOR_UGT, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(max), ugt); - } - else - { - /* x o s2 <= t (interpret t as tx o t2) - * with invertibility condition: - * (=> (= tx min) (bvule s2 t2)) - * where - * min is the signed minimum value with getSize(min) = wx */ - Node min = bv::utils::mkMinSigned(wx); - Node ule = nm->mkNode(BITVECTOR_ULE, s2, t2); - scl = nm->mkNode(IMPLIES, tx.eqNode(min), ule); - } - } - else if (s2.isNull()) - { - if (pol) - { - /* s1 o x > t (interpret t as t1 o tx) - * with invertibility condition: - * (and (bvsge s1 t1) (=> (= s1 t1) (distinct tx ones))) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1); - Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode()); - scl = nm->mkNode(AND, sge, imp); - } - else - { - /* s1 o x <= t (interpret t as t1 o tx) - * with invertibility condition: - * (bvsle s1 t1) */ - scl = nm->mkNode(BITVECTOR_SLE, s1, t1); - } - } - else - { - if (pol) - { - /* s1 o x o s2 > t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvsge s1 t1) - * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2))) - * where - * ones = ~0 with getSize(ones) = wx */ - Node n = bv::utils::mkOnes(wx); - Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGT, s2, t2)); - scl = nm->mkNode(AND, sge, imp); - } - else - { - /* s1 o x o s2 <= t (interpret t as t1 o tx o t2) - * with invertibility condition: - * (and - * (bvsle s1 t1) - * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2))) - * where - * z = 0 with getSize(z) = wx */ - Node z = bv::utils::mkZero(wx); - Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1); - Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); - Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULE, s2, t2)); - scl = nm->mkNode(AND, sle, imp); - } - } - } - scr = s1.isNull() ? x : bv::utils::mkConcat(s1, x); - if (!s2.isNull()) scr = bv::utils::mkConcat(scr, s2); - scr = nm->mkNode(litk, scr, t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; - return sc; -} - -static Node getScBvSext(bool pol, - Kind litk, - unsigned idx, - Node x, - Node sv_t, - Node t) -{ - Assert(litk == EQUAL - || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT - || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); - - NodeManager* nm = NodeManager::currentNM(); - Node scl; - Assert(idx == 0); - (void) idx; - unsigned ws = bv::utils::getSignExtendAmount(sv_t); - unsigned w = bv::utils::getSize(t); - - if (litk == EQUAL) - { - if (pol) - { - /* x sext ws = t - * with invertibility condition: - * (or (= ((_ extract u l) t) z) - * (= ((_ extract u l) t) ones)) - * where - * u = w - 1 - * l = w - 1 - ws - * z = 0 with getSize(z) = ws + 1 - * ones = ~0 with getSize(ones) = ws + 1 */ - Node ext = bv::utils::mkExtract(t, w - 1, w - 1 - ws); - Node z = bv::utils::mkZero(ws + 1); - Node n = bv::utils::mkOnes(ws + 1); - scl = nm->mkNode(OR, ext.eqNode(z), ext.eqNode(n)); - } - else - { - /* x sext ws != t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else if (litk == BITVECTOR_ULT) - { - if (pol) - { - /* x sext ws < t - * with invertibility condition: - * (distinct t z) - * where - * z = 0 with getSize(z) = w */ - Node z = bv::utils::mkZero(w); - scl = t.eqNode(z).notNode(); - } - else - { - /* x sext ws >= t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else if (litk == BITVECTOR_UGT) - { - if (pol) - { - /* x sext ws > t - * with invertibility condition: - * (distinct t ones) - * where - * ones = ~0 with getSize(ones) = w */ - Node n = bv::utils::mkOnes(w); - scl = t.eqNode(n).notNode(); - } - else - { - /* x sext ws <= t - * true (no invertibility condition) */ - scl = nm->mkConst<bool>(true); - } - } - else if (litk == BITVECTOR_SLT) - { - if (pol) - { - /* x sext ws < t - * with invertibility condition: - * (bvslt ((_ sign_extend ws) min) t) - * where - * min is the signed minimum value with getSize(min) = w - ws */ - Node min = bv::utils::mkMinSigned(w - ws); - Node ext = bv::utils::mkSignExtend(min, ws); - scl = nm->mkNode(BITVECTOR_SLT, ext, t); - } - else - { - /* x sext ws >= t - * with invertibility condition (combination of sgt and eq): - * - * (or - * (or (= ((_ extract u l) t) z) ; eq - * (= ((_ extract u l) t) ones)) - * (bvslt t ((_ zero_extend ws) max))) ; sgt - * where - * u = w - 1 - * l = w - 1 - ws - * z = 0 with getSize(z) = ws + 1 - * ones = ~0 with getSize(ones) = ws + 1 - * max is the signed maximum value with getSize(max) = w - ws */ - Node ext1 = bv::utils::mkExtract(t, w - 1, w - 1 - ws); - Node z = bv::utils::mkZero(ws + 1); - Node n = bv::utils::mkOnes(ws + 1); - Node o1 = nm->mkNode(OR, ext1.eqNode(z), ext1.eqNode(n)); - Node max = bv::utils::mkMaxSigned(w - ws); - Node ext2 = bv::utils::mkConcat(bv::utils::mkZero(ws), max); - Node o2 = nm->mkNode(BITVECTOR_SLT, t, ext2); - scl = nm->mkNode(OR, o1, o2); - } - } - else - { - Assert(litk == BITVECTOR_SGT); - if (pol) - { - /* x sext ws > t - * with invertibility condition: - * (bvslt t ((_ zero_extend ws) max)) - * where - * max is the signed maximum value with getSize(max) = w - ws */ - Node max = bv::utils::mkMaxSigned(w - ws); - Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max); - scl = nm->mkNode(BITVECTOR_SLT, t, ext); - } - else - { - /* x sext ws <= t - * with invertibility condition: - * (bvsge t (bvnot ((_ zero_extend ws) max))) - * where - * max is the signed maximum value with getSize(max) = w - ws */ - Node max = bv::utils::mkMaxSigned(w - ws); - Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max); - scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, ext)); - } - } - Node scr = nm->mkNode(litk, bv::utils::mkSignExtend(x, ws), t); - Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); - Trace("bv-invert") << "Add SC_" << BITVECTOR_SIGN_EXTEND << "(" << x - << "): " << sc << std::endl; - return sc; -} - Node BvInverter::solveBvLit(Node sv, Node lit, std::vector<unsigned>& path, @@ -2845,7 +231,7 @@ Node BvInverter::solveBvLit(Node sv, litk = k = lit.getKind(); /* Note: option --bool-to-bv is currently disabled when CBQI BV - * is enabled and the logic is quantified. + * is enabled and the logic is quantified. * We currently do not support Boolean operators * that are interpreted as bit-vector operators of width 1. */ @@ -2862,12 +248,10 @@ Node BvInverter::solveBvLit(Node sv, litk = k = lit.getKind(); } - Assert(k == EQUAL - || k == BITVECTOR_ULT - || k == BITVECTOR_SLT); + Assert(k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT); Node sv_t = lit[index]; - Node t = lit[1-index]; + Node t = lit[1 - index]; if (litk == BITVECTOR_ULT && index == 1) { litk = BITVECTOR_UGT; @@ -2895,7 +279,7 @@ Node BvInverter::solveBvLit(Node sv, Assert((nchildren == 1 && s.isNull()) || (nchildren > 1 && !s.isNull())); TypeNode solve_tn = sv_t[index].getType(); Node x = getSolveVariable(solve_tn); - Node sc; + Node ic; if (litk == EQUAL && (k == BITVECTOR_NOT || k == BITVECTOR_NEG)) { @@ -2909,8 +293,8 @@ Node BvInverter::solveBvLit(Node sv, { t = nm->mkNode(BITVECTOR_XOR, t, s); } - else if (litk == EQUAL && k == BITVECTOR_MULT - && s.isConst() && bv::utils::getBit(s, 0)) + else if (litk == EQUAL && k == BITVECTOR_MULT && s.isConst() + && bv::utils::getBit(s, 0)) { unsigned w = bv::utils::getSize(s); Integer s_val = s.getConst<BitVector>().toInteger(); @@ -2924,31 +308,31 @@ Node BvInverter::solveBvLit(Node sv, } else if (k == BITVECTOR_MULT) { - sc = getScBvMult(pol, litk, k, index, x, s, t); + ic = utils::getICBvMult(pol, litk, k, index, x, s, t); } else if (k == BITVECTOR_SHL) { - sc = getScBvShl(pol, litk, k, index, x, s, t); + ic = utils::getICBvShl(pol, litk, k, index, x, s, t); } else if (k == BITVECTOR_UREM_TOTAL) { - sc = getScBvUrem(pol, litk, k, index, x, s, t); + ic = utils::getICBvUrem(pol, litk, k, index, x, s, t); } else if (k == BITVECTOR_UDIV_TOTAL) { - sc = getScBvUdiv(pol, litk, k, index, x, s, t); + ic = utils::getICBvUdiv(pol, litk, k, index, x, s, t); } else if (k == BITVECTOR_AND || k == BITVECTOR_OR) { - sc = getScBvAndOr(pol, litk, k, index, x, s, t); + ic = utils::getICBvAndOr(pol, litk, k, index, x, s, t); } else if (k == BITVECTOR_LSHR) { - sc = getScBvLshr(pol, litk, k, index, x, s, t); + ic = utils::getICBvLshr(pol, litk, k, index, x, s, t); } else if (k == BITVECTOR_ASHR) { - sc = getScBvAshr(pol, litk, k, index, x, s, t); + ic = utils::getICBvAshr(pol, litk, k, index, x, s, t); } else if (k == BITVECTOR_CONCAT) { @@ -2969,33 +353,39 @@ Node BvInverter::solveBvLit(Node sv, NodeBuilder<> nb(BITVECTOR_CONCAT); for (unsigned i = 0; i < nchildren; i++) { - if (i < index) { upper -= bv::utils::getSize(sv_t[i]); } - else if (i > index) { lower += bv::utils::getSize(sv_t[i]); } + if (i < index) + { + upper -= bv::utils::getSize(sv_t[i]); + } + else if (i > index) + { + lower += bv::utils::getSize(sv_t[i]); + } } t = bv::utils::mkExtract(t, upper, lower); } else { - sc = getScBvConcat(pol, litk, index, x, sv_t, t); + ic = utils::getICBvConcat(pol, litk, index, x, sv_t, t); } } else if (k == BITVECTOR_SIGN_EXTEND) { - sc = getScBvSext(pol, litk, index, x, sv_t, t); + ic = utils::getICBvSext(pol, litk, index, x, sv_t, t); } else if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT) { - sc = getScBvUltUgt(pol, litk, x, t); + ic = utils::getICBvUltUgt(pol, litk, x, t); } else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT) { - sc = getScBvSltSgt(pol, litk, x, t); + ic = utils::getICBvSltSgt(pol, litk, x, t); } else if (pol == false) { - Assert (litk == EQUAL); - sc = nm->mkNode(DISTINCT, x, t); - Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << sc + Assert(litk == EQUAL); + ic = nm->mkNode(DISTINCT, x, t); + Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic << std::endl; } else @@ -3005,17 +395,20 @@ Node BvInverter::solveBvLit(Node sv, return Node::null(); } - if (!sc.isNull()) + if (!ic.isNull()) { - /* We generate a choice term (choice x0. SC => x0 <k> s <litk> t) for + /* We generate a choice term (choice x0. ic => x0 <k> s <litk> t) for * x <k> s <litk> t. When traversing down, this choice term determines - * the value for x <k> s = (choice x0. SC => x0 <k> s <litk> t), i.e., + * the value for x <k> s = (choice x0. ic => x0 <k> s <litk> t), i.e., * from here on, the propagated literal is a positive equality. */ litk = EQUAL; pol = true; /* t = fresh skolem constant */ - t = getInversionNode(sc, solve_tn, m); - if (t.isNull()) { return t; } + t = getInversionNode(ic, solve_tn, m); + if (t.isNull()) + { + return t; + } } sv_t = sv_t[index]; @@ -3025,24 +418,24 @@ Node BvInverter::solveBvLit(Node sv, Assert(sv_t == sv); TypeNode solve_tn = sv.getType(); Node x = getSolveVariable(solve_tn); - Node sc; + Node ic; if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT) { - sc = getScBvUltUgt(pol, litk, x, t); + ic = utils::getICBvUltUgt(pol, litk, x, t); } else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT) { - sc = getScBvSltSgt(pol, litk, x, t); + ic = utils::getICBvSltSgt(pol, litk, x, t); } else if (pol == false) { - Assert (litk == EQUAL); - sc = nm->mkNode(DISTINCT, x, t); - Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << sc + Assert(litk == EQUAL); + ic = nm->mkNode(DISTINCT, x, t); + Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic << std::endl; } - return sc.isNull() ? t : getInversionNode(sc, solve_tn, m); + return ic.isNull() ? t : getInversionNode(ic, solve_tn, m); } /*---------------------------------------------------------------------------*/ diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp new file mode 100644 index 000000000..8ad26a422 --- /dev/null +++ b/src/theory/quantifiers/bv_inverter_utils.cpp @@ -0,0 +1,2592 @@ +/********************* */ +/*! \file bv_inverter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief inverse rules for bit-vector operators + **/ + +#include "theory/quantifiers/bv_inverter_utils.h" +#include "theory/bv/theory_bv_utils.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace utils { + +Node getICBvUltUgt(bool pol, Kind k, Node x, Node t) +{ + Assert(k == BITVECTOR_ULT || k == BITVECTOR_UGT); + + NodeManager* nm = NodeManager::currentNM(); + unsigned w = bv::utils::getSize(t); + Node ic; + + if (k == BITVECTOR_ULT) + { + if (pol == true) + { + /* x < t + * with invertibility condition: + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkZero(w)); + Node scr = nm->mkNode(k, x, t); + ic = nm->mkNode(IMPLIES, scl, scr); + } + else + { + /* x >= t + * with invertibility condition: + * true (no invertibility condition) */ + ic = nm->mkNode(NOT, nm->mkNode(k, x, t)); + } + } + else + { + Assert(k == BITVECTOR_UGT); + if (pol == true) + { + /* x > t + * with invertibility condition: + * (distinct t ones) + * where + * ones = ~0 with getSize(ones) = w */ + Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w)); + Node scr = nm->mkNode(k, x, t); + ic = nm->mkNode(IMPLIES, scl, scr); + } + else + { + /* x <= t + * with invertibility condition: + * true (no invertibility condition) */ + ic = nm->mkNode(NOT, nm->mkNode(k, x, t)); + } + } + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvSltSgt(bool pol, Kind k, Node x, Node t) +{ + Assert(k == BITVECTOR_SLT || k == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + unsigned w = bv::utils::getSize(t); + Node ic; + + if (k == BITVECTOR_SLT) + { + if (pol == true) + { + /* x < t + * with invertibility condition: + * (distinct t min) + * where + * min is the minimum signed value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node scl = nm->mkNode(DISTINCT, min, t); + Node scr = nm->mkNode(k, x, t); + ic = nm->mkNode(IMPLIES, scl, scr); + } + else + { + /* x >= t + * with invertibility condition: + * true (no invertibility condition) */ + ic = nm->mkNode(NOT, nm->mkNode(k, x, t)); + } + } + else + { + Assert(k == BITVECTOR_SGT); + if (pol == true) + { + /* x > t + * with invertibility condition: + * (distinct t max) + * where + * max is the signed maximum value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node scl = nm->mkNode(DISTINCT, t, max); + Node scr = nm->mkNode(k, x, t); + ic = nm->mkNode(IMPLIES, scl, scr); + } + else + { + /* x <= t + * with invertibility condition: + * true (no invertibility condition) */ + ic = nm->mkNode(NOT, nm->mkNode(k, x, t)); + } + } + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvMult( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) +{ + Assert(k == BITVECTOR_MULT); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + Node scl; + unsigned w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + + if (litk == EQUAL) + { + Node z = bv::utils::mkZero(w); + + if (pol) + { + /* x * s = t + * with invertibility condition (synthesized): + * (= (bvand (bvor (bvneg s) s) t) t) + * + * is equivalent to: + * ctz(t) >= ctz(s) + * -> + * (or + * (= t z) + * (and + * (bvuge (bvand t (bvneg t)) (bvand s (bvneg s))) + * (distinct s z))) + * where + * z = 0 with getSize(z) = w */ + Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); + scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_AND, o, t), t); + } + else + { + /* x * s != t + * with invertibility condition: + * (or (distinct t z) (distinct s z)) + * where + * z = 0 with getSize(z) = w */ + scl = nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()); + } + } + else if (litk == BITVECTOR_ULT) + { + if (pol) + { + /* x * s < t + * with invertibility condition (synthesized): + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = nm->mkNode(DISTINCT, t, z); + } + else + { + /* x * s >= t + * with invertibility condition (synthesized): + * (bvuge (bvor (bvneg s) s) t) */ + Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); + scl = nm->mkNode(BITVECTOR_UGE, o, t); + } + } + else if (litk == BITVECTOR_UGT) + { + if (pol) + { + /* x * s > t + * with invertibility condition (synthesized): + * (bvult t (bvor (bvneg s) s)) */ + Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); + scl = nm->mkNode(BITVECTOR_ULT, t, o); + } + else + { + /* x * s <= t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else if (litk == BITVECTOR_SLT) + { + if (pol) + { + /* x * s < t + * with invertibility condition (synthesized): + * (bvslt (bvand (bvnot (bvneg t)) (bvor (bvneg s) s)) t) */ + Node a1 = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t)); + Node a2 = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); + scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_AND, a1, a2), t); + } + else + { + /* x * s >= t + * with invertibility condition (synthesized): + * (bvsge (bvand (bvor (bvneg s) s) max) t) + * where + * max is the signed maximum value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s); + Node a = nm->mkNode(BITVECTOR_AND, o, max); + scl = nm->mkNode(BITVECTOR_SGE, a, t); + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (pol) + { + /* x * s > t + * with invertibility condition (synthesized): + * (bvslt t (bvsub t (bvor (bvor s t) (bvneg s)))) */ + Node o = nm->mkNode(BITVECTOR_OR, + nm->mkNode(BITVECTOR_OR, s, t), + nm->mkNode(BITVECTOR_NEG, s)); + Node sub = nm->mkNode(BITVECTOR_SUB, t, o); + scl = nm->mkNode(BITVECTOR_SLT, t, sub); + } + else + { + /* x * s <= t + * with invertibility condition (synthesized): + * (not (and (= s z) (bvslt t s))) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = nm->mkNode(AND, s.eqNode(z), nm->mkNode(BITVECTOR_SLT, t, s)); + scl = scl.notNode(); + } + } + + Node scr = + nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvUrem( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) +{ + Assert(k == BITVECTOR_UREM_TOTAL); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + Node scl; + unsigned w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + + if (litk == EQUAL) + { + if (idx == 0) + { + if (pol) + { + /* x % s = t + * with invertibility condition (synthesized): + * (bvuge (bvnot (bvneg s)) t) */ + Node neg = nm->mkNode(BITVECTOR_NEG, s); + scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t); + } + else + { + /* x % s != t + * with invertibility condition: + * (or (distinct s (_ bv1 w)) (distinct t z)) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = nm->mkNode( + OR, s.eqNode(bv::utils::mkOne(w)).notNode(), t.eqNode(z).notNode()); + } + } + else + { + if (pol) + { + /* s % x = t + * with invertibility condition (synthesized): + * (bvuge (bvand (bvsub (bvadd t t) s) s) t) + * + * is equivalent to: + * (or (= s t) + * (and (bvugt s t) + * (bvugt (bvsub s t) t) + * (or (= t z) (distinct (bvsub s (_ bv1 w)) t)))) + * where + * z = 0 with getSize(z) = w */ + Node add = nm->mkNode(BITVECTOR_PLUS, t, t); + Node sub = nm->mkNode(BITVECTOR_SUB, add, s); + Node a = nm->mkNode(BITVECTOR_AND, sub, s); + scl = nm->mkNode(BITVECTOR_UGE, a, t); + } + else + { + /* s % x != t + * with invertibility condition: + * (or (distinct s z) (distinct t z)) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); + } + } + } + else if (litk == BITVECTOR_ULT) + { + if (idx == 0) + { + if (pol) + { + /* x % s < t + * with invertibility condition: + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = t.eqNode(z).notNode(); + } + else + { + /* x % s >= t + * with invertibility condition (synthesized): + * (bvuge (bvnot (bvneg s)) t) */ + Node neg = nm->mkNode(BITVECTOR_NEG, s); + scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t); + } + } + else + { + if (pol) + { + /* s % x < t + * with invertibility condition: + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = t.eqNode(z).notNode(); + } + else + { + /* s % x >= t + * with invertibility condition (combination of = and >): + * (or + * (bvuge (bvand (bvsub (bvadd t t) s) s) t) ; eq, synthesized + * (bvult t s)) ; ugt, synthesized */ + Node add = nm->mkNode(BITVECTOR_PLUS, t, t); + Node sub = nm->mkNode(BITVECTOR_SUB, add, s); + Node a = nm->mkNode(BITVECTOR_AND, sub, s); + Node sceq = nm->mkNode(BITVECTOR_UGE, a, t); + Node scugt = nm->mkNode(BITVECTOR_ULT, t, s); + scl = nm->mkNode(OR, sceq, scugt); + } + } + } + else if (litk == BITVECTOR_UGT) + { + if (idx == 0) + { + if (pol) + { + /* x % s > t + * with invertibility condition (synthesized): + * (bvult t (bvnot (bvneg s))) */ + Node nt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s)); + scl = nm->mkNode(BITVECTOR_ULT, t, nt); + } + else + { + /* x % s <= t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else + { + if (pol) + { + /* s % x > t + * with invertibility condition (synthesized): + * (bvult t s) */ + scl = nm->mkNode(BITVECTOR_ULT, t, s); + } + else + { + /* s % x <= t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + } + else if (litk == BITVECTOR_SLT) + { + if (idx == 0) + { + if (pol) + { + /* x % s < t + * with invertibility condition (synthesized): + * (bvslt (bvnot t) (bvor (bvneg s) (bvneg t))) */ + Node o1 = nm->mkNode(BITVECTOR_NEG, s); + Node o2 = nm->mkNode(BITVECTOR_NEG, t); + Node o = nm->mkNode(BITVECTOR_OR, o1, o2); + scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_NOT, t), o); + } + else + { + /* x % s >= t + * with invertibility condition (synthesized): + * (or (bvslt t s) (bvsge z s)) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + Node s1 = nm->mkNode(BITVECTOR_SLT, t, s); + Node s2 = nm->mkNode(BITVECTOR_SGE, z, s); + scl = nm->mkNode(OR, s1, s2); + } + } + else + { + Node z = bv::utils::mkZero(w); + + if (pol) + { + /* s % x < t + * with invertibility condition (synthesized): + * (or (bvslt s t) (bvslt z t)) + * where + * z = 0 with getSize(z) = w */ + Node slt1 = nm->mkNode(BITVECTOR_SLT, s, t); + Node slt2 = nm->mkNode(BITVECTOR_SLT, z, t); + scl = nm->mkNode(OR, slt1, slt2); + } + else + { + /* s % x >= t + * with invertibility condition: + * (and + * (=> (bvsge s z) (bvsge s t)) + * (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t))) + * where + * z = 0 with getSize(z) = w */ + Node i1 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SGE, s, z), + nm->mkNode(BITVECTOR_SGE, s, t)); + Node i2 = nm->mkNode( + IMPLIES, + nm->mkNode(AND, + nm->mkNode(BITVECTOR_SLT, s, z), + nm->mkNode(BITVECTOR_SGE, t, z)), + nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t)); + scl = nm->mkNode(AND, i1, i2); + } + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (idx == 0) + { + Node z = bv::utils::mkZero(w); + + if (pol) + { + /* x % s > t + * with invertibility condition: + * + * (and + * (and + * (=> (bvsgt s z) (bvslt t (bvnot (bvneg s)))) + * (=> (bvsle s z) (distinct t max))) + * (or (distinct t z) (distinct s (_ bv1 w)))) + * where + * z = 0 with getSize(z) = w + * and max is the maximum signed value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node nt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s)); + Node i1 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SGT, s, z), + nm->mkNode(BITVECTOR_SLT, t, nt)); + Node i2 = nm->mkNode( + IMPLIES, nm->mkNode(BITVECTOR_SLE, s, z), t.eqNode(max).notNode()); + Node a1 = nm->mkNode(AND, i1, i2); + Node a2 = nm->mkNode( + OR, t.eqNode(z).notNode(), s.eqNode(bv::utils::mkOne(w)).notNode()); + scl = nm->mkNode(AND, a1, a2); + } + else + { + /* x % s <= t + * with invertibility condition (synthesized): + * (bvslt ones (bvand (bvneg s) t)) + * where + * z = 0 with getSize(z) = w + * and ones = ~0 with getSize(ones) = w */ + Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, s), t); + scl = nm->mkNode(BITVECTOR_SLT, bv::utils::mkOnes(w), a); + } + } + else + { + if (pol) + { + /* s % x > t + * with invertibility condition: + * (and + * (=> (bvsge s z) (bvsgt s t)) + * (=> (bvslt s z) + * (bvsgt (bvlshr (bvsub s (_ bv1 w)) (_ bv1 w)) t))) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + Node i1 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SGE, s, z), + nm->mkNode(BITVECTOR_SGT, s, t)); + Node shr = nm->mkNode( + BITVECTOR_LSHR, bv::utils::mkDec(s), bv::utils::mkOne(w)); + Node i2 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SLT, s, z), + nm->mkNode(BITVECTOR_SGT, shr, t)); + scl = nm->mkNode(AND, i1, i2); + } + else + { + /* s % x <= t + * with invertibility condition (synthesized): + * (or (bvult t min) (bvsge t s)) + * where + * min is the minimum signed value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node o1 = nm->mkNode(BITVECTOR_ULT, t, min); + Node o2 = nm->mkNode(BITVECTOR_SGE, t, s); + scl = nm->mkNode(OR, o1, o2); + } + } + } + + Node scr = + nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvUdiv( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) +{ + Assert(k == BITVECTOR_UDIV_TOTAL); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + unsigned w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + Node scl; + Node z = bv::utils::mkZero(w); + + if (litk == EQUAL) + { + if (idx == 0) + { + if (pol) + { + /* x udiv s = t + * with invertibility condition (synthesized): + * (= (bvudiv (bvmul s t) s) t) + * + * is equivalent to: + * (or + * (and (= t (bvnot z)) + * (or (= s z) (= s (_ bv1 w)))) + * (and (distinct t (bvnot z)) + * (distinct s z) + * (not (umulo s t)))) + * + * where + * umulo(s, t) is true if s * t produces and overflow + * and z = 0 with getSize(z) = w */ + Node mul = nm->mkNode(BITVECTOR_MULT, s, t); + Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s); + scl = nm->mkNode(EQUAL, div, t); + } + else + { + /* x udiv s != t + * with invertibility condition: + * (or (distinct s z) (distinct t ones)) + * where + * z = 0 with getSize(z) = w + * and ones = ~0 with getSize(ones) = w */ + Node ones = bv::utils::mkOnes(w); + scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(ones).notNode()); + } + } + else + { + if (pol) + { + /* s udiv x = t + * with invertibility condition (synthesized): + * (= (bvudiv s (bvudiv s t)) t) + * + * is equivalent to: + * (or + * (= s t) + * (= t (bvnot z)) + * (and + * (bvuge s t) + * (or + * (= (bvurem s t) z) + * (bvule (bvadd (bvudiv s (bvadd t (_ bv1 w))) (_ bv1 w)) + * (bvudiv s t))) + * (=> (= s (bvnot (_ bv0 8))) (distinct t (_ bv0 8))))) + * + * where + * z = 0 with getSize(z) = w */ + Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t); + scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, div), t); + } + else + { + /* s udiv x != t + * with invertibility condition (w > 1): + * true (no invertibility condition) + * + * with invertibility condition (w == 1): + * (= (bvand s t) z) + * + * where + * z = 0 with getSize(z) = w */ + if (w > 1) + { + scl = nm->mkConst<bool>(true); + } + else + { + scl = nm->mkNode(BITVECTOR_AND, s, t).eqNode(z); + } + } + } + } + else if (litk == BITVECTOR_ULT) + { + if (idx == 0) + { + if (pol) + { + /* x udiv s < t + * with invertibility condition (synthesized): + * (and (bvult z s) (bvult z t)) + * where + * z = 0 with getSize(z) = w */ + Node u1 = nm->mkNode(BITVECTOR_ULT, z, s); + Node u2 = nm->mkNode(BITVECTOR_ULT, z, t); + scl = nm->mkNode(AND, u1, u2); + } + else + { + /* x udiv s >= t + * with invertibility condition (synthesized): + * (= (bvand (bvudiv (bvmul s t) t) s) s) */ + Node mul = nm->mkNode(BITVECTOR_MULT, s, t); + Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, t); + scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_AND, div, s), s); + } + } + else + { + if (pol) + { + /* s udiv x < t + * with invertibility condition (synthesized): + * (and (bvult z (bvnot (bvand (bvneg t) s))) (bvult z t)) + * where + * z = 0 with getSize(z) = w */ + Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, t), s); + Node u1 = nm->mkNode(BITVECTOR_ULT, z, nm->mkNode(BITVECTOR_NOT, a)); + Node u2 = nm->mkNode(BITVECTOR_ULT, z, t); + scl = nm->mkNode(AND, u1, u2); + } + else + { + /* s udiv x >= t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + } + else if (litk == BITVECTOR_UGT) + { + if (idx == 0) + { + if (pol) + { + /* x udiv s > t + * with invertibility condition: + * (bvugt (bvudiv ones s) t) + * where + * ones = ~0 with getSize(ones) = w */ + Node ones = bv::utils::mkOnes(w); + Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); + scl = nm->mkNode(BITVECTOR_UGT, div, t); + } + else + { + /* x udiv s <= t + * with invertibility condition (synthesized): + * (bvuge (bvor s t) (bvnot (bvneg s))) */ + Node u1 = nm->mkNode(BITVECTOR_OR, s, t); + Node u2 = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s)); + scl = nm->mkNode(BITVECTOR_UGE, u1, u2); + } + } + else + { + if (pol) + { + /* s udiv x > t + * with invertibility condition (synthesized): + * (bvult t ones) + * where + * ones = ~0 with getSize(ones) = w */ + Node ones = bv::utils::mkOnes(w); + scl = nm->mkNode(BITVECTOR_ULT, t, ones); + } + else + { + /* s udiv x <= t + * with invertibility condition (synthesized): + * (bvult z (bvor (bvnot s) t)) + * where + * z = 0 with getSize(z) = w */ + scl = nm->mkNode( + BITVECTOR_ULT, + z, + nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NOT, s), t)); + } + } + } + else if (litk == BITVECTOR_SLT) + { + if (idx == 0) + { + if (pol) + { + /* x udiv s < t + * with invertibility condition: + * (=> (bvsle t z) (bvslt (bvudiv min s) t)) + * where + * z = 0 with getSize(z) = w + * and min is the minimum signed value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node sle = nm->mkNode(BITVECTOR_SLE, t, z); + Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s); + Node slt = nm->mkNode(BITVECTOR_SLT, div, t); + scl = nm->mkNode(IMPLIES, sle, slt); + } + else + { + /* x udiv s >= t + * with invertibility condition: + * (or + * (bvsge (bvudiv ones s) t) + * (bvsge (bvudiv max s) t)) + * where + * ones = ~0 with getSize(ones) = w + * and max is the maximum signed value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node ones = bv::utils::mkOnes(w); + Node udiv1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); + Node udiv2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, max, s); + Node sge1 = nm->mkNode(BITVECTOR_SGE, udiv1, t); + Node sge2 = nm->mkNode(BITVECTOR_SGE, udiv2, t); + scl = nm->mkNode(OR, sge1, sge2); + } + } + else + { + if (pol) + { + /* s udiv x < t + * with invertibility condition (synthesized): + * (or (bvslt s t) (bvsge t z)) + * where + * z = 0 with getSize(z) = w */ + Node slt = nm->mkNode(BITVECTOR_SLT, s, t); + Node sge = nm->mkNode(BITVECTOR_SGE, t, z); + scl = nm->mkNode(OR, slt, sge); + } + else + { + /* s udiv x >= t + * with invertibility condition (w > 1): + * (and + * (=> (bvsge s z) (bvsge s t)) + * (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t))) + * + * with invertibility condition (w == 1): + * (bvsge s t) + * + * where + * z = 0 with getSize(z) = w */ + + if (w > 1) + { + Node div = nm->mkNode(BITVECTOR_LSHR, s, bv::utils::mkConst(w, 1)); + Node i1 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SGE, s, z), + nm->mkNode(BITVECTOR_SGE, s, t)); + Node i2 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SLT, s, z), + nm->mkNode(BITVECTOR_SGE, div, t)); + scl = nm->mkNode(AND, i1, i2); + } + else + { + scl = nm->mkNode(BITVECTOR_SGE, s, t); + } + } + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (idx == 0) + { + if (pol) + { + /* x udiv s > t + * with invertibility condition: + * (or + * (bvsgt (bvudiv ones s) t) + * (bvsgt (bvudiv max s) t)) + * where + * ones = ~0 with getSize(ones) = w + * and max is the maximum signed value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node ones = bv::utils::mkOnes(w); + Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s); + Node sgt1 = nm->mkNode(BITVECTOR_SGT, div1, t); + Node div2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, max, s); + Node sgt2 = nm->mkNode(BITVECTOR_SGT, div2, t); + scl = nm->mkNode(OR, sgt1, sgt2); + } + else + { + /* x udiv s <= t + * with invertibility condition (combination of = and <): + * (or + * (= (bvudiv (bvmul s t) s) t) ; eq, synthesized + * (=> (bvsle t z) (bvslt (bvudiv min s) t))) ; slt + * where + * z = 0 with getSize(z) = w + * and min is the minimum signed value with getSize(min) = w */ + Node mul = nm->mkNode(BITVECTOR_MULT, s, t); + Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s); + Node o1 = nm->mkNode(EQUAL, div1, t); + Node min = bv::utils::mkMinSigned(w); + Node sle = nm->mkNode(BITVECTOR_SLE, t, z); + Node div2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s); + Node slt = nm->mkNode(BITVECTOR_SLT, div2, t); + Node o2 = nm->mkNode(IMPLIES, sle, slt); + scl = nm->mkNode(OR, o1, o2); + } + } + else + { + if (pol) + { + /* s udiv x > t + * with invertibility condition (w > 1): + * (and + * (=> (bvsge s z) (bvsgt s t)) + * (=> (bvslt s z) (bvsgt (bvlshr s (_ bv1 w)) t))) + * + * with invertibility condition (w == 1): + * (bvsgt s t) + * + * where + * z = 0 with getSize(z) = w */ + if (w > 1) + { + Node div = nm->mkNode(BITVECTOR_LSHR, s, bv::utils::mkConst(w, 1)); + Node i1 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SGE, s, z), + nm->mkNode(BITVECTOR_SGT, s, t)); + Node i2 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SLT, s, z), + nm->mkNode(BITVECTOR_SGT, div, t)); + scl = nm->mkNode(AND, i1, i2); + } + else + { + scl = nm->mkNode(BITVECTOR_SGT, s, t); + } + } + else + { + /* s udiv x <= t + * with invertibility condition (synthesized): + * (not (and (bvslt t (bvnot #x0)) (bvslt t s))) + * <-> + * (or (bvsge t ones) (bvsge t s)) + * where + * ones = ~0 with getSize(ones) = w */ + Node ones = bv::utils::mkOnes(w); + Node sge1 = nm->mkNode(BITVECTOR_SGE, t, ones); + Node sge2 = nm->mkNode(BITVECTOR_SGE, t, s); + scl = nm->mkNode(OR, sge1, sge2); + } + } + } + + Node scr = + nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvAndOr( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) +{ + Assert(k == BITVECTOR_AND || k == BITVECTOR_OR); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + unsigned w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + Node scl; + + if (litk == EQUAL) + { + if (pol) + { + /* x & s = t + * x | s = t + * with invertibility condition: + * (= (bvand t s) t) + * (= (bvor t s) t) */ + scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s)); + } + else + { + if (k == BITVECTOR_AND) + { + /* x & s = t + * with invertibility condition: + * (or (distinct s z) (distinct t z)) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); + } + else + { + /* x | s = t + * with invertibility condition: + * (or (distinct s ones) (distinct t ones)) + * where + * ones = ~0 with getSize(ones) = w */ + Node n = bv::utils::mkOnes(w); + scl = nm->mkNode(OR, s.eqNode(n).notNode(), t.eqNode(n).notNode()); + } + } + } + else if (litk == BITVECTOR_ULT) + { + if (pol) + { + if (k == BITVECTOR_AND) + { + /* x & s < t + * with invertibility condition (synthesized): + * (distinct t z) + * where + * z = 0 with getSize(z) = 0 */ + Node z = bv::utils::mkZero(w); + scl = t.eqNode(z).notNode(); + } + else + { + /* x | s < t + * with invertibility condition (synthesized): + * (bvult s t) */ + scl = nm->mkNode(BITVECTOR_ULT, s, t); + } + } + else + { + if (k == BITVECTOR_AND) + { + /* x & s >= t + * with invertibility condition (synthesized): + * (bvuge s t) */ + scl = nm->mkNode(BITVECTOR_UGE, s, t); + } + else + { + /* x | s >= t + * with invertibility condition (synthesized): + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + } + else if (litk == BITVECTOR_UGT) + { + if (pol) + { + if (k == BITVECTOR_AND) + { + /* x & s > t + * with invertibility condition (synthesized): + * (bvult t s) */ + scl = nm->mkNode(BITVECTOR_ULT, t, s); + } + else + { + /* x | s > t + * with invertibility condition (synthesized): + * (bvult t ones) + * where + * ones = ~0 with getSize(ones) = w */ + scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w)); + } + } + else + { + if (k == BITVECTOR_AND) + { + /* x & s <= t + * with invertibility condition (synthesized): + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + else + { + /* x | s <= t + * with invertibility condition (synthesized): + * (bvuge t s) */ + scl = nm->mkNode(BITVECTOR_UGE, t, s); + } + } + } + else if (litk == BITVECTOR_SLT) + { + if (pol) + { + if (k == BITVECTOR_AND) + { + /* x & s < t + * with invertibility condition (synthesized): + * (bvslt (bvand (bvnot (bvneg t)) s) t) */ + Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t)); + scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_AND, nnt, s), t); + } + else + { + /* x | s < t + * with invertibility condition (synthesized): + * (bvslt (bvor (bvnot (bvsub s t)) s) t) */ + Node st = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_SUB, s, t)); + scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_OR, st, s), t); + } + } + else + { + if (k == BITVECTOR_AND) + { + /* x & s >= t + * with invertibility condition (case = combined with synthesized + * bvsgt): (or + * (= (bvand s t) t) + * (bvslt t (bvand (bvsub t s) s))) */ + Node sc_sgt = nm->mkNode( + BITVECTOR_SLT, + t, + nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_SUB, t, s), s)); + Node sc_eq = nm->mkNode(BITVECTOR_AND, s, t).eqNode(t); + scl = sc_eq.orNode(sc_sgt); + } + else + { + /* x | s >= t + * with invertibility condition (synthesized): + * (bvsge s (bvand s t)) */ + scl = nm->mkNode(BITVECTOR_SGE, s, nm->mkNode(BITVECTOR_AND, s, t)); + } + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (pol) + { + /* x & s > t + * x | s > t + * with invertibility condition (synthesized): + * (bvslt t (bvand s max)) + * (bvslt t (bvor s max)) + * where + * max is the signed maximum value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(k, s, max)); + } + else + { + if (k == BITVECTOR_AND) + { + /* x & s <= t + * with invertibility condition (synthesized): + * (bvuge s (bvand t min)) + * where + * min is the signed minimum value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + scl = nm->mkNode(BITVECTOR_UGE, s, nm->mkNode(BITVECTOR_AND, t, min)); + } + else + { + /* x | s <= t + * with invertibility condition (synthesized): + * (bvsge t (bvor s min)) + * where + * min is the signed minimum value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_OR, s, min)); + } + } + } + Node scr = nm->mkNode(litk, nm->mkNode(k, x, s), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +namespace { +Node defaultShiftIC(Kind litk, Kind shk, Node s, Node t) +{ + unsigned w; + NodeBuilder<> nb(OR); + NodeManager* nm; + + nm = NodeManager::currentNM(); + + w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + + nb << nm->mkNode(litk, s, t); + for (unsigned i = 1; i <= w; i++) + { + Node sw = bv::utils::mkConst(w, i); + nb << nm->mkNode(litk, nm->mkNode(shk, s, sw), t); + } + if (nb.getNumChildren() == 1) return nb[0]; + return nb.constructNode(); +} +} // namespace + +Node getICBvLshr( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) +{ + Assert(k == BITVECTOR_LSHR); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + Node scl; + unsigned w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + Node z = bv::utils::mkZero(w); + + if (litk == EQUAL) + { + if (idx == 0) + { + Node ww = bv::utils::mkConst(w, w); + + if (pol) + { + /* x >> s = t + * with invertibility condition (synthesized): + * (= (bvlshr (bvshl t s) s) t) */ + Node shl = nm->mkNode(BITVECTOR_SHL, t, s); + Node lshr = nm->mkNode(BITVECTOR_LSHR, shl, s); + scl = lshr.eqNode(t); + } + else + { + /* x >> s != t + * with invertibility condition: + * (or (distinct t z) (bvult s w)) + * where + * z = 0 with getSize(z) = w + * and w = getSize(s) = getSize(t) */ + scl = nm->mkNode( + OR, t.eqNode(z).notNode(), nm->mkNode(BITVECTOR_ULT, s, ww)); + } + } + else + { + if (pol) + { + /* s >> x = t + * with invertibility condition: + * (or (= (bvlshr s i) t) ...) + * for i in 0..w */ + scl = defaultShiftIC(EQUAL, BITVECTOR_LSHR, s, t); + } + else + { + /* s >> x != t + * with invertibility condition: + * (or (distinct s z) (distinct t z)) + * where + * z = 0 with getSize(z) = w */ + scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); + } + } + } + else if (litk == BITVECTOR_ULT) + { + if (idx == 0) + { + if (pol) + { + /* x >> s < t + * with invertibility condition (synthesized): + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + scl = t.eqNode(z).notNode(); + } + else + { + /* x >> s >= t + * with invertibility condition (synthesized): + * (= (bvlshr (bvshl t s) s) t) */ + Node ts = nm->mkNode(BITVECTOR_SHL, t, s); + scl = nm->mkNode(BITVECTOR_LSHR, ts, s).eqNode(t); + } + } + else + { + if (pol) + { + /* s >> x < t + * with invertibility condition (synthesized): + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + scl = t.eqNode(z).notNode(); + } + else + { + /* s >> x >= t + * with invertibility condition (synthesized): + * (bvuge s t) */ + scl = nm->mkNode(BITVECTOR_UGE, s, t); + } + } + } + else if (litk == BITVECTOR_UGT) + { + if (idx == 0) + { + if (pol) + { + /* x >> s > t + * with invertibility condition (synthesized): + * (bvult t (bvlshr (bvnot s) s)) */ + Node lshr = nm->mkNode(BITVECTOR_LSHR, nm->mkNode(BITVECTOR_NOT, s), s); + scl = nm->mkNode(BITVECTOR_ULT, t, lshr); + } + else + { + /* x >> s <= t + * with invertibility condition: + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else + { + if (pol) + { + /* s >> x > t + * with invertibility condition (synthesized): + * (bvult t s) */ + scl = nm->mkNode(BITVECTOR_ULT, t, s); + } + else + { + /* s >> x <= t + * with invertibility condition: + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + } + else if (litk == BITVECTOR_SLT) + { + if (idx == 0) + { + if (pol) + { + /* x >> s < t + * with invertibility condition (synthesized): + * (bvslt (bvlshr (bvnot (bvneg t)) s) t) */ + Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t)); + Node lshr = nm->mkNode(BITVECTOR_LSHR, nnt, s); + scl = nm->mkNode(BITVECTOR_SLT, lshr, t); + } + else + { + /* x >> s >= t + * with invertibility condition: + * (=> (not (= s z)) (bvsge (bvlshr ones s) t)) + * where + * z = 0 with getSize(z) = w + * and ones = ~0 with getSize(ones) = w */ + Node ones = bv::utils::mkOnes(w); + Node lshr = nm->mkNode(BITVECTOR_LSHR, ones, s); + Node nz = s.eqNode(z).notNode(); + scl = nz.impNode(nm->mkNode(BITVECTOR_SGE, lshr, t)); + } + } + else + { + if (pol) + { + /* s >> x < t + * with invertibility condition (synthesized): + * (or (bvslt s t) (bvslt z t)) + * where + * z = 0 with getSize(z) = w */ + Node st = nm->mkNode(BITVECTOR_SLT, s, t); + Node zt = nm->mkNode(BITVECTOR_SLT, z, t); + scl = st.orNode(zt); + } + else + { + /* s >> x >= t + * with invertibility condition: + * (and + * (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t)) + * (=> (bvsge s z) (bvsge s t))) + * where + * z = 0 with getSize(z) = w */ + Node one = bv::utils::mkConst(w, 1); + Node sz = nm->mkNode(BITVECTOR_SLT, s, z); + Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one); + Node sge1 = nm->mkNode(BITVECTOR_SGE, lshr, t); + Node sge2 = nm->mkNode(BITVECTOR_SGE, s, t); + scl = sz.impNode(sge1).andNode(sz.notNode().impNode(sge2)); + } + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (idx == 0) + { + if (pol) + { + /* x >> s > t + * with invertibility condition (synthesized): + * (bvslt t (bvlshr (bvshl max s) s)) + * where + * max is the signed maximum value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node shl = nm->mkNode(BITVECTOR_SHL, max, s); + Node lshr = nm->mkNode(BITVECTOR_LSHR, shl, s); + scl = nm->mkNode(BITVECTOR_SLT, t, lshr); + } + else + { + /* x >> s <= t + * with invertibility condition (synthesized): + * (bvsge t (bvlshr t s)) */ + scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_LSHR, t, s)); + } + } + else + { + if (pol) + { + /* s >> x > t + * with invertibility condition: + * (and + * (=> (bvslt s z) (bvsgt (bvlshr s one) t)) + * (=> (bvsge s z) (bvsgt s t))) + * where + * z = 0 and getSize(z) = w */ + Node one = bv::utils::mkOne(w); + Node sz = nm->mkNode(BITVECTOR_SLT, s, z); + Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one); + Node sgt1 = nm->mkNode(BITVECTOR_SGT, lshr, t); + Node sgt2 = nm->mkNode(BITVECTOR_SGT, s, t); + scl = sz.impNode(sgt1).andNode(sz.notNode().impNode(sgt2)); + } + else + { + /* s >> x <= t + * with invertibility condition (synthesized): + * (or (bvult t min) (bvsge t s)) + * where + * min is the minimum signed value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node ult = nm->mkNode(BITVECTOR_ULT, t, min); + Node sge = nm->mkNode(BITVECTOR_SGE, t, s); + scl = ult.orNode(sge); + } + } + } + Node scr = + nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvAshr( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) +{ + Assert(k == BITVECTOR_ASHR); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + Node scl; + unsigned w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + Node z = bv::utils::mkZero(w); + Node n = bv::utils::mkOnes(w); + + if (litk == EQUAL) + { + if (idx == 0) + { + if (pol) + { + /* x >> s = t + * with invertibility condition: + * (and + * (=> (bvult s w) (= (bvashr (bvshl t s) s) t)) + * (=> (bvuge s w) (or (= t ones) (= t z))) + * ) + * where + * z = 0 with getSize(z) = w + * and ones = ~0 with getSize(ones) = w + * and w = getSize(t) = getSize(s) */ + Node ww = bv::utils::mkConst(w, w); + Node shl = nm->mkNode(BITVECTOR_SHL, t, s); + Node ashr = nm->mkNode(BITVECTOR_ASHR, shl, s); + Node ult = nm->mkNode(BITVECTOR_ULT, s, ww); + Node imp1 = ult.impNode(ashr.eqNode(t)); + Node to = t.eqNode(n); + Node tz = t.eqNode(z); + Node imp2 = ult.notNode().impNode(to.orNode(tz)); + scl = imp1.andNode(imp2); + } + else + { + /* x >> s != t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else + { + if (pol) + { + /* s >> x = t + * with invertibility condition: + * (or (= (bvashr s i) t) ...) + * for i in 0..w */ + scl = defaultShiftIC(EQUAL, BITVECTOR_ASHR, s, t); + } + else + { + /* s >> x != t + * with invertibility condition: + * (and + * (or (not (= t z)) (not (= s z))) + * (or (not (= t ones)) (not (= s ones)))) + * where + * z = 0 with getSize(z) = w + * and ones = ~0 with getSize(ones) = w */ + scl = nm->mkNode( + AND, + nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()), + nm->mkNode(OR, t.eqNode(n).notNode(), s.eqNode(n).notNode())); + } + } + } + else if (litk == BITVECTOR_ULT) + { + if (idx == 0) + { + if (pol) + { + /* x >> s < t + * with invertibility condition (synthesized): + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + scl = t.eqNode(z).notNode(); + } + else + { + /* x >> s >= t + * with invertibility condition (synthesized): + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else + { + if (pol) + { + /* s >> x < t + * with invertibility condition (synthesized): + * (and (not (and (bvuge s t) (bvslt s z))) (not (= t z))) + * where + * z = 0 with getSize(z) = w */ + Node st = nm->mkNode(BITVECTOR_UGE, s, t); + Node sz = nm->mkNode(BITVECTOR_SLT, s, z); + Node tz = t.eqNode(z).notNode(); + scl = st.andNode(sz).notNode().andNode(tz); + } + else + { + /* s >> x >= t + * with invertibility condition (synthesized): + * (not (and (bvult s (bvnot s)) (bvult s t))) */ + Node ss = nm->mkNode(BITVECTOR_ULT, s, nm->mkNode(BITVECTOR_NOT, s)); + Node st = nm->mkNode(BITVECTOR_ULT, s, t); + scl = ss.andNode(st).notNode(); + } + } + } + else if (litk == BITVECTOR_UGT) + { + if (idx == 0) + { + if (pol) + { + /* x >> s > t + * with invertibility condition (synthesized): + * (bvult t ones) + * where + * ones = ~0 with getSize(ones) = w */ + scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w)); + } + else + { + /* x >> s <= t + * with invertibility condition (synthesized): + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else + { + if (pol) + { + /* s >> x > t + * with invertibility condition (synthesized): + * (or (bvslt s (bvlshr s (bvnot t))) (bvult t s)) */ + Node lshr = nm->mkNode(BITVECTOR_LSHR, s, nm->mkNode(BITVECTOR_NOT, t)); + Node ts = nm->mkNode(BITVECTOR_ULT, t, s); + Node slt = nm->mkNode(BITVECTOR_SLT, s, lshr); + scl = slt.orNode(ts); + } + else + { + /* s >> x <= t + * with invertibility condition (synthesized): + * (or (bvult s min) (bvuge t s)) + * where + * min is the minimum signed value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node ult = nm->mkNode(BITVECTOR_ULT, s, min); + Node uge = nm->mkNode(BITVECTOR_UGE, t, s); + scl = ult.orNode(uge); + } + } + } + else if (litk == BITVECTOR_SLT) + { + if (idx == 0) + { + if (pol) + { + /* x >> s < t + * with invertibility condition: + * (bvslt (bvashr min s) t) + * where + * min is the minimum signed value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_ASHR, min, s), t); + } + else + { + /* x >> s >= t + * with invertibility condition: + * (bvsge (bvlshr max s) t) + * where + * max is the signed maximum value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + scl = nm->mkNode(BITVECTOR_SGE, nm->mkNode(BITVECTOR_LSHR, max, s), t); + } + } + else + { + if (pol) + { + /* s >> x < t + * with invertibility condition (synthesized): + * (or (bvslt s t) (bvslt z t)) + * where + * z = 0 and getSize(z) = w */ + Node st = nm->mkNode(BITVECTOR_SLT, s, t); + Node zt = nm->mkNode(BITVECTOR_SLT, z, t); + scl = st.orNode(zt); + } + else + { + /* s >> x >= t + * with invertibility condition (synthesized): + * (not (and (bvult t (bvnot t)) (bvslt s t))) */ + Node tt = nm->mkNode(BITVECTOR_ULT, t, nm->mkNode(BITVECTOR_NOT, t)); + Node st = nm->mkNode(BITVECTOR_SLT, s, t); + scl = tt.andNode(st).notNode(); + } + } + } + else + { + Assert(litk == BITVECTOR_SGT); + Node max = bv::utils::mkMaxSigned(w); + if (idx == 0) + { + Node lshr = nm->mkNode(BITVECTOR_LSHR, max, s); + if (pol) + { + /* x >> s > t + * with invertibility condition (synthesized): + * (bvslt t (bvlshr max s))) + * where + * max is the signed maximum value with getSize(max) = w */ + scl = nm->mkNode(BITVECTOR_SLT, t, lshr); + } + else + { + /* x >> s <= t + * with invertibility condition (synthesized): + * (bvsge t (bvnot (bvlshr max s))) + * where + * max is the signed maximum value with getSize(max) = w */ + scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, lshr)); + } + } + else + { + if (pol) + { + /* s >> x > t + * with invertibility condition (synthesized): + * (and (bvslt t (bvand s max)) (bvslt t (bvor s max))) + * where + * max is the signed maximum value with getSize(max) = w */ + Node sam = nm->mkNode(BITVECTOR_AND, s, max); + Node som = nm->mkNode(BITVECTOR_OR, s, max); + Node slta = nm->mkNode(BITVECTOR_SLT, t, sam); + Node slto = nm->mkNode(BITVECTOR_SLT, t, som); + scl = slta.andNode(slto); + } + else + { + /* s >> x <= t + * with invertibility condition (synthesized): + * (or (bvsge t z) (bvsge t s)) + * where + * z = 0 and getSize(z) = w */ + Node tz = nm->mkNode(BITVECTOR_SGE, t, z); + Node ts = nm->mkNode(BITVECTOR_SGE, t, s); + scl = tz.orNode(ts); + } + } + } + Node scr = + nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvShl( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t) +{ + Assert(k == BITVECTOR_SHL); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + Node scl; + unsigned w = bv::utils::getSize(s); + Assert(w == bv::utils::getSize(t)); + Node z = bv::utils::mkZero(w); + + if (litk == EQUAL) + { + if (idx == 0) + { + Node ww = bv::utils::mkConst(w, w); + + if (pol) + { + /* x << s = t + * with invertibility condition (synthesized): + * (= (bvshl (bvlshr t s) s) t) */ + Node lshr = nm->mkNode(BITVECTOR_LSHR, t, s); + Node shl = nm->mkNode(BITVECTOR_SHL, lshr, s); + scl = shl.eqNode(t); + } + else + { + /* x << s != t + * with invertibility condition: + * (or (distinct t z) (bvult s w)) + * with + * w = getSize(s) = getSize(t) + * and z = 0 with getSize(z) = w */ + scl = nm->mkNode( + OR, t.eqNode(z).notNode(), nm->mkNode(BITVECTOR_ULT, s, ww)); + } + } + else + { + if (pol) + { + /* s << x = t + * with invertibility condition: + * (or (= (bvshl s i) t) ...) + * for i in 0..w */ + scl = defaultShiftIC(EQUAL, BITVECTOR_SHL, s, t); + } + else + { + /* s << x != t + * with invertibility condition: + * (or (distinct s z) (distinct t z)) + * where + * z = 0 with getSize(z) = w */ + scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); + } + } + } + else if (litk == BITVECTOR_ULT) + { + if (idx == 0) + { + if (pol) + { + /* x << s < t + * with invertibility condition (synthesized): + * (not (= t z)) */ + scl = t.eqNode(z).notNode(); + } + else + { + /* x << s >= t + * with invertibility condition (synthesized): + * (bvuge (bvshl ones s) t) */ + Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s); + scl = nm->mkNode(BITVECTOR_UGE, shl, t); + } + } + else + { + if (pol) + { + /* s << x < t + * with invertibility condition (synthesized): + * (not (= t z)) */ + scl = t.eqNode(z).notNode(); + } + else + { + /* s << x >= t + * with invertibility condition: + * (or (bvuge (bvshl s i) t) ...) + * for i in 0..w */ + scl = defaultShiftIC(BITVECTOR_UGE, BITVECTOR_SHL, s, t); + } + } + } + else if (litk == BITVECTOR_UGT) + { + if (idx == 0) + { + if (pol) + { + /* x << s > t + * with invertibility condition (synthesized): + * (bvult t (bvshl ones s)) + * where + * ones = ~0 with getSize(ones) = w */ + Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s); + scl = nm->mkNode(BITVECTOR_ULT, t, shl); + } + else + { + /* x << s <= t + * with invertibility condition: + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else + { + if (pol) + { + /* s << x > t + * with invertibility condition: + * (or (bvugt (bvshl s i) t) ...) + * for i in 0..w */ + scl = defaultShiftIC(BITVECTOR_UGT, BITVECTOR_SHL, s, t); + } + else + { + /* s << x <= t + * with invertibility condition: + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + } + else if (litk == BITVECTOR_SLT) + { + if (idx == 0) + { + if (pol) + { + /* x << s < t + * with invertibility condition (synthesized): + * (bvslt (bvshl (bvlshr min s) s) t) + * where + * min is the signed minimum value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node lshr = nm->mkNode(BITVECTOR_LSHR, min, s); + Node shl = nm->mkNode(BITVECTOR_SHL, lshr, s); + scl = nm->mkNode(BITVECTOR_SLT, shl, t); + } + else + { + /* x << s >= t + * with invertibility condition (synthesized): + * (bvsge (bvand (bvshl max s) max) t) + * where + * max is the signed maximum value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node shl = nm->mkNode(BITVECTOR_SHL, max, s); + scl = nm->mkNode(BITVECTOR_SGE, nm->mkNode(BITVECTOR_AND, shl, max), t); + } + } + else + { + if (pol) + { + /* s << x < t + * with invertibility condition (synthesized): + * (bvult (bvshl min s) (bvadd t min)) + * where + * min is the signed minimum value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node shl = nm->mkNode(BITVECTOR_SHL, min, s); + Node add = nm->mkNode(BITVECTOR_PLUS, t, min); + scl = nm->mkNode(BITVECTOR_ULT, shl, add); + } + else + { + /* s << x >= t + * with invertibility condition: + * (or (bvsge (bvshl s i) t) ...) + * for i in 0..w */ + scl = defaultShiftIC(BITVECTOR_SGE, BITVECTOR_SHL, s, t); + } + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (idx == 0) + { + if (pol) + { + /* x << s > t + * with invertibility condition (synthesized): + * (bvslt t (bvand (bvshl max s) max)) + * where + * max is the signed maximum value with getSize(max) = w */ + Node max = bv::utils::mkMaxSigned(w); + Node shl = nm->mkNode(BITVECTOR_SHL, max, s); + scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(BITVECTOR_AND, shl, max)); + } + else + { + /* x << s <= t + * with invertibility condition (synthesized): + * (bvult (bvlshr t (bvlshr t s)) min) + * where + * min is the signed minimum value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + Node ts = nm->mkNode(BITVECTOR_LSHR, t, s); + scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, ts), min); + } + } + else + { + if (pol) + { + /* s << x > t + * with invertibility condition: + * (or (bvsgt (bvshl s i) t) ...) + * for i in 0..w */ + scl = defaultShiftIC(BITVECTOR_SGT, BITVECTOR_SHL, s, t); + } + else + { + /* s << x <= t + * with invertibility condition (synthesized): + * (bvult (bvlshr t s) min) + * where + * min is the signed minimum value with getSize(min) = w */ + Node min = bv::utils::mkMinSigned(w); + scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, s), min); + } + } + } + Node scr = + nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvConcat(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t) +{ + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + Kind k = sv_t.getKind(); + Assert(k == BITVECTOR_CONCAT); + NodeManager* nm = NodeManager::currentNM(); + unsigned nchildren = sv_t.getNumChildren(); + unsigned w1 = 0, w2 = 0; + unsigned w = bv::utils::getSize(t), wx = bv::utils::getSize(x); + NodeBuilder<> nbs1(BITVECTOR_CONCAT), nbs2(BITVECTOR_CONCAT); + Node s1, s2; + Node t1, t2, tx; + Node scl, scr; + + if (idx != 0) + { + if (idx == 1) + { + s1 = sv_t[0]; + } + else + { + for (unsigned i = 0; i < idx; ++i) + { + nbs1 << sv_t[i]; + } + s1 = nbs1.constructNode(); + } + w1 = bv::utils::getSize(s1); + t1 = bv::utils::mkExtract(t, w - 1, w - w1); + } + + tx = bv::utils::mkExtract(t, w - w1 - 1, w - w1 - wx); + + if (idx != nchildren - 1) + { + if (idx == nchildren - 2) + { + s2 = sv_t[nchildren - 1]; + } + else + { + for (unsigned i = idx + 1; i < nchildren; ++i) + { + nbs2 << sv_t[i]; + } + s2 = nbs2.constructNode(); + } + w2 = bv::utils::getSize(s2); + Assert(w2 == w - w1 - wx); + t2 = bv::utils::mkExtract(t, w2 - 1, 0); + } + + Assert(!s1.isNull() || t1.isNull()); + Assert(!s2.isNull() || t2.isNull()); + Assert(!s1.isNull() || !s2.isNull()); + Assert(s1.isNull() || w1 == bv::utils::getSize(t1)); + Assert(s2.isNull() || w2 == bv::utils::getSize(t2)); + + if (litk == EQUAL) + { + if (s1.isNull()) + { + if (pol) + { + /* x o s2 = t (interpret t as tx o t2) + * with invertibility condition: + * (= s2 t2) */ + scl = s2.eqNode(t2); + } + else + { + /* x o s2 != t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else if (s2.isNull()) + { + if (pol) + { + /* s1 o x = t (interpret t as t1 o tx) + * with invertibility condition: + * (= s1 t1) */ + scl = s1.eqNode(t1); + } + else + { + /* s1 o x != t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else + { + if (pol) + { + /* s1 o x o s2 = t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and (= s1 t1) (= s2 t2)) */ + scl = nm->mkNode(AND, s1.eqNode(t1), s2.eqNode(t2)); + } + else + { + /* s1 o x o s2 != t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + } + else if (litk == BITVECTOR_ULT) + { + if (s1.isNull()) + { + if (pol) + { + /* x o s2 < t (interpret t as tx o t2) + * with invertibility condition: + * (=> (= tx z) (bvult s2 t2)) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node ult = nm->mkNode(BITVECTOR_ULT, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(z), ult); + } + else + { + /* x o s2 >= t (interpret t as tx o t2) + * (=> (= tx ones) (bvuge s2 t2)) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node uge = nm->mkNode(BITVECTOR_UGE, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(n), uge); + } + } + else if (s2.isNull()) + { + if (pol) + { + /* s1 o x < t (interpret t as t1 o tx) + * with invertibility condition: + * (and (bvule s1 t1) (=> (= s1 t1) (distinct tx z))) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1); + Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode()); + scl = nm->mkNode(AND, ule, imp); + } + else + { + /* s1 o x >= t (interpret t as t1 o tx) + * with invertibility condition: + * (bvuge s1 t1) */ + scl = nm->mkNode(BITVECTOR_UGE, s1, t1); + } + } + else + { + if (pol) + { + /* s1 o x o s2 < t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvule s1 t1) + * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2))) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULT, s2, t2)); + scl = nm->mkNode(AND, ule, imp); + } + else + { + /* s1 o x o s2 >= t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvuge s1 t1) + * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2))) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGE, s2, t2)); + scl = nm->mkNode(AND, uge, imp); + } + } + } + else if (litk == BITVECTOR_UGT) + { + if (s1.isNull()) + { + if (pol) + { + /* x o s2 > t (interpret t as tx o t2) + * with invertibility condition: + * (=> (= tx ones) (bvugt s2 t2)) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node ugt = nm->mkNode(BITVECTOR_UGT, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(n), ugt); + } + else + { + /* x o s2 <= t (interpret t as tx o t2) + * with invertibility condition: + * (=> (= tx z) (bvule s2 t2)) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node ule = nm->mkNode(BITVECTOR_ULE, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(z), ule); + } + } + else if (s2.isNull()) + { + if (pol) + { + /* s1 o x > t (interpret t as t1 o tx) + * with invertibility condition: + * (and (bvuge s1 t1) (=> (= s1 t1) (distinct tx ones))) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1); + Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode()); + scl = nm->mkNode(AND, uge, imp); + } + else + { + /* s1 o x <= t (interpret t as t1 o tx) + * with invertibility condition: + * (bvule s1 t1) */ + scl = nm->mkNode(BITVECTOR_ULE, s1, t1); + } + } + else + { + if (pol) + { + /* s1 o x o s2 > t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvuge s1 t1) + * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2))) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node uge = nm->mkNode(BITVECTOR_UGE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGT, s2, t2)); + scl = nm->mkNode(AND, uge, imp); + } + else + { + /* s1 o x o s2 <= t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvule s1 t1) + * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2))) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node ule = nm->mkNode(BITVECTOR_ULE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULE, s2, t2)); + scl = nm->mkNode(AND, ule, imp); + } + } + } + else if (litk == BITVECTOR_SLT) + { + if (s1.isNull()) + { + if (pol) + { + /* x o s2 < t (interpret t as tx o t2) + * with invertibility condition: + * (=> (= tx min) (bvult s2 t2)) + * where + * min is the signed minimum value with getSize(min) = wx */ + Node min = bv::utils::mkMinSigned(wx); + Node ult = nm->mkNode(BITVECTOR_ULT, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(min), ult); + } + else + { + /* x o s2 >= t (interpret t as tx o t2) + * (=> (= tx max) (bvuge s2 t2)) + * where + * max is the signed maximum value with getSize(max) = wx */ + Node max = bv::utils::mkMaxSigned(wx); + Node uge = nm->mkNode(BITVECTOR_UGE, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(max), uge); + } + } + else if (s2.isNull()) + { + if (pol) + { + /* s1 o x < t (interpret t as t1 o tx) + * with invertibility condition: + * (and (bvsle s1 t1) (=> (= s1 t1) (distinct tx z))) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1); + Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(z).notNode()); + scl = nm->mkNode(AND, sle, imp); + } + else + { + /* s1 o x >= t (interpret t as t1 o tx) + * with invertibility condition: + * (bvsge s1 t1) */ + scl = nm->mkNode(BITVECTOR_SGE, s1, t1); + } + } + else + { + if (pol) + { + /* s1 o x o s2 < t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvsle s1 t1) + * (=> (and (= s1 t1) (= tx z)) (bvult s2 t2))) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULT, s2, t2)); + scl = nm->mkNode(AND, sle, imp); + } + else + { + /* s1 o x o s2 >= t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvsge s1 t1) + * (=> (and (= s1 t1) (= tx ones)) (bvuge s2 t2))) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGE, s2, t2)); + scl = nm->mkNode(AND, sge, imp); + } + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (s1.isNull()) + { + if (pol) + { + /* x o s2 > t (interpret t as tx o t2) + * with invertibility condition: + * (=> (= tx max) (bvugt s2 t2)) + * where + * max is the signed maximum value with getSize(max) = wx */ + Node max = bv::utils::mkMaxSigned(wx); + Node ugt = nm->mkNode(BITVECTOR_UGT, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(max), ugt); + } + else + { + /* x o s2 <= t (interpret t as tx o t2) + * with invertibility condition: + * (=> (= tx min) (bvule s2 t2)) + * where + * min is the signed minimum value with getSize(min) = wx */ + Node min = bv::utils::mkMinSigned(wx); + Node ule = nm->mkNode(BITVECTOR_ULE, s2, t2); + scl = nm->mkNode(IMPLIES, tx.eqNode(min), ule); + } + } + else if (s2.isNull()) + { + if (pol) + { + /* s1 o x > t (interpret t as t1 o tx) + * with invertibility condition: + * (and (bvsge s1 t1) (=> (= s1 t1) (distinct tx ones))) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1); + Node imp = nm->mkNode(IMPLIES, s1.eqNode(t1), tx.eqNode(n).notNode()); + scl = nm->mkNode(AND, sge, imp); + } + else + { + /* s1 o x <= t (interpret t as t1 o tx) + * with invertibility condition: + * (bvsle s1 t1) */ + scl = nm->mkNode(BITVECTOR_SLE, s1, t1); + } + } + else + { + if (pol) + { + /* s1 o x o s2 > t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvsge s1 t1) + * (=> (and (= s1 t1) (= tx ones)) (bvugt s2 t2))) + * where + * ones = ~0 with getSize(ones) = wx */ + Node n = bv::utils::mkOnes(wx); + Node sge = nm->mkNode(BITVECTOR_SGE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(n)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_UGT, s2, t2)); + scl = nm->mkNode(AND, sge, imp); + } + else + { + /* s1 o x o s2 <= t (interpret t as t1 o tx o t2) + * with invertibility condition: + * (and + * (bvsle s1 t1) + * (=> (and (= s1 t1) (= tx z)) (bvule s2 t2))) + * where + * z = 0 with getSize(z) = wx */ + Node z = bv::utils::mkZero(wx); + Node sle = nm->mkNode(BITVECTOR_SLE, s1, t1); + Node a = nm->mkNode(AND, s1.eqNode(t1), tx.eqNode(z)); + Node imp = nm->mkNode(IMPLIES, a, nm->mkNode(BITVECTOR_ULE, s2, t2)); + scl = nm->mkNode(AND, sle, imp); + } + } + } + scr = s1.isNull() ? x : bv::utils::mkConcat(s1, x); + if (!s2.isNull()) scr = bv::utils::mkConcat(scr, s2); + scr = nm->mkNode(litk, scr, t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << ic << std::endl; + return ic; +} + +Node getICBvSext(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t) +{ + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); + + NodeManager* nm = NodeManager::currentNM(); + Node scl; + Assert(idx == 0); + (void)idx; + unsigned ws = bv::utils::getSignExtendAmount(sv_t); + unsigned w = bv::utils::getSize(t); + + if (litk == EQUAL) + { + if (pol) + { + /* x sext ws = t + * with invertibility condition: + * (or (= ((_ extract u l) t) z) + * (= ((_ extract u l) t) ones)) + * where + * u = w - 1 + * l = w - 1 - ws + * z = 0 with getSize(z) = ws + 1 + * ones = ~0 with getSize(ones) = ws + 1 */ + Node ext = bv::utils::mkExtract(t, w - 1, w - 1 - ws); + Node z = bv::utils::mkZero(ws + 1); + Node n = bv::utils::mkOnes(ws + 1); + scl = nm->mkNode(OR, ext.eqNode(z), ext.eqNode(n)); + } + else + { + /* x sext ws != t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else if (litk == BITVECTOR_ULT) + { + if (pol) + { + /* x sext ws < t + * with invertibility condition: + * (distinct t z) + * where + * z = 0 with getSize(z) = w */ + Node z = bv::utils::mkZero(w); + scl = t.eqNode(z).notNode(); + } + else + { + /* x sext ws >= t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else if (litk == BITVECTOR_UGT) + { + if (pol) + { + /* x sext ws > t + * with invertibility condition: + * (distinct t ones) + * where + * ones = ~0 with getSize(ones) = w */ + Node n = bv::utils::mkOnes(w); + scl = t.eqNode(n).notNode(); + } + else + { + /* x sext ws <= t + * true (no invertibility condition) */ + scl = nm->mkConst<bool>(true); + } + } + else if (litk == BITVECTOR_SLT) + { + if (pol) + { + /* x sext ws < t + * with invertibility condition: + * (bvslt ((_ sign_extend ws) min) t) + * where + * min is the signed minimum value with getSize(min) = w - ws */ + Node min = bv::utils::mkMinSigned(w - ws); + Node ext = bv::utils::mkSignExtend(min, ws); + scl = nm->mkNode(BITVECTOR_SLT, ext, t); + } + else + { + /* x sext ws >= t + * with invertibility condition (combination of sgt and eq): + * + * (or + * (or (= ((_ extract u l) t) z) ; eq + * (= ((_ extract u l) t) ones)) + * (bvslt t ((_ zero_extend ws) max))) ; sgt + * where + * u = w - 1 + * l = w - 1 - ws + * z = 0 with getSize(z) = ws + 1 + * ones = ~0 with getSize(ones) = ws + 1 + * max is the signed maximum value with getSize(max) = w - ws */ + Node ext1 = bv::utils::mkExtract(t, w - 1, w - 1 - ws); + Node z = bv::utils::mkZero(ws + 1); + Node n = bv::utils::mkOnes(ws + 1); + Node o1 = nm->mkNode(OR, ext1.eqNode(z), ext1.eqNode(n)); + Node max = bv::utils::mkMaxSigned(w - ws); + Node ext2 = bv::utils::mkConcat(bv::utils::mkZero(ws), max); + Node o2 = nm->mkNode(BITVECTOR_SLT, t, ext2); + scl = nm->mkNode(OR, o1, o2); + } + } + else + { + Assert(litk == BITVECTOR_SGT); + if (pol) + { + /* x sext ws > t + * with invertibility condition: + * (bvslt t ((_ zero_extend ws) max)) + * where + * max is the signed maximum value with getSize(max) = w - ws */ + Node max = bv::utils::mkMaxSigned(w - ws); + Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max); + scl = nm->mkNode(BITVECTOR_SLT, t, ext); + } + else + { + /* x sext ws <= t + * with invertibility condition: + * (bvsge t (bvnot ((_ zero_extend ws) max))) + * where + * max is the signed maximum value with getSize(max) = w - ws */ + Node max = bv::utils::mkMaxSigned(w - ws); + Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max); + scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, ext)); + } + } + Node scr = nm->mkNode(litk, bv::utils::mkSignExtend(x, ws), t); + Node ic = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); + Trace("bv-invert") << "Add SC_" << BITVECTOR_SIGN_EXTEND << "(" << x + << "): " << ic << std::endl; + return ic; +} + +} // namespace utils +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h new file mode 100644 index 000000000..0fec00579 --- /dev/null +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file bv_inverter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief inverse rules for bit-vector operators + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BV_INVERTER_UTILS_H +#define __CVC4__BV_INVERTER_UTILS_H + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace utils { + +/* Get invertibility condition for BITVECTOR_ULT and BITVECTOR_UGT. */ +Node getICBvUltUgt(bool pol, Kind k, Node x, Node t); + +/* Get invertibility condition for BITVECTOR_SLT and BITVECTOR_SGT. */ +Node getICBvSltSgt(bool pol, Kind k, Node x, Node t); + +/* Get invertibility condition for BITVECTOR_MUL. */ +Node getICBvMult( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t); + +/* Get invertibility condition for BITVECTOR_UREM. */ +Node getICBvUrem( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t); + +/* Get invertibility condition for BITVECTOR_UDIV. */ +Node getICBvUdiv( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t); + +/* Get invertibility condition for BITVECTOR_AND and BITVECTOR_OR. */ +Node getICBvAndOr( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t); + +/* Get invertibility condition for BITVECTOR_LSHR. */ +Node getICBvLshr( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t); + +/* Get invertibility condition for BITVECTOR_ASHR. */ +Node getICBvAshr( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t); + +/* Get invertibility condition for BITVECTOR_SHL. */ +Node getICBvShl( + bool pol, Kind litk, Kind k, unsigned idx, Node x, Node s, Node t); + +/* Get invertibility condition for BITVECTOR_CONCAT. */ +Node getICBvConcat( + bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t); + +/* Get invertibility condition for BITVECTOR_SEXT. */ +Node getICBvSext(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t); + +} // namespace utils +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 +#endif |