summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/logic_info.cpp51
-rw-r--r--src/theory/logic_info.h55
2 files changed, 98 insertions, 8 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index ba7119071..d0c1e4b6a 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -37,7 +37,9 @@ LogicInfo::LogicInfo() :
d_sharingTheories(0),
d_integers(true),
d_reals(true),
- d_linear(false) {
+ d_linear(false),
+ d_differenceLogic(false),
+ d_locked(false) {
for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
d_theories[id] = false;// ensure it's cleared
@@ -51,11 +53,16 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
d_sharingTheories(0),
d_integers(false),
d_reals(false),
- d_linear(false) {
+ d_linear(false),
+ d_differenceLogic(false),
+ d_locked(false) {
+
setLogicString(logicString);
+ lock();
}
std::string LogicInfo::getLogicString() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
if(d_logicString == "") {
size_t seen = 0; // make sure we support all the active theories
@@ -108,6 +115,7 @@ std::string LogicInfo::getLogicString() const {
}
void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
+ Assert(!d_locked, "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
}
@@ -124,6 +132,16 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
if(!strcmp(p, "QF_SAT") || *p == '\0') {
// propositional logic only; we're done.
p += 6;
+ } else if(!strcmp(p, "QF_ALL_SUPPORTED")) {
+ // the "all theories included" logic, no quantifiers
+ enableEverything();
+ disableQuantifiers();
+ p += 16;
+ } else if(!strcmp(p, "ALL_SUPPORTED")) {
+ // the "all theories included" logic, with quantifiers
+ enableEverything();
+ enableQuantifiers();
+ p += 13;
} else {
if(!strncmp(p, "QF_", 3)) {
disableQuantifiers();
@@ -211,7 +229,18 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
d_logicString = logicString;
}
+void LogicInfo::enableEverything() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ *this = LogicInfo();
+}
+
+void LogicInfo::disableEverything() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ *this = LogicInfo("");
+}
+
void LogicInfo::enableTheory(theory::TheoryId theory) {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
if(!d_theories[theory]) {
if(isTrueTheory(theory)) {
++d_sharingTheories;
@@ -222,6 +251,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) {
}
void LogicInfo::disableTheory(theory::TheoryId theory) {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
if(d_theories[theory]) {
if(isTrueTheory(theory)) {
Assert(d_sharingTheories > 0);
@@ -237,12 +267,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) {
}
void LogicInfo::enableIntegers() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
enableTheory(THEORY_ARITH);
d_integers = true;
}
void LogicInfo::disableIntegers() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_integers = false;
if(!d_reals) {
@@ -251,12 +283,14 @@ void LogicInfo::disableIntegers() {
}
void LogicInfo::enableReals() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
enableTheory(THEORY_ARITH);
d_reals = true;
}
void LogicInfo::disableReals() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_reals = false;
if(!d_integers) {
@@ -265,21 +299,34 @@ void LogicInfo::disableReals() {
}
void LogicInfo::arithOnlyDifference() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = true;
d_differenceLogic = true;
}
void LogicInfo::arithOnlyLinear() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = true;
d_differenceLogic = false;
}
void LogicInfo::arithNonLinear() {
+ Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = false;
d_differenceLogic = false;
}
+LogicInfo LogicInfo::getUnlockedCopy() const {
+ if(d_locked) {
+ LogicInfo info = *this;
+ info.d_locked = false;
+ return info;
+ } else {
+ return *this;
+ }
+}
+
}/* CVC4 namespace */
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index d5b8be58d..33a059bb9 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -54,6 +54,8 @@ class LogicInfo {
bool d_linear; /**< linear-only arithmetic in this logic? */
bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
+ bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
+
/**
* Returns true iff this is a "true" theory (one that must be worried
* about for sharing
@@ -95,12 +97,19 @@ public:
std::string getLogicString() const;
/** Is sharing enabled for this logic? */
- bool isSharingEnabled() const { return d_sharingTheories > 1; }
+ bool isSharingEnabled() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_sharingTheories > 1;
+ }
/** Is the given theory module active in this logic? */
- bool isTheoryEnabled(theory::TheoryId theory) const { return d_theories[theory]; }
+ bool isTheoryEnabled(theory::TheoryId theory) const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_theories[theory];
+ }
/** Is this a quantified logic? */
bool isQuantified() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
}
@@ -110,6 +119,7 @@ public:
* use "isPure(theory) && !isQuantified()".
*/
bool isPure(theory::TheoryId theory) const {
+ Assert(d_locked, "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() &&
@@ -120,13 +130,25 @@ public:
// these are for arithmetic
/** Are integers in this logic? */
- bool areIntegersUsed() const { return d_integers; }
+ bool areIntegersUsed() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_integers;
+ }
/** Are reals in this logic? */
- bool areRealsUsed() const { return d_reals; }
+ bool areRealsUsed() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_reals;
+ }
/** Does this logic only linear arithmetic? */
- bool isLinear() const { return d_linear || d_differenceLogic; }
+ bool isLinear() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_linear || d_differenceLogic;
+ }
/** Does this logic only permit difference reasoning? (implies linear) */
- bool isDifferenceLogic() const { return d_differenceLogic; }
+ bool isDifferenceLogic() const {
+ Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_differenceLogic;
+ }
// MUTATORS
@@ -138,6 +160,18 @@ public:
void setLogicString(std::string logicString) throw(IllegalArgumentException);
/**
+ * Enable all functionality. All theories, plus quantifiers, will be
+ * enabled.
+ */
+ void enableEverything();
+
+ /**
+ * Disable all functionality. The result will be a LogicInfo with
+ * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
+ */
+ void disableEverything();
+
+ /**
* Enable the given theory module.
*/
void enableTheory(theory::TheoryId theory);
@@ -181,6 +215,15 @@ public:
/** Permit nonlinear arithmetic in this logic. */
void arithNonLinear();
+ // LOCKING FUNCTIONALITY
+
+ /** Lock this LogicInfo, disabling further mutation and allowing queries */
+ void lock() { d_locked = true; }
+ /** Check whether this LogicInfo is locked, disallowing further mutation */
+ bool isLocked() const { return d_locked; }
+ /** Get a copy of this LogicInfo that is identical, but unlocked */
+ LogicInfo getUnlockedCopy() const;
+
};/* class LogicInfo */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback