From 4877909b806329e5e0e14dcfc3c404b8e4f6c0af Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 10 Nov 2021 13:10:16 -0800 Subject: 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 +--- 7 files changed, 72 insertions(+), 18 deletions(-) (limited to 'src') 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"); -- cgit v1.2.3