diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-12 21:27:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-12 19:27:33 -0700 |
commit | 0d51f9839eb4a242de33576d884af82004d68cf2 (patch) | |
tree | 2a24fc86716af2c44b2554b22ffa0a00399b4a92 /src/theory/logic_info.cpp | |
parent | 8ddd5e82c8e896977d5573b639524264c7207d85 (diff) |
Minor simplifications to LogicInfo (#6737)test-tag2
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r-- | src/theory/logic_info.cpp | 30 |
1 files changed, 11 insertions, 19 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 05f8c7a9f..8ba43aa1a 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -122,20 +122,10 @@ bool LogicInfo::hasEverything() const PrettyCheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - // 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; + LogicInfo everything; + everything.enableEverything(isHigherOrder()); + everything.lock(); + return (*this == everything); } /** Is this the all-exclusive logic? (Here, that means propositional logic) */ @@ -223,16 +213,18 @@ bool LogicInfo::operator==(const LogicInfo& other) const { PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency"); - bool res = d_cardinalityConstraints == other.d_cardinalityConstraints - && d_higherOrder == other.d_higherOrder; + if (d_cardinalityConstraints != other.d_cardinalityConstraints || + d_higherOrder != other.d_higherOrder ) + { + return false; + } if(isTheoryEnabled(theory::THEORY_ARITH)) { 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 && res; - } else { - return res; + && d_differenceLogic == other.d_differenceLogic; } + return true; } bool LogicInfo::operator<=(const LogicInfo& other) const { |