diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-28 05:42:28 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-28 05:43:31 +0100 |
commit | fe9b2276fac81030eb9803d4327f7458bae2576e (patch) | |
tree | 8a1b4ea9fec5b625e8f3b44d1f43d2a476ef576c /src/smt | |
parent | 0c624b4f57c5f1bc3c94058fe5b1da4bdd724041 (diff) |
Disable prenex by default when using fmf bound int, minor improvement to datatypes rewriter
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 918d6f30d..d039377a1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1279,7 +1279,7 @@ void SmtEngine::setDefaults() { options::decisionMode.set(decMode); options::decisionStopOnly.set(stoponly); } - //local theory extensions + //local theory extensions if( options::localTheoryExt() ){ //no E-matching? if( !options::instMaxLevel.wasSetByUser() ){ @@ -1305,6 +1305,9 @@ void SmtEngine::setDefaults() { //if bounded integers are set, use no MBQI by default options::mbqiMode.set( quantifiers::MBQI_NONE ); } + if( ! options::prenexQuant.wasSetByUser() ){ + options::prenexQuant.set( quantifiers::PRENEX_NONE ); + } } if( options::ufssSymBreak() ){ options::sortInference.set( true ); @@ -1314,7 +1317,7 @@ void SmtEngine::setDefaults() { options::finiteModelFind.set( true ); } } - + //now, have determined whether finite model find is on/off //apply finite model finding options if( options::finiteModelFind() ){ @@ -1340,7 +1343,7 @@ void SmtEngine::setDefaults() { } } } - + //implied options... if( options::recurseCbqi() ){ options::cbqi.set( true ); |