diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 11:29:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-13 11:29:47 -0500 |
commit | 8fd4ac8bff4aa7a4b4e04e35f6944d303d5cf498 (patch) | |
tree | 0344ffc01fbc5d27faf19e0ef0a0de36551145eb /src | |
parent | 47b910a85de71b6617e4d1d210dcb57de597961b (diff) |
Properly implement logic info for separation logic (#3176)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/logic_info.cpp | 25 | ||||
-rw-r--r-- | src/theory/logic_info.h | 5 |
2 files changed, 22 insertions, 8 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 37b25163a..34ea5f9b1 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -283,6 +283,11 @@ std::string LogicInfo::getLogicString() const { if(!isQuantified()) { ss << "QF_"; } + if (d_theories[THEORY_SEP]) + { + ss << "SEP_"; + ++seen; + } if(d_theories[THEORY_ARRAYS]) { ss << (d_sharingTheories == 1 ? "AX" : "A"); ++seen; @@ -328,10 +333,6 @@ std::string LogicInfo::getLogicString() const { ss << "FS"; ++seen; } - if(d_theories[THEORY_SEP]) { - ss << "SEP"; - ++seen; - } if(seen != d_sharingTheories) { Unhandled("can't extract a logic string from LogicInfo; at least one " "active theory is unknown to LogicInfo::getLogicString() !"); @@ -412,6 +413,11 @@ void LogicInfo::setLogicString(std::string logicString) } else { enableQuantifiers(); } + if (!strncmp(p, "SEP_", 4)) + { + enableSeparationLogic(); + p += 4; + } if(!strncmp(p, "AX", 2)) { enableTheory(THEORY_ARRAYS); p += 2; @@ -511,10 +517,6 @@ void LogicInfo::setLogicString(std::string logicString) enableTheory(THEORY_SETS); p += 2; } - if(!strncmp(p, "SEP", 3)) { - enableTheory(THEORY_SEP); - p += 3; - } } } @@ -588,6 +590,13 @@ void LogicInfo::enableSygus() enableHigherOrder(); } +void LogicInfo::enableSeparationLogic() +{ + enableTheory(THEORY_SEP); + enableTheory(THEORY_UF); + enableTheory(THEORY_SETS); +} + void LogicInfo::enableIntegers() { PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 969810a6f..a19936c34 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -206,6 +206,11 @@ public: * This means enabling quantifiers, datatypes, UF, integers, and higher order. */ void enableSygus(); + /** + * Enable everything that is needed for separation logic. This means enabling + * the theories of separation logic, UF and sets. + */ + void enableSeparationLogic(); // these are for arithmetic |