Properly implement logic info for separation logic (#3176)

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 37b25163a4e5cf3af3a4b3fb7722d905b98f65bc..34ea5f9b16700e6eb96fe708c7aee0194e3c206e 100644 (file)
--- 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 969810a6f705916ed9f26b6eb2c7af4c462793ef..a19936c343bdba7084a9e2d95bb965e657af42c1 100644 (file)
--- 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
 

diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 27e2aa2c35b0ec3530139ee93bdb28d006c1f0b1..2eaf664cd25930701e5e92f811f3e377c36944fe 100644 (file)
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_SEP_LIA)
 (assert (not (_ emp Int Int)))
 (check-sat)

diff --git a/test/regress/regress1/sep/sep-find2.smt2 b/test/regress/regress1/sep/sep-find2.smt2
index 356f866c186acebecb4093327001447a2b196675..3d6188894eb21352bd8aca9f8b31bbec9b3d8420 100644 (file)
--- a/test/regress/regress1/sep/sep-find2.smt2
+++ b/test/regress/regress1/sep/sep-find2.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_ALL_SUPPORTED)
+(set-logic QF_SEP_LIA)
 (set-info :status unsat)
 
 (declare-const x1 Int)

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 2cc53bef3d03536ea016dd9e7c63a6ebaeae4554..c2ca621d9565bba5a6924af74d12373ad74a5e45 100644 (file)
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -541,13 +541,13 @@ public:
     info.arithOnlyLinear();
     info.disableIntegers();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVFPDTLRASEP" );
+    TS_ASSERT_EQUALS(info.getLogicString(), "SEP_AUFBVFPDTLRA");
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
     info.disableQuantifiers();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVFPDTLRASEP" );
+    TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
@@ -556,7 +556,7 @@ public:
     info.enableIntegers();
     info.disableReals();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFFPLIASEP" );
+    TS_ASSERT_EQUALS(info.getLogicString(), "QF_SEP_AUFFPLIA");
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );