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 4437 of file z3++.h.

Constructor & Destructor Documentation

◆ on_clause()

on_clause ( solver s,
on_clause_eh_t on_clause_eh 
)
inline

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

4451 : c(s.ctx()) {
4452 m_on_clause = on_clause_eh;
4453 Z3_solver_register_on_clause(c, s, this, _on_clause_eh);
4454 c.check_error();
4455 }
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition z3++.h:222
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:11752