From 39a85cc99f3b9f3d203490f5918ebe56bd916d64 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Oct 2017 00:12:02 -0500 Subject: CBQI BV quick heuristics (#1239) Adds two heuristics for cbqi-bv, both disabled by default. The first optimistically solves for boundary points of inequalities. The second randomly interleaves inversion and value instantiations. Adds some newly solved regressions from SMT LIB. --- src/options/quantifiers_options | 6 +- src/theory/quantifiers/ceg_t_instantiator.cpp | 192 +++++++++++++++++--------- 2 files changed, 128 insertions(+), 70 deletions(-) (limited to 'src') diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 2e765ce6b..d3f8c9f6a 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -334,7 +334,11 @@ option quantEprMatching --quant-epr-match bool :default true # CEGQI for BV option cbqiBv --cbqi-bv bool :read-write :default false - use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors + use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors +option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false + 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 ### local theory extensions options diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 91c29c6de..ad99f1135 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -897,12 +897,15 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf, unsigned iid = d_inst_id_counter; Node inst = d_inverter->solve_bv_lit( sv, slit, true, path, &m, d_inst_id_to_status[iid] ); 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++; }else{ + Trace("cegqi-bv") << "...failed to solve." << std::endl; // cleanup information if we failed to solve d_inst_id_to_status.erase( iid ); } @@ -920,11 +923,23 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, return lit; } } else { + bool useSlack = false; + if (k == EQUAL) { + // always use slack for disequalities + useSlack = true; + } else if (k == BITVECTOR_ULT || k == BITVECTOR_SLT) { + if (options::cbqiBvSlackIneq()) { + useSlack = true; + } + } else { + // others should be rewritten + Assert(false); + return Node::null(); + } // 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 (k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_ULE || - k == BITVECTOR_SLT || k == BITVECTOR_SLE) { + if (useSlack) { Node s = atom[0]; Node t = atom[1]; // only handle equalities between bitvectors @@ -934,19 +949,43 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, 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; - Node ret = nm->mkNode(kind::EQUAL, s, - nm->mkNode(kind::BITVECTOR_PLUS, t, 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; - return ret; + }else{ + ret = s.eqNode(t); + Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; } + return ret; + } + } 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; } } return Node::null(); @@ -976,79 +1015,94 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv ); if( iti!=d_var_to_inst_id.end() ){ Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; - // get inst id list - Trace("cegqi-bv") << " " << iti->second.size() << " candidate instantiations for " << pv << " : " << std::endl; - // the order of instantiation ids we will try - std::vector< unsigned > 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 - // this helps robustness, since picking the same literal every time may be lead to a stream of value instantiations - std::random_shuffle( iti->second.begin(), iti->second.end() ); + // if interleaving, do not do inversion half the time + if (!options::cbqiBvInterleaveValue() || rand() % 2 == 0) { + // get inst id list + Trace("cegqi-bv") << " " << iti->second.size() + << " candidate instantiations for " << pv << " : " + << 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 + // this helps robustness, since picking the same literal every time may + // lead to a stream of value instantiations, whereas with randomization + // 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; jsecond.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]; + 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; - } - - // debug printing - if( Trace.isOn("cegqi-bv") ){ - 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; + // 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; } - // process information about solved status - std::unordered_map< unsigned, BvInverterStatus >::iterator its = d_inst_id_to_status.find( inst_id ); - Assert( its!=d_inst_id_to_status.end() ); - if( !(*its).second.d_conds.empty() ){ - Trace("cegqi-bv") << " ...with " << (*its).second.d_conds.size() << " side conditions : " << std::endl; - for( unsigned k=0; k<(*its).second.d_conds.size(); k++ ){ - Node cond = (*its).second.d_conds[k]; - Trace("cegqi-bv") << " " << cond << std::endl; + + // debug printing + if (Trace.isOn("cegqi-bv")) { + 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; + } + // process information about solved status + std::unordered_map::iterator its = + d_inst_id_to_status.find(inst_id); + Assert(its != d_inst_id_to_status.end()); + if (!its->second.d_conds.empty()) { + Trace("cegqi-bv") << " ...with " << its->second.d_conds.size() + << " side conditions : " << std::endl; + for (unsigned k = 0; k < its->second.d_conds.size(); k++) { + Node cond = its->second.d_conds[k]; + Trace("cegqi-bv") << " " << cond << std::endl; + } } + Trace("cegqi-bv") << std::endl; } - Trace("cegqi-bv") << std::endl; - } - - // currently we take select the first literal - if( inst_ids_try.empty() ){ - // try the first one - inst_ids_try.push_back( inst_id ); - } else { - // selection criteria across multiple literals goes here - + // currently we select the first literal + if (inst_ids_try.empty()) { + // 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 )=0, otherwise worst-case performance for constructing - // instantiations is exponential on the number of variables in this quantifier - for( unsigned j = 0; jsecond[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]; - // try instantiation pv -> inst_term - TermProperties pv_prop_bv; - Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl; - d_var_to_curr_inst_id[pv] = inst_id; - if( ci->doAddInstantiationInc( pv, inst_term, pv_prop_bv, sf, effort ) ){ - return true; + + // now, try all instantiation ids we want to try + // typically size( inst_ids_try )=0, otherwise worst-case performance for + // constructing + // instantiations is exponential on the number of variables in this + // quantifier + for (unsigned j = 0; j < inst_ids_try.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]; + // try instantiation pv -> inst_term + TermProperties pv_prop_bv; + Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term + << std::endl; + d_var_to_curr_inst_id[pv] = inst_id; + if (ci->doAddInstantiationInc(pv, inst_term, pv_prop_bv, sf, effort)) { + return true; + } } + Trace("cegqi-bv") << "...failed to add instantiation for " << pv + << std::endl; + d_var_to_curr_inst_id.erase(pv); + } else { + Trace("cegqi-bv") << "...do not do instantiation for " << pv + << " (skip, based on heuristic)" << std::endl; } - Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl; - d_var_to_curr_inst_id.erase( pv ); } return false; -- cgit v1.2.3