From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Aug 2019 16:29:47 +0000 (-0500)
Subject: Properly implement logic info for separation logic (#3176)
X-Git-Tag: cvc5-1.0.0~4025
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8fd4ac8bff4aa7a4b4e04e35f6944d303d5cf498;p=cvc5.git

Properly implement logic info for separation logic (#3176)
---

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
 
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index 27e2aa2c3..2eaf664cd 100644
--- 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 356f866c1..3d6188894 100644
--- 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 2cc53bef3..c2ca621d9 100644
--- 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() );