diff options
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 71 |
1 files changed, 56 insertions, 15 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 1c9e3d0ef..f2c6df0b6 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -36,6 +36,7 @@ LogicInfo::LogicInfo() d_sharingTheories(0), d_integers(true), d_reals(true), + d_transcendentals(true), d_linear(false), d_differenceLogic(false), d_cardinalityConstraints(false), @@ -53,6 +54,7 @@ LogicInfo::LogicInfo(std::string logicString) d_sharingTheories(0), d_integers(false), d_reals(false), + d_transcendentals(false), d_linear(false), d_differenceLogic(false), d_cardinalityConstraints(false), @@ -69,6 +71,7 @@ LogicInfo::LogicInfo(const char* logicString) d_sharingTheories(0), d_integers(false), d_reals(false), + d_transcendentals(false), d_linear(false), d_differenceLogic(false), d_cardinalityConstraints(false), @@ -156,6 +159,18 @@ bool LogicInfo::areRealsUsed() const { return d_reals; } +bool LogicInfo::areTranscendentalsUsed() 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 transcendentals are used"); + return d_transcendentals; +} + bool LogicInfo::isLinear() const { PrettyCheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); @@ -193,11 +208,10 @@ bool LogicInfo::operator==(const LogicInfo& other) const { 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; + return d_integers == other.d_integers && d_reals == other.d_reals + && d_transcendentals == other.d_transcendentals + && d_linear == other.d_linear + && d_differenceLogic == other.d_differenceLogic; } else { return true; } @@ -214,11 +228,10 @@ bool LogicInfo::operator<=(const LogicInfo& other) const { 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); + return (!d_integers || other.d_integers) && (!d_reals || other.d_reals) + && (!d_transcendentals || other.d_transcendentals) + && (d_linear || !other.d_linear) + && (d_differenceLogic || !other.d_differenceLogic); } else { return true; } @@ -235,11 +248,10 @@ bool LogicInfo::operator>=(const LogicInfo& other) const { 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); + return (d_integers || !other.d_integers) && (d_reals || !other.d_reals) + && (d_transcendentals || !other.d_transcendentals) + && (!d_linear || other.d_linear) + && (!d_differenceLogic || other.d_differenceLogic); } else { return true; } @@ -301,6 +313,7 @@ std::string LogicInfo::getLogicString() const { ss << (areIntegersUsed() ? "I" : ""); ss << (areRealsUsed() ? "R" : ""); ss << "A"; + ss << (areTranscendentalsUsed() ? "T" : ""); } ++seen; } @@ -471,11 +484,21 @@ void LogicInfo::setLogicString(std::string logicString) enableReals(); arithNonLinear(); p += 3; + if (*p == 'T') + { + arithTranscendentals(); + p += 1; + } } else if(!strncmp(p, "NIRA", 4)) { enableIntegers(); enableReals(); arithNonLinear(); p += 4; + if (*p == 'T') + { + arithTranscendentals(); + p += 1; + } } if(!strncmp(p, "FS", 2)) { enableTheory(THEORY_SETS); @@ -581,11 +604,28 @@ void LogicInfo::disableReals() { } } +void LogicInfo::arithTranscendentals() +{ + PrettyCheckArgument( + !d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + d_logicString = ""; + d_transcendentals = true; + if (!d_reals) + { + enableReals(); + } + if (d_linear) + { + arithNonLinear(); + } +} + void LogicInfo::arithOnlyDifference() { PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; + d_transcendentals = false; } void LogicInfo::arithOnlyLinear() { @@ -593,6 +633,7 @@ void LogicInfo::arithOnlyLinear() { d_logicString = ""; d_linear = true; d_differenceLogic = false; + d_transcendentals = false; } void LogicInfo::arithNonLinear() { |