(** 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.drv" import "smt-libv2-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_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 *) (* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't have the same name for the function to_uint *) theory bv.BV64 syntax converter of_int "((_ int2bv 64) %1)" syntax function to_uint "(bv2int %1)" remove prop Nth_bv_is_nth remove prop Nth_bv_is_nth2 end theory bv.BV32 syntax converter of_int "((_ int2bv 32) %1)" syntax function to_uint "(bv2int %1)" remove prop Nth_bv_is_nth remove prop Nth_bv_is_nth2 end theory bv.BV16 syntax converter of_int "((_ int2bv 16) %1)" syntax function to_uint "(bv2int %1)" remove prop Nth_bv_is_nth remove prop Nth_bv_is_nth2 end theory bv.BV8 syntax converter of_int "((_ int2bv 8) %1)" syntax function to_uint "(bv2int %1)" remove prop Nth_bv_is_nth remove prop Nth_bv_is_nth2 end