From: yoni206 Date: Tue, 28 Jul 2020 17:44:55 +0000 (-0700) Subject: Supporting seq.nth (#4723) X-Git-Tag: cvc5-1.0.0~3076 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ad41fe71b9f7d206ee6d1c642bb7926bffea6c7;p=cvc5.git Supporting seq.nth (#4723) This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences. Tests that use this operator are also included. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index fa995a00a..c009f69e5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -305,6 +305,7 @@ const static std::unordered_map s_kinds{ {SEQ_SUFFIX, CVC4::Kind::STRING_SUFFIX}, {CONST_SEQUENCE, CVC4::Kind::CONST_SEQUENCE}, {SEQ_UNIT, CVC4::Kind::SEQ_UNIT}, + {SEQ_NTH, CVC4::Kind::SEQ_NTH}, /* Quantifiers --------------------------------------------------------- */ {FORALL, CVC4::Kind::FORALL}, {EXISTS, CVC4::Kind::EXISTS}, @@ -580,6 +581,7 @@ const static std::unordered_map {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, {CVC4::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, {CVC4::Kind::SEQ_UNIT, SEQ_UNIT}, + {CVC4::Kind::SEQ_NTH, SEQ_NTH}, /* Quantifiers ----------------------------------------------------- */ {CVC4::Kind::FORALL, FORALL}, {CVC4::Kind::EXISTS, EXISTS}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 9e1ce3ecf..f56e48cad 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2510,6 +2510,15 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child1) */ SEQ_UNIT, + /** + * Sequence nth, corresponding to the nth element of a sequence. + * Parameters: 2 + * -[1] Sequence term. + * -[2] Integer term. + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + */ + SEQ_NTH, /* Quantifiers ----------------------------------------------------------- */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 69c4eabfd..eef23edfd 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -181,6 +181,7 @@ void Smt2::addStringOperators() { addOperator(api::SEQ_REV, "seq.rev"); addOperator(api::SEQ_REPLACE_ALL, "seq.replace_all"); addOperator(api::SEQ_UNIT, "seq.unit"); + addOperator(api::SEQ_NTH, "seq.nth"); } // at the moment, we only use this syntax for smt2.6 if (getLanguage() == language::input::LANG_SMTLIB_V2_6 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 23503ea28..d6b304a78 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -662,6 +662,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::REGEXP_EMPTY: case kind::REGEXP_SIGMA: case kind::SEQ_UNIT: + case kind::SEQ_NTH: case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break; case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; @@ -1231,6 +1232,7 @@ static string smtKindString(Kind k, Variant v) case kind::REGEXP_COMPLEMENT: return "re.comp"; case kind::SEQUENCE_TYPE: return "Seq"; case kind::SEQ_UNIT: return "seq.unit"; + case kind::SEQ_NTH: return "seq.nth"; //sep theory case kind::SEP_STAR: return "sep"; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c8896b621..9ff6ec6f5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2508,7 +2508,13 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): checking assertion " << assertion << endl; Node n = assertion; - + Node nr = Rewriter::rewrite(substitutions.apply(n)); + Trace("boolean-terms") << "n: " << n << endl; + Trace("boolean-terms") << "nr: " << nr << endl; + if (nr.isConst() && nr.getConst()) + { + continue; + } // Apply any define-funs from the problem. { unordered_map cache; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 226dcbd17..131a48ae9 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -83,6 +83,7 @@ constant CONST_SEQUENCE \ "a sequence of characters" operator SEQ_UNIT 1 "a sequence of length one" +operator SEQ_NTH 2 "The nth element of a sequence" # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" @@ -169,5 +170,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 endtheory diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index 6ea467ae9..82aa21185 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -210,6 +210,7 @@ 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"; default: return "?"; } } diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index bc5de3a8a..c62129385 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -212,7 +212,8 @@ enum class Rewrite : uint32_t LEN_CONV_INV, LEN_SEQ_UNIT, CHARAT_ELIM, - SEQ_UNIT_EVAL + SEQ_UNIT_EVAL, + SEQ_NTH_EVAL }; /** diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 292960e6a..f05c32356 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1488,6 +1488,10 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteSeqUnit(node); } + else if (nk == SEQ_NTH) + { + retNode = rewriteSeqNth(node); + } Trace("sequences-postrewrite") << "Strings::SequencesRewriter::postRewrite returning " << retNode @@ -1507,6 +1511,33 @@ RewriteResponse SequencesRewriter::preRewrite(TNode node) return RewriteResponse(REWRITE_DONE, node); } +Node SequencesRewriter::rewriteSeqNth(Node node) +{ + Assert(node.getKind() == SEQ_NTH); + Node ret; + Node s = node[0]; + Node i = node[1]; + if (s.isConst() && i.isConst()) + { + size_t len = Word::getLength(s); + size_t pos = i.getConst().getNumerator().toUnsignedInt(); + if (pos < len) + { + std::vector elements = Word::getChars(s); + ret = elements[pos]; + return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL); + } + else + { + return node; + } + } + else + { + return node; + } +} + Node SequencesRewriter::rewriteCharAt(Node node) { Assert(node.getKind() == STRING_CHARAT); diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 47a20a7ca..ed09397d3 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -264,6 +264,13 @@ class SequencesRewriter : public TheoryRewriter */ Node rewriteSeqUnit(Node node); + /** rewrite seq.nth + * This is the entry point for post-rewriting terms n of the form + * seq.nth(s, i) + * Returns the rewritten form of node. + */ + Node rewriteSeqNth(Node node); + /** length preserving rewrite * * Given input n, this returns a string n' whose length is equivalent to n. diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 302c69e83..755f70833 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -138,6 +138,11 @@ class SkolemCache // where b is a regular expression, n is the number of occurrences of b // in a, and k(0)=0. SK_OCCUR_LEN, + // For function k: ((Seq U) x Int) -> U + // exists k. + // forall s, n. + // k(s, n) is some undefined value of sort U + SK_NTH, }; /** * Returns a skolem of type string that is cached for (a,b,id) and has diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1fffd9638..84fd08e7c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -594,6 +594,40 @@ TrustNode TheoryStrings::expandDefinition(Node node) 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_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 12ddb8a3d..b9d0899f2 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -376,6 +376,30 @@ class SeqUnitTypeRule } }; +class SeqNthTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + { + TypeNode t = n[0].getType(check); + TypeNode t1 = t.getSequenceElementType(); + if (check) + { + if (!t.isSequence()) + { + throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth"); + } + TypeNode t2 = n[1].getType(check); + if (!t2.isInteger()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting an integer start term in nth"); + } + } + return t1; + } +}; + /** Properties of the sequence type */ struct SequenceProperties { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a3dbd847a..7f3c693c0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -861,6 +861,8 @@ set(regress_0_tests regress0/sep/skolem_emp.smt2 regress0/sep/trees-1.smt2 regress0/sep/wand-crash.smt2 + regress0/seq/intseq.smt2 + regress0/seq/intseq_dt.smt2 regress0/seq/seq-2var.smt2 regress0/seq/seq-ex1.smt2 regress0/seq/seq-ex2.smt2 @@ -869,6 +871,10 @@ set(regress_0_tests regress0/seq/seq-ex5-dd.smt2 regress0/seq/seq-ex5.smt2 regress0/seq/seq-nemp.smt2 + 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-rewrites.smt2 regress0/sets/abt-min.smt2 regress0/sets/abt-te-exh.smt2 diff --git a/test/regress/regress0/seq/intseq.smt2 b/test/regress/regress0/seq/intseq.smt2 new file mode 100644 index 000000000..e9d07e050 --- /dev/null +++ b/test/regress/regress0/seq/intseq.smt2 @@ -0,0 +1,14 @@ +;EXPECT: unsat +(set-logic ALL) +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun s@0 () (Seq Int)) +(declare-fun s@1 () (Seq Int)) +(declare-fun s@2 () (Seq Int)) +(assert (not + (=> (= (ControlFlow 0 0) 170) (let ((anon0_correct (=> (= s@0 (seq.++ (as seq.empty (Seq Int)) (seq.unit 0))) (=> (and (= s@1 (seq.++ s@0 (seq.unit 1))) (= s@2 (seq.++ s@1 (seq.unit 2)))) (and (=> (= (ControlFlow 0 135) (- 0 217)) (= (seq.len s@2) 3)) (=> (= (seq.len s@2) 3) (=> (= (ControlFlow 0 135) (- 0 224)) (= (seq.extract s@2 1 2) (seq.++ (seq.unit 1) (seq.unit 2)))))))))) +(let ((PreconditionGeneratedEntry_correct (=> (= (ControlFlow 0 170) 135) anon0_correct))) +PreconditionGeneratedEntry_correct))) +)) +(check-sat) diff --git a/test/regress/regress0/seq/intseq_dt.smt2 b/test/regress/regress0/seq/intseq_dt.smt2 new file mode 100644 index 000000000..36d2f4842 --- /dev/null +++ b/test/regress/regress0/seq/intseq_dt.smt2 @@ -0,0 +1,20 @@ +;COMMAND-LINE: --dt-nested-rec +;EXPECT: unsat +(set-logic ALL) +(declare-fun tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-datatypes ((T@Value 0)(T@ValueArray 0)) (((Integer (|i#Integer| Int) ) (Vector (|v#Vector| T@ValueArray) ) ) ((ValueArray (|v#ValueArray| (Seq T@Value)) ) ) )) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun s@0 () T@ValueArray) +(declare-fun s@1 () T@ValueArray) +(declare-fun s@2 () T@ValueArray) +(declare-fun s@3 () T@ValueArray) +(declare-fun s@4 () T@ValueArray) +(declare-fun s@5 () T@ValueArray) +(set-info :boogie-vc-id test) +(assert (not + (=> (= (ControlFlow 0 0) 427) (let ((anon0_correct (=> (= s@0 (ValueArray (as seq.empty (Seq T@Value)))) (and (=> (= (ControlFlow 0 331) (- 0 448)) (= (seq.len (|v#ValueArray| s@0)) 0)) (=> (= (seq.len (|v#ValueArray| s@0)) 0) (=> (= s@1 (ValueArray (seq.++ (|v#ValueArray| s@0) (seq.unit (Integer 0))))) (=> (and (= s@2 (ValueArray (seq.++ (|v#ValueArray| s@1) (seq.unit (Integer 1))))) (= s@3 (ValueArray (seq.++ (|v#ValueArray| s@2) (seq.unit (Integer 2)))))) (and (=> (= (ControlFlow 0 331) (- 0 490)) (= (seq.len (|v#ValueArray| s@3)) 3)) (=> (= (seq.len (|v#ValueArray| s@3)) 3) (and (=> (= (ControlFlow 0 331) (- 0 497)) (= (seq.nth (|v#ValueArray| s@3) 1) (Integer 1))) (=> (= (seq.nth (|v#ValueArray| s@3) 1) (Integer 1)) (=> (= s@4 (ValueArray (seq.extract (|v#ValueArray| s@3) 0 (- (seq.len (|v#ValueArray| s@3)) 1)))) (and (=> (= (ControlFlow 0 331) (- 0 517)) (= (seq.len (|v#ValueArray| s@4)) 2)) (=> (= (seq.len (|v#ValueArray| s@4)) 2) (=> (= s@5 (ValueArray (seq.++ (|v#ValueArray| s@4) (|v#ValueArray| s@4)))) (and (=> (= (ControlFlow 0 331) (- 0 534)) (= (seq.len (|v#ValueArray| s@5)) 4)) (=> (= (seq.len (|v#ValueArray| s@5)) 4) (=> (= (ControlFlow 0 331) (- 0 541)) (= (seq.nth (|v#ValueArray| s@5) 3) (Integer 1)))))))))))))))))))) +(let ((PreconditionGeneratedEntry_correct (=> (= (ControlFlow 0 427) 331) anon0_correct))) +PreconditionGeneratedEntry_correct))) +)) +(check-sat) diff --git a/test/regress/regress0/seq/seq-nth-uf-z.smt2 b/test/regress/regress0/seq/seq-nth-uf-z.smt2 new file mode 100644 index 000000000..0ae8a702b --- /dev/null +++ b/test/regress/regress0/seq/seq-nth-uf-z.smt2 @@ -0,0 +1,11 @@ +;EXPECT: unsat +(set-logic ALL) +(declare-fun a () (Seq Int)) +(declare-fun b () (Seq Int)) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(assert (or (= x z) (= y z))) +(assert (not (= (seq.nth a x) (seq.nth a z)))) +(assert (not (= (seq.nth b y) (seq.nth b z)))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/seq/seq-nth-uf.smt2 b/test/regress/regress0/seq/seq-nth-uf.smt2 new file mode 100644 index 000000000..af0b93170 --- /dev/null +++ b/test/regress/regress0/seq/seq-nth-uf.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_UFSLIA) +(set-info :status unsat) +(declare-fun a () (Seq Int)) +(declare-fun b () (Seq Int)) +(declare-fun c () (Seq Int)) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (or (= a b) (= a c))) +(assert (not (= (seq.nth a x) (seq.nth b x)))) +(assert (not (= (seq.nth a y) (seq.nth c y)))) +(check-sat) diff --git a/test/regress/regress0/seq/seq-nth-undef.smt2 b/test/regress/regress0/seq/seq-nth-undef.smt2 new file mode 100644 index 000000000..765b3e2f6 --- /dev/null +++ b/test/regress/regress0/seq/seq-nth-undef.smt2 @@ -0,0 +1,6 @@ +;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 new file mode 100644 index 000000000..765b3e2f6 --- /dev/null +++ b/test/regress/regress0/seq/seq-nth.smt2 @@ -0,0 +1,6 @@ +;EXPECT: sat +(set-logic ALL) +(declare-fun s () (Seq Int)) +(assert (= 5 (seq.nth s 5))) +(assert (= 2 (seq.len s))) +(check-sat)