From: Andrew Reynolds Date: Thu, 13 Sep 2018 13:01:30 +0000 (-0500) Subject: Decision strategy: incorporate CEGQI (#2460) X-Git-Tag: cvc5-1.0.0~4654 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=527fb3c6c00ba1516f85e6e024d71d5c6ffba93b;p=cvc5.git Decision strategy: incorporate CEGQI (#2460) --- diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 78cc2ac04..2d8d61736 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -433,7 +433,6 @@ public: Node expandDefinition(LogicRequest &logicRequest, Node node); void setMasterEqualityEngine(eq::EqualityEngine* eq); - void setQuantifiersEngine(QuantifiersEngine* qe); void check(Theory::Effort e); bool needsCheckLastEffort(); diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 9b82c1f4b..95a60afac 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -69,15 +69,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) InstStrategyCegqi::~InstStrategyCegqi() { - for (std::map::iterator i = d_cinst.begin(), - iend = d_cinst.end(); - i != iend; - ++i) - { - CegInstantiator* instantiator = (*i).second; - delete instantiator; - } - d_cinst.clear(); + } bool InstStrategyCegqi::needsCheck(Theory::Effort e) @@ -189,6 +181,27 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) } } } + // The decision strategy for this quantified formula ensures that its + // counterexample literal is decided on first. It is user-context dependent. + std::map>::iterator itds = + d_dstrat.find(q); + DecisionStrategy* dlds = nullptr; + if (itds == d_dstrat.end()) + { + d_dstrat[q].reset( + new DecisionStrategySingleton("CexLiteral", + ceLit, + d_quantEngine->getSatContext(), + d_quantEngine->getValuation())); + dlds = d_dstrat[q].get(); + } + else + { + dlds = itds->second.get(); + } + // it is appended to the list of strategies + d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds); return true; }else{ return false; @@ -574,50 +587,6 @@ bool InstStrategyCegqi::doCbqi(Node q) return it->second != CEG_UNHANDLED; } -Node InstStrategyCegqi::getNextDecisionRequestProc(Node q, - std::map& proc) -{ - if( proc.find( q )==proc.end() ){ - proc[q] = true; - //first check children - std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q ); - if( itc!=d_children_quant.end() ){ - for( unsigned j=0; jsecond.size(); j++ ){ - Node d = getNextDecisionRequestProc( itc->second[j], proc ); - if( !d.isNull() ){ - return d; - } - } - } - //then check self - if( hasAddedCbqiLemma( q ) ){ - Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); - bool value; - if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; - return cel; - } - } - } - return Node::null(); -} - -Node InstStrategyCegqi::getNextDecisionRequest(unsigned& priority) -{ - std::map< Node, bool > proc; - //for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - for( NodeSet::const_iterator it = d_added_cbqi_lemma.begin(); it != d_added_cbqi_lemma.end(); ++it ){ - Node q = *it; - Node d = getNextDecisionRequestProc( q, proc ); - if( !d.isNull() ){ - priority = 0; - return d; - } - } - return Node::null(); -} - void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { if( e==0 ){ CegInstantiator * cinst = getInstantiator( q ); @@ -708,23 +677,25 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { } CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { - std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q ); + std::map>::iterator it = + d_cinst.find(q); if( it==d_cinst.end() ){ - CegInstantiator* cinst = - new CegInstantiator(d_quantEngine, d_out.get(), true, true); - d_cinst[q] = cinst; - return cinst; - }else{ - return it->second; + d_cinst[q].reset( + new CegInstantiator(d_quantEngine, d_out.get(), true, true)); + return d_cinst[q].get(); } + return it->second.get(); } void InstStrategyCegqi::presolve() { - if( options::cbqiPreRegInst() ){ - for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ - Trace("cbqi-presolve") << "Presolve " << it->first << std::endl; - it->second->presolve( it->first ); - } + if (!options::cbqiPreRegInst()) + { + return; + } + for (std::pair>& ci : d_cinst) + { + Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl; + ci.second->presolve(ci.first); } } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 433de52a8..c3cbf8100 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -18,6 +18,7 @@ #ifndef __CVC4__INST_STRATEGY_CBQI_H #define __CVC4__INST_STRATEGY_CBQI_H +#include "theory/decision_manager.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "util/statistics_registry.h" @@ -84,8 +85,6 @@ class InstStrategyCegqi : public QuantifiersModule void preRegisterQuantifier(Node q) override; // presolve void presolve() override; - /** get next decision request */ - Node getNextDecisionRequest(unsigned& priority) override; /** Do nested quantifier elimination. */ Node doNestedQE(Node q, std::vector& inst_terms, Node lem, bool doVts); @@ -135,7 +134,12 @@ class InstStrategyCegqi : public QuantifiersModule * The instantiator for each quantified formula q registered to this class. * This object is responsible for finding instantiatons for q. */ - std::map d_cinst; + std::map> d_cinst; + /** + * The decision strategy for each quantified formula q registered to this + * class. + */ + std::map> d_dstrat; /** the current quantified formula we are processing */ Node d_curr_quant; //---------------------- for vts delta minimization @@ -164,8 +168,6 @@ class InstStrategyCegqi : public QuantifiersModule void registerCounterexampleLemma(Node q, Node lem); /** has added cbqi lemma */ bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } - /** get next decision request with dependency checking */ - Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ); /** process functions */ void process(Node q, Theory::Effort effort, int e);