From 3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 9 Oct 2017 17:06:30 -0700 Subject: [PATCH] CBQI BV: Add inverse for more operators. (#1213) This implements side conditions and the instantiation via word-level inversion for operators BITVECTOR_AND, BITVECTOR_OR, BITVECTOR_UREM (Index=1), BITVECTOR_LSHR (index=0). --- src/theory/quantifiers/bv_inverter.cpp | 196 ++++++++++++++---- .../quantifiers/qbv-test-invert-bvand.smt2 | 9 + .../quantifiers/qbv-test-invert-bvlshr-0.smt2 | 9 + .../quantifiers/qbv-test-invert-bvor.smt2 | 9 + .../quantifiers/qbv-test-invert-bvult-0.smt2 | 8 + .../quantifiers/qbv-test-invert-bvult-1.smt2 | 8 + .../quantifiers/qbv-test-invert-bvurem-1.smt2 | 9 + .../quantifiers/qbv-test-invert-mul.smt2 | 1 - 8 files changed, 206 insertions(+), 43 deletions(-) create mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 create mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 create mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 create mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 create mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 create mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 5152b2917..169b16f63 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -18,11 +18,28 @@ #include #include "theory/quantifiers/term_database.h" +#include "theory/bv/theory_bv_utils.h" using namespace CVC4; using namespace CVC4::kind; +using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; +/* Drop child at given index from expression. + * E.g., dropChild((x + y + z), 1) -> (x + z) */ +static Node dropChild(Node n, unsigned index) { + unsigned nchildren = n.getNumChildren(); + Assert(index < nchildren); + Kind k = n.getKind(); + Assert(k == AND || k == OR || k == BITVECTOR_MULT || k == BITVECTOR_PLUS); + NodeBuilder<> nb(NodeManager::currentNM(), k); + for (unsigned i = 0; i < nchildren; ++i) { + if (i == index) continue; + nb << n[i]; + } + return nb.constructNode(); +} + Node BvInverter::getSolveVariable(TypeNode tn) { std::map::iterator its = d_solve_var.find(tn); if (its == d_solve_var.end()) { @@ -245,55 +262,150 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, NodeManager* nm = NodeManager::currentNM(); while (!path.empty()) { unsigned index = path.back(); - Assert(sv_t.getNumChildren() <= 2); Assert(index < sv_t.getNumChildren()); path.pop_back(); Kind k = sv_t.getKind(); - // inversions - if (k == BITVECTOR_PLUS) { - t = nm->mkNode(BITVECTOR_SUB, t, sv_t[1 - index]); - } else if (k == BITVECTOR_SUB) { - t = nm->mkNode(BITVECTOR_PLUS, t, sv_t[1 - index]); - } else if (k == BITVECTOR_MULT) { - // t = skv (fresh skolem constant) - TypeNode solve_tn = sv_t[index].getType(); - Node x = getSolveVariable(solve_tn); - // with side condition: - // ctz(t) >= ctz(s) <-> x * s = t - // where - // ctz(t) >= ctz(s) -> (t & -t) >= (s & -s) - Node s = sv_t[1 - index]; - // left hand side of side condition - Node scl = nm->mkNode( - BITVECTOR_UGE, - nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)), - nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s))); - // right hand side of side condition - Node scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_MULT, x, s), 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_NEG || k == BITVECTOR_NOT) { - t = NodeManager::currentNM()->mkNode(k, t); - //}else if( k==BITVECTOR_AND || k==BITVECTOR_OR ){ + /* inversions */ + if (k == BITVECTOR_CONCAT) { // TODO - //}else if( k==BITVECTOR_CONCAT ){ - // TODO - //}else if( k==BITVECTOR_SHL || k==BITVECTOR_LSHR ){ - // TODO - //}else if( k==BITVECTOR_ASHR ){ - // TODO - } else { - Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " << k + Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " + << k << ", from " << sv_t << std::endl; return Node::null(); + } else { + Node s = sv_t.getNumChildren() == 2 + ? sv_t[1 - index] + : dropChild(sv_t, index); + /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS) + * are commutative (no case split based on index). */ + if (k == BITVECTOR_PLUS) { + t = nm->mkNode(BITVECTOR_SUB, t, s); + } else if (k == BITVECTOR_SUB) { + t = nm->mkNode(BITVECTOR_PLUS, t, s); + } else if (k == BITVECTOR_MULT) { + /* t = skv (fresh skolem constant) + * with side condition: + * ctz(t) >= ctz(s) <-> x * s = t + * where + * ctz(t) >= ctz(s) -> (t & -t) >= (s & -s) */ + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable(solve_tn); + /* left hand side of side condition */ + Node scl = nm->mkNode( + BITVECTOR_UGE, + nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)), + nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s))); + /* right hand side of side condition */ + Node scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_MULT, x, s), 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_UREM_TOTAL) { + /* t = skv (fresh skolem constant) */ + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable(solve_tn); + Node scl, scr; + if (index == 0) { + /* x % s = t + * with side condition: + * TODO */ + Trace("bv-invert") << "bv-invert : Unsupported for index " << index + << ", from " << sv_t << std::endl; + return Node::null(); + } else { + /* s % x = t + * with side conditions: + * s > t + * && s-t > t + * && (t = 0 || t != s-1) */ + Node s_gt_t = nm->mkNode(BITVECTOR_UGT, s, t); + Node s_m_t = nm->mkNode(BITVECTOR_SUB, s, t); + Node smt_gt_t = nm->mkNode(BITVECTOR_UGT, s_m_t, t); + Node t_eq_z = nm->mkNode(EQUAL, + t, bv::utils::mkZero(bv::utils::getSize(t))); + Node s_m_o = nm->mkNode(BITVECTOR_SUB, + s, bv::utils::mkOne(bv::utils::getSize(s))); + Node t_d_smo = nm->mkNode(DISTINCT, t, s_m_o); + + scl = nm->mkNode(AND, + nm->mkNode(AND, s_gt_t, smt_gt_t), + nm->mkNode(OR, t_eq_z, t_d_smo)); + scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UREM_TOTAL, s, x), t); + } + Node sc = nm->mkNode(IMPLIES, scl, scr); + status.d_conds.push_back(sc); + Node skv = getInversionNode(sc, solve_tn); + t = skv; + } else if (k == BITVECTOR_AND || k == BITVECTOR_OR) { + /* t = skv (fresh skolem constant) + * with side condition: + * t & s = t + * t | s = t */ + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable(solve_tn); + Node scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s)); + Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); + Node sc = nm->mkNode(IMPLIES, scl, scr); + status.d_conds.push_back(sc); + Node skv = getInversionNode(sc, solve_tn); + t = skv; + } else if (k == BITVECTOR_LSHR) { + /* t = skv (fresh skolem constant) */ + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable(solve_tn); + Node scl, scr; + if (index == 0) { + /* x >> s = t + * with side condition: + * s = 0 || clz(t) >= s + * -> + * s = 0 || ((z o t) << s)[2w-1 : w] = z + * with w = getSize(t) = getSize(s) and z = 0 with getSize(z) = w */ + unsigned w = bv::utils::getSize(s); + Node z = bv::utils::mkZero(w); + Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t); + Node zot_shl_s = nm->mkNode(BITVECTOR_SHL, z_o_t, s); + Node ext = bv::utils::mkExtract(zot_shl_s, 2*w-1, w); + scl = nm->mkNode(OR, + nm->mkNode(EQUAL, s, z), + nm->mkNode(EQUAL, ext, z)); + scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_LSHR, x, s), t); + Node sc = nm->mkNode(IMPLIES, scl, scr); + status.d_conds.push_back(sc); + Node skv = getInversionNode(sc, solve_tn); + t = skv; + } else { + // TODO: index == 1 + /* s >> x = t + * with side conditions: + * (s = 0 && t = 0) + * || (clz(t) >= clz(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(); + } + } 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 { + Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " + << k + << ", from " << sv_t << std::endl; + return Node::null(); + } } sv_t = sv_t[index]; } diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 new file mode 100644 index 000000000..040bc33c1 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvand x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 new file mode 100644 index 000000000..2fb5d9bec --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvlshr x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 new file mode 100644 index 000000000..c83b0ca73 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 new file mode 100644 index 000000000..f54abccfd --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (bvult x a) ))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 new file mode 100644 index 000000000..a10f2fbea --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (bvult a x)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 new file mode 100644 index 000000000..6a1987c49 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 index 235d353ef..84e9fa7ce 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 @@ -4,7 +4,6 @@ (set-info :status sat) (declare-fun a () (_ BitVec 32)) (declare-fun b () (_ BitVec 32)) -(declare-fun c () (_ BitVec 32)) (assert (forall ((x (_ BitVec 32))) (not (= (bvmul x a) b)))) -- 2.30.2