From 4877909b806329e5e0e14dcfc3c404b8e4f6c0af Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 10 Nov 2021 13:10:16 -0800 Subject: [PATCH] api: Add Solver::mkRegexpAll(). (#7614) --- src/api/cpp/cvc5.cpp | 13 +++++++++++++ src/api/cpp/cvc5.h | 14 ++++++++++---- src/api/java/io/github/cvc5/api/Solver.java | 20 ++++++++++++++++---- src/api/java/jni/solver.cpp | 15 +++++++++++++++ src/api/python/cvc5.pxd | 3 ++- src/api/python/cvc5.pxi | 21 +++++++++++++++------ src/parser/smt2/smt2.cpp | 4 +--- test/unit/api/cpp/solver_black.cpp | 13 ++++++++++--- test/unit/api/java/SolverTest.java | 7 +++++++ test/unit/api/python/test_solver.py | 10 ++++++++-- 10 files changed, 97 insertions(+), 23 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index ae0ee2ceb..4dcfb466e 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5796,6 +5796,19 @@ Term Solver::mkReal(int64_t num, int64_t den) const CVC5_API_TRY_CATCH_END; } +Term Solver::mkRegexpAll() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + Node res = d_nodeMgr->mkNode( + cvc5::kind::REGEXP_STAR, + d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALLCHAR, std::vector())); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::mkRegexpNone() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 91a6ae447..ab9a4de25 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3443,17 +3443,23 @@ class CVC5_EXPORT Solver Term mkReal(int64_t num, int64_t den) const; /** - * Create a regular expression none (re.none) term. - * @return the empty term + * Create a regular expression all (re.all) term. + * @return the all term */ - Term mkRegexpNone() const; + Term mkRegexpAll() const; /** * Create a regular expression allchar (re.allchar) term. - * @return the sigma term + * @return the allchar term */ Term mkRegexpAllchar() const; + /** + * Create a regular expression none (re.none) term. + * @return the none term + */ + Term mkRegexpNone() const; + /** * Create a constant representing an empty set of the given sort. * @param sort the sort of the set elements. diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 09ad66f5b..16220228c 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -851,8 +851,8 @@ public class Solver implements IPointer, AutoCloseable private native long mkReal(long pointer, long num, long den); /** - * Create a regular expression empty term. - * @return the empty term + * Create a regular expression none (re.none) term. + * @return the none term */ public Term mkRegexpNone() { @@ -863,8 +863,20 @@ public class Solver implements IPointer, AutoCloseable private native long mkRegexpNone(long pointer); /** - * Create a regular expression sigma term. - * @return the sigma term + * Create a regular expression all (re.all) term. + * @return the all term + */ + public Term mkRegexpAll() + { + long termPointer = mkRegexpAll(pointer); + return new Term(this, termPointer); + } + + private native long mkRegexpAll(long pointer); + + /** + * Create a regular expression allchar (re.allchar) term. + * @return the allchar term */ public Term mkRegexpAllchar() { diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index a3ce49f4e..2e4404362 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -990,6 +990,21 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpNone( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_api_Solver + * Method: mkRegexpAll + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkRegexpAll(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast(pointer); + Term* retPointer = new Term(solver->mkRegexpAll()); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Solver * Method: mkRegexpAllchar diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index baee5899e..9dae7da96 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -215,8 +215,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkInteger(const uint64_t i) except + Term mkInteger(const string& s) except + Term mkReal(const string& s) except + - Term mkRegexpNone() except + + Term mkRegexpAll() except + Term mkRegexpAllchar() except + + Term mkRegexpNone() except + Term mkEmptySet(Sort s) except + Term mkEmptyBag(Sort s) except + Term mkSepEmp() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 9e1aeaca1..1df252e86 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1130,24 +1130,33 @@ cdef class Solver: term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode()) return term - def mkRegexpNone(self): - """Create a regular expression empty term. + def mkRegexpAll(self): + """Create a regular expression all (re.all) term. - :return: the empty term + :return: the all term """ cdef Term term = Term(self) - term.cterm = self.csolver.mkRegexpNone() + term.cterm = self.csolver.mkRegexpAll() return term def mkRegexpAllchar(self): - """Create a regular expression sigma term. + """Create a regular expression allchar (re.allchar) term. - :return: the sigma term + :return: the allchar term """ cdef Term term = Term(self) term.cterm = self.csolver.mkRegexpAllchar() return term + def mkRegexpNone(self): + """Create a regular expression none (re.none) term. + + :return: the none term + """ + cdef Term term = Term(self) + term.cterm = self.csolver.mkRegexpNone() + return term + def mkEmptySet(self, Sort s): """Create a constant representing an empty set of the given sort. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 1fc7a637f..b4f39a315 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -145,9 +145,7 @@ void Smt2::addDatatypesOperators() } void Smt2::addStringOperators() { - defineVar( - "re.all", - getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpAllchar())); + defineVar("re.all", getSolver()->mkRegexpAll()); addOperator(api::STRING_CONCAT, "str.++"); addOperator(api::STRING_LENGTH, "str.len"); addOperator(api::STRING_SUBSTR, "str.substr"); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 37aed63be..51a0f38b5 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -595,12 +595,11 @@ TEST_F(TestApiBlackSolver, mkReal) ASSERT_NO_THROW(d_solver.mkReal(val4, val4)); } -TEST_F(TestApiBlackSolver, mkRegexpNone) +TEST_F(TestApiBlackSolver, mkRegexpAll) { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); - ASSERT_NO_THROW( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); + ASSERT_NO_THROW(d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); } TEST_F(TestApiBlackSolver, mkRegexpAllchar) @@ -611,6 +610,14 @@ TEST_F(TestApiBlackSolver, mkRegexpAllchar) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); } +TEST_F(TestApiBlackSolver, mkRegexpNone) +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + ASSERT_NO_THROW( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); +} + TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } TEST_F(TestApiBlackSolver, mkSepNil) diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 161854421..6a08d79c6 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -639,6 +639,13 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); } + @Test void mkRegexpAll() + { + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); + } + @Test void mkRegexpAllchar() { Sort strSort = d_solver.getStringSort(); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 71ab17465..89e99bd9e 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -643,13 +643,19 @@ def test_mk_real(solver): solver.mkReal(val4, val4) -def test_mk_regexp_empty(solver): +def test_mk_regexp_none(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone()) -def test_mk_regexp_sigma(solver): +def test_mk_regexp_all(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAll()) + + +def test_mk_regexp_allchar(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar()) -- 2.30.2