diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-21 09:42:07 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-21 09:42:07 +0100 |
commit | 32b0aba2c2c27ad038d34c8554a4bae76e8dd363 (patch) | |
tree | e6e737d10b53c0c13dfba072cdec6d1f9b5449a2 /src | |
parent | f70804a7159390fcb01d8c1ec208fbfd8e544fba (diff) |
Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 24 |
4 files changed, 36 insertions, 13 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 86b0faaf6..74cdee0b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1319,7 +1319,6 @@ void SmtEngine::setDefaults() { if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } - //for finite model finding if( ! options::instWhenMode.wasSetByUser()){ //instantiate only on last call if( options::eMatching() ){ @@ -1327,6 +1326,14 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } + if( options::mbqiMode()==quantifiers::MBQI_ABS ){ + if( !options::preSkolemQuant.wasSetByUser() ){ + options::preSkolemQuant.set( true ); + } + if( !options::fmfOneInstPerRound.wasSetByUser() ){ + options::fmfOneInstPerRound.set( true ); + } + } } //implied options... diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index dad173ff5..a428633cc 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -41,7 +41,7 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true option cnfQuant --cnf-quant bool :default false apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies -option nnfQuant --nnf-quant bool :default false +option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas option clauseSplit --clause-split bool :default false @@ -88,7 +88,7 @@ option fmfFunWellDefined --fmf-fun bool :default false option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) @@ -127,7 +127,7 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :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 +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :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 diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 08fcf319d..e9f85d454 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -29,17 +29,17 @@ namespace quantifiers { static const std::string instWhenHelp = "\ Modes currently supported by the --inst-when option:\n\ \n\ -full (default)\n\ +full-last-call (default)\n\ ++ Alternate running instantiation rounds at full effort and last\n\ + call. In other words, interleave instantiation and theory combination.\n\ +\n\ +full\n\ + Run instantiation round at full effort, before theory combination.\n\ \n\ full-delay \n\ + Run instantiation round at full effort, before theory combination, after\n\ all other theories have finished.\n\ \n\ -full-last-call\n\ -+ Alternate running instantiation rounds at full effort and last\n\ - call. In other words, interleave instantiation and theory combination.\n\ -\n\ last-call\n\ + Run instantiation at last call effort, after theory combination and\n\ and theories report sat.\n\ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0ed175393..1e6ec3a02 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -309,11 +309,19 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; Kind k = body[0].getKind(); + if( body[0].getKind()==OR || body[0].getKind()==AND ){ + k = body[0].getKind()==AND ? OR : AND; for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - children.push_back( computeNNF( body[0][i].notNode() ) ); + Node nc = computeNNF( body[0][i].notNode() ); + if( nc.getKind()==k ){ + for( unsigned j=0; j<nc.getNumChildren(); j++ ){ + children.push_back( nc[j] ); + } + }else{ + children.push_back( nc ); + } } - k = body[0].getKind()==AND ? OR : AND; }else if( body[0].getKind()==IFF ){ for( int i=0; i<2; i++ ){ Node nn = i==0 ? body[0][i] : body[0][i].notNode(); @@ -335,10 +343,18 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; bool childrenChanged = false; + bool isAssoc = body.getKind()==AND || body.getKind()==OR; for( int i=0; i<(int)body.getNumChildren(); i++ ){ Node nc = computeNNF( body[i] ); - children.push_back( nc ); - childrenChanged = childrenChanged || nc!=body[i]; + if( isAssoc && nc.getKind()==body.getKind() ){ + for( unsigned j=0; j<nc.getNumChildren(); j++ ){ + children.push_back( nc[j] ); + } + childrenChanged = true; + }else{ + children.push_back( nc ); + childrenChanged = childrenChanged || nc!=body[i]; + } } if( childrenChanged ){ return NodeManager::currentNM()->mkNode( body.getKind(), children ); |