diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-03 22:15:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-03 22:15:33 +0000 |
commit | 8af4e7b765815a89671ac2c62554b773d4dda290 (patch) | |
tree | b40f53d82e16d41510ff52d82a991598df6583dc /src/theory/logic_info.cpp | |
parent | 39a66fe81b66498c82d1638c58c3c4ccc8f586db (diff) |
Comparisons for LogicInfos, and associated tests
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index d0c1e4b6a..9660986cf 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -61,6 +61,20 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : lock(); } +LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : + d_logicString(""), + d_theories(), + d_sharingTheories(0), + d_integers(false), + d_reals(false), + d_linear(false), + d_differenceLogic(false), + d_locked(false) { + + setLogicString(logicString); + lock(); +} + std::string LogicInfo::getLogicString() const { Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { @@ -329,4 +343,8 @@ LogicInfo LogicInfo::getUnlockedCopy() const { } } +std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) { + return out << logic.getLogicString(); +} + }/* CVC4 namespace */ |