summaryrefslogtreecommitdiff
path: root/src/theory/logic_info.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r--src/theory/logic_info.cpp285
1 files changed, 285 insertions, 0 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
new file mode 100644
index 000000000..ba7119071
--- /dev/null
+++ b/src/theory/logic_info.cpp
@@ -0,0 +1,285 @@
+/********************* */
+/*! \file logic_info.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class giving information about a logic (group a theory modules
+ ** and configuration information)
+ **
+ ** A class giving information about a logic (group of theory modules and
+ ** configuration information).
+ **/
+
+#include <string>
+#include <cstring>
+#include <sstream>
+
+#include "expr/kind.h"
+#include "theory/logic_info.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+
+LogicInfo::LogicInfo() :
+ d_logicString(""),
+ d_theories(),
+ d_sharingTheories(0),
+ d_integers(true),
+ d_reals(true),
+ d_linear(false) {
+
+ for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
+ d_theories[id] = false;// ensure it's cleared
+ enableTheory(id);
+ }
+}
+
+LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
+ d_logicString(""),
+ d_theories(),
+ d_sharingTheories(0),
+ d_integers(false),
+ d_reals(false),
+ d_linear(false) {
+ setLogicString(logicString);
+}
+
+std::string LogicInfo::getLogicString() const {
+ if(d_logicString == "") {
+ size_t seen = 0; // make sure we support all the active theories
+
+ stringstream ss;
+ if(!isQuantified()) {
+ ss << "QF_";
+ }
+ if(d_theories[THEORY_ARRAY]) {
+ ss << (d_sharingTheories == 1 ? "AX" : "A");
+ ++seen;
+ }
+ if(d_theories[THEORY_UF]) {
+ ss << "UF";
+ ++seen;
+ }
+ if(d_theories[THEORY_BV]) {
+ ss << "BV";
+ ++seen;
+ }
+ if(d_theories[THEORY_DATATYPES]) {
+ ss << "DT";
+ ++seen;
+ }
+ if(d_theories[THEORY_ARITH]) {
+ if(isDifferenceLogic()) {
+ ss << (areIntegersUsed() ? "I" : "");
+ ss << (areRealsUsed() ? "R" : "");
+ ss << "DL";
+ } else {
+ ss << (isLinear() ? "L" : "N");
+ ss << (areIntegersUsed() ? "I" : "");
+ ss << (areRealsUsed() ? "R" : "");
+ ss << "A";
+ }
+ ++seen;
+ }
+
+ if(seen != d_sharingTheories) {
+ Unhandled("can't extract a logic string from LogicInfo; at least one "
+ "active theory is unknown to LogicInfo::getLogicString() !");
+ }
+
+ if(seen == 0) {
+ ss << "SAT";
+ }
+
+ d_logicString = ss.str();
+ }
+ return d_logicString;
+}
+
+void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
+ for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
+ d_theories[id] = false;// ensure it's cleared
+ }
+ d_sharingTheories = 0;
+
+ // Below, ONLY use enableTheory()/disableTheory() rather than
+ // accessing d_theories[] directly. This makes sure to set up
+ // sharing properly.
+
+ enableTheory(THEORY_BUILTIN);
+ enableTheory(THEORY_BOOL);
+
+ const char* p = logicString.c_str();
+ if(!strcmp(p, "QF_SAT") || *p == '\0') {
+ // propositional logic only; we're done.
+ p += 6;
+ } else {
+ if(!strncmp(p, "QF_", 3)) {
+ disableQuantifiers();
+ p += 3;
+ } else {
+ enableQuantifiers();
+ }
+ if(!strncmp(p, "AX", 2)) {
+ enableTheory(THEORY_ARRAY);
+ p += 2;
+ } else {
+ if(*p == 'A') {
+ enableTheory(THEORY_ARRAY);
+ ++p;
+ }
+ if(!strncmp(p, "UF", 2)) {
+ enableTheory(THEORY_UF);
+ p += 2;
+ }
+ if(!strncmp(p, "BV", 2)) {
+ enableTheory(THEORY_BV);
+ p += 2;
+ }
+ if(!strncmp(p, "DT", 2)) {
+ enableTheory(THEORY_DATATYPES);
+ p += 2;
+ }
+ if(!strncmp(p, "IDL", 3)) {
+ enableIntegers();
+ disableReals();
+ arithOnlyDifference();
+ p += 3;
+ } else if(!strncmp(p, "RDL", 3)) {
+ disableIntegers();
+ enableReals();
+ arithOnlyDifference();
+ p += 3;
+ } else if(!strncmp(p, "IRDL", 4)) {
+ // "IRDL" ?! --not very useful, but getLogicString() can produce
+ // that string, so we really had better be able to read it back in.
+ enableIntegers();
+ enableReals();
+ arithOnlyDifference();
+ p += 4;
+ } else if(!strncmp(p, "LIA", 3)) {
+ enableIntegers();
+ disableReals();
+ arithOnlyLinear();
+ p += 3;
+ } else if(!strncmp(p, "LRA", 3)) {
+ disableIntegers();
+ enableReals();
+ arithOnlyLinear();
+ p += 3;
+ } else if(!strncmp(p, "LIRA", 4)) {
+ enableIntegers();
+ enableReals();
+ arithOnlyLinear();
+ p += 4;
+ } else if(!strncmp(p, "NIA", 3)) {
+ enableIntegers();
+ disableReals();
+ arithNonLinear();
+ p += 3;
+ } else if(!strncmp(p, "NRA", 3)) {
+ disableIntegers();
+ enableReals();
+ arithNonLinear();
+ p += 3;
+ } else if(!strncmp(p, "NIRA", 4)) {
+ enableIntegers();
+ enableReals();
+ arithNonLinear();
+ p += 4;
+ }
+ }
+ }
+ if(*p != '\0') {
+ stringstream err;
+ err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString;
+ IllegalArgument(logicString, err.str().c_str());
+ }
+
+ // ensure a getLogic() returns the same thing as was set
+ d_logicString = logicString;
+}
+
+void LogicInfo::enableTheory(theory::TheoryId theory) {
+ if(!d_theories[theory]) {
+ if(isTrueTheory(theory)) {
+ ++d_sharingTheories;
+ }
+ d_logicString = "";
+ d_theories[theory] = true;
+ }
+}
+
+void LogicInfo::disableTheory(theory::TheoryId theory) {
+ if(d_theories[theory]) {
+ if(isTrueTheory(theory)) {
+ Assert(d_sharingTheories > 0);
+ --d_sharingTheories;
+ }
+ if(theory == THEORY_BUILTIN ||
+ theory == THEORY_BOOL) {
+ return;
+ }
+ d_logicString = "";
+ d_theories[theory] = false;
+ }
+}
+
+void LogicInfo::enableIntegers() {
+ d_logicString = "";
+ enableTheory(THEORY_ARITH);
+ d_integers = true;
+}
+
+void LogicInfo::disableIntegers() {
+ d_logicString = "";
+ d_integers = false;
+ if(!d_reals) {
+ disableTheory(THEORY_ARITH);
+ }
+}
+
+void LogicInfo::enableReals() {
+ d_logicString = "";
+ enableTheory(THEORY_ARITH);
+ d_reals = true;
+}
+
+void LogicInfo::disableReals() {
+ d_logicString = "";
+ d_reals = false;
+ if(!d_integers) {
+ disableTheory(THEORY_ARITH);
+ }
+}
+
+void LogicInfo::arithOnlyDifference() {
+ d_logicString = "";
+ d_linear = true;
+ d_differenceLogic = true;
+}
+
+void LogicInfo::arithOnlyLinear() {
+ d_logicString = "";
+ d_linear = true;
+ d_differenceLogic = false;
+}
+
+void LogicInfo::arithNonLinear() {
+ d_logicString = "";
+ d_linear = false;
+ d_differenceLogic = false;
+}
+
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback