summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-12-07 12:43:15 -0600
committerajreynol <andrew.j.reynolds@gmail.com>2016-12-07 12:43:31 -0600
commite8c09abb9165278b13491c83bdcbe17ae535126e (patch)
tree1101d3e878bcfd9e12cd64aaad3017aa320c896b /src/smt
parent0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (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.cpp4
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() );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback