From bef33ceaf0a6b69d76b4fd61cb03c990e86bc41c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 20 Oct 2021 16:12:55 -0700 Subject: [PATCH] api: Add Solver::mkSepEmp(). (#7432) @alex-ozdemir --- src/api/cpp/cvc5.cpp | 14 +++++++++++++- src/api/cpp/cvc5.h | 6 ++++++ src/api/java/cvc5/Solver.java | 12 ++++++++++++ src/api/java/jni/cvc5_Solver.cpp | 18 +++++++++++++++++- src/api/python/cvc5.pxd | 1 + src/api/python/cvc5.pxi | 9 +++++++++ src/parser/smt2/smt2.cpp | 16 +++++++--------- test/python/unit/api/test_solver.py | 4 ++++ test/unit/api/java/cvc5/SolverTest.java | 7 ++++++- test/unit/api/solver_black.cpp | 2 ++ 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 @@ -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 b0bee500c..c46d60aee 100644 --- 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 c28ea412f..53c050c96 100644 --- 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(pointer); + Term* retPointer = new Term(solver->mkSepEmp()); + return reinterpret_cast(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(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())); -- 2.30.2