From 834cf962a1849ffce77bf8fe9e6b74fbed26c3ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Mar 2019 11:23:01 -0700 Subject: [PATCH] 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 --- src/api/api_seq.cpp | 1 + src/api/c++/z3++.h | 27 +++++++++++++++++++++++++++ src/api/dotnet/ArrayExpr.cs | 6 ++++++ src/api/dotnet/Context.cs | 13 ++++++++++++- src/api/dotnet/SeqExpr.cs | 5 +++++ src/api/python/z3/z3.py | 5 +++++ src/api/z3_api.h | 10 ++++++++++ 7 files changed, 66 insertions(+), 1 deletion(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 08307c0bc..b06a63507 100644 --- a/src/api/api_seq.cpp +++ b/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); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index fb0657aa2..c8aac77d3 100644 --- a/src/api/c++/z3++.h +++ b/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. diff --git a/src/api/dotnet/ArrayExpr.cs b/src/api/dotnet/ArrayExpr.cs index c53763886..d0e45561d 100644 --- a/src/api/dotnet/ArrayExpr.cs +++ b/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); } + } + } } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index cdaae332b..150283ea5 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2454,7 +2454,7 @@ namespace Microsoft.Z3 /// /// Retrieve sequence of length one at index. /// - 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)); } + /// + /// Retrieve element at index. + /// + 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)); + } + /// /// Extract subsequence. /// diff --git a/src/api/dotnet/SeqExpr.cs b/src/api/dotnet/SeqExpr.cs index bfab1fa36..1544d630f 100644 --- a/src/api/dotnet/SeqExpr.cs +++ b/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); } + } } } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f31df5a4f..880bf009f 100644 --- a/src/api/python/z3/z3.py +++ b/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) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ce59210f1..2ca2c14d9 100644 --- a/src/api/z3_api.h +++ b/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.