diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 22:36:55 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 22:36:55 -0600 |
commit | 2ce92038d8455637e313a1c2d0ce5d31a3d42b10 (patch) | |
tree | ce599c2e981bbd79d024e90cff6e97468b42712b /src/theory/quantifiers | |
parent | 93f084750d8a76d63fc74d242944bce0635c2194 (diff) |
Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 28 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 7 |
7 files changed, 47 insertions, 48 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index c94775aec..797ca8f70 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -169,7 +169,7 @@ void FirstOrderModelIG::resetEvaluate(){ // each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ ++d_eval_formulas; - //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; + Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl; //Notice() << "Eval " << n << std::endl; if( n.getKind()==NOT ){ int val = evaluate( n[0], depIndex, ri ); @@ -447,7 +447,7 @@ void FirstOrderModelIG::makeEvalUfModel( Node n ){ d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] ); d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] ); //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl; - //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 ); + //d_eval_uf_model[n].debugPrint( std::cout, d_qe->getModel(), 2 ); } } } @@ -578,7 +578,7 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a void FirstOrderModelFmc::processInitialize( bool ispre ) { if( ispre ){ - if( options::fmfFmcInterval() && intervalOp.isNull() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && intervalOp.isNull() ){ std::vector< TypeNode > types; for(unsigned i=0; i<2; i++){ types.push_back(NodeManager::currentNM()->integerType()); @@ -616,7 +616,7 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) { Node FirstOrderModelFmc::getStarElement(TypeNode tn) { Node st = getStar(tn); - if( options::fmfFmcInterval() && tn.isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && tn.isInteger() ){ st = getInterval( st, st ); } return st; diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 174e26a5a..c7d7b7415 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -60,9 +60,9 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true; } } - if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){ + if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){ //for star: check if all children are defined and have generalizations - if( options::fmfFmcCoverSimplify() && c[index]==st ){ + if( c[index]==st ){ ///options::fmfFmcCoverSimplify() //check if all children exist and are complete int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0); if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){ @@ -92,7 +92,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> return d_data; }else{ int minIndex = -1; - if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){ for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ //if( !m->isInterval( it->first ) ){ // std::cout << "Not an interval during getGenIndex " << it->first << std::endl; @@ -327,7 +327,7 @@ QModelBuilder( c, qe ){ bool FullModelChecker::optBuildAtFullModel() { //need to build after full model has taken effect if we are constructing interval models // this is because we need to have a constant in all integer equivalence classes - return options::fmfFmcInterval(); + return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL; } void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ @@ -443,7 +443,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; } children.push_back(ri); - if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){ + if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ if (fm->isModelBasisTerm(ri) ) { ri = fm->getStar( ri.getType() ); }else{ @@ -485,7 +485,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } - if( options::fmfFmcInterval() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){ convertIntervalModel( fm, op ); } @@ -1103,7 +1103,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, } }else{ if( !v.isNull() ){ - if( options::fmfFmcInterval() && v.getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && v.getType().isInteger() ){ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { if( fm->isInRange( v, it->first ) ){ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); @@ -1165,7 +1165,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c Trace("fmc-debug3") << "isCompat " << c << std::endl; Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i<cond.size(); i++) { - if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){ Node iv = doIntervalMeet( fm, cond[i], c[i-1], false ); if( iv.isNull() ){ return 0; @@ -1184,7 +1184,7 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i<cond.size(); i++) { if( cond[i]!=c[i-1] ) { - if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){ Node iv = doIntervalMeet( fm, cond[i], c[i-1] ); if( !iv.isNull() ){ cond[i] = iv; @@ -1254,7 +1254,7 @@ Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) { } void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) { - Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl; + Trace("fmc-debug") << "Make default vec, intervals = " << (options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl; //get function symbol for f cond.push_back(d_quant_cond[f]); for (unsigned i=0; i<f[0].getNumChildren(); i++) { diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 468c78978..cb63ccd45 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -273,17 +273,15 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ ++(d_statistics.d_num_quants_init); } //try to add it - if( optInstGen() ){ - Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; - //add model basis instantiation - if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ - d_quant_basis_match_added[f] = true; - return 1; - }else{ - //shouldn't happen usually, but will occur if x != y is a required literal for f. - //Notice() << "No model basis for " << f << std::endl; - d_quant_basis_match_added[f] = false; - } + Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; + //add model basis instantiation + if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ + d_quant_basis_match_added[f] = true; + return 1; + }else{ + //shouldn't happen usually, but will occur if x != y is a required literal for f. + //Notice() << "No model basis for " << f << std::endl; + d_quant_basis_match_added[f] = false; } } return 0; @@ -418,6 +416,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //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; + Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl; eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 5006a8a61..f314584cd 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -37,7 +37,7 @@ ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ){ Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; - if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){ + if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){ Trace("model-engine-debug") << "...make fmc builder." << std::endl; d_builder = new fmcheck::FullModelChecker( c, qe ); }else if( options::mbqiMode()==MBQI_INTERVAL ){ @@ -212,7 +212,7 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1; + int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : 1; for( int e=0; e<e_max; e++) { if (d_addedLemmas==0) { for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ @@ -230,6 +230,8 @@ int ModelEngine::checkModel(){ if( optOneQuantPerRound() && d_addedLemmas>0 ){ break; } + }else{ + Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl; } } } @@ -248,11 +250,12 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_builder->d_addedLemmas = 0; d_builder->d_incomplete_check = false; if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ + Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl; d_triedLemmas += d_builder->d_triedLemmas; d_addedLemmas += d_builder->d_addedLemmas; d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check; }else{ - Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; + Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; Debug("inst-fmf-ei") << " Instantiation Constants: "; for( size_t i=0; i<f[0].getNumChildren(); i++ ){ Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 7c4cb3651..d5c755ad2 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -65,7 +65,7 @@ typedef enum { /** mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ - //MBQI_FMC_INTERVAL, + MBQI_FMC_INTERVAL, /** mbqi with interval abstraction of uninterpreted sorts */ MBQI_INTERVAL, } MbqiMode; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index f485b981c..190c7ddc9 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -76,9 +76,8 @@ option eagerInstQuant --eager-inst-quant bool :default false option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" choose literal matching mode -option cbqi --enable-cbqi/--disable-cbqi bool :default false - turns on counterexample-based quantifier instantiation [off by default] -/turns off counterexample-based quantifier instantiation +option cbqi --enable-cbqi bool :default false + turns on counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default false turns on recursive counterexample-based quantifier instantiation @@ -97,30 +96,23 @@ option finiteModelFind --finite-model-find bool :default false option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false + only add one instantiation per quantifier per round for mbqi +option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false + only add instantiations for one quantifier per round for mbqi -option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true - disable simple models in full model check for finite model finding -option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true - disable covering simplification of fmc models -option fmfFmcInterval --fmf-fmc-interval bool :default false - construct interval models for fmc models - -option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false - only add one instantiation per quantifier per round for fmf -option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false - only add instantiations for one quantifier per round for fmf option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding option fmfRelevantDomain --fmf-relevant-domain bool :default false use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) -option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true - enable Inst-Gen instantiation techniques for finite model finding (default) -/disable Inst-Gen instantiation techniques for finite model finding +option fmfInstGen /--disable-fmf-inst-gen bool :default true + disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques - +option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true + disable simple models in full model check for finite model finding option fmfBoundInt --fmf-bound-int bool :default false finite model finding on bounded integer quantification diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index a119bcaf6..4929fa60b 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -87,9 +87,12 @@ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ fmc \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ Modulo Theories.\n\ \n\ +fmc-interval \n\ ++ Same as fmc, but with intervals for models of integer functions.\n\ +\n\ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ \n\ @@ -166,6 +169,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi return MBQI_INST_GEN; } else if(optarg == "fmc") { return MBQI_FMC; + } else if(optarg == "fmc-interval") { + return MBQI_FMC_INTERVAL; } else if(optarg == "interval") { return MBQI_INTERVAL; } else if(optarg == "help") { |