diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-10 04:34:34 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-10 04:34:34 +0000 |
commit | 71b15fb7279c9e52b1b2b538887db2c1a44a8fa7 (patch) | |
tree | cf9159368d0aa259d06a993e163abd57e5578adb /src | |
parent | b7733c47c0f32c0ad112e59e999ed2490ba6f602 (diff) |
Finally tracked down problems in regressions and fuzz results (this also
explains why my build was giving different answers from Dejan's build).
Problem was that if you run:
cvc4 --check-models foo.smt
it would fail, but if you run
cvc4 --check-models --produce-models foo.smt
it would succeed. Even though produce-models is supposed to be automatically
set when you set check-models, it seems this was happening too late. Fixed by
removing any distinction between produce-models and check-models in the
heuristic setting code. Kind of ugly though.
Also, disable models if nonlinear arithmetic is on.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index df9526571..761fe3b8c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -744,7 +744,7 @@ void SmtEngine::setLogicInternal() throw() { if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) { // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); // bool uncSimp = false && !qf_sat && !options::incrementalSolving(); - bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && + bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::checkModels() && (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV)); Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; options::unconstrainedSimp.set(uncSimp); @@ -883,10 +883,23 @@ void SmtEngine::setLogicInternal() throw() { } // For now, these array theory optimizations do not support model-building - if (options::produceModels()) { + if (options::produceModels() || options::checkModels()) { options::arraysOptimizeLinear.set(false); options::arraysLazyRIntro1.set(false); } + + // Non-linear arithmetic does not support models + if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) && + !d_logic.isLinear()) { + if (options::produceModels()) { + Notice() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl; + setOption("produce-models", SExpr("false")); + } + if (options::checkModels()) { + Notice() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl; + setOption("check-models", SExpr("false")); + } + } } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) |