diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
commit | 1c779966545190efa59b019572237562eea66dbf (patch) | |
tree | f827fe0e4bcbbca8c84174f815948b3212391423 /src/theory/quantifiers/model_engine.cpp | |
parent | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (diff) |
more minor updates to inst gen and representative selection, clean up of equality query
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 34 |
1 files changed, 8 insertions, 26 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 87f842862..defb58bf2 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -153,19 +153,6 @@ 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(); @@ -177,20 +164,11 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " "; for( size_t i=0; i<it->second.size(); i++ ){ - Trace("model-engine-debug") << it->second[i] << " "; + //Trace("model-engine-debug") << it->second[i] << " "; + Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getInternalRepresentative( it->second[i] ); + Trace("model-engine-debug") << r << " "; } 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; - } } } } @@ -242,6 +220,7 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; } + d_statistics.d_exh_inst_lemmas += addedLemmas; return addedLemmas; } @@ -361,13 +340,15 @@ ModelEngine::Statistics::Statistics(): d_eval_formulas("ModelEngine::Eval_Formulas", 0 ), d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ), d_eval_lits("ModelEngine::Eval_Lits", 0 ), - d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ) + d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ), + d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_eval_formulas); StatisticsRegistry::registerStat(&d_eval_uf_terms); StatisticsRegistry::registerStat(&d_eval_lits); StatisticsRegistry::registerStat(&d_eval_lits_unknown); + StatisticsRegistry::registerStat(&d_exh_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ @@ -376,6 +357,7 @@ ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_eval_uf_terms); StatisticsRegistry::unregisterStat(&d_eval_lits); StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); + StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); } |