Merge branch 'master' into issue4367issue4367

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);