From 96c6ec71ccdde72c6cbc850df94c8965cda8d7db Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 19 Oct 2020 17:44:12 -0700 Subject: [PATCH] Expand `seq.nth` lazily (#5287) Our first support for seq.nth eliminated it eagerly during expandDefinitions. This PR changes that, by eliminating it lazily, as done with other extended string operators. --- src/theory/strings/extf_solver.cpp | 3 +- src/theory/strings/sequences_rewriter.cpp | 3 +- src/theory/strings/term_registry.cpp | 2 +- src/theory/strings/theory_strings.cpp | 37 +------------- .../strings/theory_strings_preprocess.cpp | 49 +++++++++++++++++++ src/theory/strings/theory_strings_utils.cpp | 2 +- test/regress/CMakeLists.txt | 3 +- .../regress0/seq/seq-nth-undef-unsat.smt2 | 17 +++++++ test/regress/regress0/seq/seq-nth-undef.smt2 | 7 --- test/regress/regress0/seq/seq-nth.smt2 | 2 +- test/regress/regress0/seq/seq-types.smt2 | 11 +++++ 11 files changed, 88 insertions(+), 48 deletions(-) create mode 100644 test/regress/regress0/seq/seq-nth-undef-unsat.smt2 delete mode 100644 test/regress/regress0/seq/seq-nth-undef.smt2 create mode 100644 test/regress/regress0/seq/seq-types.smt2 diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 88edaeff7..53cd92ac2 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -65,6 +65,7 @@ ExtfSolver::ExtfSolver(SolverState& s, d_extt.addFunctionKind(kind::STRING_TOUPPER); d_extt.addFunctionKind(kind::STRING_REV); d_extt.addFunctionKind(kind::SEQ_UNIT); + d_extt.addFunctionKind(kind::SEQ_NTH); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -188,7 +189,7 @@ bool ExtfSolver::doReduction(int effort, Node n) NodeManager* nm = NodeManager::currentNM(); Assert(k == STRING_SUBSTR || k == STRING_UPDATE || k == STRING_STRCTN || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI - || k == STRING_STRREPL || k == STRING_STRREPLALL + || k == STRING_STRREPL || k == STRING_STRREPLALL || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV); diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 43918d6b1..2cefe6b09 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -18,6 +18,7 @@ #include "expr/attribute.h" #include "expr/node_builder.h" +#include "expr/sequence.h" #include "theory/rewriter.h" #include "theory/strings/arith_entail.h" #include "theory/strings/regexp_entail.h" @@ -1525,7 +1526,7 @@ Node SequencesRewriter::rewriteSeqNth(Node node) size_t pos = i.getConst().getNumerator().toUnsignedInt(); if (pos < len) { - std::vector elements = Word::getChars(s); + std::vector elements = s.getConst().getVec(); ret = elements[pos]; return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL); } diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 71671d8f1..b5b2a5a13 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -141,7 +141,7 @@ void TermRegistry::preRegisterTerm(TNode n) { if (k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL || k == STRING_SUBSTR || k == STRING_STRREPLALL - || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL + || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL || k == STRING_STRCTN || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV || k == STRING_UPDATE) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0375fd311..2b2c25333 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -118,6 +118,8 @@ void TheoryStrings::finishInit() d_equalityEngine->addFunctionKind(kind::STRING_IN_REGEXP, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_TO_CODE, eagerEval); d_equalityEngine->addFunctionKind(kind::SEQ_UNIT, eagerEval); + // `seq.nth` is not always defined, and so we do not evaluate it eagerly. + d_equalityEngine->addFunctionKind(kind::SEQ_NTH, false); // extended functions d_equalityEngine->addFunctionKind(kind::STRING_STRCTN, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_LEQ, eagerEval); @@ -578,41 +580,6 @@ TrustNode TheoryStrings::expandDefinition(Node node) ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); return TrustNode::mkTrustRewrite(node, ret, nullptr); } - - if (node.getKind() == SEQ_NTH) - { - // str.nth(s,i) ---> - // ite(0<=i<=len(s), witness k. 0<=i<=len(s)->unit(k) = seq.at(s,i), - // uf(s,i)) - NodeManager* nm = NodeManager::currentNM(); - Node s = node[0]; - Node i = node[1]; - Node len = nm->mkNode(STRING_LENGTH, s); - Node cond = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, len)); - TypeNode elemType = s.getType().getSequenceElementType(); - Node k = nm->mkBoundVar(elemType); - Node bvl = nm->mkNode(BOUND_VAR_LIST, k); - std::vector argTypes; - argTypes.push_back(s.getType()); - argTypes.push_back(nm->integerType()); - TypeNode ufType = nm->mkFunctionType(argTypes, elemType); - SkolemCache* sc = d_termReg.getSkolemCache(); - Node uf = sc->mkTypedSkolemCached( - ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, "Uf"); - Node ret = nm->mkNode( - ITE, - cond, - nm->mkNode(WITNESS, - bvl, - nm->mkNode(IMPLIES, - cond, - nm->mkNode(SEQ_UNIT, k) - .eqNode(nm->mkNode(STRING_CHARAT, s, i)))), - nm->mkNode(APPLY_UF, uf, s, i)); - return TrustNode::mkTrustRewrite(node, ret, nullptr); - } - return TrustNode::null(); } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 966964bc8..a8c1a6573 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -418,6 +418,55 @@ Node StringsPreprocess::reduce(Node t, retNode = stoit; } + else if (t.getKind() == kind::SEQ_NTH) + { + // processing term: str.nth( s, n) + // similar to substr. + Node s = t[0]; + Node n = t[1]; + Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); + Node t12 = nm->mkNode(PLUS, n, one); + Node lt0 = nm->mkNode(STRING_LENGTH, s); + // start point is greater than or equal zero + Node c1 = nm->mkNode(GEQ, n, zero); + // start point is less than end of string + Node c2 = nm->mkNode(GT, lt0, n); + // check whether this application of seq.nth is defined. + Node cond = nm->mkNode(AND, c1, c2); + + // nodes for the case where `seq.nth` is defined. + Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); + Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); + Node unit = nm->mkNode(SEQ_UNIT, skt); + Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, unit, sk2)); + // length of first skolem is second argument + Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); + Node lsk2 = nm->mkNode(STRING_LENGTH, sk2); + Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, t12)); + Node b1 = nm->mkNode(AND, b11, b12, b13); + + // nodes for the case where `seq.nth` is undefined. + std::vector argTypes; + argTypes.push_back(s.getType()); + argTypes.push_back(nm->integerType()); + TypeNode elemType = s.getType().getSequenceElementType(); + TypeNode ufType = nm->mkFunctionType(argTypes, elemType); + Node uf = sc->mkTypedSkolemCached( + ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, "Uf"); + Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n)); + + // the full ite, split on definedness of `seq.nth` + Node lemma = nm->mkNode(ITE, cond, b1, b2); + + // assert: + // IF n >=0 AND n < len( s ) + // THEN: s = sk1 ++ unit(skt) ++ sk2 AND + // len( sk1 ) = n AND + // ( len( sk2 ) = len( s )- (n+1) + // ELSE: skt = Uf(s, n), where Uf is a cached skolem function. + asserts.push_back(lemma); + retNode = skt; + } else if (t.getKind() == kind::STRING_STRREPL) { // processing term: replace( x, y, z ) diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index d48f081e1..286c0dc04 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -382,7 +382,7 @@ TypeNode getOwnerStringType(Node n) TypeNode tn; Kind k = n.getKind(); if (k == STRING_STRIDOF || k == STRING_LENGTH || k == STRING_STRCTN - || k == STRING_PREFIX || k == STRING_SUFFIX) + || k == SEQ_NTH || k == STRING_PREFIX || k == STRING_SUFFIX) { // owning string type is the type of first argument tn = n[0].getType(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cb3c9d9f8..583b129c7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -894,8 +894,9 @@ set(regress_0_tests regress0/seq/seq-nth.smt2 regress0/seq/seq-nth-uf.smt2 regress0/seq/seq-nth-uf-z.smt2 - regress0/seq/seq-nth-undef.smt2 + regress0/seq/seq-nth-undef-unsat.smt2 regress0/seq/seq-rewrites.smt2 + regress0/seq/seq-types.smt2 regress0/sets/abt-min.smt2 regress0/sets/abt-te-exh.smt2 regress0/sets/abt-te-exh2.smt2 diff --git a/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 b/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 new file mode 100644 index 000000000..4fe2a85a9 --- /dev/null +++ b/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --strings-exp -q +;EXPECT: unsat +(set-logic ALL) +(declare-fun s () (Seq Int)) +(declare-fun n () Int) + +(assert (=> (and (<= 0 n ) (< n (seq.len s))) (= (seq.nth s n) 6))) +(assert (=> (>= 0 n) (= (seq.nth s n) 7))) +(assert (=> (>= n (seq.len s)) (= (seq.nth s n) 8))) +(assert (distinct (seq.unit 6) (seq.extract s n 1))) +(assert (distinct (seq.unit 7) (seq.extract s n 1))) +(assert (distinct (seq.unit 8) (seq.extract s n 1))) +(assert (> n 0)) +(assert (< n (seq.len s))) +(assert (> (seq.len s) 0)) +(check-sat) + diff --git a/test/regress/regress0/seq/seq-nth-undef.smt2 b/test/regress/regress0/seq/seq-nth-undef.smt2 deleted file mode 100644 index 3ff2ab096..000000000 --- a/test/regress/regress0/seq/seq-nth-undef.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -; COMMAND-LINE: --strings-exp -;EXPECT: sat -(set-logic ALL) -(declare-fun s () (Seq Int)) -(assert (= 5 (seq.nth s 5))) -(assert (= 2 (seq.len s))) -(check-sat) diff --git a/test/regress/regress0/seq/seq-nth.smt2 b/test/regress/regress0/seq/seq-nth.smt2 index 3ff2ab096..ff22a3288 100644 --- a/test/regress/regress0/seq/seq-nth.smt2 +++ b/test/regress/regress0/seq/seq-nth.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp +; COMMAND-LINE: --strings-exp --no-check-models ;EXPECT: sat (set-logic ALL) (declare-fun s () (Seq Int)) diff --git a/test/regress/regress0/seq/seq-types.smt2 b/test/regress/regress0/seq/seq-types.smt2 new file mode 100644 index 000000000..d51c96270 --- /dev/null +++ b/test/regress/regress0/seq/seq-types.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp -q +;EXPECT: unsat +(set-logic ALL) +(declare-fun s () (Seq Int)) +(declare-fun n () Int) +(assert (= 5 (seq.nth s n))) +(assert (< n (seq.len s))) +(assert (> n 0)) +(assert (= (seq.unit 6) (seq.at s n))) +(check-sat) + -- 2.30.2