From a39ad6584c1d61e22e72b53c3838f4f675ed2e19 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 24 Dec 2015 05:38:43 -0500 Subject: 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. --- src/theory/logic_info.h | 132 ++++++++---------------------------------------- 1 file changed, 22 insertions(+), 110 deletions(-) (limited to 'src/theory/logic_info.h') diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 9cecc88b7..54b735114 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -104,84 +104,43 @@ public: std::string getLogicString() const; /** Is sharing enabled for this logic? */ - bool isSharingEnabled() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return d_sharingTheories > 1; - } + bool isSharingEnabled() const; /** Is the given theory module active in this logic? */ - bool isTheoryEnabled(theory::TheoryId theory) const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return d_theories[theory]; - } + bool isTheoryEnabled(theory::TheoryId theory) const; /** Is this a quantified logic? */ - bool isQuantified() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return isTheoryEnabled(theory::THEORY_QUANTIFIERS); - } + bool isQuantified() const; /** Is this the all-inclusive logic? */ - bool hasEverything() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - LogicInfo everything; - everything.lock(); - return *this == everything; - } + bool hasEverything() const; /** Is this the all-exclusive logic? (Here, that means propositional logic) */ - bool hasNothing() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - LogicInfo nothing(""); - nothing.lock(); - return *this == nothing; - } + bool hasNothing() const; /** * Is this a pure logic (only one "true" background theory). Quantifiers * can exist in such logics though; to test for quantifier-free purity, * use "isPure(theory) && !isQuantified()". */ - bool isPure(theory::TheoryId theory) const { - 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() && - ( !isTrueTheory(theory) || d_sharingTheories == 1 ) && - ( isTrueTheory(theory) || d_sharingTheories == 0 ); - } + bool isPure(theory::TheoryId theory) const; // these are for arithmetic /** Are integers in this logic? */ - bool areIntegersUsed() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); - return d_integers; - } + bool areIntegersUsed() const; + /** Are reals in this logic? */ - bool areRealsUsed() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); - return d_reals; - } + bool areRealsUsed() const; + /** Does this logic only linear arithmetic? */ - bool isLinear() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); - return d_linear || d_differenceLogic; - } + bool isLinear() const; + /** Does this logic only permit difference reasoning? (implies linear) */ - bool isDifferenceLogic() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); - return d_differenceLogic; - } + bool isDifferenceLogic() const; + /** Does this logic allow cardinality constraints? */ - bool hasCardinalityConstraints() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); - return d_cardinalityConstraints; - } + bool hasCardinalityConstraints() const; // MUTATORS @@ -258,74 +217,27 @@ public: // COMPARISON /** Are these two LogicInfos equal? */ - bool operator==(const LogicInfo& other) const { - 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; - } - } - CheckArgument(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 operator==(const LogicInfo& other) const; + /** Are these two LogicInfos disequal? */ bool operator!=(const LogicInfo& other) const { return !(*this == other); } + /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */ bool operator>(const LogicInfo& other) const { return *this >= other && *this != other; } + /** Is this LogicInfo "less than" (does it contain strictly less) the other? */ bool operator<(const LogicInfo& other) const { return *this <= other && *this != other; } /** Is this LogicInfo "less than or equal" the other? */ - bool operator<=(const LogicInfo& other) const { - 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; - } - } - 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) && - (!d_reals || other.d_reals) && - (d_linear || !other.d_linear) && - (d_differenceLogic || !other.d_differenceLogic); - } else { - return true; - } - } + bool operator<=(const LogicInfo& other) const; + /** Is this LogicInfo "greater than or equal" the other? */ - bool operator>=(const LogicInfo& other) const { - 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; - } - } - 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) && - (d_reals || !other.d_reals) && - (!d_linear || other.d_linear) && - (!d_differenceLogic || other.d_differenceLogic); - } else { - return true; - } - } + bool operator>=(const LogicInfo& other) const; /** Are two LogicInfos comparable? That is, is one of <= or > true? */ bool isComparableTo(const LogicInfo& other) const { -- cgit v1.2.3