diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-01 08:46:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-01 08:46:07 -0500 |
| commit | 04154c08c1af81bb751376ae9379c071a95c5a3f (patch) | |
| tree | 7a89b64878297c2a5009271ceb58023b4e76c8b1 /src/theory/strings/extf_solver.cpp | |
| parent | 4e1c078cfc49030b7e96485d777509ce4bc57a5a (diff) | |
Inferences and model construction taking into account seq.unit (#4607)
Towards theory of sequences.
This makes the strings solver handle seq.unit, which requires two new inferences and updates to its model construction.
It also fixes a bug in the best content heuristic, which previously failed to update the best score.
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) { |