Z3
Public Member Functions
on_clause Class Reference

Public Member Functions

 on_clause (solver &s, on_clause_eh_t &on_clause_eh)
 

Detailed Description

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

Constructor & Destructor Documentation

◆ on_clause()

on_clause ( solver s,
on_clause_eh_t on_clause_eh 
)
inline

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

4115  : c(s.ctx()) {
4116  m_on_clause = on_clause_eh;
4117  Z3_solver_register_on_clause(c, s, this, _on_clause_eh);
4118  c.check_error();
4119  }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:190
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.
def on_clause_eh(ctx, p, clause)
Definition: z3py.py:11350