diff options
Diffstat (limited to 'src/smt/solver_engine.cpp')
| -rw-r--r-- | src/smt/solver_engine.cpp | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 911e0a960..fc6ec3915 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -417,10 +417,10 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) bool SolverEngine::isValidGetInfoFlag(const std::string& key) const { - if (key == "all-statistics" || key == "error-behavior" || key == "name" - || key == "version" || key == "authors" || key == "status" - || key == "reason-unknown" || key == "assertion-stack-levels" - || key == "all-options" || key == "time") + if (key == "all-statistics" || key == "error-behavior" || key == "filename" + || key == "name" || key == "version" || key == "authors" + || key == "status" || key == "time" || key == "reason-unknown" + || key == "assertion-stack-levels" || key == "all-options") { return true; } @@ -455,7 +455,7 @@ std::string SolverEngine::getInfo(const std::string& key) const } if (key == "authors") { - return toSExpr(Configuration::about()); + return toSExpr("the " + Configuration::getName() + " authors"); } if (key == "status") { @@ -1081,7 +1081,7 @@ Node SolverEngine::getValue(const Node& ex) const // AJR : necessary? if (!n.getType().isFunction()) { - n = Rewriter::rewrite(n); + n = d_env->getRewriter()->rewrite(n); } Trace("smt") << "--- getting value of " << n << endl; @@ -1224,7 +1224,8 @@ Result SolverEngine::blockModel() // get expanded assertions std::vector<Node> eassertsProc = getExpandedAssertions(); - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); @@ -1247,7 +1248,8 @@ Result SolverEngine::blockModelValues(const std::vector<Node>& exprs) // get expanded assertions std::vector<Node> eassertsProc = getExpandedAssertions(); // we always do block model values mode here - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); return assertFormula(eblocker); } |