diff options
Diffstat (limited to 'src/theory/strings/extf_solver.cpp')
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 961d976cf..4ee2f4919 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -65,6 +65,7 @@ ExtfSolver::ExtfSolver(context::Context* c, d_extt.addFunctionKind(kind::STRING_TOLOWER); d_extt.addFunctionKind(kind::STRING_TOUPPER); d_extt.addFunctionKind(kind::STRING_REV); + d_extt.addFunctionKind(kind::SEQ_UNIT); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -138,16 +139,18 @@ bool ExtfSolver::doReduction(int effort, Node n) } } } - else + else if (k == STRING_SUBSTR) { - if (k == STRING_SUBSTR) - { - r_effort = 1; - } - else if (k != STRING_IN_REGEXP) - { - r_effort = 2; - } + r_effort = 1; + } + else if (k == SEQ_UNIT) + { + // never necessary to reduce seq.unit + return false; + } + else if (k != STRING_IN_REGEXP) + { + r_effort = 2; } if (effort != r_effort) { |