diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-17 04:05:17 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-17 04:05:17 +0000 |
commit | 44498017455cce207bf9cb0a1ebbf67c4a4d77cf (patch) | |
tree | 18f0bf80ea93cfd1f0e49cf38b7f0baf2d457285 /src/theory/logic_info.cpp | |
parent | db35c4be8bd37746e1c27e446291c82556df1d05 (diff) |
* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORTED logic
* Java bindings fixes: fixed access to ostreams, iterators
* Make SmtEngine::setUserAttribute() (and others) take a const string&
* Also a few compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 91 |
1 files changed, 50 insertions, 41 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index d2cf57643..e76e2ace9 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -76,52 +76,61 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : std::string LogicInfo::getLogicString() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { - size_t seen = 0; // make sure we support all the active theories + LogicInfo qf_all_supported; + qf_all_supported.disableQuantifiers(); + qf_all_supported.lock(); + if(hasEverything()) { + d_logicString = "ALL_SUPPORTED"; + } else if(*this == qf_all_supported) { + d_logicString = "QF_ALL_SUPPORTED"; + } else { + size_t seen = 0; // make sure we support all the active theories - stringstream ss; - if(!isQuantified()) { - ss << "QF_"; - } - if(d_theories[THEORY_ARRAY]) { - ss << (d_sharingTheories == 1 ? "AX" : "A"); - ++seen; - } - if(d_theories[THEORY_UF]) { - ss << "UF"; - ++seen; - } - if(d_theories[THEORY_BV]) { - ss << "BV"; - ++seen; - } - if(d_theories[THEORY_DATATYPES]) { - ss << "DT"; - ++seen; - } - if(d_theories[THEORY_ARITH]) { - if(isDifferenceLogic()) { - ss << (areIntegersUsed() ? "I" : ""); - ss << (areRealsUsed() ? "R" : ""); - ss << "DL"; - } else { - ss << (isLinear() ? "L" : "N"); - ss << (areIntegersUsed() ? "I" : ""); - ss << (areRealsUsed() ? "R" : ""); - ss << "A"; + stringstream ss; + if(!isQuantified()) { + ss << "QF_"; + } + if(d_theories[THEORY_ARRAY]) { + ss << (d_sharingTheories == 1 ? "AX" : "A"); + ++seen; + } + if(d_theories[THEORY_UF]) { + ss << "UF"; + ++seen; + } + if(d_theories[THEORY_BV]) { + ss << "BV"; + ++seen; + } + if(d_theories[THEORY_DATATYPES]) { + ss << "DT"; + ++seen; + } + if(d_theories[THEORY_ARITH]) { + if(isDifferenceLogic()) { + ss << (areIntegersUsed() ? "I" : ""); + ss << (areRealsUsed() ? "R" : ""); + ss << "DL"; + } else { + ss << (isLinear() ? "L" : "N"); + ss << (areIntegersUsed() ? "I" : ""); + ss << (areRealsUsed() ? "R" : ""); + ss << "A"; + } + ++seen; } - ++seen; - } - if(seen != d_sharingTheories) { - Unhandled("can't extract a logic string from LogicInfo; at least one " - "active theory is unknown to LogicInfo::getLogicString() !"); - } + if(seen != d_sharingTheories) { + Unhandled("can't extract a logic string from LogicInfo; at least one " + "active theory is unknown to LogicInfo::getLogicString() !"); + } - if(seen == 0) { - ss << "SAT"; - } + if(seen == 0) { + ss << "SAT"; + } - d_logicString = ss.str(); + d_logicString = ss.str(); + } } return d_logicString; } |