From 1d145ff68ba6e4abaf77adfe97b072f63c4d7231 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 8 Nov 2021 18:51:58 -0800 Subject: [PATCH] regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609) This renames kinds REGEXP_EMPTY to REGEXP_NONE and REGEXP_SIGMA to REGEXP_ALLCHAR to match their SMT-LIB representation (re.none, re.allchar). It further renames api::Solver::mkRegexpEmpty() to mkRegexpNone and api::Solver::mkRegexpSigma to mkRegexpAllchar. --- src/api/cpp/cvc5.cpp | 24 ++++++------ src/api/cpp/cvc5.h | 8 ++-- src/api/cpp/cvc5_kind.h | 10 ++--- src/api/java/io/github/cvc5/api/Solver.java | 12 +++--- src/api/java/jni/solver.cpp | 12 +++--- src/api/python/cvc5.pxd | 4 +- src/api/python/cvc5.pxi | 8 ++-- src/expr/node_manager.h | 2 +- src/parser/smt2/smt2.cpp | 6 +-- src/printer/smt2/smt2_printer.cpp | 4 +- src/theory/strings/kinds | 10 ++--- src/theory/strings/regexp_elim.cpp | 10 ++--- src/theory/strings/regexp_entail.cpp | 11 +++--- src/theory/strings/regexp_operation.cpp | 35 ++++++++++------- src/theory/strings/regexp_solver.cpp | 6 +-- src/theory/strings/sequences_rewriter.cpp | 38 +++++++++---------- src/theory/strings/theory_strings_utils.cpp | 11 +++--- test/python/unit/api/test_solver.py | 8 ++-- test/unit/api/java/SolverTest.java | 12 +++--- test/unit/api/solver_black.cpp | 12 +++--- test/unit/theory/regexp_operation_black.cpp | 4 +- test/unit/theory/sequences_rewriter_white.cpp | 11 +++--- 22 files changed, 134 insertions(+), 124 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 9684c29c5..797d2e473 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -349,8 +349,8 @@ const static std::unordered_map s_kinds{ {REGEXP_RANGE, cvc5::Kind::REGEXP_RANGE}, {REGEXP_REPEAT, cvc5::Kind::REGEXP_REPEAT}, {REGEXP_LOOP, cvc5::Kind::REGEXP_LOOP}, - {REGEXP_EMPTY, cvc5::Kind::REGEXP_EMPTY}, - {REGEXP_SIGMA, cvc5::Kind::REGEXP_SIGMA}, + {REGEXP_NONE, cvc5::Kind::REGEXP_NONE}, + {REGEXP_ALLCHAR, cvc5::Kind::REGEXP_ALLCHAR}, {REGEXP_COMPLEMENT, cvc5::Kind::REGEXP_COMPLEMENT}, // maps to the same kind as the string versions {SEQ_CONCAT, cvc5::Kind::STRING_CONCAT}, @@ -661,8 +661,8 @@ const static std::unordered_map {cvc5::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT}, {cvc5::Kind::REGEXP_LOOP, REGEXP_LOOP}, {cvc5::Kind::REGEXP_LOOP_OP, REGEXP_LOOP}, - {cvc5::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, - {cvc5::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, + {cvc5::Kind::REGEXP_NONE, REGEXP_NONE}, + {cvc5::Kind::REGEXP_ALLCHAR, REGEXP_ALLCHAR}, {cvc5::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, {cvc5::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, {cvc5::Kind::SEQ_UNIT, SEQ_UNIT}, @@ -5103,14 +5103,14 @@ Sort Solver::mkTupleSortHelper(const std::vector& sorts) const Term Solver::mkTermFromKind(Kind kind) const { - CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY - || kind == REGEXP_SIGMA || kind == SEP_EMP, + CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_NONE + || kind == REGEXP_ALLCHAR || kind == SEP_EMP, kind) - << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP"; + << "PI, REGEXP_NONE, REGEXP_ALLCHAR or SEP_EMP"; //////// all checks before this line Node res; cvc5::Kind k = extToIntKind(kind); - if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) + if (kind == REGEXP_NONE || kind == REGEXP_ALLCHAR) { Assert(isDefinedIntKind(k)); res = d_nodeMgr->mkNode(k, std::vector()); @@ -5796,24 +5796,24 @@ Term Solver::mkReal(int64_t num, int64_t den) const CVC5_API_TRY_CATCH_END; } -Term Solver::mkRegexpEmpty() const +Term Solver::mkRegexpNone() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = - d_nodeMgr->mkNode(cvc5::kind::REGEXP_EMPTY, std::vector()); + d_nodeMgr->mkNode(cvc5::kind::REGEXP_NONE, std::vector()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// CVC5_API_TRY_CATCH_END; } -Term Solver::mkRegexpSigma() const +Term Solver::mkRegexpAllchar() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = - d_nodeMgr->mkNode(cvc5::kind::REGEXP_SIGMA, std::vector()); + d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALLCHAR, std::vector()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 1ecf8715b..5b0cc0b45 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3443,16 +3443,16 @@ class CVC5_EXPORT Solver Term mkReal(int64_t num, int64_t den) const; /** - * Create a regular expression empty term. + * Create a regular expression none (re.none) term. * @return the empty term */ - Term mkRegexpEmpty() const; + Term mkRegexpNone() const; /** - * Create a regular expression sigma term. + * Create a regular expression allchar (re.allchar) term. * @return the sigma term */ - Term mkRegexpSigma() const; + Term mkRegexpAllchar() const; /** * Create a constant representing an empty set of the given sort. diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 57941aa5f..162ec24e7 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -3016,25 +3016,25 @@ enum Kind : int32_t */ REGEXP_LOOP, /** - * Regexp empty. + * Regexp none. * * Parameters: none * * Create with: - * - `Solver::mkRegexpEmpty() const` + * - `Solver::mkRegexpNone() const` * - `Solver::mkTerm(Kind kind) const` */ - REGEXP_EMPTY, + REGEXP_NONE, /** * Regexp all characters. * * Parameters: none * * Create with: - * - `Solver::mkRegexpSigma() const` + * - `Solver::mkRegexpAllchar() const` * - `Solver::mkTerm(Kind kind) const` */ - REGEXP_SIGMA, + REGEXP_ALLCHAR, /** * Regexp complement. * diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 0479dce3d..09ad66f5b 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -854,25 +854,25 @@ public class Solver implements IPointer, AutoCloseable * Create a regular expression empty term. * @return the empty term */ - public Term mkRegexpEmpty() + public Term mkRegexpNone() { - long termPointer = mkRegexpEmpty(pointer); + long termPointer = mkRegexpNone(pointer); return new Term(this, termPointer); } - private native long mkRegexpEmpty(long pointer); + private native long mkRegexpNone(long pointer); /** * Create a regular expression sigma term. * @return the sigma term */ - public Term mkRegexpSigma() + public Term mkRegexpAllchar() { - long termPointer = mkRegexpSigma(pointer); + long termPointer = mkRegexpAllchar(pointer); return new Term(this, termPointer); } - private native long mkRegexpSigma(long pointer); + private native long mkRegexpAllchar(long pointer); /** * Create a constant representing an empty set of the given sort. diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index cb4d58591..a3ce49f4e 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -977,30 +977,30 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkReal__JJJ( /* * Class: io_github_cvc5_api_Solver - * Method: mkRegexpEmpty + * Method: mkRegexpNone * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpEmpty( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpNone( JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); - Term* retPointer = new Term(solver->mkRegexpEmpty()); + Term* retPointer = new Term(solver->mkRegexpNone()); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_api_Solver - * Method: mkRegexpSigma + * Method: mkRegexpAllchar * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpSigma( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRegexpAllchar( JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); - Term* retPointer = new Term(solver->mkRegexpSigma()); + Term* retPointer = new Term(solver->mkRegexpAllchar()); return reinterpret_cast(retPointer); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index a2c238985..baee5899e 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -215,8 +215,8 @@ 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 mkRegexpEmpty() except + - Term mkRegexpSigma() except + + Term mkRegexpNone() except + + Term mkRegexpAllchar() 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 05138e9bc..9e1aeaca1 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1130,22 +1130,22 @@ cdef class Solver: term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode()) return term - def mkRegexpEmpty(self): + def mkRegexpNone(self): """Create a regular expression empty term. :return: the empty term """ cdef Term term = Term(self) - term.cterm = self.csolver.mkRegexpEmpty() + term.cterm = self.csolver.mkRegexpNone() return term - def mkRegexpSigma(self): + def mkRegexpAllchar(self): """Create a regular expression sigma term. :return: the sigma term """ cdef Term term = Term(self) - term.cterm = self.csolver.mkRegexpSigma() + term.cterm = self.csolver.mkRegexpAllchar() return term def mkEmptySet(self, Sort s): diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d0c607a4b..1208a0e03 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -394,7 +394,7 @@ class NodeManager * - We can avoid creating a temporary vector in some cases, e.g., when we * want to create a node with a fixed, large number of children * - It makes sure that calls to `mkNode` that braced-init-lists work as - * expected, e.g., mkNode(REGEXP_EMPTY, {}) will call this overload instead + * expected, e.g., mkNode(REGEXP_NONE, {}) will call this overload instead * of creating a node with a null node as a child. */ Node mkNode(Kind kind, std::initializer_list children); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b86c564d0..7add605c5 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -147,7 +147,7 @@ void Smt2::addDatatypesOperators() void Smt2::addStringOperators() { defineVar( "re.all", - getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma())); + getSolver()->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpAllchar())); addOperator(api::STRING_CONCAT, "str.++"); addOperator(api::STRING_LENGTH, "str.len"); addOperator(api::STRING_SUBSTR, "str.substr"); @@ -636,8 +636,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) defineType("RegLan", d_solver->getRegExpSort(), true, true); defineType("Int", d_solver->getIntegerSort(), true, true); - defineVar("re.none", d_solver->mkRegexpEmpty()); - defineVar("re.allchar", d_solver->mkRegexpSigma()); + defineVar("re.none", d_solver->mkRegexpNone()); + defineVar("re.allchar", d_solver->mkRegexpAllchar()); // Boolean is a placeholder defineVar("seq.empty", diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 231390504..5d4387658 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1178,8 +1178,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::STRING_STOI: return "str.to_int"; case kind::STRING_IN_REGEXP: return "str.in_re"; case kind::STRING_TO_REGEXP: return "str.to_re"; - case kind::REGEXP_EMPTY: return "re.none"; - case kind::REGEXP_SIGMA: return "re.allchar"; + case kind::REGEXP_NONE: return "re.none"; + case kind::REGEXP_ALLCHAR: return "re.allchar"; case kind::REGEXP_CONCAT: return "re.++"; case kind::REGEXP_UNION: return "re.union"; case kind::REGEXP_INTER: return "re.inter"; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 9faa935e1..d23e44cee 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -48,7 +48,7 @@ sort STRING_TYPE \ sort REGEXP_TYPE \ Cardinality::INTEGERS \ well-founded \ - "NodeManager::currentNM()->mkNode(REGEXP_EMPTY)" \ + "NodeManager::currentNM()->mkNode(REGEXP_NONE)" \ "util/string.h" \ "RegExp type" @@ -103,8 +103,8 @@ operator REGEXP_OPT 1 "regexp ?" operator REGEXP_RANGE 2 "regexp range" operator REGEXP_COMPLEMENT 1 "regexp complement" -operator REGEXP_EMPTY 0 "regexp empty" -operator REGEXP_SIGMA 0 "regexp all characters" +operator REGEXP_NONE 0 "regexp empty" +operator REGEXP_ALLCHAR 0 "regexp all characters" constant REGEXP_REPEAT_OP \ struct \ @@ -143,8 +143,8 @@ typerule REGEXP_LOOP "SimpleTypeRule" typerule REGEXP_COMPLEMENT "SimpleTypeRule" typerule STRING_TO_REGEXP "SimpleTypeRule" typerule STRING_IN_REGEXP "SimpleTypeRule" -typerule REGEXP_EMPTY "SimpleTypeRule" -typerule REGEXP_SIGMA "SimpleTypeRule" +typerule REGEXP_NONE "SimpleTypeRule" +typerule REGEXP_ALLCHAR "SimpleTypeRule" ### operators that apply to both strings and sequences diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index b3dc309d5..d5b7606f2 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -121,7 +121,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) if (fl.isNull()) { if (!hasPivotIndex && c.getKind() == REGEXP_STAR - && c[0].getKind() == REGEXP_SIGMA) + && c[0].getKind() == REGEXP_ALLCHAR) { hasPivotIndex = true; pivotIndex = i; @@ -167,7 +167,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // We do not need to include memberships of the form // (str.substr x n 1) in re.allchar // since we know that by construction, n < len( x ). - if (re[i].getKind() != REGEXP_SIGMA) + if (re[i].getKind() != REGEXP_ALLCHAR) { Node currMem = nm->mkNode(STRING_IN_REGEXP, curr, re[i]); conc.push_back(currMem); @@ -212,13 +212,13 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) gap_minsize.push_back(0); gap_exact.push_back(true); } - else if (c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_SIGMA) + else if (c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_ALLCHAR) { // found a gap of any size onlySigmasAndConsts = true; gap_exact[gap_exact.size() - 1] = false; } - else if (c.getKind() == REGEXP_SIGMA) + else if (c.getKind() == REGEXP_ALLCHAR) { // add one to the minimum size of the gap onlySigmasAndConsts = true; @@ -565,7 +565,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) for (const Node& r : disj) { Assert(r.getKind() != REGEXP_UNION); - Assert(r.getKind() != REGEXP_SIGMA); + Assert(r.getKind() != REGEXP_ALLCHAR); lenOnePeriod = false; // lenOnePeriod is true if this regular expression is a single character // regular expression diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index be1646403..530f34455 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -116,7 +116,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector& mchildren, mchildren.pop_back(); do_next = true; } - else if (rc.getKind() == REGEXP_RANGE || rc.getKind() == REGEXP_SIGMA) + else if (rc.getKind() == REGEXP_RANGE + || rc.getKind() == REGEXP_ALLCHAR) { if (!isConstRegExp(rc)) { @@ -513,11 +514,11 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s, return true; } } - case REGEXP_EMPTY: + case REGEXP_NONE: { return false; } - case REGEXP_SIGMA: + case REGEXP_ALLCHAR: { if (s.size() == index_start + 1) { @@ -654,7 +655,7 @@ Node RegExpEntail::getFixedLengthForRegexp(Node n) return ret; } } - else if (n.getKind() == REGEXP_SIGMA || n.getKind() == REGEXP_RANGE) + else if (n.getKind() == REGEXP_ALLCHAR || n.getKind() == REGEXP_RANGE) { return nm->mkConst(Rational(1)); } @@ -710,7 +711,7 @@ bool RegExpEntail::regExpIncludes(Node r1, Node r2) return false; } NodeManager* nm = NodeManager::currentNM(); - Node sigma = nm->mkNode(REGEXP_SIGMA, std::vector{}); + Node sigma = nm->mkNode(REGEXP_ALLCHAR, std::vector{}); Node sigmaStar = nm->mkNode(REGEXP_STAR, sigma); std::vector v1, v2; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 81ac75c84..fff512f98 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -35,11 +35,11 @@ RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc) : EnvObj(env), d_true(NodeManager::currentNM()->mkConst(true)), d_false(NodeManager::currentNM()->mkConst(false)), - d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY, + d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_NONE, std::vector{})), d_zero(NodeManager::currentNM()->mkConst(::cvc5::Rational(0))), d_one(NodeManager::currentNM()->mkConst(::cvc5::Rational(1))), - d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, + d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_ALLCHAR, std::vector{})), d_sigma_star( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)), @@ -84,7 +84,7 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r) d_constCache[cur] = tmp.isConst() ? RE_C_CONRETE_CONSTANT : RE_C_VARIABLE; } - else if (ck == REGEXP_SIGMA || ck == REGEXP_RANGE) + else if (ck == REGEXP_ALLCHAR || ck == REGEXP_RANGE) { d_constCache[cur] = RE_C_CONSTANT; } @@ -136,8 +136,8 @@ int RegExpOpr::delta( Node r, Node &exp ) { Kind k = r.getKind(); switch (k) { - case REGEXP_EMPTY: - case REGEXP_SIGMA: + case REGEXP_NONE: + case REGEXP_ALLCHAR: case REGEXP_RANGE: { // does not contain empty string @@ -295,11 +295,13 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode) d_deriv_cache[dv] = p; } else { switch( r.getKind() ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { ret = 2; break; } - case kind::REGEXP_SIGMA: { + case kind::REGEXP_ALLCHAR: + { retNode = d_emptySingleton; break; } @@ -550,11 +552,13 @@ Node RegExpOpr::derivativeSingle(Node r, cvc5::String c) } else { Kind k = r.getKind(); switch( k ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { retNode = d_emptyRegexp; break; } - case kind::REGEXP_SIGMA: { + case kind::REGEXP_ALLCHAR: + { retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); break; } @@ -719,7 +723,8 @@ void RegExpOpr::firstChars(Node r, std::set &pcset, SetNodes &pvset) SetNodes vset; Kind k = r.getKind(); switch( k ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { break; } case kind::REGEXP_RANGE: { @@ -792,7 +797,7 @@ void RegExpOpr::firstChars(Node r, std::set &pcset, SetNodes &pvset) firstChars(r[0], cset, vset); break; } - case kind::REGEXP_SIGMA: + case kind::REGEXP_ALLCHAR: case kind::REGEXP_COMPLEMENT: default: { // we do not expect to call this function on regular expressions that @@ -1198,7 +1203,7 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) { r1 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr1); r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vr2); } - else if (nk == STRING_TO_REGEXP || nk == REGEXP_SIGMA || nk == REGEXP_RANGE + else if (nk == STRING_TO_REGEXP || nk == REGEXP_ALLCHAR || nk == REGEXP_RANGE || nk == REGEXP_COMPLEMENT || nk == REGEXP_LOOP) { // this leaves n unchanged @@ -1466,11 +1471,13 @@ std::string RegExpOpr::mkString( Node r ) { } else { int k = r.getKind(); switch( k ) { - case kind::REGEXP_EMPTY: { + case kind::REGEXP_NONE: + { retStr += "\\E"; break; } - case kind::REGEXP_SIGMA: { + case kind::REGEXP_ALLCHAR: + { retStr += "."; break; } diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 050ec594a..04de0ea44 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -52,7 +52,7 @@ RegExpSolver::RegExpSolver(Env& env, d_regexp_opr(env, tr.getSkolemCache()) { d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String("")); - d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY); + d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_NONE); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } @@ -656,8 +656,8 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector& nf_exp) Node ret = r; switch (r.getKind()) { - case REGEXP_EMPTY: - case REGEXP_SIGMA: + case REGEXP_NONE: + case REGEXP_ALLCHAR: case REGEXP_RANGE: break; case STRING_TO_REGEXP: { diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 783e258fa..babf260fc 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -789,10 +789,10 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node) changed = true; emptyRe = c; } - else if (c.getKind() == REGEXP_EMPTY) + else if (c.getKind() == REGEXP_NONE) { // re.++( ..., empty, ... ) ---> empty - Node ret = nm->mkNode(REGEXP_EMPTY); + Node ret = nm->mkNode(REGEXP_NONE); return returnRewrite(node, ret, Rewrite::RE_CONCAT_EMPTY); } else @@ -868,7 +868,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node) { curr = Node::null(); } - else if (curr[0].getKind() == REGEXP_SIGMA) + else if (curr[0].getKind() == REGEXP_ALLCHAR) { Assert(!lastAllStar); lastAllStar = true; @@ -932,7 +932,7 @@ Node SequencesRewriter::rewriteStarRegExp(TNode node) // ("")* ---> "" return returnRewrite(node, node[0], Rewrite::RE_STAR_EMPTY_STRING); } - else if (node[0].getKind() == REGEXP_EMPTY) + else if (node[0].getKind() == REGEXP_NONE) { // (empty)* ---> "" retNode = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))); @@ -992,7 +992,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) } } } - else if (ni.getKind() == REGEXP_EMPTY) + else if (ni.getKind() == REGEXP_NONE) { if (nk == REGEXP_INTER) { @@ -1000,7 +1000,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) } // otherwise, can ignore } - else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_SIGMA) + else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_ALLCHAR) { if (nk == REGEXP_UNION) { @@ -1032,11 +1032,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) Node retNode; if (nk == REGEXP_INTER) { - retNode = nm->mkNode(kind::REGEXP_EMPTY); + retNode = nm->mkNode(kind::REGEXP_NONE); } else { - retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA)); + retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR)); } return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT); } @@ -1047,11 +1047,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) { if (nk == REGEXP_INTER) { - retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA)); + retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR)); } else { - retNode = nm->mkNode(kind::REGEXP_EMPTY); + retNode = nm->mkNode(kind::REGEXP_NONE); } } else @@ -1091,7 +1091,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node) if (u < l) { std::vector nvec; - retNode = nm->mkNode(REGEXP_EMPTY, nvec); + retNode = nm->mkNode(REGEXP_NONE, nvec); } else if (u == l) { @@ -1184,7 +1184,7 @@ Node SequencesRewriter::rewriteRangeRegExp(TNode node) if (ch[0] > ch[1]) { // re.range( "B", "A" ) ---> re.none - Node retNode = nm->mkNode(REGEXP_EMPTY); + Node retNode = nm->mkNode(REGEXP_NONE); return returnRewrite(node, retNode, Rewrite::RE_RANGE_EMPTY); } return node; @@ -1199,7 +1199,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) TypeNode stype = x.getType(); TypeNode rtype = r.getType(); - if(r.getKind() == kind::REGEXP_EMPTY) + if (r.getKind() == kind::REGEXP_NONE) { Node retNode = NodeManager::currentNM()->mkConst(false); return returnRewrite(node, retNode, Rewrite::RE_IN_EMPTY); @@ -1212,7 +1212,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) Node retNode = NodeManager::currentNM()->mkConst(test); return returnRewrite(node, retNode, Rewrite::RE_IN_EVAL); } - else if (r.getKind() == kind::REGEXP_SIGMA) + else if (r.getKind() == kind::REGEXP_ALLCHAR) { Node one = nm->mkConst(Rational(1)); Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x)); @@ -1260,7 +1260,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) } } } - if (r[0].getKind() == kind::REGEXP_SIGMA) + if (r[0].getKind() == kind::REGEXP_ALLCHAR) { Node retNode = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR); @@ -1277,12 +1277,12 @@ Node SequencesRewriter::rewriteMembership(TNode node) for (size_t i = 0; i < nchildren; i++) { Node rc = r[i]; - Assert(rc.getKind() != kind::REGEXP_EMPTY); - if (rc.getKind() == kind::REGEXP_SIGMA) + Assert(rc.getKind() != kind::REGEXP_NONE); + if (rc.getKind() == kind::REGEXP_ALLCHAR) { allSigmaMinSize++; } - else if (rc.getKind() == REGEXP_STAR && rc[0].getKind() == REGEXP_SIGMA) + else if (rc.getKind() == REGEXP_STAR && rc[0].getKind() == REGEXP_ALLCHAR) { allSigmaStrict = false; } @@ -3245,7 +3245,7 @@ std::pair SequencesRewriter::firstMatch(Node n, Node r) Assert(r.getType().isRegExp()); NodeManager* nm = NodeManager::currentNM(); - Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA)); + Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR)); Node re = nm->mkNode(REGEXP_CONCAT, r, sigmaStar); String s = n.getConst(); diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 9ab65f6ec..59bb0755c 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -285,7 +285,7 @@ bool isConstantLike(Node n) { return n.isConst() || n.getKind() == SEQ_UNIT; } bool isUnboundedWildcard(const std::vector& rs, size_t start) { size_t i = start; - while (i < rs.size() && rs[i].getKind() == REGEXP_SIGMA) + while (i < rs.size() && rs[i].getKind() == REGEXP_ALLCHAR) { i++; } @@ -295,7 +295,7 @@ bool isUnboundedWildcard(const std::vector& rs, size_t start) return false; } - return rs[i].getKind() == REGEXP_STAR && rs[i][0].getKind() == REGEXP_SIGMA; + return rs[i].getKind() == REGEXP_STAR && rs[i][0].getKind() == REGEXP_ALLCHAR; } bool isSimpleRegExp(Node r) @@ -313,8 +313,9 @@ bool isSimpleRegExp(Node r) return false; } } - else if (n.getKind() != REGEXP_SIGMA - && (n.getKind() != REGEXP_STAR || n[0].getKind() != REGEXP_SIGMA)) + else if (n.getKind() != REGEXP_ALLCHAR + && (n.getKind() != REGEXP_STAR + || n[0].getKind() != REGEXP_ALLCHAR)) { return false; } @@ -376,7 +377,7 @@ bool isStringKind(Kind k) bool isRegExpKind(Kind k) { - return k == REGEXP_EMPTY || k == REGEXP_SIGMA || k == STRING_TO_REGEXP + return k == REGEXP_NONE || k == REGEXP_ALLCHAR || k == STRING_TO_REGEXP || k == REGEXP_CONCAT || k == REGEXP_UNION || k == REGEXP_INTER || k == REGEXP_STAR || k == REGEXP_PLUS || k == REGEXP_OPT || k == REGEXP_RANGE || k == REGEXP_LOOP || k == REGEXP_RV diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index c7398aa3b..71ab17465 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -646,13 +646,13 @@ def test_mk_real(solver): def test_mk_regexp_empty(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpEmpty()) + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone()) def test_mk_regexp_sigma(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma()) + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar()) def test_mk_sep_emp(solver): @@ -690,8 +690,8 @@ def test_mk_term(solver): # mkTerm(Kind kind) const solver.mkPi() - solver.mkTerm(kinds.RegexpEmpty) - solver.mkTerm(kinds.RegexpSigma) + solver.mkTerm(kinds.RegexpNone) + solver.mkTerm(kinds.RegexpAllchar) with pytest.raises(RuntimeError): solver.mkTerm(kinds.ConstBV) diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 2f134b6bf..161854421 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -632,18 +632,18 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkReal(val4, val4)); } - @Test void mkRegexpEmpty() + @Test void mkRegexpNone() { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); - assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty())); + assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); } - @Test void mkRegexpSigma() + @Test void mkRegexpAllchar() { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); - assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); + assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); } @Test void mkSepEmp() @@ -683,8 +683,8 @@ class SolverTest // mkTerm(Kind kind) const assertDoesNotThrow(() -> d_solver.mkTerm(PI)); - assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_EMPTY)); - assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_SIGMA)); + assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_NONE)); + assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_ALLCHAR)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(CONST_BITVECTOR)); // mkTerm(Kind kind, Term child) const diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index ab47ae90b..79a4aa63e 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -592,20 +592,20 @@ TEST_F(TestApiBlackSolver, mkReal) ASSERT_NO_THROW(d_solver.mkReal(val4, val4)); } -TEST_F(TestApiBlackSolver, mkRegexpEmpty) +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.mkRegexpEmpty())); + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); } -TEST_F(TestApiBlackSolver, mkRegexpSigma) +TEST_F(TestApiBlackSolver, mkRegexpAllchar) { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); ASSERT_NO_THROW( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); } TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } @@ -643,8 +643,8 @@ TEST_F(TestApiBlackSolver, mkTerm) // mkTerm(Kind kind) const ASSERT_NO_THROW(d_solver.mkTerm(PI)); - ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_EMPTY)); - ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_SIGMA)); + ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE)); + ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR)); ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC5ApiException); // mkTerm(Kind kind, Term child) const diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index c6b921542..8d3a672f7 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -61,7 +61,7 @@ class TestTheoryBlackRegexpOperation : public TestSmt TEST_F(TestTheoryBlackRegexpOperation, basic) { - Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA); + Node sigma = d_nodeManager->mkNode(REGEXP_ALLCHAR); Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma); Node a = d_nodeManager->mkNode(STRING_TO_REGEXP, d_nodeManager->mkConst(String("a"))); @@ -88,7 +88,7 @@ TEST_F(TestTheoryBlackRegexpOperation, basic) TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) { - Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA); + Node sigma = d_nodeManager->mkNode(REGEXP_ALLCHAR); Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma); Node a = d_nodeManager->mkNode(STRING_TO_REGEXP, d_nodeManager->mkConst(String("a"))); diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index bcac315a7..165479b78 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -713,7 +713,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) std::vector emptyVec; Node sigStar = d_nodeManager->mkNode( - kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec)); + kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, emptyVec)); Node foo = d_nodeManager->mkConst(String("FOO")); Node a = d_nodeManager->mkConst(String("A")); Node b = d_nodeManager->mkConst(String("B")); @@ -833,7 +833,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) std::vector emptyVec; Node sigStar = d_nodeManager->mkNode( - kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyVec)); + kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, emptyVec)); Node foo = d_nodeManager->mkConst(String("FOO")); Node a = d_nodeManager->mkConst(String("A")); Node b = d_nodeManager->mkConst(String("B")); @@ -1796,7 +1796,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership) // (str.contains x "ABC") Node sig_star = d_nodeManager->mkNode( kind::REGEXP_STAR, - d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty)); + d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, vec_empty)); Node lhs = d_nodeManager->mkNode( kind::STRING_IN_REGEXP, x, @@ -1814,7 +1814,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership) // (str.contains x "ABC") Node sig_star = d_nodeManager->mkNode( kind::REGEXP_STAR, - d_nodeManager->mkNode(kind::REGEXP_SIGMA, vec_empty)); + d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, vec_empty)); Node lhs = d_nodeManager->mkNode( kind::STRING_IN_REGEXP, x, @@ -1832,7 +1832,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_regexp_concat) Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node allStar = d_nodeManager->mkNode( - kind::REGEXP_STAR, d_nodeManager->mkNode(kind::REGEXP_SIGMA, emptyArgs)); + kind::REGEXP_STAR, + d_nodeManager->mkNode(kind::REGEXP_ALLCHAR, emptyArgs)); Node xReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, x); Node yReg = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, y); -- 2.30.2