diff options
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 6 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 7 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 6 | ||||
-rw-r--r-- | src/theory/strings/word.cpp | 138 | ||||
-rw-r--r-- | src/theory/strings/word.h | 4 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/ho/issue4477.smt2 | 11 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_word_white.h | 4 |
9 files changed, 170 insertions, 11 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d591c29de..95f4b1a67 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2630,8 +2630,8 @@ CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple'; TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel'; -HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->'; -HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda'; +HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; +HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda'; /** * A sequence of printable ASCII characters (except backslash) that starts diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 91260d1db..9ca2194f4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -315,6 +315,12 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const return d_logic.isTheoryEnabled(theory); } +bool Smt2::isHoEnabled() const +{ + return getLogic().isHigherOrder() + && d_solver->getExprManager()->getOptions().getUfHo(); +} + bool Smt2::logicIsSet() { return d_logicSet; } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 35d088601..af1e36795 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -98,6 +98,13 @@ class Smt2 : public Parser bool isTheoryEnabled(theory::TheoryId theory) const; + /** + * Checks if higher-order support is enabled. + * + * @return true if higher-order support is enabled, false otherwise + */ + bool isHoEnabled() const; + bool logicIsSet() override; /** diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 55d58b860..4f74d7c15 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -264,7 +264,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // Add a constant string to the side with more `cn`s to restore // the difference in number of `cn`s std::vector<Node> vec(diff, cn); - trimmed[j].push_back(Word::mkWord(vec)); + trimmed[j].push_back(Word::mkWordFlatten(vec)); } } @@ -602,7 +602,7 @@ Node SequencesRewriter::rewriteConcat(Node node) std::vector<Node> wvec; wvec.push_back(preNode); wvec.push_back(tmpNode[0]); - preNode = Word::mkWord(wvec); + preNode = Word::mkWordFlatten(wvec); node_vec.push_back(preNode); } else @@ -644,7 +644,7 @@ Node SequencesRewriter::rewriteConcat(Node node) std::vector<Node> vec; vec.push_back(preNode); vec.push_back(tmpNode); - preNode = Word::mkWord(vec); + preNode = Word::mkWordFlatten(vec); } } } diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index e9ab2652e..3f6a9de32 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -14,6 +14,7 @@ #include "theory/strings/word.h" +#include "expr/sequence.h" #include "util/string.h" using namespace CVC4::kind; @@ -28,23 +29,28 @@ Node Word::mkEmptyWord(TypeNode tn) { return mkEmptyWord(CONST_STRING); } + else if (tn.isSequence()) + { + std::vector<Expr> seq; + return NodeManager::currentNM()->mkConst( + ExprSequence(tn.getSequenceElementType().toType(), seq)); + } Unimplemented(); return Node::null(); } Node Word::mkEmptyWord(Kind k) { - NodeManager* nm = NodeManager::currentNM(); if (k == CONST_STRING) { std::vector<unsigned> vec; - return nm->mkConst(String(vec)); + return NodeManager::currentNM()->mkConst(String(vec)); } Unimplemented(); return Node::null(); } -Node Word::mkWord(const std::vector<Node>& xs) +Node Word::mkWordFlatten(const std::vector<Node>& xs) { Assert(!xs.empty()); NodeManager* nm = NodeManager::currentNM(); @@ -61,6 +67,22 @@ Node Word::mkWord(const std::vector<Node>& xs) } return nm->mkConst(String(vec)); } + else if (k == CONST_SEQUENCE) + { + std::vector<Expr> seq; + TypeNode tn = xs[0].getType(); + for (TNode x : xs) + { + Assert(x.getType() == tn); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const std::vector<Node>& vecc = sx.getVec(); + for (const Node& c : vecc) + { + seq.push_back(c.toExpr()); + } + } + return NodeManager::currentNM()->mkConst(ExprSequence(tn.toType(), seq)); + } Unimplemented(); return Node::null(); } @@ -72,6 +94,10 @@ size_t Word::getLength(TNode x) { return x.getConst<String>().size(); } + else if (k == CONST_SEQUENCE) + { + return x.getConst<ExprSequence>().getSequence().size(); + } Unimplemented(); return 0; } @@ -111,6 +137,13 @@ bool Word::strncmp(TNode x, TNode y, std::size_t n) String sy = y.getConst<String>(); return sx.strncmp(sy, n); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.strncmp(sy, n); + } Unimplemented(); return false; } @@ -125,6 +158,13 @@ bool Word::rstrncmp(TNode x, TNode y, std::size_t n) String sy = y.getConst<String>(); return sx.rstrncmp(sy, n); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.rstrncmp(sy, n); + } Unimplemented(); return false; } @@ -139,6 +179,13 @@ std::size_t Word::find(TNode x, TNode y, std::size_t start) String sy = y.getConst<String>(); return sx.find(sy, start); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.find(sy, start); + } Unimplemented(); return 0; } @@ -153,6 +200,13 @@ std::size_t Word::rfind(TNode x, TNode y, std::size_t start) String sy = y.getConst<String>(); return sx.rfind(sy, start); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.rfind(sy, start); + } Unimplemented(); return 0; } @@ -167,6 +221,13 @@ bool Word::hasPrefix(TNode x, TNode y) String sy = y.getConst<String>(); return sx.hasPrefix(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.hasPrefix(sy); + } Unimplemented(); return false; } @@ -181,6 +242,13 @@ bool Word::hasSuffix(TNode x, TNode y) String sy = y.getConst<String>(); return sx.hasSuffix(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.hasSuffix(sy); + } Unimplemented(); return false; } @@ -198,6 +266,16 @@ Node Word::replace(TNode x, TNode y, TNode t) String st = t.getConst<String>(); return nm->mkConst(String(sx.replace(sy, st))); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + Assert(t.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& st = t.getConst<ExprSequence>().getSequence(); + Sequence res = sx.replace(sy, st); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -210,6 +288,12 @@ Node Word::substr(TNode x, std::size_t i) String sx = x.getConst<String>(); return nm->mkConst(String(sx.substr(i))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + Sequence res = sx.substr(i); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -222,6 +306,12 @@ Node Word::substr(TNode x, std::size_t i, std::size_t j) String sx = x.getConst<String>(); return nm->mkConst(String(sx.substr(i, j))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + Sequence res = sx.substr(i, j); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -237,6 +327,12 @@ Node Word::suffix(TNode x, std::size_t i) String sx = x.getConst<String>(); return nm->mkConst(String(sx.suffix(i))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + Sequence res = sx.suffix(i); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -251,6 +347,13 @@ bool Word::noOverlapWith(TNode x, TNode y) String sy = y.getConst<String>(); return sx.noOverlapWith(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.noOverlapWith(sy); + } Unimplemented(); return false; } @@ -265,6 +368,13 @@ std::size_t Word::overlap(TNode x, TNode y) String sy = y.getConst<String>(); return sx.overlap(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.overlap(sy); + } Unimplemented(); return 0; } @@ -279,10 +389,32 @@ std::size_t Word::roverlap(TNode x, TNode y) String sy = y.getConst<String>(); return sx.roverlap(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.roverlap(sy); + } Unimplemented(); return 0; } +bool Word::isRepeated(TNode x) +{ + Kind k = x.getKind(); + if (k == CONST_STRING) + { + return x.getConst<String>().isRepeated(); + } + else if (k == CONST_SEQUENCE) + { + return x.getConst<ExprSequence>().getSequence().isRepeated(); + } + Unimplemented(); + return false; +} + Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev) { Assert(x.isConst() && y.isConst()); diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index b84ea6874..ad1d9bc74 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -37,7 +37,7 @@ class Word static Node mkEmptyWord(Kind k); /** make word from constants in (non-empty) vector vec */ - static Node mkWord(const std::vector<Node>& xs); + static Node mkWordFlatten(const std::vector<Node>& xs); /** Return the length of word x */ static size_t getLength(TNode x); @@ -139,6 +139,8 @@ class Word * Notice that x.overlap(y) = y.roverlap(x) */ static std::size_t roverlap(TNode x, TNode y); + /** Return true if word x is a repetition of the same character */ + static bool isRepeated(TNode x); /** Split constant * * This returns the suffix remainder (resp. prefix remainder when isRev is diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 20985a5f8..0f1b090d4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -540,6 +540,7 @@ set(regress_0_tests regress0/ho/ho-matching-nested-app.smt2 regress0/ho/ho-std-fmf.smt2 regress0/ho/hoa0008.smt2 + regress0/ho/issue4477.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/match-middle.smt2 diff --git a/test/regress/regress0/ho/issue4477.smt2 b/test/regress/regress0/ho/issue4477.smt2 new file mode 100644 index 000000000..7162d260c --- /dev/null +++ b/test/regress/regress0/ho/issue4477.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: no-competition +; SCRUBBER: grep -o "Symbol '->' not declared" +; EXPECT: Symbol '->' not declared +; EXIT: 1 +(set-logic ALL) +(declare-sort s 0) +(declare-fun a () s) +(declare-fun b () s) +(declare-fun c (s) s) +(assert (forall ((d (-> s s))) (distinct (d a) (c a) b))) +(check-sat) diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h index d84df7836..6b594d904 100644 --- a/test/unit/theory/theory_strings_word_white.h +++ b/test/unit/theory/theory_strings_word_white.h @@ -67,10 +67,10 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite std::vector<Node> vec; vec.push_back(abc); - Node abcMk = Word::mkWord(vec); + Node abcMk = Word::mkWordFlatten(vec); TS_ASSERT_EQUALS(abc, abcMk); vec.push_back(a); - Node abcaMk = Word::mkWord(vec); + Node abcaMk = Word::mkWordFlatten(vec); TS_ASSERT_EQUALS(abca, abcaMk); TS_ASSERT(Word::getLength(empty) == 0); |