diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
commit | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (patch) | |
tree | a79f142c5b6fbeaec34978f8da2b2db308a33e79 /src/theory/quantifiers/model_engine.cpp | |
parent | 5b4c416608bda1df62e1ffe7131648a89882ddc7 (diff) |
cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 48 |
1 files changed, 35 insertions, 13 deletions
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; + } } } } |