make it easier to iterate over arguments of an application

Signed-off-by: Nikolaj Bjorner <[email protected]>

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

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