drivers/z3_432.drv

   1 (** Why3 driver for Z3 >= 4.3.2 *)
   2
   3 (* Do not set any logic, let z3 choose by itself
   4    prelude "(set-logic AUFNIRA)"
   5 *)
   6
   7 prelude ";; produced by z3_432.drv ;;"
   8
   9 (* Counterexamples: set model parser *)
  10 model_parser "smtv2"
  11
  12 import "smt-libv2.gen"
  13 filename "%f-%t-%g.smt2"
  14 printer "smtv2"
  15 import "no-bv.gen"
  16 import "discrimination.gen"
  17
  18 (* Performed introductions depending on whether counterexamples are
  19    requested, as said by the meta "get_counterexmp". When this meta
  20    set, this transformation introduces the model variables that are
  21    still embedded in the goal. When it is not set, it removes all
  22    these unused-ce-related variables, even in the context.  *)
  23 transformation "counterexamples_dependent_intros"
  24
  25 transformation "inline_trivial"
  26 transformation "eliminate_builtin"
  27 transformation "detect_polymorphism"
  28 transformation "eliminate_definition"
  29 (* We could keep more definitions by using
  30    transformation "eliminate_definition_conditionally"
  31    instead, but some proofs are lost
  32    (examples/logic/triangle_inequality.why)
  33 *)
  34 transformation "eliminate_inductive"
  35 transformation "eliminate_epsilon"
  36 transformation "eliminate_algebraic_if_poly"
  37 transformation "eliminate_literal"
  38
  39 transformation "simplify_formula"
  40 (*transformation "simplify_trivial_quantification"*)
  41
  42 (* Prepare for counter-example query: get rid of some quantifiers (makes it
  43 possible to query model values of the variables in premises) and introduce
  44 counter-example projections  *)
  45 transformation "prepare_for_counterexmp"
  46
  47 transformation "discriminate_if_poly"
  48 transformation "encoding_smt_if_poly"
  49
  50
  51 (** Error messages specific to Z3 *)
  52
  53 outofmemory "(error \".*out of memory\")"
  54 outofmemory "Failed to verify: pthread_create"
  55 outofmemory "std::bad_alloc"
  56 outofmemory "Resource temporarily unavailable"
  57 outofmemory "Cannot allocate memory"
  58 steplimitexceeded "Maximal allocation counts .* have been exceeded"
  59 steplimitexceeded "(error \".*number of configured allocations exceeded\")"
  60 timeout "^timeout$"
  61 timeout "interrupted by timeout"
  62
  63 (** Extra theories supported by Z3 *)
  64
  65 (* div/mod of Z3 seems to be Euclidean Division *)
  66 theory int.EuclideanDivision
  67   syntax function div "(div %1 %2)"
  68   syntax function mod "(mod %1 %2)"
  69   remove prop Mod_bound
  70   remove prop Div_mod
  71   remove prop Mod_1
  72   remove prop Div_1
  73 end
  74
  75 theory real.FromInt
  76   syntax function from_int "(to_real %1)"
  77   remove prop Zero
  78   remove prop One
  79   remove prop Add
  80   remove prop Sub
  81   remove prop Mul
  82   remove prop Neg
  83 end
  84
  85 (* does not work: Z3 segfaults
  86 theory real.Trigonometry
  87
  88   syntax function cos "(cos %1)"
  89   syntax function sin "(sin %1)"
  90   syntax function pi "pi"
  91   syntax function tan "(tan %1)"
  92   syntax function atan "(atan %1)"
  93
  94 end
  95 *)