From: Andres Noetzli Date: Wed, 20 Apr 2022 21:44:01 +0000 (-0700) Subject: Remove unused `SEQ_NTH_TOTAL` kind (#8048) X-Git-Tag: cvc5-1.0.1~237 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76d9f4359231c2443b7040bac100bb1abcff8d79;p=cvc5.git Remove unused `SEQ_NTH_TOTAL` kind (#8048) Originally, the idea was to expand the definition of `SEQ_NTH` to use `SEQ_NTH_TOTAL` (i.e., a total version of that operator), but we have since then decided to just use `SEQ_NTH`. --- diff --git a/src/parser/parser.h b/src/parser/parser.h index 750ec1d7d..47bb7d7d6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -25,7 +25,6 @@ #include "api/cpp/cvc5.h" #include "cvc5_export.h" -#include "expr/kind.h" #include "expr/symbol_manager.h" #include "expr/symbol_table.h" #include "parser/input.h" diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index bec5fd363..5f14efce7 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -97,7 +97,6 @@ parameterized SEQ_UNIT SEQ_UNIT_OP 1 \ "a sequence of length one. First parameter is a SeqUnitOp. Second is a term" 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" @@ -196,6 +195,5 @@ typerule CONST_SEQUENCE ::cvc5::internal::theory::strings::ConstSequenceTypeRule typerule SEQ_UNIT_OP "SimpleTypeRule" typerule SEQ_UNIT ::cvc5::internal::theory::strings::SeqUnitTypeRule typerule SEQ_NTH ::cvc5::internal::theory::strings::SeqNthTypeRule -typerule SEQ_NTH_TOTAL ::cvc5::internal::theory::strings::SeqNthTypeRule endtheory diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index bc651cb70..e4d702905 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -228,7 +228,6 @@ const char* toString(Rewrite r) 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_TOTAL_OOB: return "SEQ_NTH_TOTAL_OOB"; case Rewrite::SEQ_NTH_EVAL_SYM: return "SEQ_NTH_EVAL_SYM"; default: return "?"; } diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index ff58989c9..98a3bc866 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -229,7 +229,6 @@ enum class Rewrite : uint32_t CHARAT_ELIM, SEQ_UNIT_EVAL, SEQ_NTH_EVAL, - SEQ_NTH_TOTAL_OOB, SEQ_NTH_EVAL_SYM }; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 83288b55f..3b3290b26 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1717,7 +1717,7 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteSeqUnit(node); } - else if (nk == SEQ_NTH || nk == SEQ_NTH_TOTAL) + else if (nk == SEQ_NTH) { retNode = rewriteSeqNth(node); } @@ -1743,33 +1743,9 @@ RewriteResponse SequencesRewriter::preRewrite(TNode node) return RewriteResponse(REWRITE_DONE, node); } -TrustNode SequencesRewriter::expandDefinition(Node node) -{ - Trace("strings-exp-def") << "SequencesRewriter::expandDefinition : " << node - << std::endl; - - if (node.getKind() == kind::SEQ_NTH) - { - NodeManager* nm = NodeManager::currentNM(); - 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, nm->mkConstInt(Rational(0)), n), - nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); - Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n); - Node uf = SkolemCache::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(); -} - Node SequencesRewriter::rewriteSeqNth(Node node) { - Assert(node.getKind() == SEQ_NTH || node.getKind() == SEQ_NTH_TOTAL); + Assert(node.getKind() == SEQ_NTH); Node s = node[0]; Node i = node[1]; if (s.isConst() && i.isConst()) @@ -1786,13 +1762,6 @@ Node SequencesRewriter::rewriteSeqNth(Node node) return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL); } } - if (node.getKind() == SEQ_NTH_TOTAL) - { - // return arbitrary term - NodeManager* nm = NodeManager::currentNM(); - Node ret = nm->mkGroundValue(s.getType().getSequenceElementType()); - return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB); - } } std::vector prefix, suffix; diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 451a27e4f..e7b1831f1 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -132,8 +132,6 @@ class SequencesRewriter : public TheoryRewriter public: RewriteResponse postRewrite(TNode node) override; RewriteResponse preRewrite(TNode node) override; - /** Expand definition */ - TrustNode expandDefinition(Node n) override; /** rewrite equality * diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6549944b6..52ff94510 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -62,7 +62,6 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee) d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); d_equalityEngine->addFunctionKind(kind::SEQ_NTH); - d_equalityEngine->addFunctionKind(kind::SEQ_NTH_TOTAL); // do not interpret APPLY_UF if we are not assigning function values if (!d_enableFuncModels) { diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 50210380a..7720cdcc9 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -131,7 +131,7 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a) bool TheoryEngineModelBuilder::isAssignable(TNode n) { if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR - || n.getKind() == kind::SEQ_NTH_TOTAL || n.getKind() == kind::SEQ_NTH) + || n.getKind() == kind::SEQ_NTH) { // selectors are always assignable (where we guarantee that they are not // evaluatable here) diff --git a/test/regress/cli/regress0/seq/seq-expand-defs.smt2 b/test/regress/cli/regress0/seq/seq-expand-defs.smt2 index 065dd6bd5..cafb516ba 100644 --- a/test/regress/cli/regress0/seq/seq-expand-defs.smt2 +++ b/test/regress/cli/regress0/seq/seq-expand-defs.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --strings-exp -q ; EXPECT: sat -; EXPECT: (((seq.nth y 7) 404)) +; EXPECT: (((seq.nth y 7) (seq.nth (as seq.empty (Seq Int)) 7))) ; EXPECT: (((str.from_code x) "?")) (set-logic ALL) (set-option :produce-models true)