Z3
 
Loading...
Searching...
No Matches
on_clause Class Reference

#include <z3++.h>

Public Member Functions

 on_clause (solver &s, on_clause_eh_t &on_clause_eh)
 

Detailed Description

Definition at line 4270 of file z3++.h.

Constructor & Destructor Documentation

◆ on_clause()

on_clause ( solver & s,
on_clause_eh_t & on_clause_eh )
inline

Definition at line 4284 of file z3++.h.

4284 : c(s.ctx()) {
4285 m_on_clause = on_clause_eh;
4286 Z3_solver_register_on_clause(c, s, this, _on_clause_eh);
4287 c.check_error();
4288 }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition z3++.h:192
void Z3_API Z3_solver_register_on_clause(Z3_context c, Z3_solver s, void *user_context, Z3_on_clause_eh on_clause_eh)
register a callback to that retrieves assumed, inferred and deleted clauses during search.
on_clause_eh(ctx, p, n, dep, clause)
Definition z3py.py:11523