diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7feaa7e61..43d3e1125 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -37,6 +37,7 @@ #include "util/result.h" #include "util/sexpr.h" #include "util/stats.h" +#include "theory/logic_info.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -131,7 +132,12 @@ class CVC4_PUBLIC SmtEngine { /** * The logic we're in. */ - std::string d_logic; + LogicInfo d_logic; + + /** + * Whether the logic has been set yet. + */ + bool d_logicIsSet; /** * Whether or not we have added any assertions/declarations/definitions @@ -212,7 +218,7 @@ class CVC4_PUBLIC SmtEngine { /** * Internally handle the setting of a logic. */ - void setLogicInternal(const std::string& logic) throw(); + void setLogicInternal(const LogicInfo& logic) throw(); friend class ::CVC4::smt::SmtEnginePrivate; @@ -226,7 +232,6 @@ class CVC4_PUBLIC SmtEngine { /** how the SMT engine got the answer -- SAT solver or DE */ BackedStat<std::string> d_statResultSource; - public: /** @@ -245,6 +250,11 @@ public: void setLogic(const std::string& logic) throw(ModalException); /** + * Set the logic of the script. + */ + void setLogic(const LogicInfo& logic) throw(ModalException); + + /** * Set information about the script executing. */ void setInfo(const std::string& key, const SExpr& value) |