summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/cut_log.h2
-rw-r--r--src/theory/arith/delta_rational.h1
-rw-r--r--src/theory/logic_info.cpp186
-rw-r--r--src/theory/logic_info.h132
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp4
-rw-r--r--src/theory/theory_model.cpp8
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback