diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-05-11 08:47:02 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-11 08:47:02 -0700 |
commit | 1e0ff61c96c455287fd7986ce353dc2754f85d4f (patch) | |
tree | c7ed06c967361829a9c01c02389cd1cadb2a60c8 /src/smt | |
parent | 5e2366d542e17ba5064a56f2581ada99c0046ddc (diff) |
Fix ackermannize preprocessing pass. (#1904)
Ackermannization did not consider cases where UF are Boolean. Model generation is
still not supported, but now guarded against when bit-vectors are combined with arrays
and/or uninterpreted functions and --bitblast=eager.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 43 |
1 files changed, 32 insertions, 11 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c40096e3f..49eb42447 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1324,6 +1324,38 @@ void SmtEngine::setDefaults() { options::sygusRepairConst.set(false); } + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + { + if (options::incrementalSolving()) + { + if (options::incrementalSolving.wasSetByUser()) + { + throw OptionException(std::string( + "Eager bit-blasting does not currently support incremental mode. " + "Try --bitblast=lazy")); + } + Notice() << "SmtEngine: turning off incremental to support eager " + << "bit-blasting" << endl; + setOption("incremental", SExpr("false")); + } + if (options::produceModels() + && (d_logic.isTheoryEnabled(THEORY_ARRAYS) + || d_logic.isTheoryEnabled(THEORY_UF))) + { + if (options::bitblastMode.wasSetByUser() + || options::produceModels.wasSetByUser()) + { + throw OptionException(std::string( + "Eager bit-blasting currently does not support model generation " + "for the combination of bit-vectors with arrays or uinterpreted " + "functions. Try --bitblast=lazy")); + } + Notice() << "SmtEngine: setting bit-blast mode to lazy to support model" + << "generation" << endl; + setOption("bitblastMode", SExpr("lazy")); + } + } + if(options::forceLogicString.wasSetByUser()) { d_logic = LogicInfo(options::forceLogicString()); }else if (options::solveIntAsBV() > 0) { @@ -1668,17 +1700,6 @@ void SmtEngine::setDefaults() { } } - - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && - options::incrementalSolving()) { - if (options::incrementalSolving.wasSetByUser()) { - throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\ - Try --bitblast=lazy")); - } - Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl; - setOption("incremental", SExpr("false")); - } - if (! options::bvEagerExplanations.wasSetByUser() && d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV)) { |