diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 48 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 5 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_util.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 |
10 files changed, 84 insertions, 49 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 36f265c30..4a89a4dd3 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -91,7 +91,7 @@ void InstMatch::debugPrint( const char* c ){ // Debug( c ) << std::endl; //} } - +/* void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ for( size_t i=0; i<f[0].getNumChildren(); i++ ){ Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); @@ -113,13 +113,15 @@ void InstMatch::makeInternal( QuantifiersEngine* qe ){ } } } - +*/ void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); - if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); + if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){ + d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second ); } + //if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){ + // d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); + //} } } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 426adc02d..43c0d26c7 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -55,9 +55,9 @@ public: /** is complete? */ bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } /** make complete */ - void makeComplete( Node f, QuantifiersEngine* qe ); + //void makeComplete( Node f, QuantifiersEngine* qe ); /** make internal: ensure that no term in d_map contains instantiation constants */ - void makeInternal( QuantifiersEngine* qe ); + //void makeInternal( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); /** get value */ @@ -96,7 +96,8 @@ public: //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ; Assert( !var.isNull() ); Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations - var.getType() == n.getType() ); + //var.getType() == n.getType() + n.getType().isSubtypeOf( var.getType() ) ); d_map[var] = n; } size_t size(){ return d_map.size(); } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 027ac67eb..8d935a323 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -28,7 +28,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ +QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){ } @@ -67,7 +67,12 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl; //reset the quantifiers engine Debug("inst-engine-ctrl") << "Reset IE" << std::endl; - d_quantEngine->resetInstantiationRound( effort ); + //reset the instantiators + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ + if( d_quantEngine->getInstantiator( i ) ){ + d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort ); + } + } //iterate over an internal effort level e int e = 0; int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2; @@ -125,22 +130,26 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } } -void InstantiationEngine::check( Theory::Effort e ){ +bool InstantiationEngine::needsCheck( Theory::Effort e ){ if( e==Theory::EFFORT_FULL ){ d_ierCounter++; } //determine if we should perform check, based on instWhenMode - bool performCheck = false; + d_performCheck = false; if( options::instWhenMode()==INST_WHEN_FULL ){ - performCheck = ( e >= Theory::EFFORT_FULL ); + d_performCheck = ( e >= Theory::EFFORT_FULL ); }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){ - performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); + d_performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL ); }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){ - performCheck = ( e >= Theory::EFFORT_LAST_CALL ); + d_performCheck = ( e >= Theory::EFFORT_LAST_CALL ); }else{ - performCheck = true; + d_performCheck = true; } - if( performCheck ){ + return d_performCheck; +} + +void InstantiationEngine::check( Theory::Effort e ){ + if( d_performCheck ){ Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl; double clSet = 0; if( Trace.isOn("inst-engine") ){ diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 6d995097a..b3bbbce4a 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -34,6 +34,7 @@ private: bool d_setIncomplete; /** inst round counter */ int d_ierCounter; + bool d_performCheck; /** whether each quantifier is active */ std::map< Node, bool > d_quant_active; /** whether we have added cbqi lemma */ @@ -62,6 +63,7 @@ public: InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true ); ~InstantiationEngine(){} + bool needsCheck( Theory::Effort e ); void check( Theory::Effort e ); void registerQuantifier( Node f ); void assertNode( Node f ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index f2e195d2e..8b34a3a12 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -33,20 +33,20 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -bool TermArgBasisTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ +bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ if( argIndex<(int)n.getNumChildren() ){ Node r; if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){ r = n[ argIndex ]; }else{ - r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] ); + r = fm->getRepresentative( n[ argIndex ] ); } std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r ); if( it==d_data.end() ){ - d_data[r].addTerm2( qe, n, argIndex+1 ); + d_data[r].addTerm2( fm, n, argIndex+1 ); return true; }else{ - return it->second.addTerm2( qe, n, argIndex+1 ); + return it->second.addTerm2( fm, n, argIndex+1 ); } }else{ return false; @@ -99,6 +99,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } } } + //END FOR DEBUGGING }else{ d_curr_model = fm; d_addedLemmas = 0; @@ -162,6 +163,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){ break; } + }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + d_numQuantSat++; } } Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / "; @@ -267,7 +270,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ if( !n.getAttribute(BasisNoMatchAttribute()) ){ //need to consider if it is not congruent modulo model basis - if( !tabt.addTerm( d_qe, n ) ){ + if( !tabt.addTerm( fm, n ) ){ BasisNoMatchAttribute bnma; n.setAttribute(bnma,true); } @@ -311,7 +314,7 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ } bool ModelEngineBuilder::optExhInstNonInstGenQuant(){ - return true; + return options::fmfNewInstGen(); } void ModelEngineBuilder::setEffort( int effort ){ diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index d0348dff8..7331daf8e 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -23,6 +23,7 @@ namespace CVC4 { namespace theory { +namespace quantifiers { /** Attribute true for nodes that should not be used when considered for inst-gen basis */ struct BasisNoMatchAttributeId {}; @@ -35,17 +36,14 @@ typedef expr::Attribute< BasisNoMatchAttributeId, class TermArgBasisTrie { private: - bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex ); + bool addTerm2( FirstOrderModel* fm, Node n, int argIndex ); public: /** the data */ std::map< Node, TermArgBasisTrie > d_data; public: - bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } + bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); } };/* class TermArgBasisTrie */ - -namespace quantifiers { - /** model builder class * This class is capable of building candidate models based on the current quantified formulas * that are asserted. Use: diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 40a61f7c5..87f842862 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -52,21 +52,19 @@ void ModelEngine::check( Theory::Effort e ){ FirstOrderModel* fm = d_quantEngine->getModel(); //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers int addedLemmas = 0; - Trace("model-engine") << "---Model Engine Round---" << std::endl; + //quantifiers are initialized, we begin an instantiation round + double clSet = 0; + if( Trace.isOn("model-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + } + ++(d_statistics.d_inst_rounds); //two effort levels: first try exhaustive instantiation without axioms, then with. int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; for( int effort=startEffort; effort<2; effort++ ){ // for effort = 0, we only instantiate non-axioms // for effort = 1, we instantiate everything if( addedLemmas==0 ){ - //quantifiers are initialized, we begin an instantiation round - double clSet = 0; - if( Trace.isOn("model-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - } - ++(d_statistics.d_inst_rounds); - //reset the quantifiers engine - d_quantEngine->resetInstantiationRound( e ); + Trace("model-engine") << "---Model Engine Round---" << std::endl; //initialize the model Trace("model-engine-debug") << "Build model..." << std::endl; d_builder->setEffort( effort ); @@ -91,10 +89,6 @@ void ModelEngine::check( Theory::Effort e ){ //check quantifiers that inst-gen didn't apply to addedLemmas += checkModel( check_model_no_inst_gen ); } - if( Trace.isOn("model-engine") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; - } } if( addedLemmas==0 ){ //if we have not added lemmas yet and axiomInstMode=trust, then we are done @@ -107,6 +101,10 @@ void ModelEngine::check( Theory::Effort e ){ } } } + if( Trace.isOn("model-engine") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + } if( addedLemmas==0 ){ Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; //CVC4 will answer SAT or unknown @@ -155,6 +153,19 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){ #endif } +bool containsNN( Node n, Node nc ){ + if( n==nc ){ + return true; + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( containsNN( n[i], nc ) ){ + return true; + } + } + return false; + } +} + int ModelEngine::checkModel( int checkOption ){ int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); @@ -169,6 +180,17 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine-debug") << it->second[i] << " "; } Trace("model-engine-debug") << std::endl; + for( size_t i=0; i<it->second.size(); i++ ){ + std::vector< Node > eqc; + d_quantEngine->getEqualityQuery()->getEquivalenceClass( it->second[i], eqc ); + Trace("model-engine-debug-eqc") << " " << it->second[i] << " : { "; + for( size_t j=0; j<eqc.size(); j++ ){ + if( it->second[i]!=eqc[j] && containsNN( it->second[i], eqc[j] ) ){ + Trace("model-engine-debug-eqc") << eqc[j] << " "; + } + } + Trace("model-engine-debug-eqc") << "}" << std::endl; + } } } } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 724c76e82..5802a05cd 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -61,9 +61,12 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false option userPatternsQuant /--ignore-user-patterns bool :default true ignore user-provided patterns for quantifier instantiation -option flipDecision --enable-flip-decision/ bool :default false +option flipDecision --flip-decision/ bool :default false turns on flip decision heuristic +option internalReps --disable-quant-internal-reps/ bool :default true + disables instantiating with representatives chosen by quantifiers engine + option finiteModelFind --finite-model-find bool :default false use finite model finding heuristic for quantifier instantiation diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 18aaab01f..bb6855c47 100755 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -77,6 +77,8 @@ class EqualityQuery { public:
EqualityQuery(){}
virtual ~EqualityQuery(){};
+ /** reset */
+ virtual void reset() = 0;
/** contains term */
virtual bool hasTerm( Node a ) = 0;
/** get the representative of the equivalence class of a */
@@ -85,11 +87,6 @@ public: virtual bool areEqual( Node a, Node b ) = 0;
/** returns true is a and b are disequal in the current context */
virtual bool areDisequal( Node a, Node b ) = 0;
- /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
- If cbqi is active, this will return a term in the equivalence class of "a" that does
- not contain instantiation constants, if such a term exists.
- */
- virtual Node getInternalRepresentative( Node a ) = 0;
/** get the equality engine associated with this query */
virtual eq::EqualityEngine* getEngine() = 0;
/** get the equivalence class of a */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 493b9e931..d637fa25f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -144,7 +144,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ computeModelBasisArgAttribute( n ); if( !n.getAttribute(NoMatchAttribute()) ){ if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){ - //only set no match if not a model basis argument term NoMatchAttribute nma; n.setAttribute(nma,true); congruentCount++; @@ -171,7 +170,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !en.getAttribute(NoMatchAttribute()) ){ Node op = en.getOperator(); if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ - //only set no match if not a model basis argument term NoMatchAttribute nma; en.setAttribute(nma,true); congruentCount++; |