diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-04 19:28:44 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-04 21:28:44 -0500 |
commit | af5832b414fbee30904014aaf68a7f3b277b693d (patch) | |
tree | 5b6738aa895913c2858ff8751c573c51c6bd7b99 /src/theory | |
parent | 1e8a4e25751263a923a8d4cfd4d404fc0d24aa03 (diff) |
Only enable transcendentals if logic is N[I]RAT (#2052)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/logic_info.cpp | 71 | ||||
-rw-r--r-- | src/theory/logic_info.h | 7 |
2 files changed, 63 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() { diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index cbb04604e..5eac6a3da 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -51,6 +51,8 @@ class CVC4_PUBLIC LogicInfo { bool d_integers; /** are reals used in this logic? */ bool d_reals; + /** transcendentals in this logic? */ + bool d_transcendentals; /** linear-only arithmetic in this logic? */ bool d_linear; /** difference-only arithmetic in this logic? */ @@ -138,6 +140,9 @@ public: /** Are reals in this logic? */ bool areRealsUsed() const; + /** Are transcendentals in this logic? */ + bool areTranscendentalsUsed() const; + /** Does this logic only linear arithmetic? */ bool isLinear() const; @@ -206,6 +211,8 @@ public: void enableReals(); /** Disable the use of reals in this logic. */ void disableReals(); + /** Enable the use of transcendentals in this logic. */ + void arithTranscendentals(); /** Only permit difference arithmetic in this logic. */ void arithOnlyDifference(); /** Only permit linear arithmetic in this logic. */ |