diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:00:59 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:00:59 +0100 |
commit | 73cecf65a750b9ee59486083af5ee55734da0a6a (patch) | |
tree | 43cae0e79c45f2c8204f3f5bc6e3c3f198e6845e /src/theory/quantifiers_engine.cpp | |
parent | e1e393dff082ad115ba198c32990235fb991eb13 (diff) |
Add --lte-restrict-inst-closure option. Push dt.size fairness constraints inside splitting lemmas for sygus.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 46 |
1 files changed, 31 insertions, 15 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 52b4fd17d..13822eb98 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -80,9 +80,9 @@ d_lemmas_produced_c(u){ //d_rr_tr_trie = new rrinst::TriggerTrie; //d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; - + bool needsBuilder = false; - + Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; //the model object @@ -158,7 +158,7 @@ d_lemmas_produced_c(u){ }else{ d_lte_part_inst = NULL; } - + if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || @@ -604,21 +604,35 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ } bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) { - if( n.hasAttribute(InstLevelAttribute()) ){ - int fml = d_term_db->getQAttrQuantInstLevel( f ); - unsigned ml = fml>=0 ? fml : options::instMaxLevel(); - - if( n.getAttribute(InstLevelAttribute())>ml ){ - Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); - Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; + if( options::lteRestrictInstClosure() ){ + //has to be both in inst closure and in ground assertions + if( !d_term_db->isInstClosure( n ) ){ + Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl; return false; } - }else{ - if( options::instLevelInputOnly() ){ - Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; + // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this + if( !d_term_db->hasTermCurrent( n, false ) ){ + Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl; return false; } } + if( options::instMaxLevel()!=-1 ){ + if( n.hasAttribute(InstLevelAttribute()) ){ + int fml = d_term_db->getQAttrQuantInstLevel( f ); + unsigned ml = fml>=0 ? fml : options::instMaxLevel(); + + if( n.getAttribute(InstLevelAttribute())>ml ){ + Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; + return false; + } + }else{ + if( options::instLevelInputOnly() ){ + Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; + return false; + } + } + } return true; } @@ -775,7 +789,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo Trace("inst-add-debug") << std::endl; //check based on instantiation level - if( options::instMaxLevel()!=-1 ){ + if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ for( unsigned i=0; i<terms.size(); i++ ){ if( !isTermEligibleForInstantiation( terms[i], f, true ) ){ return false; @@ -1247,7 +1261,9 @@ int getDepth( Node n ){ //smaller the score, the better int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){ int s; - if( options::instMaxLevel()!=-1 ){ + if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ + return -1; + }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ s = n.getAttribute(InstLevelAttribute()); |