diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/cut_log.h | 2 | ||||
-rw-r--r-- | src/theory/arith/delta_rational.h | 1 | ||||
-rw-r--r-- | src/theory/logic_info.cpp | 186 | ||||
-rw-r--r-- | src/theory/logic_info.h | 132 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 8 |
6 files changed, 204 insertions, 129 deletions
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index bbed13418..f4d392995 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -234,7 +234,7 @@ std::ostream& operator<<(std::ostream& os, const NodeLog& nl); class ApproximateSimplex; class TreeLog { private: - ApproximateSimplex* d_generator; + ApproximateSimplex* d_generator CVC4_UNUSED; int next_exec_ord; typedef std::map<int, NodeLog> ToNodeMap; diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 5f67847d8..39d5a9d64 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -22,6 +22,7 @@ #include <ostream> #include "base/exception.h" +#include "base/cvc4_assert.h" #include "util/integer.h" #include "util/rational.h" diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 15600fefc..02eeefcaf 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -78,8 +78,167 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : lock(); } +/** Is sharing enabled for this logic? */ +bool LogicInfo::isSharingEnabled() const { + PrettyCheckArgument(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 LogicInfo::isTheoryEnabled(theory::TheoryId theory) const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_theories[theory]; +} + +/** Is this a quantified logic? */ +bool LogicInfo::isQuantified() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return isTheoryEnabled(theory::THEORY_QUANTIFIERS); +} + +/** Is this the all-inclusive logic? */ +bool LogicInfo::hasEverything() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + LogicInfo everything; + everything.lock(); + return *this == everything; +} + +/** Is this the all-exclusive logic? (Here, that means propositional logic) */ +bool LogicInfo::hasNothing() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + LogicInfo nothing(""); + nothing.lock(); + return *this == nothing; +} + +bool LogicInfo::isPure(theory::TheoryId theory) const { + PrettyCheckArgument(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 LogicInfo::areIntegersUsed() 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 integers are used"); + return d_integers; +} + +bool LogicInfo::areRealsUsed() 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 reals are used"); + return d_reals; +} + +bool LogicInfo::isLinear() 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 it's linear"); + return d_linear || d_differenceLogic; +} + +bool LogicInfo::isDifferenceLogic() 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 it's difference logic"); + return d_differenceLogic; +} + +bool LogicInfo::hasCardinalityConstraints() const { + PrettyCheckArgument(d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); + return d_cardinalityConstraints; +} + + +bool LogicInfo::operator==(const LogicInfo& other) const { + PrettyCheckArgument(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; + } + } + + 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; + } else { + return true; + } +} + +bool LogicInfo::operator<=(const LogicInfo& other) const { + PrettyCheckArgument(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; + } + } + 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); + } else { + return true; + } +} + +bool LogicInfo::operator>=(const LogicInfo& other) const { + PrettyCheckArgument(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; + } + } + 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); + } else { + return true; + } +} + std::string LogicInfo::getLogicString() const { - CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + PrettyCheckArgument( + d_locked, *this, + "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { LogicInfo qf_all_supported; qf_all_supported.disableQuantifiers(); @@ -156,7 +315,8 @@ std::string LogicInfo::getLogicString() const { } void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!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 } @@ -299,17 +459,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } void LogicInfo::enableEverything() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(); } void LogicInfo::disableEverything() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); *this = LogicInfo(""); } void LogicInfo::enableTheory(theory::TheoryId theory) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(!d_theories[theory]) { if(isTrueTheory(theory)) { ++d_sharingTheories; @@ -320,7 +480,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) { } void LogicInfo::disableTheory(theory::TheoryId theory) { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); if(d_theories[theory]) { if(isTrueTheory(theory)) { Assert(d_sharingTheories > 0); @@ -336,14 +496,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } void LogicInfo::enableIntegers() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_integers = true; } void LogicInfo::disableIntegers() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_integers = false; if(!d_reals) { @@ -352,14 +512,14 @@ void LogicInfo::disableIntegers() { } void LogicInfo::enableReals() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; enableTheory(THEORY_ARITH); d_reals = true; } void LogicInfo::disableReals() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_reals = false; if(!d_integers) { @@ -368,21 +528,21 @@ void LogicInfo::disableReals() { } void LogicInfo::arithOnlyDifference() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = true; } void LogicInfo::arithOnlyLinear() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; d_linear = true; d_differenceLogic = false; } void LogicInfo::arithNonLinear() { - CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); + PrettyCheckArgument(!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 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 { diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 798576ec3..b92d72ef4 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1817,11 +1817,9 @@ void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& c std::map< int, std::vector< Node > > disj; std::map< int, std::vector< Node > > fvs; for( unsigned i=0; i<body.getNumChildren(); i++ ){ - int pid = getPurifyIdLit( body[i] ); - + int pid CVC4_UNUSED = getPurifyIdLit( body[i] ); } //mark as an attribute //Node attr = NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, body ); - } } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a39d74bb0..fb5fb0f0c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -22,10 +22,11 @@ #include "theory/uf/theory_uf_model.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; + +namespace CVC4 { +namespace theory { TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) : d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) @@ -963,3 +964,6 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) } } } + +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ |