diff options
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++ ){ |