From: Andrew Reynolds Date: Fri, 12 Jan 2018 22:05:52 +0000 (-0600) Subject: Improvements for CBQI BV (#1504) X-Git-Tag: cvc5-1.0.0~5358 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=17820d7e0606b19e22dc082b2f438b323ac49ff8;p=cvc5.git Improvements for CBQI BV (#1504) --- diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 275d7238d..e617819d7 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -994,12 +994,15 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, if (!inst.isNull()) { inst = Rewriter::rewrite(inst); - Trace("cegqi-bv") << "...solved form is " << inst << std::endl; - // store information for id and increment - d_var_to_inst_id[pv].push_back(iid); - d_inst_id_to_term[iid] = inst; - d_inst_id_to_alit[iid] = alit; - d_inst_id_counter++; + if (inst.isConst() || !ci->hasNestedQuantification()) + { + Trace("cegqi-bv") << "...solved form is " << inst << std::endl; + // store information for id and increment + d_var_to_inst_id[pv].push_back(iid); + d_inst_id_to_term[iid] = inst; + d_inst_id_to_alit[iid] = alit; + d_inst_id_counter++; + } } else { @@ -1022,90 +1025,80 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, Node atom = lit.getKind() == NOT ? lit[0] : lit; bool pol = lit.getKind() != NOT; Kind k = atom.getKind(); - if (pol && k == EQUAL) + if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT) { - // positively asserted equalities between bitvector terms we always leave - // unmodified - if (atom[0].getType().isBitVector()) { - return lit; - } + // others are unhandled + return Node::null(); + } + else if (!atom[0].getType().isBitVector()) + { + return Node::null(); + } + else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP + || (pol && k == EQUAL)) + { + return lit; } - else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP) + NodeManager* nm = NodeManager::currentNM(); + Node s = atom[0]; + Node t = atom[1]; + + Node sm = ci->getModelValue(s); + Node tm = ci->getModelValue(t); + Assert(!sm.isNull() && sm.isConst()); + Assert(!tm.isNull() && tm.isConst()); + Trace("cegqi-bv") << "Model value: " << std::endl; + Trace("cegqi-bv") << " " << s << " " << k << " " << t << " is " + << std::endl; + Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl; + + Node ret; + if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK) { - // if option is set, disequalities and inequalities we leave unmodified - if ((k == EQUAL && atom[0].getType().isBitVector()) || k == BITVECTOR_ULT - || k == BITVECTOR_SLT) + // if using slack, we convert constraints to a positive equality based on + // the current model M, e.g.: + // (not) s ~ t ---> s = t + ( s^M - t^M ) + if (sm != tm) + { + Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm)); + Assert(slack.isConst()); + // remember the slack value for the asserted literal + d_alit_to_model_slack[lit] = slack; + ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack)); + Trace("cegqi-bv") << "Slack is " << slack << std::endl; + } + else { - return lit; + ret = s.eqNode(t); } } else { - bool useSlack = false; - if (k == EQUAL && atom[0].getType().isBitVector()) + // turn disequality into an inequality + // e.g. s != t becomes s < t or t < s + if (k == EQUAL) { - // always use slack for disequalities - useSlack = true; - } else if (k == BITVECTOR_ULT || k == BITVECTOR_SLT) { - if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK) + if (Random::getRandom().pickWithProb(0.5)) { - useSlack = true; + std::swap(s, t); } - } else { - // others are not unhandled - return Node::null(); + pol = true; } - // for all other predicates, we convert them to a positive equality based on - // the current model M, e.g.: - // (not) s ~ t ---> s = t + ( s^M - t^M ) - if (useSlack) { - Node s = atom[0]; - Node t = atom[1]; - // only handle equalities between bitvectors - if (s.getType().isBitVector()) { - NodeManager* nm = NodeManager::currentNM(); - Node sm = ci->getModelValue(s); - Assert(!sm.isNull() && sm.isConst()); - Node tm = ci->getModelValue(t); - Assert(!tm.isNull() && tm.isConst()); - Node ret; - if (sm != tm) { - Node slack = - Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, sm, tm)); - Assert(slack.isConst()); - // remember the slack value for the asserted literal - d_alit_to_model_slack[lit] = slack; - ret = nm->mkNode(kind::EQUAL, s, - nm->mkNode(kind::BITVECTOR_PLUS, t, slack)); - Trace("cegqi-bv") << "Process " << lit << " as " << ret - << ", slack is " << slack << std::endl; - } else { - ret = s.eqNode(t); - Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; - } - return ret; - } + // otherwise, we optimistically solve for the boundary point of an + // inequality, for example: + // for s < t, we solve s+1 = t + // for ~( s < t ), we solve s = t + // notice that this equality does not necessarily hold in the model, and + // hence the corresponding instantiation strategy is not guaranteed to be + // monotonic. + if (!pol) + { + ret = s.eqNode(t); } else { - // otherwise, we optimistically solve for the boundary point of an inequality - // for example - // for s < t, we solve s+1 = t - // for ~( s < t ), we solve s = t - // notice that this equality does not necessarily hold in the model, and - // hence the corresponding instantiation strategy is not guaranteed to be - // monotonic. - Node ret; - if (!pol) { - ret = atom[0].eqNode(atom[1]); - } else { - unsigned one = 1; - BitVector bval(atom[0].getType().getConst(), one); - Node bv_one = NodeManager::currentNM()->mkConst(bval); - ret = NodeManager::currentNM() - ->mkNode(kind::BITVECTOR_PLUS, atom[0], bv_one) - .eqNode(atom[1]); - } - return ret; + Node bv_one = bv::utils::mkOne(bv::utils::getSize(s)); + ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t); } } - return Node::null(); + Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; + return ret; } bool BvInstantiator::processAssertion(CegInstantiator* ci, @@ -1126,7 +1119,10 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl; } } - processLiteral(ci, sf, pv, rlit, alit, effort); + if (!rlit.isNull()) + { + processLiteral(ci, sf, pv, rlit, alit, effort); + } } return false; } @@ -1163,8 +1159,6 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, Trace("cegqi-bv") << " ...this is the first variable" << std::endl; } } - // the order of instantiation ids we will try - std::vector inst_ids_try; // until we have a model-preserving selection function for BV, this must // be heuristic (we only pick one literal) // hence we randomize the list @@ -1173,53 +1167,47 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, // we may find an invertible literal that leads to a useful instantiation. std::random_shuffle(iti->second.begin(), iti->second.end()); - for (unsigned j = 0; j < iti->second.size(); j++) { - unsigned inst_id = iti->second[j]; - Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); - Node inst_term = d_inst_id_to_term[inst_id]; - Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end()); - Node alit = d_inst_id_to_alit[inst_id]; - - // get the slack value introduced for the asserted literal - Node curr_slack_val; - std::unordered_map::iterator itms = - d_alit_to_model_slack.find(alit); - if (itms != d_alit_to_model_slack.end()) { - curr_slack_val = itms->second; - } + if (Trace.isOn("cegqi-bv")) + { + for (unsigned j = 0, size = iti->second.size(); j < size; j++) + { + unsigned inst_id = iti->second[j]; + Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); + Node inst_term = d_inst_id_to_term[inst_id]; + Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end()); + Node alit = d_inst_id_to_alit[inst_id]; + + // get the slack value introduced for the asserted literal + Node curr_slack_val; + std::unordered_map::iterator itms = + d_alit_to_model_slack.find(alit); + if (itms != d_alit_to_model_slack.end()) + { + curr_slack_val = itms->second; + } - // debug printing - if (Trace.isOn("cegqi-bv")) { + // debug printing Trace("cegqi-bv") << " [" << j << "] : "; Trace("cegqi-bv") << inst_term << std::endl; if (!curr_slack_val.isNull()) { Trace("cegqi-bv") << " ...with slack value : " << curr_slack_val << std::endl; } + Trace("cegqi-bv-debug") << " ...from : " << alit << std::endl; Trace("cegqi-bv") << std::endl; } - - // currently: - // We select the first literal, and - // for the first variable, we select all - // if cbqiMultiInst is enabled. - if (inst_ids_try.empty() || (firstVar && options::cbqiMultiInst())) - { - // try the first one - inst_ids_try.push_back(inst_id); - } else { - // selection criteria across multiple literals goes here - } } // Now, try all instantiation ids we want to try - // Typically size( inst_ids_try )<=1, otherwise worst-case performance + // Typically we try only one, otherwise worst-case performance // for constructing instantiations is exponential on the number of // variables in this quantifier prefix. bool ret = false; - bool revertOnSuccess = inst_ids_try.size() > 1; - for (unsigned j = 0; j < inst_ids_try.size(); j++) { - unsigned inst_id = inst_ids_try[j]; + bool tryMultipleInst = firstVar && options::cbqiMultiInst(); + bool revertOnSuccess = tryMultipleInst; + for (unsigned j = 0, size = iti->second.size(); j < size; j++) + { + unsigned inst_id = iti->second[j]; Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); Node inst_term = d_inst_id_to_term[inst_id]; Node alit = d_inst_id_to_alit[inst_id]; @@ -1236,6 +1224,11 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, ret = true; } ci->markSolved(alit, false); + // we are done unless we try multiple instances + if (!tryMultipleInst) + { + break; + } } if (ret) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 17214112b..472316cae 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -920,7 +920,8 @@ Node QuantifiersRewriter::computeVariableElimLitBv(Node lit, visit.pop_back(); if (std::find(args.begin(), args.end(), cur) != args.end()) { - linear[cur] = linear.find(cur) == linear.end(); + bool lval = linear.find(cur) == linear.end(); + linear[cur] = lval; } if (visited.find(cur) == visited.end()) { diff --git a/test/regress/regress0/sygus/Base16_1.sy b/test/regress/regress0/sygus/Base16_1.sy index 5833751cb..b54c7688b 100644 --- a/test/regress/regress0/sygus/Base16_1.sy +++ b/test/regress/regress0/sygus/Base16_1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-qe-preproc --cbqi-bv-rm-extract --sygus-out=status --cbqi-bv --cegqi-si=all +; COMMAND-LINE: --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all (set-logic BV) (define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))