diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2016-11-18 15:01:59 -0800 |
---|---|---|
committer | Clark Barrett <barrett@cs.stanford.edu> | 2016-11-18 15:01:59 -0800 |
commit | 4f98fc506f3cb09a59d8418fd0043e59e4aee57e (patch) | |
tree | 864e93b36eeb52304542f108d2067ea5c37d6dfd /src/theory/logic_info.cpp | |
parent | ba7dd534de8f5d9bd746a7ed4c4a7b6ba11628e3 (diff) |
Add support for set-logic ALL, fix compiler error in GCC 6.1
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 6ac1c5e32..0e4ccf0f7 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -242,9 +242,9 @@ std::string LogicInfo::getLogicString() const { qf_all_supported.disableQuantifiers(); qf_all_supported.lock(); if(hasEverything()) { - d_logicString = "ALL_SUPPORTED"; + d_logicString = "ALL"; } else if(*this == qf_all_supported) { - d_logicString = "QF_ALL_SUPPORTED"; + d_logicString = "QF_ALL"; } else { size_t seen = 0; // make sure we support all the active theories @@ -341,11 +341,21 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc enableEverything(); disableQuantifiers(); p += 16; + } else if(!strcmp(p, "QF_ALL")) { + // the "all theories included" logic, no quantifiers + enableEverything(); + disableQuantifiers(); + p += 6; } else if(!strcmp(p, "ALL_SUPPORTED")) { // the "all theories included" logic, with quantifiers enableEverything(); enableQuantifiers(); p += 13; + } else if(!strcmp(p, "ALL")) { + // the "all theories included" logic, with quantifiers + enableEverything(); + enableQuantifiers(); + p += 3; } else { if(!strncmp(p, "QF_", 3)) { disableQuantifiers(); |