diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:15 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:31 -0600 |
commit | e8c09abb9165278b13491c83bdcbe17ae535126e (patch) | |
tree | 1101d3e878bcfd9e12cd64aaad3017aa320c896b /src/theory/quantifiers_engine.cpp | |
parent | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (diff) |
Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a3b6293fb..2d79826a6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -251,8 +251,7 @@ void QuantifiersEngine::finishInit(){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); } - if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || - options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ + if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){ d_qsplit = new quantifiers::QuantDSplit( this, c ); d_modules.push_back( d_qsplit ); } @@ -328,6 +327,20 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { return mo==m || mo==NULL; } +bool QuantifiersEngine::isFiniteBound( Node q, Node v ) { + if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){ + return true; + }else{ + TypeNode tn = v.getType(); + if( tn.isSort() && options::finiteModelFind() ){ + return true; + }else if( getTermDatabase()->mayComplete( tn ) ){ + return true; + } + } + return false; +} + void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; for( unsigned i=0; i<d_modules.size(); i++ ){ |