Z3
Loading...
Searching...
No Matches
z3
on_clause
Public Member Functions
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
4319
of file
z3++.h
.
Constructor & Destructor Documentation
◆
on_clause()
on_clause
(
solver
&
s
,
on_clause_eh_t
&
on_clause_eh
)
inline
Definition at line
4333
of file
z3++.h
.
4333
: c(s.ctx()) {
4334
m_on_clause =
on_clause_eh
;
4335
Z3_solver_register_on_clause
(c, s,
this
, _on_clause_eh);
4336
c.
check_error
();
4337
}
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition
z3++.h:192
Z3_solver_register_on_clause
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.
z3py.on_clause_eh
on_clause_eh(ctx, p, n, dep, clause)
Definition
z3py.py:11708
Generated on Sat Dec 20 2025 19:33:22 for Z3 by
1.9.8