solver_propagate_declare method

Z3_func_decl solver_propagate_declare(
  1. Z3_context c,
  2. Z3_symbol name,
  3. int n,
  4. Pointer<Z3_sort> domain,
  5. Z3_sort range,
)

Create uninterpreted function declaration for the user propagator. When expressions using the function are created by the solver invoke a callback to \ref Z3_solver_propagate_created with arguments

  1. context and callback solve
  2. declared_expr: expression using function that was used as the top-level symbol
  3. declared_id: a unique identifier (unique within the current scope) to track the expression.

def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))

Implementation

Z3_func_decl solver_propagate_declare(
  Z3_context c,
  Z3_symbol name,
  int n,
  ffi.Pointer<Z3_sort> domain,
  Z3_sort range,
) {
  return _solver_propagate_declare(
    c,
    name,
    n,
    domain,
    range,
  );
}