z3_432.drv 1.4 KB
 MARCHE Claude committed Feb 19, 2015 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 ``````(** Why3 driver for Z3 >= 4.3.2 *) (* Do not set any logic, let z3 choose by itself prelude "(set-logic AUFNIRA)" *) import "smt-libv2.drv" import "discrimination.gen" transformation "inline_trivial" transformation "eliminate_builtin" transformation "detect_polymorphism" transformation "eliminate_definition_if_poly" transformation "eliminate_inductive" transformation "eliminate_algebraic_if_poly" transformation "eliminate_epsilon" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) 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 *)``````