summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cpp/cvc5.cpp14
-rw-r--r--src/api/cpp/cvc5.h6
-rw-r--r--src/api/java/cvc5/Solver.java12
-rw-r--r--src/api/java/jni/cvc5_Solver.cpp18
-rw-r--r--src/api/python/cvc5.pxd1
-rw-r--r--src/api/python/cvc5.pxi9
-rw-r--r--src/parser/smt2/smt2.cpp16
-rw-r--r--test/python/unit/api/test_solver.py4
-rw-r--r--test/unit/api/java/cvc5/SolverTest.java7
-rw-r--r--test/unit/api/solver_black.cpp2
10 files changed, 77 insertions, 12 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2bc101bec..bb39ae86d 100644
--- 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 e6a19c771..c46b00d0e 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3444,6 +3444,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
* @return the separation logic nil term
diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
index b0bee500c..c46d60aee 100644
--- a/src/api/java/cvc5/Solver.java
+++ b/src/api/java/cvc5/Solver.java
@@ -882,6 +882,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
* @return the separation logic nil term
diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp
index c28ea412f..53c050c96 100644
--- a/src/api/java/jni/cvc5_Solver.cpp
+++ b/src/api/java/jni/cvc5_Solver.cpp
@@ -1061,6 +1061,22 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env,
/*
* 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
* Signature: (JJ)J
*/
@@ -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 e458b635d..02b572120 100644
--- 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 2ce8efb08..4627859b9 100644
--- 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 e1ce29b65..be7bdcb0f 100644
--- 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 29d637dc6..6052a057f 100644
--- 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 d153b8a91..6f9d8206d 100644
--- 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 a294ad6ca..c9527c2d4 100644
--- 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()));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback