diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/logic_info.cpp | 26 | ||||
-rw-r--r-- | src/theory/logic_info.h | 32 |
2 files changed, 29 insertions, 29 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 9660986cf..c4ae81927 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -76,7 +76,7 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : } std::string LogicInfo::getLogicString() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + 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 @@ -129,7 +129,7 @@ std::string LogicInfo::getLogicString() const { } void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!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 } @@ -244,17 +244,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } void LogicInfo::enableEverything() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); } void LogicInfo::disableEverything() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(""); } void LogicInfo::enableTheory(theory::TheoryId theory) { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -265,7 +265,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -281,14 +281,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_integers = true; } void LogicInfo::disableIntegers() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -297,14 +297,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_reals = true; } void LogicInfo::disableReals() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -313,21 +313,21 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; } void LogicInfo::arithOnlyLinear() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = false; } void LogicInfo::arithNonLinear() { - Assert(!d_locked, "This LogicInfo is locked, and cannot be modified"); + CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = false; d_differenceLogic = false; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 36b71e931..8cd326039 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -105,25 +105,25 @@ public: /** Is sharing enabled for this logic? */ bool isSharingEnabled() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(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 isTheoryEnabled(theory::TheoryId theory) const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_theories[theory]; } /** Is this a quantified logic? */ bool isQuantified() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES); } /** Is this the all-inclusive logic? */ bool hasEverything() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); LogicInfo everything; everything.lock(); return *this == everything; @@ -131,7 +131,7 @@ public: /** Is this the all-exclusive logic? (Here, that means propositional logic) */ bool hasNothing() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); LogicInfo nothing(""); nothing.lock(); return *this == nothing; @@ -143,7 +143,7 @@ public: * use "isPure(theory) && !isQuantified()". */ bool isPure(theory::TheoryId theory) const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(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() && @@ -155,22 +155,22 @@ public: /** Are integers in this logic? */ bool areIntegersUsed() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_integers; } /** Are reals in this logic? */ bool areRealsUsed() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_reals; } /** Does this logic only linear arithmetic? */ bool isLinear() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_linear || d_differenceLogic; } /** Does this logic only permit difference reasoning? (implies linear) */ bool isDifferenceLogic() const { - Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); return d_differenceLogic; } @@ -252,13 +252,13 @@ public: /** Are these two LogicInfos equal? */ bool operator==(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(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; } } - Assert(d_sharingTheories == other.d_sharingTheories, "LogicInfo internal inconsistency"); + CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); if(isTheoryEnabled(theory::THEORY_ARITH)) { return d_integers == other.d_integers && @@ -283,13 +283,13 @@ public: } /** Is this LogicInfo "less than or equal" the other? */ bool operator<=(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(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; } } - Assert(d_sharingTheories <= other.d_sharingTheories, "LogicInfo internal inconsistency"); + CheckArgument(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) && @@ -302,13 +302,13 @@ public: } /** Is this LogicInfo "greater than or equal" the other? */ bool operator>=(const LogicInfo& other) const { - Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried"); + CheckArgument(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; } } - Assert(d_sharingTheories >= other.d_sharingTheories, "LogicInfo internal inconsistency"); + CheckArgument(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) && |