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/sequences_rewriter.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/sequences_rewriter.cpp')
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 20b892d0f..bb0fa1d97 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -576,6 +576,11 @@ Node SequencesRewriter::rewriteLength(Node node) Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]); return returnRewrite(node, retNode, Rewrite::LEN_CONV_INV); } + else if (nk0 == SEQ_UNIT) + { + Node retNode = nm->mkConst(Rational(1)); + return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT); + } return node; } @@ -1836,6 +1841,7 @@ Node SequencesRewriter::rewriteContains(Node node) nb << emp.eqNode(t); for (const Node& c : vec) { + Assert(c.getType() == t.getType()); nb << c.eqNode(t); } @@ -3171,7 +3177,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) Assert(ratLen.getDenominator() == 1); Integer intLen = ratLen.getNumerator(); uint32_t u = intLen.getUnsignedInt(); - if (stype.isString()) + if (stype.isString()) // string-only { res = nm->mkConst(String(std::string(u, 'A'))); } @@ -3233,7 +3239,7 @@ Node SequencesRewriter::rewriteSeqUnit(Node node) { std::vector<Expr> seq; seq.push_back(node[0].toExpr()); - TypeNode stype = nm->mkSequenceType(node[0].getType()); + TypeNode stype = node[0].getType(); Node ret = nm->mkConst(ExprSequence(stype.toType(), seq)); return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL); } |