solver_get_consequences method

int solver_get_consequences(
  1. Z3_context c,
  2. Z3_solver s,
  3. Z3_ast_vector assumptions,
  4. Z3_ast_vector variables,
  5. Z3_ast_vector consequences,
)

\brief retrieve consequences from solver that determine values of the supplied function symbols.

def_API('Z3_solver_get_consequences', LBOOL, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR), _in(AST_VECTOR)))

Implementation

int solver_get_consequences(
  Z3_context c,
  Z3_solver s,
  Z3_ast_vector assumptions,
  Z3_ast_vector variables,
  Z3_ast_vector consequences,
) {
  return _solver_get_consequences(
    c,
    s,
    assumptions,
    variables,
    consequences,
  );
}