From: Mathias Preiner Date: Thu, 12 Oct 2017 00:58:33 +0000 (-0700) Subject: Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224) X-Git-Tag: cvc5-1.0.0~5562 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6d8cd9e46e4e3ac39f468e45b107ec4a0e5b9a2;p=cvc5.git Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224) --- diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index d209c4d73..9b84c8ecf 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -22,10 +22,11 @@ #include "theory/bv/theory_bv_utils.h" -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { /* Drop child at given index from expression. * E.g., dropChild((x + y + z), 1) -> (x + z) */ @@ -270,11 +271,22 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, /* inversions */ if (k == BITVECTOR_CONCAT) { - // TODO - Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " - << k - << ", from " << sv_t << std::endl; - return Node::null(); + /* x = t[upper:lower] + * where + * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index + * lower = getSize(sv_t[i]) for i > index + */ + unsigned upper, lower; + upper = bv::utils::getSize(t) - 1; + lower = 0; + NodeBuilder<> nb(nm, BITVECTOR_CONCAT); + for (unsigned i = 0; i < sv_t.getNumChildren(); 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 { Node s = sv_t.getNumChildren() == 2 ? sv_t[1 - index] @@ -396,10 +408,100 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, << ", from " << sv_t << std::endl; return Node::null(); } + } else if (k == BITVECTOR_UDIV_TOTAL) { + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable(solve_tn); + Node s = sv_t[1 - index]; + unsigned w = bv::utils::getSize(s); + Node scl, scr; + Node zero = bv::utils::mkConst(w, 0u); + + /* x udiv s = t */ + if (index == 0) { + /* with side conditions: + * !umulo(s * t) + */ + scl = nm->mkNode(NOT, bv::utils::mkUmulo(s, t)); + scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, x, s), t); + /* s udiv x = t */ + } else { + /* with side conditions: + * (t = 0 && (s = 0 || s != 2^w-1)) + * || s >= t + * || t = 2^w-1 + */ + Node ones = bv::utils::mkOnes(w); + Node t_eq_zero = nm->mkNode(EQUAL, t, zero); + Node s_eq_zero = nm->mkNode(EQUAL, s, zero); + Node s_ne_ones = nm->mkNode(DISTINCT, s, ones); + Node s_ge_t = nm->mkNode(BITVECTOR_UGE, s, t); + Node t_eq_ones = nm->mkNode(EQUAL, t, ones); + scl = nm->mkNode( + OR, + nm->mkNode(AND, t_eq_zero, nm->mkNode(OR, s_eq_zero, s_ne_ones)), + s_ge_t, t_eq_ones); + scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, x), t); + } + + /* overall side condition */ + Node sc = nm->mkNode(IMPLIES, scl, scr); + /* add side condition */ + status.d_conds.push_back(sc); + + /* get the skolem node for this side condition*/ + Node skv = getInversionNode(sc, solve_tn); + /* now solving with the skolem node as the RHS */ + t = skv; + } else if (k == BITVECTOR_SHL) { + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable(solve_tn); + Node s = sv_t[1 - index]; + unsigned w = bv::utils::getSize(s); + Node scl, scr; + + /* x << s = t */ + if (index == 0) { + /* with side conditions: + * (s = 0 || ctz(t) >= s) + * <-> + * (s = 0 || ((t o z) >> (z o s))[w-1:0] = z) + * + * where + * w = getSize(s) = getSize(t) = getSize (z) && z = 0 + */ + Node zero = bv::utils::mkConst(w, 0u); + Node s_eq_zero = nm->mkNode(EQUAL, s, zero); + Node t_conc_zero = nm->mkNode(BITVECTOR_CONCAT, t, zero); + Node zero_conc_s = nm->mkNode(BITVECTOR_CONCAT, zero, s); + Node shr_s = nm->mkNode(BITVECTOR_LSHR, t_conc_zero, zero_conc_s); + Node extr_shr_s = bv::utils::mkExtract(shr_s, w - 1, 0); + Node ctz_t_ge_s = nm->mkNode(EQUAL, extr_shr_s, zero); + scl = nm->mkNode(OR, s_eq_zero, ctz_t_ge_s); + scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_SHL, x, s), t); + /* s << x = t */ + } else { + /* with side conditions: + * (s = 0 && t = 0) + * || (ctz(t) >= ctz(s) + * && (t = 0 || + * "remaining shifted bits in t match corresponding bits in s")) + */ + Trace("bv-invert") << "bv-invert : Unsupported for index " << index + << ", from " << sv_t << std::endl; + return Node::null(); + } + + /* overall side condition */ + Node sc = nm->mkNode(IMPLIES, scl, scr); + /* add side condition */ + status.d_conds.push_back(sc); + + /* get the skolem node for this side condition*/ + Node skv = getInversionNode(sc, solve_tn); + /* now solving with the skolem node as the RHS */ + t = skv; } else if (k == BITVECTOR_NEG || k == BITVECTOR_NOT) { t = NodeManager::currentNM()->mkNode(k, t); - //}else if( k==BITVECTOR_CONCAT ){ - // TODO //}else if( k==BITVECTOR_ASHR ){ // TODO } else { @@ -472,3 +574,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node lit, bool pol, } return Node::null(); } + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index eb33e2c82..e045ad44c 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -92,6 +92,11 @@ TESTS = \ bug822.smt2 \ qbv-test-invert-mul.smt2 \ qbv-simple-2vars-vo.smt2 \ + qbv-test-invert-concat-0.smt2 \ + qbv-test-invert-concat-1.smt2 \ + qbv-test-invert-shl.smt2 \ + qbv-test-invert-udiv-0.smt2 \ + qbv-test-invert-udiv-1.smt2 \ qbv-test-urem-rewrite.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 new file mode 100644 index 000000000..f4e19fc52 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 64)) + +(assert (forall ((x (_ BitVec 32))) (not (= (concat x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 new file mode 100644 index 000000000..827e74605 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 64)) + +(assert (forall ((x (_ BitVec 32))) (not (= (concat a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 new file mode 100644 index 000000000..97a0662eb --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvshl x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 new file mode 100644 index 000000000..becfc5315 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 16)) +(declare-fun b () (_ BitVec 16)) + +(assert (distinct a b (_ bv0 16))) +(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 new file mode 100644 index 000000000..0373cf8f3 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 16)) +(declare-fun b () (_ BitVec 16)) + +(assert (distinct a b (_ bv0 16))) +(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv a x) b)))) + +(check-sat)