mk_tactic method

Z3_tactic mk_tactic(
  1. Z3_context c,
  2. Z3_string name
)

@name Tactics, Simplifiers and Probes / /**@{/ /** \brief Return a tactic associated with the given name. The complete list of tactics may be obtained using the procedures #Z3_get_num_tactics and #Z3_get_tactic_name. It may also be obtained using the command \ccode{(help-tactic)} in the SMT 2.0 front-end.

Tactics are the basic building block for creating custom solvers for specific problem domains.

def_API('Z3_mk_tactic', TACTIC, (_in(CONTEXT), _in(STRING)))

Implementation

Z3_tactic mk_tactic(
  Z3_context c,
  Z3_string name,
) {
  return _mk_tactic(
    c,
    name,
  );
}