api: Add Solver::mkSepEmp(). (#7432)

@alex-ozdemir

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2bc101bec1d98130ecbfdf212fbd1d819ce58cd3..bb39ae86d48f6dba9df5a0a9bf7f6790aedf5115 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5082,7 +5082,7 @@ Term Solver::mkTermFromKind(Kind kind) const
   CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY
                                    || kind == REGEXP_SIGMA || kind == SEP_EMP,
                                kind)
-      << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
+      << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP";
   //////// all checks before this line
   Node res;
   cvc5::Kind k = extToIntKind(kind);
@@ -5822,6 +5822,18 @@ Term Solver::mkEmptyBag(const Sort& sort) const
   CVC5_API_TRY_CATCH_END;
 }
 
+Term Solver::mkSepEmp() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  Node res = getNodeManager()->mkNullaryOperator(d_nodeMgr->booleanType(),
+                                                 cvc5::Kind::SEP_EMP);
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::mkSepNil(const Sort& sort) const
 {
   CVC5_API_TRY_CATCH_BEGIN;

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e6a19c77185b256158604c37f5dcd4a7324e65ec..c46b00d0e2601dc6e3d4ae2a0bbf3cfb2ddf5db8 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3443,6 +3443,12 @@ class CVC5_EXPORT Solver
    */
   Term mkEmptyBag(const Sort& sort) const;
 
+  /**
+   * Create a separation logic empty term.
+   * @return the separation logic empty term
+   */
+  Term mkSepEmp() const;
+
   /**
    * Create a separation logic nil term.
    * @param sort the sort of the nil term

diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
index b0bee500c4c7970f52bedaa13fec9ae570cd34fb..c46d60aee0d160a27c827a4394c252e5b6690a61 100644 (file)
--- a/src/api/java/cvc5/Solver.java
+++ b/src/api/java/cvc5/Solver.java
@@ -881,6 +881,18 @@ public class Solver implements IPointer
 
   private native long mkEmptyBag(long pointer, long sortPointer);
 
+  /**
+   * Create a separation logic empty term.
+   * @return the separation logic empty term
+   */
+  public Term mkSepEmp()
+  {
+    long termPointer = mkSepEmp(pointer);
+    return new Term(this, termPointer);
+  }
+
+  private native long mkSepEmp(long pointer);
+
   /**
    * Create a separation logic nil term.
    * @param sort the sort of the nil term

diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp
index c28ea412fb47a59bbbf625c9a2f1d6e70594d354..53c050c96cec8d74d13ef15ee952018cf16148e8 100644 (file)
--- a/src/api/java/jni/cvc5_Solver.cpp
+++ b/src/api/java/jni/cvc5_Solver.cpp
@@ -1059,6 +1059,22 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env,
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
+/*
+ * Class:     cvc5_Solver
+ * Method:    mkSepEmp
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env,
+                                                  jobject,
+                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  Term* retPointer = new Term(solver->mkSepEmp());
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
 /*
  * Class:     cvc5_Solver
  * Method:    mkSepNil
@@ -2591,4 +2607,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env,
   DatatypeDecl* ret = new DatatypeDecl();
   return reinterpret_cast<jlong>(ret);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
\ No newline at end of file
+}

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index e458b635df1a65f8a11e5d1974127f325d9072c5..02b5721209fc8284bbc7ff8906434b723b1e82b5 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -219,6 +219,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkRegexpSigma() except +
         Term mkEmptySet(Sort s) except +
         Term mkEmptyBag(Sort s) except +
+        Term mkSepEmp() except +
         Term mkSepNil(Sort sort) except +
         Term mkString(const string& s) except +
         Term mkString(const wstring& s) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 2ce8efb087503dc69081195dea9a5e35081086a9..4627859b9b6210e27452d8a5161a4ff321e169e2 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1168,6 +1168,15 @@ cdef class Solver:
         term.cterm = self.csolver.mkEmptyBag(s.csort)
         return term
 
+    def mkSepEmp(self):
+        """Create a separation logic empty term.
+
+        :return: the separation logic empty term
+        """
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkSepEmp()
+        return term
+
     def mkSepNil(self, Sort sort):
         """Create a separation logic nil term.
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e1ce29b65af006347887269bdc76b9b77cb8254f..be7bdcb0fa409dde8d773c666235026e75b8c40f 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -263,14 +263,16 @@ void Smt2::addFloatingPointOperators() {
 }
 
 void Smt2::addSepOperators() {
+  defineVar("sep.emp", d_solver->mkSepEmp());
+  // the Boolean sort is a placeholder here since we don't have type info
+  // without type annotation
+  defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
   addOperator(api::SEP_STAR, "sep");
   addOperator(api::SEP_PTO, "pto");
   addOperator(api::SEP_WAND, "wand");
-  addOperator(api::SEP_EMP, "emp");
   Parser::addOperator(api::SEP_STAR);
   Parser::addOperator(api::SEP_PTO);
   Parser::addOperator(api::SEP_WAND);
-  Parser::addOperator(api::SEP_EMP);
 }
 
 void Smt2::addCoreSymbols()
@@ -551,7 +553,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
 
     if (d_logic.areTranscendentalsUsed())
     {
-      defineVar("real.pi", d_solver->mkTerm(api::PI));
+      defineVar("real.pi", d_solver->mkPi());
       addTranscendentalOperators();
     }
     if (!strictModeEnabled())
@@ -677,12 +679,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addFloatingPointOperators();
   }
 
-  if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
-    // the Boolean sort is a placeholder here since we don't have type info
-    // without type annotation
-    defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
-    defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP));
-
+  if (d_logic.isTheoryEnabled(theory::THEORY_SEP))
+  {
     addSepOperators();
   }
 

diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 29d637dc6060ae51d906903af221f1af3e8a309f..6052a057fda5ab81d9ecc35b48481e630b23d6c2 100644 (file)
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -644,6 +644,10 @@ def test_mk_regexp_sigma(solver):
     solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma())
 
 
+def test_mk_sep_emp(solver):
+    solver.mkSepEmp();
+
+
 def test_mk_sep_nil(solver):
     solver.mkSepNil(solver.getBooleanSort())
     with pytest.raises(RuntimeError):

diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java
index d153b8a91f9f02a9de108c2ea1243c5873f892d6..6f9d8206db5ea5b01e6e2a800e9e977da71634e6 100644 (file)
--- a/test/unit/api/java/cvc5/SolverTest.java
+++ b/test/unit/api/java/cvc5/SolverTest.java
@@ -623,6 +623,11 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
   }
 
+  @Test void mkSepEmp()
+  {
+    assertDoesNotThrow(() -> d_solver.mkSepEmp());
+  }
+
   @Test void mkSepNil()
   {
     assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort()));
@@ -2342,4 +2347,4 @@ class SolverTest
             + "\"Z\")))",
         projection.toString());
   }
-}
\ No newline at end of file
+}

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index a294ad6cac437b21e062f406e95c7b7d5b587850..c9527c2d4dbd0908abddd9af2e9ca61f6270354e 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -597,6 +597,8 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma)
       d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
 }
 
+TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); }
+
 TEST_F(TestApiBlackSolver, mkSepNil)
 {
   ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));