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
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::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:11523
Generated by
1.12.0