diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-09 23:03:21 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-09 23:03:21 -0800 |
| commit | 3a9cacfdddd66fc122ffd4943452df4a8c70fd26 (patch) | |
| tree | 420b05552a5f05e5741d28bd69bc952426a0fac8 | |
| parent | 2b4e146c3a090e21b64d48ebb4308e5ec58a8c4b (diff) | |
regexp hack
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index b13b64f98..0716bae1a 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -194,6 +194,14 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) addedLemma = true; break; } + } else if (polarity) { + std::vector<Node> exp_n; + exp_n.push_back(assertion); + Node conc = tmp; + d_im.sendInference(nfexp, exp_n, conc, "REGEXP NF simp"); + addedLemma = true; + d_parent.getExtTheory()->markReduced(assertion); + continue; } } if (e == 1 && repUnfold.find(rep) != repUnfold.end()) |