From cfdde2f4d1d1286d2bfcaad7bf5c7be202b024ad Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 8 Jan 2018 13:24:52 +0000 Subject: [PATCH] Added apply_result::as_expr to the C++ API. Requested here: https://stackoverflow.com/questions/48071840/get-result-of-tactics-application-as-an-expression-in-z3 --- src/api/c++/z3++.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 80838256108..89b051eb535 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2101,6 +2101,19 @@ namespace z3 { check_error(); return model(ctx(), new_m); } + expr as_expr() const { + unsigned n = size(); + if (n == 0) + return ctx().bool_val(true); + else if (n == 1) + return operator[](0).as_expr(); + else { + array args(n); + for (unsigned i = 0; i < n; i++) + args[i] = operator[](i).as_expr(); + return expr(ctx(), Z3_mk_or(ctx(), n, args.ptr())); + } + } friend std::ostream & operator<<(std::ostream & out, apply_result const & r); }; inline std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; }