Skip to main content

Z3_mk_simplifier

Function Z3_mk_simplifier 

Source
pub unsafe extern "C" fn Z3_mk_simplifier(
    c: Z3_context,
    name: Z3_string,
) -> Option<Z3_simplifier>
Expand description

Return a simplifier associated with the given name. The complete list of simplifiers may be obtained using the procedures Z3_get_num_simplifiers and Z3_get_simplifier_name. It may also be obtained using the command (help-simplifier) in the SMT 2.0 front-end.

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