From 0309ef4aa7462c6fa2a65c1ef408dc9063bb1f21 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Dec 2020 00:38:14 -0600 Subject: [PATCH] Proper implementation of expand definitions for sequences (#5616) Expand definitions for sequences was wrong in two ways: (1) we replaced str.from_code with a witness term. This led to it being unevaluatable in models. (2) we did not handle seq.nth, meaning its model value was unevaluatable if it was out of bounds. Now it evaluates the value of the uninterpreted function we replace with. This corrects both issues and adds a regression to demonstrate both kinds of terms evaluate correctly. To do this, I added a helper function to skolem cache as well as a new (internal-only) kind SEQ_NTH_TOTAL. Notice applications of this kind should only be used for model evaluation. Notice this fixes several check-model warnings in the regressions. It still does not fix others since other things must be corrected for model evaluation (e.g. expandDefinitions must be applied on theory assertions for --debug-check-models). This will be done in later PRs. --- src/theory/strings/kinds | 2 + src/theory/strings/rewrites.cpp | 3 +- src/theory/strings/rewrites.h | 3 +- src/theory/strings/sequences_rewriter.cpp | 10 +++- src/theory/strings/skolem_cache.cpp | 13 +++++ src/theory/strings/skolem_cache.h | 5 ++ src/theory/strings/theory_strings.cpp | 49 ++++++++++++------- .../strings/theory_strings_preprocess.cpp | 8 +-- test/regress/CMakeLists.txt | 1 + .../regress/regress0/seq/seq-expand-defs.smt2 | 19 +++++++ .../regress0/seq/seq-nth-undef-unsat.smt2 | 2 +- test/regress/regress0/seq/seq-types.smt2 | 2 +- 12 files changed, 85 insertions(+), 32 deletions(-) create mode 100644 test/regress/regress0/seq/seq-expand-defs.smt2 diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 020cedb30..427e2e4e6 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -84,6 +84,7 @@ constant CONST_SEQUENCE \ operator SEQ_UNIT 1 "a sequence of length one" operator SEQ_NTH 2 "The nth element of a sequence" +operator SEQ_NTH_TOTAL 2 "The nth element of a sequence (internal, for responses to expand definitions only)" # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" @@ -171,5 +172,6 @@ typerule STRING_TOLOWER "SimpleTypeRule" typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule typerule SEQ_NTH ::CVC4::theory::strings::SeqNthTypeRule +typerule SEQ_NTH_TOTAL ::CVC4::theory::strings::SeqNthTypeRule endtheory diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index a32e5bc9e..dca793049 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -210,7 +210,8 @@ const char* toString(Rewrite r) case Rewrite::LEN_SEQ_UNIT: return "LEN_SEQ_UNIT"; case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM"; case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL"; - case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL"; + case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL"; + case Rewrite::SEQ_NTH_TOTAL_OOB: return "SEQ_NTH_TOTAL_OOB"; default: return "?"; } } diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index f9824405b..a450ae7f6 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -213,7 +213,8 @@ enum class Rewrite : uint32_t LEN_SEQ_UNIT, CHARAT_ELIM, SEQ_UNIT_EVAL, - SEQ_NTH_EVAL + SEQ_NTH_EVAL, + SEQ_NTH_TOTAL_OOB }; /** diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 2cefe6b09..1382ab0f9 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1491,7 +1491,7 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteSeqUnit(node); } - else if (nk == SEQ_NTH) + else if (nk == SEQ_NTH || nk == SEQ_NTH_TOTAL) { retNode = rewriteSeqNth(node); } @@ -1516,7 +1516,7 @@ RewriteResponse SequencesRewriter::preRewrite(TNode node) Node SequencesRewriter::rewriteSeqNth(Node node) { - Assert(node.getKind() == SEQ_NTH); + Assert(node.getKind() == SEQ_NTH || node.getKind() == SEQ_NTH_TOTAL); Node ret; Node s = node[0]; Node i = node[1]; @@ -1530,6 +1530,12 @@ Node SequencesRewriter::rewriteSeqNth(Node node) ret = elements[pos]; return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL); } + else if (node.getKind() == SEQ_NTH_TOTAL) + { + // return arbitrary term + Node ret = s.getType().getSequenceElementType().mkGroundValue(); + return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB); + } else { return node; diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index a1e04071b..f5f2dfd35 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -130,6 +130,19 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn, return mkTypedSkolemCached(tn, a, Node::null(), id, c); } +Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c) +{ + Assert(seqType.isSequence()); + NodeManager* nm = NodeManager::currentNM(); + std::vector argTypes; + argTypes.push_back(seqType); + argTypes.push_back(nm->integerType()); + TypeNode elemType = seqType.getSequenceElementType(); + TypeNode ufType = nm->mkFunctionType(argTypes, elemType); + return mkTypedSkolemCached( + ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, c); +} + Node SkolemCache::mkSkolem(const char* c) { // TODO: eliminate this diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 0a6dd367f..fa76afebd 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -159,6 +159,11 @@ class SkolemCache TypeNode tn, Node a, Node b, SkolemId id, const char* c); /** Same as mkTypedSkolemCached above for (a,[null],id) */ Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c); + /** + * Specific version for seq.nth, used for cases where the index is out of + * range for sequence type seqType. + */ + Node mkSkolemSeqNth(TypeNode seqType, const char* c); /** Returns a (uncached) skolem of type string with name c */ Node mkSkolem(const char* c); /** Returns true if n is a skolem allocated by this class */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8ce8e0ecb..8915fcd02 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -570,23 +570,21 @@ TrustNode TheoryStrings::expandDefinition(Node node) { Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; - if (node.getKind() == STRING_FROM_CODE) + if (node.getKind() == kind::SEQ_NTH) { - // str.from_code(t) ---> - // witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "") NodeManager* nm = NodeManager::currentNM(); - Node t = node[0]; - Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); - Node cond = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card)); - Node k = nm->mkBoundVar(nm->stringType()); - Node bvl = nm->mkNode(BOUND_VAR_LIST, k); - Node emp = Word::mkEmptyWord(node.getType()); - Node ret = nm->mkNode( - WITNESS, - bvl, - nm->mkNode( - ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + SkolemCache* sc = d_termReg.getSkolemCache(); + Node s = node[0]; + Node n = node[1]; + // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n)) + Node cond = nm->mkNode(AND, + nm->mkNode(LEQ, d_zero, n), + nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); + Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n); + Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf"); + Node u = nm->mkNode(APPLY_UF, uf, s, n); + Node ret = nm->mkNode(ITE, cond, ss, u); + Trace("strings-exp-def") << "...return " << ret << std::endl; return TrustNode::mkTrustRewrite(node, ret, nullptr); } return TrustNode::null(); @@ -1006,11 +1004,24 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; - // first, see if we need to expand definitions - TrustNode texp = expandDefinition(atom); - if (!texp.isNull()) + if (atom.getKind() == STRING_FROM_CODE) { - return texp; + // str.from_code(t) ---> + // witness k. ite(0 <= t < |A|, t = str.to_code(k), k = "") + NodeManager* nm = NodeManager::currentNM(); + Node t = atom[0]; + Node card = nm->mkConst(Rational(utils::getAlphabetCardinality())); + Node cond = + nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card)); + Node k = nm->mkBoundVar(nm->stringType()); + Node bvl = nm->mkNode(BOUND_VAR_LIST, k); + Node emp = Word::mkEmptyWord(atom.getType()); + Node ret = nm->mkNode( + WITNESS, + bvl, + nm->mkNode( + ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp))); + return TrustNode::mkTrustRewrite(atom, ret, nullptr); } TrustNode ret; Node atomRet = atom; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 87ab533f4..81cca34af 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -444,13 +444,7 @@ Node StringsPreprocess::reduce(Node t, 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 uf = sc->mkSkolemSeqNth(s.getType(), "Uf"); Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n)); // the full ite, split on definedness of `seq.nth` diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 689b57514..062478075 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -908,6 +908,7 @@ set(regress_0_tests regress0/seq/seq-ex4.smt2 regress0/seq/seq-ex5-dd.smt2 regress0/seq/seq-ex5.smt2 + regress0/seq/seq-expand-defs.smt2 regress0/seq/seq-nemp.smt2 regress0/seq/seq-nth.smt2 regress0/seq/seq-nth-uf.smt2 diff --git a/test/regress/regress0/seq/seq-expand-defs.smt2 b/test/regress/regress0/seq/seq-expand-defs.smt2 new file mode 100644 index 000000000..3e51627c0 --- /dev/null +++ b/test/regress/regress0/seq/seq-expand-defs.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +; EXPECT: (((seq.nth y 7) 404)) +; EXPECT: (((str.from_code x) "?")) +(set-logic ALL) +(set-option :produce-models true) +(declare-fun x () Int) +(declare-fun y () (Seq Int)) + +(assert (< (seq.len y) 5)) + +(assert (= x 63)) + +(assert (= (seq.nth y 7) 404)) + +(check-sat) + +(get-value ((seq.nth y 7))) +(get-value ((str.from_code x))) diff --git a/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 b/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 index 4fe2a85a9..85382f90e 100644 --- a/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 +++ b/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ;EXPECT: unsat (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 index d51c96270..3facf688a 100644 --- a/test/regress/regress0/seq/seq-types.smt2 +++ b/test/regress/regress0/seq/seq-types.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp -q +; COMMAND-LINE: --strings-exp ;EXPECT: unsat (set-logic ALL) (declare-fun s () (Seq Int)) -- 2.30.2