From 00e75cb0c6aedab34740b7feadb512ea3c0c7f3d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 23 Oct 2017 22:46:50 -0700 Subject: [PATCH] CBQI BV: Add ULT/SLT inverse handling. (#1268) This adds inverse handling for ULT(BV), SLT(BV) and disequalities. Rewriting of inequalities and disequalities to equalities with slack can now be disabled with an option (--cbqi-bv-inv-in-dis-eq). Function solve_bv_constraint is now merged into solve_bv_lit. --- src/options/quantifiers_options | 2 + src/smt/smt_engine.cpp | 8 + src/theory/quantifiers/bv_inverter.cpp | 283 ++++++++++++------ src/theory/quantifiers/bv_inverter.h | 10 +- src/theory/quantifiers/ceg_t_instantiator.cpp | 6 +- .../qbv-test-invert-disequality.smt2 | 10 + 6 files changed, 216 insertions(+), 103 deletions(-) create mode 100644 test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index d3f8c9f6a..05c2512cd 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -339,6 +339,8 @@ option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :defaul interleave model value instantiation with word-level inversion approach option cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true use model slack values when solving inequalities with word-level inversion approach +option cbqiBvInvInDisEq --cbqi-bv-inv-in-dis-eq bool :read-write :default false + let bv inverter handle (un)signed less than nodes ### local theory extensions options diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e32d8913d..68fda324e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1419,7 +1419,15 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl; setOption("repeat-simp", false); } + } + if (options::cbqiBv()) { + if(options::boolToBitvector.wasSetByUser()) { + throw OptionException("bool-to-bv not supported with CBQI BV"); + } + Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" + << endl; + options::boolToBitvector.set(false); } if(options::produceAssignments() && !options::produceModels()) { diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index ad1259be0..6075dc344 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -17,8 +17,9 @@ #include #include -#include "theory/rewriter.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/bv/theory_bv_utils.h" @@ -261,26 +262,180 @@ Node BvInverter::getPathToPv(Node lit, Node pv, Node sv, Node pvs, return slit; } -Node BvInverter::solve_bv_constraint(Node sv, - Node sv_t, - Node t, - Kind rk, - bool pol, - std::vector& path, - BvInverterModelQuery* m, - BvInverterStatus& status) { - unsigned index; - unsigned nchildren; +Node BvInverter::solve_bv_lit(Node sv, + Node lit, + std::vector& path, + BvInverterModelQuery* m, + BvInverterStatus& status) { + Assert(!path.empty()); + + bool pol = true; + unsigned index, nchildren; NodeManager* nm = NodeManager::currentNM(); + Kind k; + + Assert(!path.empty()); + index = path.back(); + Assert(index < lit.getNumChildren()); + path.pop_back(); + k = lit.getKind(); + + /* Note: option --bool-to-bv is currently disabled when CBQI BV + * is enabled. We currently do not support Boolean operators + * that are interpreted as bit-vector operators of width 1. */ + + /* Boolean layer ----------------------------------------------- */ + + if (k == NOT) { + pol = !pol; + lit = lit[index]; + Assert(!path.empty()); + index = path.back(); + Assert(index < lit.getNumChildren()); + path.pop_back(); + k = lit.getKind(); + } + + Assert(k == EQUAL + || k == BITVECTOR_ULT + || k == BITVECTOR_SLT + || k == BITVECTOR_COMP); + + Node sv_t = lit[index]; + Node t = lit[1-index]; + + switch (k) { + case BITVECTOR_ULT: { + TypeNode solve_tn = sv_t.getType(); + Node x = getSolveVariable(solve_tn); + Node sc; + if (index == 0) { + if (pol == true) { + /* x < t + * with side condition: + * t != 0 */ + Node scl = nm->mkNode( + DISTINCT, t, bv::utils::mkZero(bv::utils::getSize(t))); + Node scr = nm->mkNode(k, x, t); + sc = nm->mkNode(IMPLIES, scl, scr); + } else { + sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); + } + } else if (index == 1) { + if (pol == true) { + /* t < x + * with side condition: + * t != ~0 */ + Node scl = nm->mkNode( + DISTINCT, t, bv::utils::mkOnes(bv::utils::getSize(t))); + Node scr = nm->mkNode(k, t, x); + sc = nm->mkNode(IMPLIES, scl, scr); + } else { + sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); + } + } + status.d_conds.push_back(sc); + /* t = skv (fresh skolem constant) */ + Node skv = getInversionNode(sc, solve_tn); + t = skv; + if (!path.empty()) { + index = path.back(); + Assert(index < sv_t.getNumChildren()); + path.pop_back(); + sv_t = sv_t[index]; + k = sv_t.getKind(); + } + break; + } + + case BITVECTOR_SLT: { + TypeNode solve_tn = sv_t.getType(); + Node x = getSolveVariable(solve_tn); + Node sc; + unsigned w = bv::utils::getSize(t); + if (index == 0) { + if (pol == true) { + /* x < t + * with side condition: + * t != 10...0 */ + Node min = bv::utils::mkConst(BitVector(w).setBit(w - 1)); + Node scl = nm->mkNode(DISTINCT, min, t); + Node scr = nm->mkNode(k, x, t); + sc = nm->mkNode(IMPLIES, scl, scr); + } else { + sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); + } + } else if (index == 1) { + if (pol == true) { + /* t < x + * with side condition: + * t != 01...1 */ + BitVector bv = BitVector(w).setBit(w - 1); + Node max = bv::utils::mkConst(~bv); + Node scl = nm->mkNode(DISTINCT, t, max); + Node scr = nm->mkNode(k, t, x); + sc = nm->mkNode(IMPLIES, scl, scr); + } else { + sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); + } + } + status.d_conds.push_back(sc); + /* t = skv (fresh skolem constant) */ + Node skv = getInversionNode(sc, solve_tn); + t = skv; + if (!path.empty()) { + index = path.back(); + Assert(index < sv_t.getNumChildren()); + path.pop_back(); + sv_t = sv_t[index]; + k = sv_t.getKind(); + } + break; + } + + default: + Assert(k == EQUAL); + if (pol == false) { + /* x != t + * <-> + * x < t || x > t (ULT) + * with side condition: + * t != 0 || t != ~0 */ + TypeNode solve_tn = sv_t.getType(); + Node x = getSolveVariable(solve_tn); + unsigned w = bv::utils::getSize(t); + Node scl = nm->mkNode( + OR, + nm->mkNode(DISTINCT, t, bv::utils::mkZero(w)), + nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w))); + Node scr = nm->mkNode(DISTINCT, x, t); + Node sc = nm->mkNode(IMPLIES, scl, scr); + status.d_conds.push_back(sc); + /* t = skv (fresh skolem constant) */ + Node skv = getInversionNode(sc, solve_tn); + t = skv; + if (!path.empty()) { + index = path.back(); + Assert(index < sv_t.getNumChildren()); + path.pop_back(); + sv_t = sv_t[index]; + k = sv_t.getKind(); + } + } + } + + /* Bit-vector layer -------------------------------------------- */ while (!path.empty()) { index = path.back(); Assert(index < sv_t.getNumChildren()); path.pop_back(); - Kind k = sv_t.getKind(); + k = sv_t.getKind(); nchildren = sv_t.getNumChildren(); - if (k == BITVECTOR_CONCAT) { + if (k == BITVECTOR_NOT || k == BITVECTOR_NEG) { + t = nm->mkNode(k, t); + } else if (k == BITVECTOR_CONCAT) { /* x = t[upper:lower] * where * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index @@ -297,14 +452,14 @@ Node BvInverter::solve_bv_constraint(Node sv, lower += bv::utils::getSize(sv_t[i]); } t = bv::utils::mkExtract(t, upper, lower); + } else if (k == BITVECTOR_SIGN_EXTEND) { + t = bv::utils::mkExtract(t, bv::utils::getSize(sv_t[index])-1, 0); } else if (k == BITVECTOR_EXTRACT) { Trace("bv-invert") << "bv-invert : Unsupported for index " << index - << ", from " << sv_t << std::endl; + << ", from " << sv_t << std::endl; return Node::null(); - } else if (k == BITVECTOR_NEG || k == BITVECTOR_NOT) { - t = NodeManager::currentNM()->mkNode(k, t); } else { - Assert (nchildren >= 2); + Assert(nchildren >= 2); Node s = nchildren == 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). */ @@ -312,13 +467,13 @@ Node BvInverter::solve_bv_constraint(Node sv, case BITVECTOR_PLUS: t = nm->mkNode(BITVECTOR_SUB, t, s); break; + case BITVECTOR_SUB: t = nm->mkNode(BITVECTOR_PLUS, t, s); break; case BITVECTOR_MULT: { - /* t = skv (fresh skolem constant) - * with side condition: + /* with side condition: * ctz(t) >= ctz(s) <-> x * s = t * where * ctz(t) >= ctz(s) -> (t & -t) >= (s & -s) */ @@ -336,7 +491,8 @@ Node BvInverter::solve_bv_constraint(Node sv, /* add side condition */ status.d_conds.push_back(sc); - /* get the skolem node for this side condition */ + /* t = skv (fresh skolem constant) + * 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; @@ -355,7 +511,7 @@ Node BvInverter::solve_bv_constraint(Node sv, return Node::null(); } else { /* s % x = t - * with side conditions: + * with side condition: * s > t * && s-t > t * && (t = 0 || t != s-1) */ @@ -382,8 +538,7 @@ Node BvInverter::solve_bv_constraint(Node sv, case BITVECTOR_AND: case BITVECTOR_OR: { - /* t = skv (fresh skolem constant) - * with side condition: + /* with side condition: * t & s = t * t | s = t */ TypeNode solve_tn = sv_t[index].getType(); @@ -392,13 +547,13 @@ Node BvInverter::solve_bv_constraint(Node sv, Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); + /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn); t = skv; break; } case BITVECTOR_LSHR: { - /* t = skv (fresh skolem constant) */ TypeNode solve_tn = sv_t[index].getType(); Node x = getSolveVariable(solve_tn); Node scl, scr; @@ -422,11 +577,12 @@ Node BvInverter::solve_bv_constraint(Node sv, scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_LSHR, x, s), t); Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); + /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn); t = skv; } else { /* s >> x = t - * with side conditions: + * with side condition: * (s = 0 && t = 0) * || (clz(t) >= clz(s) * && (t = 0 @@ -445,18 +601,18 @@ Node BvInverter::solve_bv_constraint(Node sv, Node s = sv_t[1 - index]; unsigned w = bv::utils::getSize(s); Node scl, scr; - Node zero = bv::utils::mkConst(w, 0u); + Node zero = bv::utils::mkZero(w); if (index == 0) { /* x udiv s = t - * with side conditions: + * with side condition: * !umulo(s * t) */ scl = nm->mkNode(NOT, bv::utils::mkUmulo(s, t)); scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, x, s), t); } else { /* s udiv x = t - * with side conditions: + * with side condition: * (t = 0 && (s = 0 || s != 2^w-1)) * || s >= t * || t = 2^w-1 @@ -479,7 +635,8 @@ Node BvInverter::solve_bv_constraint(Node sv, /* add side condition */ status.d_conds.push_back(sc); - /* get the skolem node for this side condition*/ + /* t = skv (fresh skolem constant) + * 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; @@ -495,7 +652,7 @@ Node BvInverter::solve_bv_constraint(Node sv, if (index == 0) { /* x << s = t - * with side conditions: + * with side condition: * (s = 0 || ctz(t) >= s) * <-> * (s = 0 || ((t o z) >> (z o s))[w-1:0] = z) @@ -514,7 +671,7 @@ Node BvInverter::solve_bv_constraint(Node sv, scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_SHL, x, s), t); } else { /* s << x = t - * with side conditions: + * with side condition: * (s = 0 && t = 0) * || (ctz(t) >= ctz(s) * && (t = 0 || @@ -531,12 +688,14 @@ Node BvInverter::solve_bv_constraint(Node sv, /* add side condition */ status.d_conds.push_back(sc); - /* get the skolem node for this side condition*/ + /* t = skv (fresh skolem constant) + * 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; break; } + default: Trace("bv-invert") << "bv-invert : Unknown kind " << k << " for bit-vector term " << sv_t << std::endl; @@ -546,65 +705,7 @@ Node BvInverter::solve_bv_constraint(Node sv, sv_t = sv_t[index]; } Assert(sv_t == sv); - // finalize based on the kind of constraint - // TODO - if (rk == EQUAL) { - return t; - } else { - Trace("bv-invert") - << "bv-invert : Unknown relation kind for bit-vector literal " << rk - << std::endl; - return t; - } -} - -Node BvInverter::solve_bv_lit(Node sv, Node lit, bool pol, - std::vector& path, - BvInverterModelQuery* m, - BvInverterStatus& status) { - Assert(!path.empty()); - unsigned index = path.back(); - Assert(index < lit.getNumChildren()); - path.pop_back(); - Kind k = lit.getKind(); - if (k == NOT) { - Assert(index == 0); - return solve_bv_lit(sv, lit[index], !pol, path, m, status); - } else if (k == EQUAL) { - return solve_bv_constraint(sv, lit[index], lit[1 - index], k, pol, path, m, - status); - } else if (k == BITVECTOR_ULT || k == BITVECTOR_ULE || k == BITVECTOR_SLT || - k == BITVECTOR_SLE) { - if (!pol) { - if (k == BITVECTOR_ULT) { - k = index == 1 ? BITVECTOR_ULE : BITVECTOR_UGE; - } else if (k == BITVECTOR_ULE) { - k = index == 1 ? BITVECTOR_ULT : BITVECTOR_UGT; - } else if (k == BITVECTOR_SLT) { - k = index == 1 ? BITVECTOR_SLE : BITVECTOR_SGE; - } else { - Assert(k == BITVECTOR_SLE); - k = index == 1 ? BITVECTOR_SLT : BITVECTOR_SGT; - } - } else if (index == 1) { - if (k == BITVECTOR_ULT) { - k = BITVECTOR_UGT; - } else if (k == BITVECTOR_ULE) { - k = BITVECTOR_UGE; - } else if (k == BITVECTOR_SLT) { - k = BITVECTOR_SGT; - } else { - Assert(k == BITVECTOR_SLE); - k = BITVECTOR_SGE; - } - } - return solve_bv_constraint(sv, lit[index], lit[1 - index], k, true, path, m, - status); - } else { - Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector literal " - << lit << std::endl; - } - return Node::null(); + return t; } } // namespace quantifiers diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 724b3b7a7..861331170 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -85,19 +85,11 @@ class BvInverter { */ Node eliminateSkolemFunctions(TNode n, std::vector& side_conditions); - /** solve_bv_constraint - * solve for sv in constraint ( (pol ? _ : not) sv_t t ), where sv_t.path - * = sv status accumulates side conditions - */ - Node solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk, bool pol, - std::vector& path, BvInverterModelQuery* m, - BvInverterStatus& status); - /** solve_bv_lit * solve for sv in lit, where lit.path = sv * status accumulates side conditions */ - Node solve_bv_lit(Node sv, Node lit, bool pol, std::vector& path, + Node solve_bv_lit(Node sv, Node lit, std::vector& path, BvInverterModelQuery* m, BvInverterStatus& status); private: diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index ad99f1135..7620dcbc8 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -895,7 +895,7 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf, if( !slit.isNull() ){ CegInstantiatorBvInverterModelQuery m( ci ); unsigned iid = d_inst_id_counter; - Node inst = d_inverter->solve_bv_lit( sv, slit, true, path, &m, d_inst_id_to_status[iid] ); + Node inst = d_inverter->solve_bv_lit( sv, slit, path, &m, d_inst_id_to_status[iid] ); if( !inst.isNull() ){ inst = Rewriter::rewrite(inst); Trace("cegqi-bv") << "...solved form is " << inst << std::endl; @@ -917,7 +917,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node atom = lit.getKind() == NOT ? lit[0] : lit; bool pol = lit.getKind() != NOT; Kind k = atom.getKind(); - if (pol && k == EQUAL) { + if ((pol && k == EQUAL) || (options::cbqiBvInvInDisEq())) { // positively asserted equalities between bitvector terms we leave unmodifed if (atom[0].getType().isBitVector()) { return lit; @@ -960,7 +960,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, nm->mkNode(kind::BITVECTOR_PLUS, t, slack)); Trace("cegqi-bv") << "Process " << lit << " as " << ret << ", slack is " << slack << std::endl; - }else{ + } else { ret = s.eqNode(t); Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; } diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 new file mode 100644 index 000000000..814b0d90b --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-inv-in-dis-eq +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (= (bvand x a) b))) + +(check-sat) -- 2.30.2