mk_goal method

Z3_goal mk_goal(
  1. Z3_context c,
  2. bool models,
  3. bool unsat_cores,
  4. bool proofs,
)

@name Goals / /**@{/ /** \brief Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

If \c models is \c true, then model generation is enabled for the new goal.

If \c unsat_cores is \c true, then unsat core generation is enabled for the new goal.

If \c proofs is \c true, then proof generation is enabled for the new goal. Remark, the Z3 context \c c must have been created with proof generation support.

\remark Reference counting must be used to manage goals, even when the \c Z3_context was created using #Z3_mk_context instead of #Z3_mk_context_rc.

def_API('Z3_mk_goal', GOAL, (_in(CONTEXT), _in(BOOL), _in(BOOL), _in(BOOL)))

Implementation

Z3_goal mk_goal(
  Z3_context c,
  bool models,
  bool unsat_cores,
  bool proofs,
) {
  return _mk_goal(
    c,
    models,
    unsat_cores,
    proofs,
  );
}