From 2e89c2de3d3eafcc45cd1539642dda1e9c2d0ee7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2017 09:35:04 -0800 Subject: [PATCH] add par_or tactic to C++ API. #873 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 979d9aed7..37e6448c9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1933,6 +1933,7 @@ namespace z3 { friend tactic repeat(tactic const & t, unsigned max); friend tactic with(tactic const & t, params const & p); friend tactic try_for(tactic const & t, unsigned ms); + friend tactic par_or(unsigned n, tactic const* tactics); param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); } }; @@ -1966,7 +1967,14 @@ namespace z3 { t.check_error(); return tactic(t.ctx(), r); } - + inline tactic par_or(unsigned n, tactic const* tactics) { + if (n == 0) { + throw exception("a non-zero number of tactics need to be passed to par_or"); + } + array buffer(n); + for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i]; + return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr())); + } class probe : public object { Z3_probe m_probe;