drivers/z3.drv

   1 (** Why3 driver for Z3 <= 4.3.1 *)
   2
   3 prelude ";; produced by z3.drv ;;"
   4 prelude "(set-logic AUFNIRA)"
   5 (* A  : Array
   6    UF : Uninterpreted Function
   7    NIRA : NonLinear Integer Reals Arithmetic
   8 *)
   9
  10 import "smt-libv2.gen"
  11 filename "%f-%t-%g.smt2"
  12 printer "smtv2"
  13 import "discrimination.gen"
  14
  15 (* Performed introductions depending on whether counterexamples are
  16    requested, as said by the meta "get_counterexmp". When this meta
  17    set, this transformation introduces the model variables that are
  18    still embedded in the goal. When it is not set, it removes all
  19    these unused-ce-related variables, even in the context.  *)
  20 transformation "counterexamples_dependent_intros"
  21
  22 transformation "inline_trivial"
  23 transformation "eliminate_builtin"
  24 transformation "eliminate_definition"
  25 transformation "eliminate_inductive"
  26 transformation "eliminate_epsilon"
  27 transformation "eliminate_algebraic"
  28 transformation "eliminate_literal"
  29
  30 transformation "simplify_formula"
  31 (* transformation "simplify_trivial_quantification" *)
  32
  33 transformation "discriminate"
  34 transformation "encoding_smt"
  35
  36 (** Error messages specific to Z3 *)
  37
  38 outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
  39 steplimitexceeded "Maximal allocation counts .* have been exceeded\\|(error \".*number of configured allocations exceeded\")"
  40 timeout "interrupted by timeout"
  41 (* stop reporting Z3 2.19 warnings as errors *)
  42 fail "^(error \"\\(\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\).*\\)\")" "Error: \\1"
  43
  44
  45 (** Extra theories supported by Z3 *)
  46
  47 (* div/mod of Z3 seems to be Euclidean Division *)
  48 theory int.EuclideanDivision
  49   syntax function div "(div %1 %2)"
  50   syntax function mod "(mod %1 %2)"
  51   remove prop Mod_bound
  52   remove prop Div_mod
  53   remove prop Mod_1
  54   remove prop Div_1
  55 end
  56
  57 theory real.FromInt
  58   syntax function from_int "(to_real %1)"
  59   remove prop Zero
  60   remove prop One
  61   remove prop Add
  62   remove prop Sub
  63   remove prop Mul
  64   remove prop Neg
  65 end
  66
  67 (* does not work: Z3 segfaults
  68 theory real.Trigonometry
  69
  70   syntax function cos "(cos %1)"
  71   syntax function sin "(sin %1)"
  72   syntax function pi "pi"
  73   syntax function tan "(tan %1)"
  74   syntax function atan "(atan %1)"
  75
  76 end
  77 *)