diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-08 23:15:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-08 23:15:08 +0000 |
commit | 438e4336569f90adcb8c994df54bc410f56cde07 (patch) | |
tree | ab8d108445c362b017a30553bb7fcfbe84dbe305 /src/smt/smt_engine.h | |
parent | 15171a8c15cde42914a47f0d1b8bad5ebd6be6e6 (diff) |
cleanup, documentation, SMT-LIBv2 compliance
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a73dbdad9..854399bd7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -119,6 +119,11 @@ class CVC4_PUBLIC SmtEngine { AssignmentSet* d_assignments; /** + * The logic we're in. + */ + std::string d_logic; + + /** * Whether or not we have added any * assertions/declarations/definitions since the last checkSat/query * (and therefore we're not responsible for an assignment). @@ -205,10 +210,15 @@ public: ~SmtEngine(); /** + * Set the logic of the script. + */ + void setLogic(const std::string& logic) throw(ModalException); + + /** * Set information about the script executing. */ void setInfo(const std::string& key, const SExpr& value) - throw(BadOptionException); + throw(BadOptionException, ModalException); /** * Query information about the SMT environment. @@ -220,7 +230,7 @@ public: * Set an aspect of the current SMT execution environment. */ void setOption(const std::string& key, const SExpr& value) - throw(BadOptionException); + throw(BadOptionException, ModalException); /** * Get an aspect of the current SMT execution environment. |