mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

add par_and_then

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-13 08:16:39 -08:00
parent 999d17e29b
commit e7a21dfac2
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/c++/z3++.h
View file

@ -1934,6 +1934,7 @@ namespace z3 {
friend tactic with(tactic const & t, params const & p); friend tactic with(tactic const & t, params const & p);
friend tactic try_for(tactic const & t, unsigned ms); friend tactic try_for(tactic const & t, unsigned ms);
friend tactic par_or(unsigned n, tactic const* tactics); 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)); } 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())); 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 { class probe : public object {
Z3_probe m_probe; Z3_probe m_probe;
void init(Z3_probe s) { void init(Z3_probe s) {