diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
commit | d9d71e0d7885d32ef44fbd08d47b3cccd35ff6f7 (patch) | |
tree | f730bb17eba9412258c47617f144510d722d6006 /src/theory/quantifiers | |
parent | bbcfb5208c6c0f343d1a63b129c54914f66b2701 (diff) |
more cleanup of quantifiers code
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 7 | ||||
-rwxr-xr-x | src/theory/quantifiers/inst_gen.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 40 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 19 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 114 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 1 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_util.cpp | 144 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_util.h | 77 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 73 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 69 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_instantiator.cpp | 12 |
18 files changed, 405 insertions, 208 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index db0eed31e..57b99c59b 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -38,7 +38,9 @@ libquantifiers_la_SOURCES = \ quantifiers_attributes.h \ quantifiers_attributes.cpp \ inst_gen.h \ - inst_gen.cpp + inst_gen.cpp \ + quant_util.h \ + quant_util.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 685898515..28eeca624 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -27,7 +27,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ), -d_axiom_asserted( c, false ), d_forall_asserts( c ){ +d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index df9b55582..c8fcb7c44 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -48,6 +48,8 @@ private: context::CDO< bool > d_axiom_asserted; /** list of quantifiers asserted in the current context */ context::CDList<Node> d_forall_asserts; + /** is model set */ + context::CDO< bool > d_isModelSet; public: //for Theory UF: //models for each UF operator std::map< Node, uf::UfModelTree > d_uf_model_tree; @@ -78,9 +80,12 @@ public: virtual ~FirstOrderModel(){} // reset the model void reset(); -public: // initialize the model void initialize( bool considerAxioms = true ); + /** mark model set */ + void markModelSet() { d_isModelSet = true; } + /** is model set */ + bool isModelSet() { return d_isModelSet; } //the following functions are for evaluating quantifier bodies public: /** reset evaluation */ diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 324165692..ea58840f5 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -44,8 +44,8 @@ InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ }
void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){
- if( !qe->existsInstantiation( f, m, true, true ) ){
- //if( d_inst_trie[val].addInstMatch( qe, f, m, true, NULL, true ) ){
+ if( !qe->existsInstantiation( f, m, true ) ){
+ //if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
d_match_values.push_back( val );
d_matches.push_back( InstMatch( &m ) );
//}
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index a74bf0fd5..d00885abf 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -100,8 +100,8 @@ void InstMatch::debugPrint( const char* c ){ } void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ - for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){ - Node ic = qe->getTermDatabase()->d_inst_constants[f][i]; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); if( d_map.find( ic )==d_map.end() ){ d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); } @@ -145,26 +145,6 @@ Node InstMatch::getValue( Node var ){ return Node::null(); } } -/* -void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ){ - for( int i=0; i<(int)vars.size(); i++ ){ - std::map< Node, Node >::iterator it = d_map.find( vars[i] ); - if( it!=d_map.end() && !it->second.isNull() ){ - match.push_back( it->second ); - }else{ - match.push_back( qe->getTermDatabase()->getFreeVariableForInstConstant( vars[i] ) ); - } - } -} - -void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ){ - for( int i=0; i<(int)vars.size(); i++ ){ - if( d_map.find( vars[i] )!=d_map.end() && !d_map[ vars[i] ].isNull() ){ - match.push_back( d_map[ vars[i] ] ); - } - } -} -*/ /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ @@ -176,7 +156,7 @@ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, } /** exists match */ -bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ){ +bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){ if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){ return true; }else{ @@ -184,7 +164,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ - if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){ + if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ return true; } } @@ -194,7 +174,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& Node nl; it = d_data.find( nl ); if( it!=d_data.end() ){ - if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){ + if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ return true; } } @@ -210,7 +190,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& if( en!=n ){ std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en ); if( itc!=d_data.end() ){ - if( itc->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){ + if( itc->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ return true; } } @@ -223,12 +203,12 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& } } -bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){ - return existsInstMatch2( qe, f, m, modEq, 0, imtio, modInst ); +bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio ); } -bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){ - if( !existsInstMatch( qe, f, m, modEq, imtio, modInst ) ){ +bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){ addInstMatch2( qe, f, m, 0, imtio ); return true; }else{ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index feab91837..a0db1336f 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -122,10 +122,6 @@ public: void makeInternal( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); - /** compute d_match */ - //void computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ); - /** compute d_match */ - //void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ); /** get value */ Node getValue( Node var ); /** clear */ @@ -191,7 +187,7 @@ private: /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ); /** exists match */ - bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ); + bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ); public: /** the data */ std::map< Node, InstMatchTrie > d_data; @@ -204,16 +200,16 @@ public: modInst is if we return true if m is an instance of a match that exists */ bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, bool modInst = false ); + bool modInst = false, ImtIndexOrder* imtio = NULL ); /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, bool modInst = false ); + bool modInst = false, ImtIndexOrder* imtio = NULL ); };/* class InstMatchTrie */ -class InstMatchTrieOrdered { +class InstMatchTrieOrdered{ private: InstMatchTrie::ImtIndexOrder* d_imtio; InstMatchTrie d_imt; @@ -226,8 +222,11 @@ public: InstMatchTrie* getTrie() { return &d_imt; } public: /** add match m, return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false ){ - return d_imt.addInstMatch( qe, f, m, modEq, d_imtio ); + bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ + return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio ); + } + bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ + return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio ); } };/* class InstMatchTrieOrdered */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index b402638b1..027ac67eb 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -32,35 +32,6 @@ QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ } -bool InstantiationEngine::hasAddedCbqiLemma( Node f ) { - return d_ce_lit.find( f ) != d_ce_lit.end(); -} - -void InstantiationEngine::addCbqiLemma( Node f ){ - Assert( doCbqi( f ) && !hasAddedCbqiLemma( f ) ); - //code for counterexample-based quantifier instantiation - Debug("cbqi") << "Do cbqi for " << f << std::endl; - //make the counterexample body - //Node ceBody = f[1].substitute( d_quantEngine->d_vars[f].begin(), d_quantEngine->d_vars[f].end(), - // d_quantEngine->d_inst_constants[f].begin(), - // d_quantEngine->d_inst_constants[f].end() ); - //get the counterexample literal - Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f ); - Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); - d_ce_lit[ f ] = ceLit; - d_quantEngine->getTermDatabase()->setInstantiationConstantAttr( ceLit, f ); - // set attributes, mark all literals in the body of n as dependent on cel - //registerLiterals( ceLit, f ); - //require any decision on cel to be phase=true - d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - NodeBuilder<> nb(kind::OR); - nb << f << ceLit; - Node lem = nb; - Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem ); -} bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //if counterexample-based quantifier instantiation is active @@ -70,8 +41,20 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){ + d_added_cbqi_lemma[f] = true; + Debug("cbqi") << "Do cbqi for " << f << std::endl; //add cbqi lemma - addCbqiLemma( f ); + //get the counterexample literal + Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); + //require any decision on cel to be phase=true + d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + NodeBuilder<> nb(kind::OR); + nb << f << ceLit; + Node lem = nb; + Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma( lem ); addedLemma = true; } } @@ -98,7 +81,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( q ); Debug("inst-engine-debug") << "IE: Instantiate " << f << "..." << std::endl; //if this quantifier is active - if( d_quantEngine->getActive( f ) ){ + if( d_quant_active[ f ] ){ //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e; int e_use = e; if( e_use>=0 ){ @@ -165,16 +148,12 @@ void InstantiationEngine::check( Theory::Effort e ){ Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; } bool quantActive = false; - //for each quantifier currently asserted, - // such that the counterexample literal is not in positive in d_counterexample_asserts - // for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) { - // if( (*i).second ) { Debug("quantifiers") << "quantifiers: check: asserted quantifiers size" << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( options::cbqi() && hasAddedCbqiLemma( n ) ){ - Node cel = d_ce_lit[ n ]; + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); bool active, value; bool ceValue = false; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ @@ -183,7 +162,7 @@ void InstantiationEngine::check( Theory::Effort e ){ }else{ active = true; } - d_quantEngine->setActive( n, active ); + d_quant_active[n] = active; if( active ){ Debug("quantifiers") << " Active : " << n; quantActive = true; @@ -203,15 +182,14 @@ void InstantiationEngine::check( Theory::Effort e ){ } Debug("quantifiers") << std::endl; }else{ - d_quantEngine->setActive( n, true ); + d_quant_active[n] = true; quantActive = true; Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl; } Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl; - Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl; - Debug("quantifiers") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl; + Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; + Debug("quantifiers") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; } - //} if( quantActive ){ bool addedLemmas = doInstantiationRound( e ); //Debug("quantifiers-dec") << "Do instantiation, level = " << d_quantEngine->getValuation().getDecisionLevel() << std::endl; @@ -248,17 +226,17 @@ void InstantiationEngine::check( Theory::Effort e ){ void InstantiationEngine::registerQuantifier( Node f ){ //Notice() << "do cbqi " << f << " ? " << std::endl; - Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f ); + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); if( !doCbqi( f ) ){ d_quantEngine->addTermToDatabase( ceBody, true ); //need to tell which instantiators will be responsible //by default, just chose the UF instantiator - d_quantEngine->getInstantiator( theory::THEORY_UF )->setHasConstraintsFrom( f ); + d_quantEngine->getInstantiator( theory::THEORY_UF )->setQuantifierActive( f ); } //take into account user patterns if( f.getNumChildren()==3 ){ - Node subsPat = d_quantEngine->getTermDatabase()->getSubstitutedNode( f[2], f ); + Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f ); //add patterns for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; @@ -320,22 +298,6 @@ bool InstantiationEngine::doCbqi( Node f ){ -//void InstantiationEngine::registerLiterals( Node n, Node f ){ -// if( n.getAttribute(InstConstantAttribute())==f ){ -// for( int i=0; i<(int)n.getNumChildren(); i++ ){ -// registerLiterals( n[i], f ); -// } -// if( !d_ce_lit[ f ].isNull() ){ -// if( d_quantEngine->d_te->getPropEngine()->isSatLiteral( n ) && n.getKind()!=NOT ){ -// if( n!=d_ce_lit[ f ] && n.notNode()!=d_ce_lit[ f ] ){ -// Debug("quant-dep-dec") << "Make " << n << " dependent on "; -// Debug("quant-dep-dec") << d_ce_lit[ f ] << std::endl; -// d_quantEngine->getOutputChannel().dependentDecision( d_ce_lit[ f ], n ); -// } -// } -// } -// } -//} void InstantiationEngine::debugSat( int reason ){ if( reason==SAT_CBQI ){ @@ -347,7 +309,7 @@ void InstantiationEngine::debugSat( int reason ){ // if( (*i).second ) { for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Node cel = d_ce_lit[ f ]; + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); Assert( !cel.isNull() ); bool value; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ @@ -371,26 +333,20 @@ void InstantiationEngine::debugSat( int reason ){ } } -void InstantiationEngine::propagate( Theory::Effort level ){ - //propagate as decision all counterexample literals that are not asserted - for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){ - bool value; - if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){ - //if not already set, propagate as decision - //d_quantEngine->getOutputChannel().propagateAsDecision( it->second ); - Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl; - } - } -} - Node InstantiationEngine::getNextDecisionRequest(){ //propagate as decision all counterexample literals that are not asserted - for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){ - bool value; - if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){ - //if not already set, propagate as decision - Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl; - return it->second; + if( options::cbqi() ){ + for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( hasAddedCbqiLemma( f ) ){ + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + //if not already set, propagate as decision + Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << cel << std::endl; + return cel; + } + } } } return Node::null(); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 896e17ac8..6d995097a 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -30,16 +30,17 @@ private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** status of instantiation round (one of InstStrategy::STATUS_*) */ int d_inst_round_status; - /** map from universal quantifiers to their counterexample literals */ - std::map< Node, Node > d_ce_lit; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; /** inst round counter */ int d_ierCounter; + /** whether each quantifier is active */ + std::map< Node, bool > d_quant_active; + /** whether we have added cbqi lemma */ + std::map< Node, bool > d_added_cbqi_lemma; private: - bool hasAddedCbqiLemma( Node f ); - void addCbqiLemma( Node f ); -private: + /** has added cbqi lemma */ + bool hasAddedCbqiLemma( Node f ) { return d_added_cbqi_lemma.find( f )!=d_added_cbqi_lemma.end(); } /** helper functions */ bool hasNonArithmeticVariable( Node f ); bool hasApplyUf( Node f ); @@ -65,11 +66,7 @@ public: void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } - void propagate( Theory::Effort level ); Node getNextDecisionRequest(); -public: - /** get the corresponding counterexample literal for quantified formula node n */ - Node getCounterexampleLiteralFor( Node f ) { return d_ce_lit.find( f )==d_ce_lit.end() ? Node::null() : d_ce_lit[ f ]; } };/* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 6fa02a8d3..3d1ca8f0d 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -51,6 +51,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" ); } TheoryEngineModelBuilder::processBuildModel( m, fullModel ); + //mark that the model has been set + fm->markModelSet(); }else{ d_curr_model = fm; //build model for relevant symbols contained in quantified formulas @@ -338,8 +340,8 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) //for each asserted quantifier f, // - determine selection literals // - check which function/predicates have good and bad definitions for satisfying f - for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); - it != d_qe->d_phase_reqs[f].end(); ++it ){ + QuantPhaseReq* qpr = d_qe->getPhaseRequirements( f ); + for( std::map< Node, bool >::iterator it = qpr->d_phase_reqs.begin(); it != qpr->d_phase_reqs.end(); ++it ){ //the literal n is phase-required for quantifier f Node n = it->first; Node gn = d_qe->getTermDatabase()->getModelBasis( f, n ); @@ -465,8 +467,10 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ std::vector< Node > tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); + std::vector< Node > children; + children.push_back( lit ); + children.push_back( !phase ? fm->d_true : fm->d_false ); + Node eq = d_qe->getTermDatabase()->mkNodeInstConstant( IFF, children, f ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms @@ -532,7 +536,7 @@ void ModelEngineBuilderInstGen::analyzeQuantifiers( FirstOrderModel* fm ){ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ //determine selection formula, set terms in selection formula as being selected - Node s = getSelectionFormula( d_qe->getTermDatabase()->getCounterexampleBody( f ), + Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ), d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 ); Trace("sel-form") << "Selection formula for " << f << " is " << s << std::endl; if( !s.isNull() ){ @@ -580,7 +584,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ if( !m.isComplete( f ) ){ Trace("inst-gen-debug") << "- partial inst" << std::endl; //if the instantiation does not yet exist - if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true, NULL ) ){ + if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ //get the partial instantiation pf Node pf = d_qe->getInstantiation( fp, mp ); Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; @@ -732,10 +736,10 @@ bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption Node ModelEngineBuilderInstGen::getParentQuantifier( Node f ){ std::map< Node, Node >::iterator it = d_sub_quant_parent.find( f ); - if( it==d_sub_quant_parent.end() ){ + if( it==d_sub_quant_parent.end() || it->second.isNull() ){ return f; }else{ - return getParentQuantifier( it->second ); + return it->second; } } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 0b73f3c8b..7952d3c21 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -115,7 +115,6 @@ void ModelEngine::check( Theory::Effort e ){ if( options::produceModels() ){ // finish building the model in the standard way d_builder->buildModel( fm, true ); - d_quantEngine->d_model_set = true; } //if the check was incomplete, we must set incomplete flag if( d_incomplete_check ){ @@ -256,7 +255,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ //if evaluate(...)==1, then the instantiation is already true in the model // depIndex is the index of the least significant variable that this evaluation relies upon depIndex = riter.getNumTerms()-1; - eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex, &riter ); + eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; }else{ diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index f930fbec7..377fe9aa9 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -64,7 +64,6 @@ public: void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } - void propagate( Theory::Effort level ){} void debugPrint( const char* c ); public: /** statistics class */ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp new file mode 100755 index 000000000..7a2d965b8 --- /dev/null +++ b/src/theory/quantifiers/quant_util.cpp @@ -0,0 +1,144 @@ +/********************* */
+/*! \file quant_util.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: bobot, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of quantifier utilities
+ **/
+
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/inst_match.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+
+void QuantRelevance::registerQuantifier( Node f ){
+ //compute symbols in f
+ std::vector< Node > syms;
+ computeSymbols( f[1], syms );
+ d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() );
+ //set initial relevance
+ int minRelevance = -1;
+ for( int i=0; i<(int)syms.size(); i++ ){
+ d_syms_quants[ syms[i] ].push_back( f );
+ int r = getRelevance( syms[i] );
+ if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){
+ minRelevance = r;
+ }
+ }
+ if( minRelevance!=-1 ){
+ setRelevance( f, minRelevance+1 );
+ }
+}
+
+
+/** compute symbols */
+void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
+ if( std::find( syms.begin(), syms.end(), op )==syms.end() ){
+ syms.push_back( op );
+ }
+ }
+ if( n.getKind()!=FORALL ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ computeSymbols( n[i], syms );
+ }
+ }
+}
+
+/** set relevance */
+void QuantRelevance::setRelevance( Node s, int r ){
+ if( d_computeRel ){
+ int rOld = getRelevance( s );
+ if( rOld==-1 || r<rOld ){
+ d_relevance[s] = r;
+ if( s.getKind()==FORALL ){
+ for( int i=0; i<(int)d_syms[s].size(); i++ ){
+ setRelevance( d_syms[s][i], r );
+ }
+ }else{
+ for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){
+ setRelevance( d_syms_quants[s][i], r+1 );
+ }
+ }
+ }
+ }
+}
+
+
+QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
+ std::map< Node, int > phaseReqs2;
+ computePhaseReqs( n, false, phaseReqs2 );
+ for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
+ if( it->second==1 ){
+ d_phase_reqs[ it->first ] = true;
+ }else if( it->second==-1 ){
+ d_phase_reqs[ it->first ] = false;
+ }
+ }
+ Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
+ //now, compute if any patterns are equality required
+ if( computeEq ){
+ for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
+ Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl;
+ if( it->first.getKind()==EQUAL ){
+ if( it->first[0].hasAttribute(InstConstantAttribute()) ){
+ if( !it->first[1].hasAttribute(InstConstantAttribute()) ){
+ d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
+ d_phase_reqs_equality[ it->first[0] ] = it->second;
+ Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
+ }
+ }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){
+ d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
+ d_phase_reqs_equality[ it->first[1] ] = it->second;
+ Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
+ }
+ }
+ }
+ }
+}
+
+void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
+ bool newReqPol = false;
+ bool newPolarity;
+ if( n.getKind()==NOT ){
+ newReqPol = true;
+ newPolarity = !polarity;
+ }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
+ if( !polarity ){
+ newReqPol = true;
+ newPolarity = false;
+ }
+ }else if( n.getKind()==AND ){
+ if( polarity ){
+ newReqPol = true;
+ newPolarity = true;
+ }
+ }else{
+ int val = polarity ? 1 : -1;
+ if( phaseReqs.find( n )==phaseReqs.end() ){
+ phaseReqs[n] = val;
+ }else if( val!=phaseReqs[n] ){
+ phaseReqs[n] = 0;
+ }
+ }
+ if( newReqPol ){
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( n.getKind()==IMPLIES && i==0 ){
+ computePhaseReqs( n[i], !newPolarity, phaseReqs );
+ }else{
+ computePhaseReqs( n[i], newPolarity, phaseReqs );
+ }
+ }
+ }
+}
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h new file mode 100755 index 000000000..1479f910e --- /dev/null +++ b/src/theory/quantifiers/quant_util.h @@ -0,0 +1,77 @@ +/********************* */
+/*! \file quant_util.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters, bobot
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief quantifier util
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANT_UTIL_H
+#define __CVC4__THEORY__QUANT_UTIL_H
+
+#include "theory/theory.h"
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+
+
+class QuantRelevance
+{
+private:
+ /** for computing relavance */
+ bool d_computeRel;
+ /** map from quantifiers to symbols they contain */
+ std::map< Node, std::vector< Node > > d_syms;
+ /** map from symbols to quantifiers */
+ std::map< Node, std::vector< Node > > d_syms_quants;
+ /** relevance for quantifiers and symbols */
+ std::map< Node, int > d_relevance;
+ /** compute symbols */
+ void computeSymbols( Node n, std::vector< Node >& syms );
+public:
+ QuantRelevance( bool cr ) : d_computeRel( cr ){}
+ ~QuantRelevance(){}
+ /** register quantifier */
+ void registerQuantifier( Node f );
+ /** set relevance */
+ void setRelevance( Node s, int r );
+ /** get relevance */
+ int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }
+ /** get number of quantifiers for symbol s */
+ int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }
+};
+
+class QuantPhaseReq
+{
+private:
+ /** helper functions compute phase requirements */
+ void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
+public:
+ QuantPhaseReq( Node n, bool computeEq = false );
+ ~QuantPhaseReq(){}
+ /** is phase required */
+ bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
+ /** get phase requirement */
+ bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }
+ /** phase requirements for each quantifier for each instantiation literal */
+ std::map< Node, bool > d_phase_reqs;
+ std::map< Node, bool > d_phase_reqs_equality;
+ std::map< Node, Node > d_phase_reqs_equality_term;
+};
+
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d21ea252c..7bf1f30e9 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -281,11 +281,10 @@ Node QuantifiersRewriter::computeNNF( Node body ){ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ //Notice() << "Compute var elimination for " << f << std::endl; - std::map< Node, bool > litPhaseReq; - QuantifiersEngine::computePhaseReqs( body, false, litPhaseReq ); + QuantPhaseReq qpr( body ); std::vector< Node > vars; std::vector< Node > subs; - for( std::map< Node, bool >::iterator it = litPhaseReq.begin(); it != litPhaseReq.end(); ++it ){ + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; if( it->first.getKind()==EQUAL ){ if( it->second ){ diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 5261e6876..7b4440c31 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -72,12 +72,12 @@ void RelevantDomain::compute(){ for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ Node f = d_model->getAssertedQuantifier( i ); //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) - if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, f ) ){ + if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getInstConstantBody( f ), Node::null(), -1, f ) ){ success = false; } //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) RepDomain range; - if( extendFunctionDomains( d_qe->getTermDatabase()->getCounterexampleBody( f ), range ) ){ + if( extendFunctionDomains( d_qe->getTermDatabase()->getInstConstantBody( f ), range ) ){ success = false; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0614bb22a..c8c884974 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -259,7 +259,7 @@ Node TermDb::getModelBasis( Node f, Node n ){ Node TermDb::getModelBasisBody( Node f ){ if( d_model_basis_body.find( f )==d_model_basis_body.end() ){ - Node n = getCounterexampleBody( f ); + Node n = getInstConstantBody( f ); d_model_basis_body[f] = getModelBasis( f, n ); } return d_model_basis_body[f]; @@ -301,17 +301,6 @@ void TermDb::makeInstantiationConstantsFor( Node f ){ } } -void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){ - if( !n.hasAttribute(InstLevelAttribute()) ){ - InstLevelAttribute ila; - n.setAttribute(ila,level); - } - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - setInstantiationLevelAttr( n[i], level ); - } -} - - void TermDb::setInstantiationConstantAttr( Node n, Node f ){ if( !n.hasAttribute(InstConstantAttribute()) ){ bool setAttr = false; @@ -336,18 +325,49 @@ void TermDb::setInstantiationConstantAttr( Node n, Node f ){ } -Node TermDb::getCounterexampleBody( Node f ){ - std::map< Node, Node >::iterator it = d_counterexample_body.find( f ); - if( it==d_counterexample_body.end() ){ +Node TermDb::getInstConstantBody( Node f ){ + std::map< Node, Node >::iterator it = d_inst_const_body.find( f ); + if( it==d_inst_const_body.end() ){ makeInstantiationConstantsFor( f ); - Node n = getSubstitutedNode( f[1], f ); - d_counterexample_body[ f ] = n; + Node n = getInstConstantNode( f[1], f ); + d_inst_const_body[ f ] = n; return n; }else{ return it->second; } } +Node TermDb::getCounterexampleLiteral( Node f ){ + if( d_ce_lit.find( f )==d_ce_lit.end() ){ + Node ceBody = getInstConstantBody( f ); + Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); + d_ce_lit[ f ] = ceLit; + setInstantiationConstantAttr( ceLit, f ); + } + return d_ce_lit[ f ]; +} + +Node TermDb::getInstConstantNode( Node n, Node f ){ + return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); +} + +Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars, + const std::vector<Node> & inst_constants){ + Node n2 = n.substitute( vars.begin(), vars.end(), + inst_constants.begin(), + inst_constants.end() ); + setInstantiationConstantAttr( n2, f ); + return n2; +} + +Node TermDb::mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ){ + Node n = NodeManager::currentNM()->mkNode( k, children ); + setInstantiationConstantAttr( n, f ); + return n; +} + + + Node TermDb::getSkolemizedBody( Node f ){ Assert( f.getKind()==FORALL ); if( d_skolem_body.find( f )==d_skolem_body.end() ){ @@ -367,17 +387,14 @@ Node TermDb::getSkolemizedBody( Node f ){ } -Node TermDb::getSubstitutedNode( Node n, Node f ){ - return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); -} - -Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars, - const std::vector<Node> & inst_constants){ - Node n2 = n.substitute( vars.begin(), vars.end(), - inst_constants.begin(), - inst_constants.end() ); - setInstantiationConstantAttr( n2, f ); - return n2; +void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){ + if( !n.hasAttribute(InstLevelAttribute()) ){ + InstLevelAttribute ila; + n.setAttribute(ila,level); + } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setInstantiationLevelAttr( n[i], level ); + } } Node TermDb::getFreeVariableForInstConstant( Node n ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 64f3d4980..d63eebf7e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -109,6 +109,8 @@ public: /* Todo replace int by size_t */ std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents; const std::vector<Node> & getParents(TNode n, TNode f, int arg); + +//for model basis private: //map from types to model basis terms std::map< TypeNode, Node > d_model_basis_term; @@ -116,6 +118,8 @@ private: std::map< Node, Node > d_model_basis_op_term; //map from instantiation terms to their model basis equivalent std::map< Node, Node > d_model_basis_body; + /** map from universal quantifiers to model basis terms */ + std::map< Node, std::vector< Node > > d_model_basis_terms; // compute model basis arg void computeModelBasisArgAttribute( Node n ); public: @@ -127,46 +131,37 @@ public: Node getModelBasis( Node f, Node n ); //get model basis body Node getModelBasisBody( Node f ); + +//for inst constant private: - /** map from universal quantifiers to the list of variables */ - std::map< Node, std::vector< Node > > d_vars; - /** map from universal quantifiers to the list of skolem constants */ - std::map< Node, std::vector< Node > > d_skolem_constants; - /** model basis terms */ - std::map< Node, std::vector< Node > > d_model_basis_terms; - /** map from universal quantifiers to their skolemized body */ - std::map< Node, Node > d_skolem_body; + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; + /** map from universal quantifiers to their inst constant body */ + std::map< Node, Node > d_inst_const_body; + /** map from universal quantifiers to their counterexample literals */ + std::map< Node, Node > d_ce_lit; /** instantiation constants to universal quantifiers */ std::map< Node, Node > d_inst_constants_map; - /** map from universal quantifiers to their counterexample body */ - std::map< Node, Node > d_counterexample_body; - /** free variable for instantiation constant type */ - std::map< TypeNode, Node > d_free_vars; -private: /** make instantiation constants for */ void makeInstantiationConstantsFor( Node f ); -public: - /** map from universal quantifiers to the list of instantiation constants */ - std::map< Node, std::vector< Node > > d_inst_constants; - /** set instantiation level attr */ - void setInstantiationLevelAttr( Node n, uint64_t level ); /** set instantiation constant attr */ void setInstantiationConstantAttr( Node n, Node f ); +public: /** get the i^th instantiation constant of f */ Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } /** get number of instantiation constants for f */ int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); } /** get the ce body f[e/x] */ - Node getCounterexampleBody( Node f ); - /** get the skolemized body f[e/x] */ - Node getSkolemizedBody( Node f ); + Node getInstConstantBody( Node f ); + /** get counterexample literal (for cbqi) */ + Node getCounterexampleLiteral( Node f ); /** returns node n with bound vars of f replaced by instantiation constants of f node n : is the futur pattern node f : is the quantifier containing which bind the variable return a pattern where the variable are replaced by variable for instantiation. */ - Node getSubstitutedNode( Node n, Node f ); + Node getInstConstantNode( Node n, Node f ); /** same as before but node f is just linked to the new pattern by the applied attribute vars the bind variable @@ -175,15 +170,37 @@ public: Node convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars, const std::vector<Node> & nvars); + /** get iff term */ + Node getInstConstantIffTerm( Node n, bool pol ); + /** make node, validating the inst constant attribute */ + Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ); + +//for skolem +private: + /** map from universal quantifiers to the list of skolem constants */ + std::map< Node, std::vector< Node > > d_skolem_constants; + /** map from universal quantifiers to their skolemized body */ + std::map< Node, Node > d_skolem_body; +public: + /** get the skolemized body f[e/x] */ + Node getSkolemizedBody( Node f ); + +//miscellaneous +private: + /** map from universal quantifiers to the list of variables */ + std::map< Node, std::vector< Node > > d_vars; + /** free variable for instantiation constant type */ + std::map< TypeNode, Node > d_free_vars; +public: /** get free variable for instantiation constant */ Node getFreeVariableForInstConstant( Node n ); + /** set instantiation level attr */ + void setInstantiationLevelAttr( Node n, uint64_t level ); //for triggers private: /** helper function for compute var contains */ void computeVarContains2( Node n, Node parent ); - /** all triggers will be stored in this trie */ - TrTrie d_tr_trie; /** var contains */ std::map< TNode, std::vector< TNode > > d_var_contains; public: @@ -195,6 +212,10 @@ public: void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); +private: + /** all triggers will be stored in this trie */ + TrTrie d_tr_trie; +public: /** get trigger */ inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); } /** add trigger */ diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp index fc5c66b94..eabb4ceda 100644 --- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp +++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp @@ -34,10 +34,10 @@ void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){ if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ Debug("quant-quant-assert") << " -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl; - setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ Debug("quant-quant-assert") << " -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl; - setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); } } } @@ -53,11 +53,9 @@ int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e return InstStrategy::STATUS_UNFINISHED; }else if( e==5 ){ //add random addition - if( isOwnerOf( f ) ){ - InstMatch m; - if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_statistics.d_instantiations); - } + InstMatch m; + if( d_quantEngine->addInstantiation( f, m ) ){ + ++(d_statistics.d_instantiations); } } return InstStrategy::STATUS_UNKNOWN; |