mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 05:49:13 +00:00
Code Activity

remove extra field in on_clause

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-01 08:53:08 -07:00
parent aae8242483
commit 863d0e3e5e
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4288,20 +4288,20 @@ namespace z3 {
return expr(ctx(), r); return expr(ctx(), r);
} }
typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause, unsigned const status)> on_clause_eh_t; typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause)> on_clause_eh_t;
class on_clause { class on_clause {
context& c; context& c;
on_clause_eh_t m_on_clause; on_clause_eh_t m_on_clause;
static void _on_clause_eh(void* _ctx, Z3_ast _proof, unsigned n, unsigned const* dep, Z3_ast_vector _literals, unsigned const status) { static void _on_clause_eh(void* _ctx, Z3_ast _proof, unsigned n, unsigned const* dep, Z3_ast_vector _literals) {
on_clause* ctx = static_cast<on_clause*>(_ctx); on_clause* ctx = static_cast<on_clause*>(_ctx);
expr_vector lits(ctx->c, _literals); expr_vector lits(ctx->c, _literals);
expr proof(ctx->c, _proof); expr proof(ctx->c, _proof);
std::vector<unsigned> deps; std::vector<unsigned> deps;
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
deps.push_back(dep[i]); deps.push_back(dep[i]);
ctx->m_on_clause(proof, deps, lits, status); ctx->m_on_clause(proof, deps, lits);
} }
public: public:
on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) { on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) {