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.

20 files changed, 201 insertions, 2 deletions

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<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction>
         {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<bool>())
+    {
+      continue;
+    }
     // Apply any define-funs from the problem.
     {
       unordered_map<Node, Node, NodeHashFunction> 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<RString, AString>"
 
 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<Rational>().getNumerator().toUnsignedInt();
+    if (pos < len)
+    {
+      std::vector<Node> 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<TypeNode> 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)