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/quant_split.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/quant_split.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index c88430dbf..24d26e72f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -50,7 +50,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0; }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ - score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1; + //only split if goes from being unhandled -> handled by finite instantiation + // an example is datatypes with uninterpreted sort fields, which are "interpreted finite" but not "finite" + if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){ + score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1; + } } Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl; if( score>max_score ){ |