pub type Z3_tactic = *mut _Z3_tactic;
Basic building block for creating custom solvers for specific problem domains.