diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index d49fc45b3e0..9ae621dbe65 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1286,6 +1286,20 @@ static void string_issue_2298() { s.pop(); } +void iterate_args() { + std::cout << "iterate arguments\n"; + context c; + expr x = c.int_const("x"); + expr y = c.int_const("y"); + sort I = c.int_sort(); + func_decl g = function("g", I, I, I); + expr e = g(x, y); + std::cout << "expression " << e << "\n"; + for (expr arg : e) + std::cout << "arg " << arg << "\n"; + +} + int main() { try { @@ -1339,6 +1353,7 @@ int main() { recfun_example(); std::cout << "\n"; string_values(); std::cout << "\n"; string_issue_2298(); std::cout << "\n"; + iterate_args(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index fd204a5bf72..d715c73cb75 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1495,6 +1495,26 @@ namespace z3 { */ expr substitute(expr_vector const& dst); + + class iterator { + expr& e; + unsigned i; + public: + iterator(expr& e, unsigned i): e(e), i(i) {} + bool operator==(iterator const& other) noexcept { + return i == other.i; + } + bool operator!=(iterator const& other) noexcept { + return i != other.i; + } + expr operator*() const { return e.arg(i); } + iterator& operator++() { ++i; return *this; } + iterator operator++(int) { assert(false); return *this; } + }; + + iterator begin() { return iterator(*this, 0); } + iterator end() { return iterator(*this, is_app() ? num_args() : 0); } + }; #define _Z3_MK_BIN_(a, b, binop) \