diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-29 13:50:54 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-29 13:50:54 +0000 |
commit | 62988b5d0556d8dd1e0258962d2eaccbe2551281 (patch) | |
tree | d0a9f5868745f06b36d53eb19f38f30c7154500c /src/smt | |
parent | a42d1d31d9f73a1d9fdce404153598c5b94ed241 (diff) |
Disable minisat elimination when models are on
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55ac15ebc..ca8417dea 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -62,6 +62,7 @@ #include "theory/model.h" #include "printer/printer.h" #include "prop/options.h" +#include "theory/arrays/options.h" using namespace std; using namespace CVC4; @@ -833,12 +834,28 @@ void SmtEngine::setLogicInternal() throw() { } } - //until bug 371 is fixed + //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ - if( d_logic.isQuantified() ){ + if( d_logic.isQuantified() || options::produceModels() ){ options::minisatUseElim.set( false ); } } + else if (options::minisatUseElim()) { + if (options::produceModels()) { + Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << std::endl; + setOption("produce-models", SExpr("false")); + } + if (options::checkModels()) { + Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << std::endl; + setOption("check-models", SExpr("false")); + } + } + + // For now, these array theory optimizations do not support model-building + if (options::produceModels()) { + options::arraysOptimizeLinear.set(false); + options::arraysLazyRIntro1.set(false); + } } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) |