diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-09 17:03:22 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-09 17:03:22 +0000 |
commit | 3d1c71026c7b8aaa2e9689d27415d80c412ece2e (patch) | |
tree | b49f3a4809ccb933c053e69e2d6820ea5387e586 | |
parent | b7aa53c0126948cae651b91555e44f8ce2f546bc (diff) |
Turning on unconstrained simp for QF_AUFBV
-rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d0f7a0584..e0d507475 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -472,10 +472,12 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp; } - // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode + // Turn on unconstrained simplification for QF_AUFBV if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) { - bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified(); - bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving; + // bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified(); + // bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving; + bool uncSimp = !Options::current()->incrementalSolving && !d_logic.isQuantified() && + (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_BV)); Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp; } |