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.cpp8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 525b129cf..a30867ee1 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -122,6 +122,10 @@ std::string LogicInfo::getLogicString() const {
}
++seen;
}
+ if(d_theories[THEORY_SETS]) {
+ ss << "_SETS";
+ ++seen;
+ }
if(seen != d_sharingTheories) {
Unhandled("can't extract a logic string from LogicInfo; at least one "
@@ -256,6 +260,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
arithNonLinear();
p += 4;
}
+ if(!strncmp(p, "_SETS", 5)) {
+ enableTheory(THEORY_SETS);
+ p += 5;
+ }
}
}
if(*p != '\0') {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback