diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-01 09:08:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-01 09:08:46 -0500 |
commit | 79881c196e29ef341166e7a31c1183e8b537d069 (patch) | |
tree | 25466cceb67c54895bf012fd745dd864d356b153 /src/theory/strings/regexp_solver.cpp | |
parent | 7537ff075dbb2d814d722d2d72586ce78235467c (diff) |
Regular expression intersection modes (#3134)
Diffstat (limited to 'src/theory/strings/regexp_solver.cpp')
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 26 |
1 files changed, 23 insertions, 3 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index c50889e78..463891839 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -248,13 +248,19 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) { + // do not compute intersections if the re intersection mode is none + if (options::stringRegExpInterMode() == RE_INTER_NONE) + { + return true; + } if (mems.empty()) { // nothing to do return true; } - // the initial regular expression membership + // the initial regular expression membership and its constant type Node mi; + RegExpConstType rcti = RE_C_UNKNOWN; NodeManager* nm = NodeManager::currentNM(); for (const Node& m : mems) { @@ -264,15 +270,29 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) Assert(m.getKind() == NOT && m[0].getKind() == STRING_IN_REGEXP); continue; } - if (!d_regexp_opr.checkConstRegExp(m)) + RegExpConstType rct = d_regexp_opr.getRegExpConstType(m); + if (rct == RE_C_VARIABLE + || (options::stringRegExpInterMode() == RE_INTER_CONSTANT + && rct != RE_C_CONRETE_CONSTANT)) { - // cannot do intersection on RE with variables + // cannot do intersection on RE with variables, or with re.allchar based + // on option. continue; } + if (options::stringRegExpInterMode() == RE_INTER_ONE_CONSTANT) + { + if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT) + { + // if both have re.allchar, do not do intersection if the + // RE_INTER_ONE_CONSTANT option is set. + continue; + } + } if (mi.isNull()) { // first regular expression seen mi = m; + rcti = rct; continue; } bool spflag = false; |