z3.drv 1.75 KB
Newer Older
1 2
(** Why3 driver for Z3 <= 4.3.1 *)

3
prelude ";; produced by z3.drv ;;"
4
prelude "(set-logic AUFNIRA)"
5 6 7
(* A  : Array
   UF : Uninterpreted Function
   NIRA : NonLinear Integer Reals Arithmetic
8 9
*)

10
import "smt-libv2.gen"
MARCHE Claude's avatar
MARCHE Claude committed
11
printer "smtv2"
12 13 14 15 16 17 18
import "discrimination.gen"

transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
19
transformation "eliminate_literal"
20 21 22 23 24 25 26 27 28 29 30
transformation "eliminate_epsilon"

transformation "simplify_formula"
(* transformation "simplify_trivial_quantification" *)

transformation "discriminate"
transformation "encoding_smt"

(** Error messages specific to Z3 *)

outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
31
steplimitexceeded "Maximal allocation counts .* have been exceeded\\|(error \".*number of configured allocations exceeded\")"
32
timeout "interrupted by timeout"
33
(* stop reporting Z3 2.19 warnings as errors *)
34
fail "^(error \"\\(\\(W\\(A\\(R\\(N\\(I\\(N[^G]\\|[^N]\\)\\|[^I]\\)\\|[^N]\\)\\|[^R]\\)\\|[^A]\\)\\|[^W]\\).*\\)\")" "Error: \\1"
35

36

37 38 39 40
(** Extra theories supported by Z3 *)

(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
Andrei Paskevich's avatar
Andrei Paskevich committed
41 42 43 44 45 46
  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
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
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
*)