(** Why3 driver for Z3 >= 4.3.2 *) (* Do not set any logic, let z3 choose by itself prelude "(set-logic AUFNIRA)" *) (* Counterexamples: set model parser *) model_parser "smtv2" import "smt-libv2.gen" printer "smtv2" import "no-bv.gen" import "discrimination.gen" transformation "inline_trivial" transformation "eliminate_builtin" transformation "detect_polymorphism" transformation "eliminate_definition" (* We could keep more definitions by using transformation "eliminate_definition_if_poly" instead, but some proofs are lost (examples/logic/triangle_inequality.why) *) transformation "eliminate_inductive" transformation "eliminate_algebraic_if_poly" transformation "eliminate_literal" transformation "eliminate_epsilon" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) (* Prepare for counter-example query: get rid of some quantifiers (makes it possible to query model values of the variables in premises) and introduce counter-example projections *) transformation "prepare_for_counterexmp" transformation "discriminate_if_poly" transformation "encoding_smt_if_poly" (** Error messages specific to Z3 *) outofmemory "(error \".*out of memory\")\\|Cannot allocate memory" timeout "interrupted by timeout" (** Extra theories supported by Z3 *) (* div/mod of Z3 seems to be Euclidean Division *) theory int.EuclideanDivision syntax function div "(div %1 %2)" syntax function mod "(mod %1 %2)" remove prop Mod_bound remove prop Div_mod remove prop Mod_1 remove prop Div_1 end theory real.FromInt syntax function from_int "(to_real %1)" remove prop Zero remove prop One remove prop Add remove prop Sub remove prop Mul remove prop Neg end (* does not work: Z3 segfaults theory real.Trigonometry syntax function cos "(cos %1)" syntax function sin "(sin %1)" syntax function pi "pi" syntax function tan "(tan %1)" syntax function atan "(atan %1)" end *)