diff options
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 76 |
1 files changed, 49 insertions, 27 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index ecebd27c9..05f8c7a9f 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -39,7 +39,7 @@ LogicInfo::LogicInfo() d_linear(false), d_differenceLogic(false), d_cardinalityConstraints(false), - d_higherOrder(true), + d_higherOrder(false), d_locked(false) { for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) @@ -117,13 +117,25 @@ bool LogicInfo::isHigherOrder() const return d_higherOrder; } -/** Is this the all-inclusive logic? */ -bool LogicInfo::hasEverything() const { - PrettyCheckArgument(d_locked, *this, +bool LogicInfo::hasEverything() const +{ + PrettyCheckArgument(d_locked, + *this, "This LogicInfo isn't locked yet, and cannot be queried"); - LogicInfo everything; - everything.lock(); - return *this == everything; + // A logic has everything if all theories are enabled as well as quantifiers + bool doesNotHaveEverything = !isQuantified(); + for (TheoryId id = THEORY_FIRST; !doesNotHaveEverything && id < THEORY_LAST; + ++id) + { + // if not configured with symfpu, we allow THEORY_FP to be disabled and + // still *this to contain the ALL logic + if (!this->d_theories[id] + && (id != THEORY_FP || Configuration::isBuiltWithSymFPU())) + { + doesNotHaveEverything = true; + } + } + return !doesNotHaveEverything; } /** Is this the all-exclusive logic? (Here, that means propositional logic) */ @@ -275,17 +287,22 @@ std::string LogicInfo::getLogicString() const { LogicInfo qf_all_supported; qf_all_supported.disableQuantifiers(); qf_all_supported.lock(); - if(hasEverything()) { - d_logicString = "ALL"; - } else if(*this == qf_all_supported) { - d_logicString = "QF_ALL"; - } else { + stringstream ss; + if (isHigherOrder()) + { + ss << "HO_"; + } + if (!isQuantified()) + { + ss << "QF_"; + } + if (*this == qf_all_supported || hasEverything()) + { + ss << "ALL"; + } + else + { size_t seen = 0; // make sure we support all the active theories - - stringstream ss; - if(!isQuantified()) { - ss << "QF_"; - } if (d_theories[THEORY_SEP]) { ss << "SEP_"; @@ -309,7 +326,7 @@ std::string LogicInfo::getLogicString() const { if(d_theories[THEORY_FP]) { ss << "FP"; ++seen; - } + } if(d_theories[THEORY_DATATYPES]) { ss << "DT"; ++seen; @@ -350,9 +367,8 @@ std::string LogicInfo::getLogicString() const { if(seen == 0) { ss << "SAT"; } - - d_logicString = ss.str(); } + d_logicString = ss.str(); } return d_logicString; } @@ -374,6 +390,11 @@ void LogicInfo::setLogicString(std::string logicString) enableTheory(THEORY_BOOL); const char* p = logicString.c_str(); + if (!strncmp(p, "HO_", 3)) + { + enableHigherOrder(); + p += 3; + } if(*p == '\0') { // propositional logic only; we're done. } else if(!strcmp(p, "QF_SAT")) { @@ -384,14 +405,14 @@ void LogicInfo::setLogicString(std::string logicString) enableQuantifiers(); p += 3; } else if(!strcmp(p, "QF_ALL")) { - // the "all theories included" logic, no quantifiers - enableEverything(); + // the "all theories included" logic, no quantifiers. + enableEverything(d_higherOrder); disableQuantifiers(); arithNonLinear(); p += 6; } else if(!strcmp(p, "ALL")) { - // the "all theories included" logic, with quantifiers - enableEverything(); + // the "all theories included" logic, with quantifiers. + enableEverything(d_higherOrder); enableQuantifiers(); arithNonLinear(); p += 3; @@ -399,7 +420,7 @@ void LogicInfo::setLogicString(std::string logicString) else if (!strcmp(p, "HORN")) { // the HORN logic - enableEverything(); + enableEverything(d_higherOrder); enableQuantifiers(); arithNonLinear(); p += 4; @@ -541,9 +562,11 @@ void LogicInfo::setLogicString(std::string logicString) d_logicString = logicString; } -void LogicInfo::enableEverything() { +void LogicInfo::enableEverything(bool enableHigherOrder) +{ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); + this->d_higherOrder = enableHigherOrder; } void LogicInfo::disableEverything() { @@ -584,7 +607,6 @@ void LogicInfo::enableSygus() enableTheory(THEORY_UF); enableTheory(THEORY_DATATYPES); enableIntegers(); - enableHigherOrder(); } void LogicInfo::enableSeparationLogic() |