solver_propagate_consequence method

bool solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, int num_fixed, Pointer<Z3_ast> fixed, int num_eqs, Pointer<Z3_ast> eq_lhs, Pointer<Z3_ast> eq_rhs, Z3_ast conseq,)

\brief propagate a consequence based on fixed values. This is a callback a client may invoke during the fixed_eh callback. The callback adds a propagation consequence based on the fixed values of the \c ids. The solver might discard the propagation in case it is true in the current state. The function returns false in this case; otw. the function returns true. At least one propagation in the final callback has to return true in order to prevent the solver from finishing.

def_API('Z3_solver_propagate_consequence', BOOL, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, AST), _in(UINT), _in_array(4, AST), _in_array(4, AST), _in(AST)))

Implementation

bool solver_propagate_consequence(
  Z3_context c,
  Z3_solver_callback cb,
  int num_fixed,
  ffi.Pointer<Z3_ast> fixed,
  int num_eqs,
  ffi.Pointer<Z3_ast> eq_lhs,
  ffi.Pointer<Z3_ast> eq_rhs,
  Z3_ast conseq,
) {
  return _solver_propagate_consequence(
    c,
    cb,
    num_fixed,
    fixed,
    num_eqs,
    eq_lhs,
    eq_rhs,
    conseq,
  );
}