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

add par_or tactic to C++ API. #873

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-02 09:35:04 -08:00
parent 9cfd412cd0
commit 2e89c2de3d
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1933,6 +1933,7 @@ namespace z3 {
friend tactic repeat(tactic const & t, unsigned max); friend tactic repeat(tactic const & t, unsigned max);
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);
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)); }
}; };
@ -1966,7 +1967,14 @@ namespace z3 {
t.check_error(); t.check_error();
return tactic(t.ctx(), r); 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<Z3_tactic> 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 { class probe : public object {
Z3_probe m_probe; Z3_probe m_probe;