diff options
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 174 | ||||
| -rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.cpp | 16 | ||||
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.h | 5 |
3 files changed, 141 insertions, 54 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 9fe645a9a..cce56ab01 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -111,7 +111,7 @@ static bool isInvertible(Kind k, unsigned index) || k == BITVECTOR_PLUS || k == BITVECTOR_SUB || k == BITVECTOR_MULT - || (k == BITVECTOR_UREM_TOTAL && index == 1) + || k == BITVECTOR_UREM_TOTAL || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND || k == BITVECTOR_OR @@ -363,11 +363,10 @@ static Node getScBvUrem(bool pol, Node t) { Assert(k == BITVECTOR_UREM_TOTAL); - Assert(litk != EQUAL || pol == false || idx == 1); - + Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT); NodeManager* nm = NodeManager::currentNM(); - Node scl, scr; + Node scl; unsigned w = bv::utils::getSize(s); Assert (w == bv::utils::getSize(t)); Node z = bv::utils::mkZero(w); @@ -376,37 +375,46 @@ static Node getScBvUrem(bool pol, { if (idx == 0) { - Assert (pol == false); - /* x % s != t - * with side condition: - * s != 1 || t != 0 */ - scl = nm->mkNode(OR, - s.eqNode(bv::utils::mkOne(w)).notNode(), - t.eqNode(z).notNode()); - scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t); + if (pol) + { + /* x % s = t + * with side condition (synthesized): + * (not (bvult (bvnot (bvneg s)) t)) + * <-> + * ~(-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 side condition: + * s != 1 || t != 0 */ + scl = nm->mkNode(OR, + s.eqNode(bv::utils::mkOne(w)).notNode(), + t.eqNode(z).notNode()); + } } else { if (pol) { /* s % x = t - * with side condition: + * with side condition (synthesized): + * (bvuge (bvand (bvsub (bvadd t t) s) s) t) + * <-> + * (t + t - s) & s >= t + * + * is equivalent to: * s = t * || * ( s > t * && s-t > t * && (t = 0 || t != s-1) ) */ - - Node a1 = nm->mkNode(BITVECTOR_UGT, s, t); - Node a2 = nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t); - Node a3 = nm->mkNode(OR, - t.eqNode(z), - t.eqNode(bv::utils::mkDec(s)).notNode()); - - scl = nm->mkNode(OR, - t.eqNode(s), - nm->mkNode(AND, a1, nm->mkNode(AND, a2, a3))); - scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t); + 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 { @@ -414,16 +422,119 @@ static Node getScBvUrem(bool pol, * with side condition: * s != 0 || t != 0 */ scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode()); - scr = nm->mkNode(DISTINCT, nm->mkNode(k, s, x), t); } } } - else + else if (litk == BITVECTOR_ULT) { - return Node::null(); + if (idx == 0) + { + if (pol) + { + /* x % s < t + * with side condition: + * (distinct t z) + * where z = 0 with getSize(z) = w */ + scl = t.eqNode(z).notNode(); + } + else + { + /* x % s >= t + * with side 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 side condition: + * (distinct t z) + * where z = 0 with getSize(z) = w */ + scl = t.eqNode(z).notNode(); + } + else + { + /* s % x < t + * with side 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 /* litk == BITVECTOR_SLT */ + { + if (idx == 0) + { + if (pol) + { + /* x % s < t + * with side 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 side condition (synthesized): + * (or (bvslt t s) (bvsge z s)) + * where z = 0 with getSize(z) = w */ + Node s1 = nm->mkNode(BITVECTOR_SLT, t, s); + Node s2 = nm->mkNode(BITVECTOR_SGE, z, s); + scl = nm->mkNode(OR, s1, s2); + } + } + else + { + if (pol) + { + /* s % x < t + * with side 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 side condition: + * (and + * (=> (= s z) (bvsle t z)) + * (=> (bvsgt 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, + s.eqNode(z), nm->mkNode(BITVECTOR_SLE, t, z)); + Node i2 = nm->mkNode(IMPLIES, + nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, s, t)); + Node i3 = 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, i3); + return Node::null(); + } + } } - Node sc = nm->mkNode(IMPLIES, scl, scr); + 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; } @@ -1141,13 +1252,6 @@ Node BvInverter::solveBvLit(Node sv, break; case BITVECTOR_UREM_TOTAL: - if (index == 0) - { - /* x % s = t is rewritten to x - x / y * y */ - Trace("bv-invert") << "bv-invert : Unsupported for index " - << index << ", from " << sv_t << std::endl; - return Node::null(); - } sc = getScBvUrem( pol, litk, k, index, getSolveVariable(solve_tn), s, t); break; diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index f0031cd54..4b326ede6 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -1761,21 +1761,7 @@ Node BvInstantiator::rewriteTermForSolvePv( // [1] rewrite cases of non-invertible operators - // if n is urem( x, y ) where x contains pv but y does not, then - // rewrite urem( x, y ) ---> x - udiv( x, y )*y - if (n.getKind() == BITVECTOR_UREM_TOTAL) - { - if (contains_pv[n[0]] && !contains_pv[n[1]]) - { - return nm->mkNode( - BITVECTOR_SUB, - children[0], - nm->mkNode(BITVECTOR_MULT, - nm->mkNode(BITVECTOR_UDIV_TOTAL, children[0], children[1]), - children[1])); - } - } - else if (n.getKind() == EQUAL) + if (n.getKind() == EQUAL) { TNode lhs = children[0]; TNode rhs = children[1]; diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index e1d950050..6f078d2e3 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -85,8 +85,6 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite || k == BITVECTOR_ASHR || k == BITVECTOR_SHL); - Assert(litk != EQUAL - || k != BITVECTOR_UREM_TOTAL || pol == false || idx == 1); Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); // TODO amend / remove the following six lines as soon as inequality @@ -219,8 +217,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite void testGetScBvUremEqTrue0() { - TS_ASSERT_THROWS(runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem), - AssertionException); + runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); } void testGetScBvUremEqTrue1() |