Z3
 
Loading...
Searching...
No Matches
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 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