diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 18:09:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-20 18:09:27 -0500 |
| commit | 0e62e42f739e467f61f5c3d10e7b1c7356db6406 (patch) | |
| tree | a4281c5b2c0881c2d622da68322e213f7168801b /src/theory/quantifiers | |
| parent | 0a0cee14c38cac0f87772c192ef387dcd36b6977 (diff) | |
Generalize mkConcat for types (#4123)
Towards theory of sequences.
The utility function mkConcat needs a type to know what to construct in the empty string case.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 187c765d1..231c81bbf 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -818,6 +818,7 @@ Node QuantifiersRewriter::getVarElimLitString(Node lit, { if (lit[i].getKind() == STRING_CONCAT) { + TypeNode stype = lit[i].getType(); for (unsigned j = 0, nchildren = lit[i].getNumChildren(); j < nchildren; j++) { @@ -827,8 +828,8 @@ Node QuantifiersRewriter::getVarElimLitString(Node lit, Node slv = lit[1 - i]; std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j); std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end()); - Node tpre = strings::utils::mkConcat(STRING_CONCAT, preL); - Node tpost = strings::utils::mkConcat(STRING_CONCAT, postL); + Node tpre = strings::utils::mkConcat(preL, stype); + Node tpost = strings::utils::mkConcat(postL, stype); Node slvL = nm->mkNode(STRING_LENGTH, slv); Node tpreL = nm->mkNode(STRING_LENGTH, tpre); Node tpostL = nm->mkNode(STRING_LENGTH, tpost); |