diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 14:09:54 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 14:09:54 +0000 |
commit | ec320b78deaaf31bdae1b8b048f66cfb1b3a4197 (patch) | |
tree | bf5fc292d26e49de97fe6c2eff6e2667d56c1895 /src/smt | |
parent | b4fb5a6ad511f20ff88d2bf78194ef2e65dbde39 (diff) |
check last result in (get-assignment); some context cleanup
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3d6f304b5..594efcc35 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -88,8 +88,7 @@ public: /** * Pre-process an Node. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple - * passes over the Node. TODO: may need to specify a LEVEL of - * preprocessing (certain contexts need more/less ?). + * passes over the Node. */ static Node preprocess(SmtEngine& smt, TNode n) throw(NoSuchFunctionException, AssertionException); @@ -488,7 +487,8 @@ Expr SmtEngine::getValue(const Expr& e) "Cannot get value when produce-models options is off."; throw ModalException(msg); } - if(d_status.asSatisfiabilityResult() != Result::SAT || + if(d_status.isNull() || + d_status.asSatisfiabilityResult() != Result::SAT || d_haveAdditions) { const char* msg = "Cannot get value unless immediately proceded by SAT/INVALID response."; @@ -548,8 +548,13 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { "produce-assignments option is off."; throw ModalException(msg); } - // TODO also check that the last query was sat/unknown, without intervening - // assertions + if(d_status.isNull() || + d_status.asSatisfiabilityResult() != Result::SAT || + d_haveAdditions) { + const char* msg = + "Cannot get value unless immediately proceded by SAT/INVALID response."; + throw ModalException(msg); + } NodeManagerScope nms(d_nodeManager); vector<SExpr> sexprs; |