From e7a21dfac21c6f34576a7475b520695e5b5fb9fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Feb 2017 08:16:39 -0800 Subject: [PATCH] add par_and_then Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 37e6448c9..e655815ca 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1934,6 +1934,7 @@ namespace z3 { 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); + friend tactic par_and_then(tactic const& t1, tactic const& t2); param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); } }; @@ -1976,6 +1977,13 @@ namespace z3 { return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr())); } + inline tactic par_and_then(tactic const & t1, tactic const & t2) { + check_context(t1, t2); + Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2); + t1.check_error(); + return tactic(t1.ctx(), r); + } + class probe : public object { Z3_probe m_probe; void init(Z3_probe s) {