Function z3_sys::Z3_mk_tactic[][src]

pub unsafe extern "C" fn Z3_mk_tactic(
    c: Z3_context,
    name: Z3_string
) -> Z3_tactic
Expand description

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 (help-tactic) in the SMT 2.0 front-end.

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