diff options
author | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
commit | a39ad6584c1d61e22e72b53c3838f4f675ed2e19 (patch) | |
tree | ed40cb371c41ac285ca2bf41a82254a36134e132 /src/theory/logic_info.cpp | |
parent | 87b0fe9ce10d1e5e9ed5a3e7db77f46bf3f68922 (diff) |
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 186 |
1 files changed, 173 insertions, 13 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 15600fefc..02eeefcaf 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -78,8 +78,167 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : lock(); } +/** Is sharing enabled for this logic? */ +bool LogicInfo::isSharingEnabled() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_sharingTheories > 1; +} + + +/** Is the given theory module active in this logic? */ +bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_theories[theory]; +} + +/** Is this a quantified logic? */ +bool LogicInfo::isQuantified() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return isTheoryEnabled(theory::THEORY_QUANTIFIERS); +} + +/** Is this the all-inclusive logic? */ +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; +} + +/** Is this the all-exclusive logic? (Here, that means propositional logic) */ +bool LogicInfo::hasNothing() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + LogicInfo nothing(""); + nothing.lock(); + return *this == nothing; +} + +bool LogicInfo::isPure(theory::TheoryId theory) const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + // the third and fourth conjucts are really just to rule out the misleading + // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA + return isTheoryEnabled(theory) && !isSharingEnabled() && + ( !isTrueTheory(theory) || d_sharingTheories == 1 ) && + ( isTrueTheory(theory) || d_sharingTheories == 0 ); +} + +bool LogicInfo::areIntegersUsed() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); + return d_integers; +} + +bool LogicInfo::areRealsUsed() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); + return d_reals; +} + +bool LogicInfo::isLinear() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); + return d_linear || d_differenceLogic; +} + +bool LogicInfo::isDifferenceLogic() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + isTheoryEnabled(theory::THEORY_ARITH), *this, + "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); + return d_differenceLogic; +} + +bool LogicInfo::hasCardinalityConstraints() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_cardinalityConstraints; +} + + +bool LogicInfo::operator==(const LogicInfo& other) const { + PrettyCheckArgument(isLocked() && other.isLocked(), *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { + if(d_theories[id] != other.d_theories[id]) { + return false; + } + } + + PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this, + "LogicInfo internal inconsistency"); + if(isTheoryEnabled(theory::THEORY_ARITH)) { + return + d_integers == other.d_integers && + d_reals == other.d_reals && + d_linear == other.d_linear && + d_differenceLogic == other.d_differenceLogic; + } else { + return true; + } +} + +bool LogicInfo::operator<=(const LogicInfo& other) const { + PrettyCheckArgument(isLocked() && other.isLocked(), *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { + if(d_theories[id] && !other.d_theories[id]) { + return false; + } + } + PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, + "LogicInfo internal inconsistency"); + if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { + return + (!d_integers || other.d_integers) && + (!d_reals || other.d_reals) && + (d_linear || !other.d_linear) && + (d_differenceLogic || !other.d_differenceLogic); + } else { + return true; + } +} + +bool LogicInfo::operator>=(const LogicInfo& other) const { + PrettyCheckArgument(isLocked() && other.isLocked(), *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { + if(!d_theories[id] && other.d_theories[id]) { + return false; + } + } + PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, + "LogicInfo internal inconsistency"); + if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { + return + (d_integers || !other.d_integers) && + (d_reals || !other.d_reals) && + (!d_linear || other.d_linear) && + (!d_differenceLogic || other.d_differenceLogic); + } else { + return true; + } +} + std::string LogicInfo::getLogicString() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { LogicInfo qf_all_supported; qf_all_supported.disableQuantifiers(); @@ -156,7 +315,8 @@ std::string LogicInfo::getLogicString() const { } void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, + "This LogicInfo is locked, and cannot be modified"); for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { d_theories[id] = false;// ensure it's cleared } @@ -299,17 +459,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } void LogicInfo::enableEverything() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); } void LogicInfo::disableEverything() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(""); } void LogicInfo::enableTheory(theory::TheoryId theory) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -320,7 +480,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -336,14 +496,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_integers = true; } void LogicInfo::disableIntegers() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -352,14 +512,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_reals = true; } void LogicInfo::disableReals() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -368,21 +528,21 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; } void LogicInfo::arithOnlyLinear() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = false; } void LogicInfo::arithNonLinear() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = false; d_differenceLogic = false; |