Properly implement logic info for separation logic (#3176)

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