Simplify the syntax and representation of the separation logic empty heap constraint (#7268)

Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.

This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.

1 files changed, 9 insertions, 4 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d33ef5b42..42690586a 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5079,21 +5079,26 @@ Sort Solver::mkTupleSortHelper(const std::vector<Sort>& sorts) const
 
 Term Solver::mkTermFromKind(Kind kind) const
 {
-  CVC5_API_KIND_CHECK_EXPECTED(
-      kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
+  CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY
+                                   || kind == REGEXP_SIGMA || kind == SEP_EMP,
+                               kind)
       << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
   //////// all checks before this line
   Node res;
+  cvc5::Kind k = extToIntKind(kind);
   if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
   {
-    cvc5::Kind k = extToIntKind(kind);
     Assert(isDefinedIntKind(k));
     res = d_nodeMgr->mkNode(k, std::vector<Node>());
   }
+  else if (kind == SEP_EMP)
+  {
+    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->booleanType(), k);
+  }
   else
   {
     Assert(kind == PI);
-    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), cvc5::kind::PI);
+    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), k);
   }
   (void)res.getType(true); /* kick off type checking */
   increment_term_stats(kind);