expose nth over API, change _getitem_ in python bindings to use nth instead of at, add 'at' operator for the purpose of the previous semantics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_seq.cpp

@@ -145,6 +145,7 @@ extern "C" {
     MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP);
     MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP);
     MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
+    MK_BINARY(Z3_mk_seq_nth, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
     MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP);
     MK_TERNARY(Z3_mk_seq_index, mk_c(c)->get_seq_fid(), OP_SEQ_INDEX, SKIP);
     MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);

src/api/c++/z3++.h

@@ -648,10 +648,17 @@ namespace z3 {
         expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
     };
 
+    /**
+       \brief forward declarations
+     */
+    expr select(expr const & a, expr const& i);
+    expr select(expr const & a, expr_vector const & i);
+
     /**
        \brief A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean.
        Every expression has a sort.
     */
+
     class expr : public ast {
     public:
         expr(context & c):ast(c) {}
@@ -1136,6 +1143,12 @@ namespace z3 {
             check_error();
             return expr(ctx(), r);
         }
+        expr nth(expr const& index) const {
+            check_context(*this, index);
+            Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
+            check_error();
+            return expr(ctx(), r);
+        }
         expr length() const {
             Z3_ast r = Z3_mk_seq_length(ctx(), *this);
             check_error();
@@ -1167,6 +1180,20 @@ namespace z3 {
             return expr(ctx(), r);
         }
 
+        /**
+         * index operator defined on arrays and sequences.
+         */
+        expr operator[](expr const& index) const {
+            assert(is_array() || is_seq());
+            if (is_array()) {
+                return select(*this, index);
+            }
+            return nth(index);            
+        }
+
+        expr operator[](expr_vector const& index) const {
+            return select(*this, index);
+        }
 
         /**
            \brief Return a simplified version of this expression.

src/api/dotnet/ArrayExpr.cs

@@ -38,5 +38,11 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
         #endregion	
+
+        public Expr this[Expr index] 
+        {
+            get { return Context.MkSelect(this, index); }
+        }
+
     }
 }

src/api/dotnet/Context.cs

@@ -2454,7 +2454,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Retrieve sequence of length one at index.
         /// </summary>
-        public SeqExpr MkAt(SeqExpr s, IntExpr index)
+        public SeqExpr MkAt(SeqExpr s, Expr index)
         {
             Debug.Assert(s != null);
             Debug.Assert(index != null);
@@ -2462,6 +2462,17 @@ namespace Microsoft.Z3
             return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
         }
 
+        /// <summary>
+        /// Retrieve element at index.
+        /// </summary>
+        public SeqExpr MkNth(SeqExpr s, Expr index)
+        {
+            Debug.Assert(s != null);
+            Debug.Assert(index != null);
+            CheckContextMatch(s, index);
+            return new SeqExpr(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
+        }
+
         /// <summary>
         /// Extract subsequence.
         /// </summary>

src/api/dotnet/SeqExpr.cs

@@ -38,5 +38,10 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
         #endregion
+
+        public Expr this[Expr index] 
+        {
+            get { return Context.MkNth(this, index); }
+        }
     }
 }

src/api/python/z3/z3.py

@@ -9941,6 +9941,11 @@ class SeqRef(ExprRef):
         return Concat(other, self)
 
     def __getitem__(self, i):
+        if _is_int(i):
+            i = IntVal(i, self.ctx)
+        return SeqRef(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
+
+    def at(self, i):
         if _is_int(i):
             i = IntVal(i, self.ctx)
         return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)

src/api/z3_api.h

@@ -1168,6 +1168,7 @@ typedef enum {
     Z3_OP_SEQ_EXTRACT,
     Z3_OP_SEQ_REPLACE,
     Z3_OP_SEQ_AT,
+    Z3_OP_SEQ_NTH,
     Z3_OP_SEQ_LENGTH,
     Z3_OP_SEQ_INDEX,
     Z3_OP_SEQ_TO_RE,
@@ -3420,11 +3421,20 @@ extern "C" {
 
     /**
        \brief Retrieve from \c s the unit sequence positioned at position \c index.
+       The sequence is empty if the index is out of bounds.
 
        def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
      */
     Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
 
+    /**
+       \brief Retrieve from \c s the element positioned at position \c index.
+       The function is under-specified if the index is out of bounds.
+
+       def_API('Z3_mk_seq_nth' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index);
+
     /**
        \brief Return the length of the sequence \c s.