From 21f8e233e46fae32eaa6d2d4d5b4d0f36c36ba7f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 10 Jan 2014 10:50:56 -0600 Subject: [PATCH] Add stats to quantifiers conflict find. Added option for qcf. Working on handling non-APPLY_UF terms. --- src/theory/quantifiers/model_engine.cpp | 8 ++- src/theory/quantifiers/model_engine.h | 1 + src/theory/quantifiers/modes.h | 9 ++- src/theory/quantifiers/options | 5 +- src/theory/quantifiers/options_handlers.h | 29 ++++++++++ .../quantifiers/quant_conflict_find.cpp | 56 ++++++++++++++----- src/theory/quantifiers/quant_conflict_find.h | 11 ++++ 7 files changed, 102 insertions(+), 17 deletions(-) diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index bc717bbbc..9e3e77c8e 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -242,7 +242,6 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl; Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_totalLemmas << std::endl; - d_statistics.d_exh_inst_lemmas += d_addedLemmas; return d_addedLemmas; } @@ -256,6 +255,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_triedLemmas += d_builder->d_triedLemmas; d_addedLemmas += d_builder->d_addedLemmas; d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check; + d_statistics.d_mbqi_inst_lemmas += d_builder->d_addedLemmas; }else{ Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; Debug("inst-fmf-ei") << " Instantiation Constants: "; @@ -287,6 +287,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_addedLemmas += addedLemmas; d_triedLemmas += triedLemmas; + d_statistics.d_exh_inst_lemmas += addedLemmas; } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round d_incomplete_check = d_incomplete_check || riter.d_incomplete; @@ -310,15 +311,18 @@ void ModelEngine::debugPrint( const char* c ){ ModelEngine::Statistics::Statistics(): d_inst_rounds("ModelEngine::Inst_Rounds", 0), - d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 ) + d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ), + d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_exh_inst_lemmas); + StatisticsRegistry::registerStat(&d_mbqi_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); + StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index fcbba7aee..ba54d7ba4 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -68,6 +68,7 @@ public: public: IntStat d_inst_rounds; IntStat d_exh_inst_lemmas; + IntStat d_mbqi_inst_lemmas; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index d5c755ad2..7a7ce9b54 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -70,7 +70,14 @@ typedef enum { MBQI_INTERVAL, } MbqiMode; - +typedef enum { + /** default, apply at full effort */ + QCF_WHEN_MODE_DEFAULT, + /** apply at standard effort */ + QCF_WHEN_MODE_STD, + /** default */ + QCF_WHEN_MODE_STD_H, +} QcfWhenMode; }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 652526cc9..dc016be3f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -120,6 +120,9 @@ option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode policy for instantiating axioms option quantConflictFind --quant-cf bool :default false - enable eager conflict find mechanism for quantifiers + enable conflict find mechanism for quantifiers +option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" + when to invoke conflict find mechanism for quantifiers + endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 4929fa60b..e0b1e30e8 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -97,6 +97,19 @@ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ \n\ "; +static const std::string qcfWhenModeHelp = "\ +Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ +\n\ +default \n\ ++ Default, apply conflict finding at full effort.\n\ +\n\ +std \n\ ++ Apply conflict finding at standard effort.\n\ +\n\ +std-h \n\ ++ Apply conflict finding at standard effort when heuristic says to. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -186,6 +199,22 @@ inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) thr } +inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return QCF_WHEN_MODE_DEFAULT; + } else if(optarg == "std") { + return QCF_WHEN_MODE_STD; + } else if(optarg == "std-h") { + return QCF_WHEN_MODE_STD_H; + } else if(optarg == "help") { + puts(qcfWhenModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-cf-when: `") + + optarg + "'. Try --quant-cf-when help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 58840989d..1bf53db91 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -306,18 +306,20 @@ EqRegistry * QuantConflictFind::getEqRegistry( bool polarity, Node lit, bool doC void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms ) { Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) ); if( lit.getKind()==EQUAL ){ + bool allUf = false; for( unsigned i=0; i<2; i++ ){ if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){ - if( lit[i].getKind()==APPLY_UF ){ - terms.push_back( lit[i] ); - }else if( lit[i].getKind()==BOUND_VARIABLE ){ + if( lit[i].getKind()==BOUND_VARIABLE ){ //do not handle variable equalities terms.clear(); return; + }else{ + allUf = allUf && lit[i].getKind()==APPLY_UF; + terms.push_back( lit[i] ); } } } - if( terms.size()==2 && isLessThan( terms[1], terms[0] ) ){ + if( terms.size()==2 && allUf && isLessThan( terms[1], terms[0] ) ){ Node t = terms[0]; terms[0] = terms[1]; terms[1] = t; @@ -544,7 +546,8 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl; }else{ bool addedLemma = false; - if( level==Theory::EFFORT_FULL ){ + if( d_performCheck ){ + ++(d_statistics.d_inst_rounds); double clSet = 0; if( Trace.isOn("qcf-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); @@ -648,6 +651,7 @@ void QuantConflictFind::check( Theory::Effort level ) { d_quantEngine->flushLemmas(); d_conflict.set( true ); addedLemma = true; + ++(d_statistics.d_conflict_inst); break; }else{ Trace("qcf-check") << " ... Failed to add instantiation" << std::endl; @@ -678,7 +682,11 @@ void QuantConflictFind::check( Theory::Effort level ) { } bool QuantConflictFind::needsCheck( Theory::Effort level ) { - return !d_conflict && level==Theory::EFFORT_FULL; + d_performCheck = false; + if( !d_conflict && level==Theory::EFFORT_FULL ){ + d_performCheck = true; + } + return d_performCheck; } void QuantConflictFind::computeRelevantEqr() { @@ -1091,7 +1099,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo d_n = n; qni_apps.push_back( n ); }else{ - //unknown term + //for now, unknown term d_type = typ_invalid; } }else{ @@ -1143,10 +1151,20 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo if( d_n.getKind()==APPLY_UF || d_n.getKind()==EQUAL ){ //get the applications (in order) that will be matching p->getEqRegistryApps( d_n, qni_apps ); + bool isValid = true; if( qni_apps.size()>0 ){ - d_type =typ_valid_lit; + for( unsigned i=0; id_qinfo[q].isVar( d_n[i] ) ){ isValid = false; @@ -1172,13 +1190,12 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo for( unsigned i=0; i d_conflict; + bool d_performCheck; //void registerAssertion( Node n ); void registerQuant( Node q, Node n, bool hasPol, bool pol ); void flatten( Node q, Node n ); @@ -226,6 +227,16 @@ private: std::map< Node, int > d_quant_id; void debugPrintQuant( const char * c, Node q ); void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true ); +public: + /** statistics class */ + class Statistics { + public: + IntStat d_inst_rounds; + IntStat d_conflict_inst; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; }; } -- 2.30.2