diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-13 08:01:30 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-13 08:01:30 -0500 |
commit | 527fb3c6c00ba1516f85e6e024d71d5c6ffba93b (patch) | |
tree | 6612914061e63920bca6a6fdd0f779da6ccaf6f1 /src | |
parent | d80588a41753d011202d670dbf7123233b665af9 (diff) |
Decision strategy: incorporate CEGQI (#2460)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp | 101 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.h | 12 |
3 files changed, 43 insertions, 71 deletions
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<Node, CegInstantiator*>::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<Node, std::unique_ptr<DecisionStrategy>>::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<Node, bool>& 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; j<itc->second.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; i<d_quantEngine->getModel()->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<Node, std::unique_ptr<CegInstantiator>>::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<const Node, std::unique_ptr<CegInstantiator>>& 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<Node>& 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<Node, CegInstantiator*> d_cinst; + std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst; + /** + * The decision strategy for each quantified formula q registered to this + * class. + */ + std::map<Node, std::unique_ptr<DecisionStrategy>> 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); |