diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-10-09 09:49:35 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-10-09 09:49:35 +0000 |
| commit | 0131e18b811bdf2825a1cde5a6d68d523b19aacc (patch) | |
| tree | 9c4dcb4c1bf355b943926a5df85d3c3446750878 /src/smt/smt_engine.h | |
| parent | ec86769172d29ff7f5ed959866ecef339264552b (diff) | |
support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index efa48e517..7272762d8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -119,9 +119,9 @@ class CVC4_PUBLIC SmtEngine { bool d_haveAdditions; /** - * Result of last checkSat/query. + * Most recent result of last checkSat/query or (set-info :status). */ - Result d_lastResult; + Result d_status; /** * This is called by the destructor, just before destroying the @@ -173,7 +173,7 @@ public: /** * Query information about the SMT environment. */ - const SExpr& getInfo(const std::string& key) const + SExpr getInfo(const std::string& key) const throw(BadOptionException); /** @@ -185,7 +185,7 @@ public: /** * Get an aspect of the current SMT execution environment. */ - const SExpr& getOption(const std::string& key) const + SExpr getOption(const std::string& key) const throw(BadOptionException); /** |