diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-03-21 20:51:02 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-03-21 20:51:02 +0000 |
| commit | f40ec39fe48f83e1cc1a31f9e18635687bd63c76 (patch) | |
| tree | daba20eb93798b196a8fb324438152fba7f8e867 /src/smt/smt_engine.cpp | |
| parent | 84f26af22566f7c10dea45b399b944cb50b5e317 (diff) | |
Disable nonclausal simplification for QF_SAT benchmarks by default.
(Can be overridden with --simplification=batch, for example.)
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fee77df39..4f28225af 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -362,8 +362,14 @@ void SmtEngine::setLogicInternal(const std::string& s) throw() { // by default, symmetry breaker is on only for QF_UF if(! Options::current()->ufSymmetryBreakerSetByUser) { + Trace("smt") << "setting uf symmetry breaker to " << (s == "QF_UF") << std::endl; NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF"); } + // by default, nonclausal simplification is off for QF_SAT + if(! Options::current()->simplificationModeSetByUser) { + Trace("smt") << "setting simplification mode to <" << s << "> " << (s != "QF_SAT") << std::endl; + NodeManager::currentNM()->getOptions()->simplificationMode = (s == "QF_SAT" ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH); + } // If in arrays, set the UF handler to arrays if(s == "QF_AX") { |