From: Andrew Reynolds Date: Fri, 27 Oct 2017 18:58:12 +0000 (-0500) Subject: Cbqi multiple instantiation (#1289) X-Git-Tag: cvc5-1.0.0~5529 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0891ff3d00975ee9697855dcb2b6cbb232ec5523;p=cvc5.git Cbqi multiple instantiation (#1289) * Multi-instantiation heuristic for cbqi bv. * New clang format. * Minor * Minor. * Minor --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 0262012f6..ba7c8338a 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -303,6 +303,8 @@ option cbqiModel --cbqi-model bool :read-write :default true guide instantiations by model values for counterexample-based quantifier instantiation option cbqiAll --cbqi-all bool :read-write :default false apply counterexample-based instantiation to all quantified formulas +option cbqiMultiInst --cbqi-multi-inst bool :read-write :default false + when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation # CEGQI for arithmetic option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 02b2d3a1b..57bfb2d14 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -362,7 +362,13 @@ void CegInstantiator::popStackVariable() { d_stack_vars.pop_back(); } -bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort ) { +bool CegInstantiator::doAddInstantiationInc(Node pv, + Node n, + TermProperties& pv_prop, + SolvedForm& sf, + unsigned effort, + bool revertOnSuccess) +{ Node cnode = pv_prop.getCacheNode(); if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){ d_curr_subs_proc[pv][n][cnode] = true; @@ -453,12 +459,14 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; unsigned i = d_curr_index[pv]; success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort ); - if( !success ){ + if (!success || revertOnSuccess) + { Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; sf.pop_back( pv, n, pv_prop ); } } - if( success ){ + if (success && !revertOnSuccess) + { return true; }else{ Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl; @@ -472,7 +480,7 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv for( unsigned i=0; i d_theta; @@ -227,7 +229,25 @@ public: public: void pushStackVariable( Node v ); void popStackVariable(); - bool doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort ); + /** do add instantiation increment + * + * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current + * instantiation, specified by sf. + * + * This function returns true if a call to + * QuantifiersEngine::addInstantiation(...) + * was successfully made in a recursive call. + * + * The solved form sf is reverted to its original state if + * this function returns false, or + * revertOnSuccess is true and this function returns true. + */ + bool doAddInstantiationInc(Node pv, + Node n, + TermProperties& pv_prop, + SolvedForm& sf, + unsigned effort, + bool revertOnSuccess = false); Node getModelValue( Node n ); public: unsigned getNumCEAtoms() { return d_ce_atoms.size(); } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index ad4c83919..60566da1b 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -1029,10 +1029,18 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; // if interleaving, do not do inversion half the time if (!options::cbqiBvInterleaveValue() || rand() % 2 == 0) { + bool firstVar = sf.empty(); // get inst id list - Trace("cegqi-bv") << " " << iti->second.size() - << " candidate instantiations for " << pv << " : " - << std::endl; + if (Trace.isOn("cegqi-bv")) + { + Trace("cegqi-bv") << " " << iti->second.size() + << " candidate instantiations for " << pv << " : " + << std::endl; + if (firstVar) + { + 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 @@ -1081,8 +1089,12 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, Trace("cegqi-bv") << std::endl; } - // currently we select the first literal - if (inst_ids_try.empty()) { + // 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 { @@ -1090,11 +1102,12 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, } } - // 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 + // Now, try all instantiation ids we want to try + // Typically size( inst_ids_try )<=1, 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 = iti->second[j]; Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); @@ -1104,10 +1117,16 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, 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; + if (ci->doAddInstantiationInc( + pv, inst_term, pv_prop_bv, sf, effort, revertOnSuccess)) + { + ret = true; } } + if (ret) + { + return true; + } Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl; d_var_to_curr_inst_id.erase(pv);