diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 129 |
1 files changed, 101 insertions, 28 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index edf49c7ac..3d6f304b5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -18,6 +18,7 @@ #include <vector> #include <string> +#include <sstream> #include "smt/smt_engine.h" #include "smt/modal_exception.h" @@ -30,7 +31,7 @@ #include "expr/node_builder.h" #include "util/output.h" #include "util/exception.h" -#include "util/options.h" +#include "smt/options.h" #include "util/configuration.h" #include "prop/prop_engine.h" #include "theory/theory_engine.h" @@ -120,7 +121,9 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), + d_definedFunctions(NULL), d_assertionList(NULL), + d_assignments(NULL), d_haveAdditions(false), d_status() { @@ -152,6 +155,10 @@ SmtEngine::~SmtEngine() { shutdown(); + if(d_assignments != NULL) { + d_assignments->deleteSelf(); + } + if(d_assertionList != NULL) { d_assertionList->deleteSelf(); } @@ -183,15 +190,7 @@ void SmtEngine::setInfo(const string& key, const SExpr& value) throw BadOptionException("argument to (set-info :status ..) must be " "`sat' or `unsat' or `unknown'"); } - if(s == "sat") { - d_status = Result::SAT; - } else if(s == "unsat") { - d_status = Result::UNSAT; - } else if(s == "unknown") { - d_status = Result::SAT_UNKNOWN; - } else { - Unreachable(); - } + d_status = Result(s); return; } throw BadOptionException(); @@ -220,19 +219,16 @@ SExpr SmtEngine::getInfo(const string& key) const } else if(key == ":authors") { return Configuration::about(); } else if(key == ":status") { - enum Result::SAT status = d_status.asSatisfiabilityResult().isSAT(); - switch(status) { - case Result::SAT: - return SExpr("sat"); - case Result::UNSAT: - return SExpr("unsat"); - case Result::SAT_UNKNOWN: - return SExpr("unknown"); - default: - Unhandled(status); - } + return d_status.asSatisfiabilityResult().toString(); } else if(key == ":reason-unknown") { - throw BadOptionException(); + if(d_status.isUnknown()) { + stringstream ss; + ss << d_status.whyUnknown(); + return ss.str(); + } else { + throw ModalException("Can't get-info :reason-unknown when the " + "last result wasn't unknown!"); + } } else { throw BadOptionException(); } @@ -241,8 +237,31 @@ SExpr SmtEngine::getInfo(const string& key) const void SmtEngine::setOption(const string& key, const SExpr& value) throw(BadOptionException) { Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; - // FIXME implement me - throw BadOptionException(); + if(key == ":print-success") { + throw BadOptionException(); + } else if(key == ":expand-definitions") { + throw BadOptionException(); + } else if(key == ":interactive-mode") { + throw BadOptionException(); + } else if(key == ":produce-proofs") { + throw BadOptionException(); + } else if(key == ":produce-unsat-cores") { + throw BadOptionException(); + } else if(key == ":produce-models") { + throw BadOptionException(); + } else if(key == ":produce-assignments") { + throw BadOptionException(); + } else if(key == ":regular-output-channel") { + throw BadOptionException(); + } else if(key == ":diagnostic-output-channel") { + throw BadOptionException(); + } else if(key == ":random-seed") { + throw BadOptionException(); + } else if(key == ":verbosity") { + throw BadOptionException(); + } else { + throw BadOptionException(); + } } SExpr SmtEngine::getOption(const string& key) const @@ -386,7 +405,7 @@ Result SmtEngine::check() { Result SmtEngine::quickCheck() { Debug("smt") << "SMT quickCheck()" << endl; - return Result(Result::VALIDITY_UNKNOWN); + return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK); } void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) @@ -454,7 +473,7 @@ Expr SmtEngine::simplify(const Expr& e) { Unimplemented(); } -Expr SmtEngine::getValue(Expr e) +Expr SmtEngine::getValue(const Expr& e) throw(ModalException, AssertionException) { Assert(e.getExprManager() == d_exprManager); Type type = e.getType(true);// ensure expr is type-checked at this point @@ -494,19 +513,73 @@ Expr SmtEngine::getValue(Expr e) return Expr(d_exprManager, new Node(resultNode)); } +bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Type type = e.getType(true); + // must be Boolean + CheckArgument( type.isBoolean(), e, + "expected Boolean-typed variable or function application " + "in addToAssignment()" ); + Node n = e.getNode(); + // must be an APPLY of a zero-ary defined function, or a variable + CheckArgument( ( ( n.getKind() == kind::APPLY && + ( d_definedFunctions->find(n.getOperator()) != + d_definedFunctions->end() ) && + n.getNumChildren() == 0 ) || + n.getMetaKind() == kind::metakind::VARIABLE ), e, + "expected variable or defined-function application " + "in addToAssignment(),\ngot %s", e.toString().c_str() ); + if(!d_options->interactive || !d_options->produceAssignments) { + return false; + } + if(d_assignments == NULL) { + d_assignments = new(true) AssignmentSet(d_context); + } + d_assignments->insert(n); + + return true; +} + SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Debug("smt") << "SMT getAssignment()" << endl; if(!d_options->produceAssignments) { const char* msg = - "Cannot get the current assignment when produce-assignments option is off."; + "Cannot get the current assignment when " + "produce-assignments option is off."; throw ModalException(msg); } // TODO also check that the last query was sat/unknown, without intervening // assertions NodeManagerScope nms(d_nodeManager); + vector<SExpr> sexprs; + TypeNode boolType = d_nodeManager->booleanType(); + for(AssignmentSet::const_iterator i = d_assignments->begin(), + iend = d_assignments->end(); + i != iend; + ++i) { + Assert((*i).getType() == boolType); - Unimplemented(); + Node n = SmtEnginePrivate::preprocess(*this, *i); + + Debug("smt") << "--- getting value of " << n << endl; + Node resultNode = d_theoryEngine->getValue(n); + + // type-check the result we got + Assert(resultNode.isNull() || resultNode.getType(true) == boolType); + + vector<SExpr> v; + if((*i).getKind() == kind::APPLY) { + Assert((*i).getNumChildren() == 0); + v.push_back((*i).getOperator().toString()); + } else { + Assert((*i).getMetaKind() == kind::metakind::VARIABLE); + v.push_back((*i).toString()); + } + v.push_back(resultNode.toString()); + sexprs.push_back(v); + } + return SExpr(sexprs); } vector<Expr> SmtEngine::getAssertions() |