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/smt | |
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/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 30da29813..019cae9a1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1774,6 +1774,10 @@ void SmtEngine::setDefaults() { //now, have determined whether finite model find is on/off //apply finite model finding options if( options::finiteModelFind() ){ + //apply conservative quantifiers splitting + if( !options::quantDynamicSplit.wasSetByUser() ){ + options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT ); + } if( !options::eMatching.wasSetByUser() ){ options::eMatching.set( options::fmfInstEngine() ); } |