From: Andrew Reynolds Date: Tue, 25 Feb 2014 17:08:33 +0000 (-0600) Subject: Add options --full-saturate-quant and --mbqi=trust. Other minor changes. X-Git-Tag: cvc5-1.0.0~7067 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9ffaf6ed5d2de15d1982b423be6fa6d5f9d8995;p=cvc5.git Add options --full-saturate-quant and --mbqi=trust. Other minor changes. --- diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 199d3233c..9a3c07c5e 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -52,7 +52,7 @@ void InstantiationEngine::finishInit(){ i_ag->setGenerateAdditional( true ); addInstStrategy( i_ag ); //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) ); - if( !options::finiteModelFind() ){ + if( !options::finiteModelFind() && options::fullSaturateQuant() ){ addInstStrategy( new InstStrategyFreeVariable( d_quantEngine ) ); } //d_isup->setPriorityOver( i_ag ); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 9fe0407e5..738cfed60 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -37,7 +37,8 @@ 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::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){ + if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || + options::mbqiMode()==MBQI_TRUST || options::fmfBoundInt() ){ Trace("model-engine-debug") << "...make fmc builder." << std::endl; d_builder = new fmcheck::FullModelChecker( c, qe ); }else if( options::mbqiMode()==MBQI_INTERVAL ){ @@ -204,7 +205,7 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : 1; + int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); for( int e=0; egetNumAssertedQuantifiers(); i++ ){ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index b37e48ec3..89e10b175 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -70,6 +70,8 @@ typedef enum { MBQI_FMC_INTERVAL, /** mbqi with interval abstraction of uninterpreted sorts */ MBQI_INTERVAL, + /** mbqi trust (produce no instantiations) */ + MBQI_TRUST, } MbqiMode; typedef enum { diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 2041a91b8..f9cabe62b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -72,6 +72,9 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly + +option fullSaturateQuant --full-saturate-quant bool :default true + when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown 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 diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 06f5d7600..492155e02 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -226,6 +226,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi return MBQI_FMC_INTERVAL; } else if(optarg == "interval") { return MBQI_INTERVAL; + } else if(optarg == "trust") { + return MBQI_TRUST; } else if(optarg == "help") { puts(mbqiModeHelp.c_str()); exit(1); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a454d8334..36410bd50 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -54,7 +54,8 @@ d_lemmas_produced_c(u){ //the model object if( options::mbqiMode()==quantifiers::MBQI_FMC || - options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){ + options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() || + options::mbqiMode()==quantifiers::MBQI_TRUST ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" ); @@ -452,18 +453,23 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b return false; } -bool QuantifiersEngine::addLemma( Node lem ){ - Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl; - lem = Rewriter::rewrite(lem); - if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ - //d_curr_out->lemma( lem ); - d_lemmas_produced_c[ lem ] = true; +bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ + if( doCache ){ + Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl; + lem = Rewriter::rewrite(lem); + if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ + //d_curr_out->lemma( lem ); + d_lemmas_produced_c[ lem ] = true; + d_lemmas_waiting.push_back( lem ); + Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl; + return true; + }else{ + Debug("inst-engine-debug") << "Duplicate." << std::endl; + return false; + } + }else{ d_lemmas_waiting.push_back( lem ); - Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl; return true; - }else{ - Debug("inst-engine-debug") << "Duplicate." << std::endl; - return false; } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index fd51e4fb1..fbc501aec 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -86,6 +86,7 @@ class QuantifiersEngine { friend class quantifiers::InstantiationEngine; friend class quantifiers::ModelEngine; friend class quantifiers::RewriteEngine; + friend class quantifiers::QuantConflictFind; friend class inst::InstMatch; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; @@ -210,7 +211,7 @@ public: /** exist instantiation ? */ bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ - bool addLemma( Node lem ); + bool addLemma( Node lem, bool doCache = true ); /** do instantiation specified by m */ bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false ); /** add instantiation */