diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/preprocessing/passes/bv_ackermann.cpp | 9 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 43 |
2 files changed, 39 insertions, 13 deletions
diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp index 850136f9d..b5f152129 100644 --- a/src/preprocessing/passes/bv_ackermann.cpp +++ b/src/preprocessing/passes/bv_ackermann.cpp @@ -55,7 +55,12 @@ void storeFunction( if (set.find(term) == set.end()) { set.insert(term); - Node skolem = bv::utils::mkVar(bv::utils::getSize(term)); + TypeNode tn = term.getType(); + Node skolem = NodeManager::currentNM()->mkSkolem( + "BVSKOLEM$$", + tn, + "is a variable created by the ackermannization " + "preprocessing pass for theory BV"); fun_to_skolem.addSubstitution(term, skolem); } } @@ -156,7 +161,7 @@ PreprocessingPassResult BVAckermann::applyInternal( } /* replace applications of UF by skolems */ - // FIXME for model building, github issue #1118) + // FIXME for model building, github issue #1901 for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { assertionsToPreprocess->replace( 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)) { |