z3_432.drv 2.07 KB
Newer Older
1 2 3 4 5 6
(** Why3 driver for Z3 >= 4.3.2 *)

(* Do not set any logic, let z3 choose by itself
   prelude "(set-logic AUFNIRA)"
*)

7 8
prelude ";; produced by z3_432.drv ;;"

David Hauzar's avatar
David Hauzar committed
9
(* Counterexamples: set model parser *)
10
model_parser "smtv2"
David Hauzar's avatar
David Hauzar committed
11

12
import "smt-libv2.gen"
13
printer "smtv2"
14
import "no-bv.gen"
15 16 17 18 19
import "discrimination.gen"

transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
20 21 22 23 24
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)
25
*)
26 27
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
Clément Fumex's avatar
Clément Fumex committed
28
transformation "eliminate_literal"
29 30 31 32 33
transformation "eliminate_epsilon"

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

34
(* Prepare for counter-example query: get rid of some quantifiers (makes it
35 36 37
possible to query model values of the variables in premises) and introduce
counter-example projections  *)
transformation "prepare_for_counterexmp"
38

39 40 41 42 43 44 45
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"


(** Error messages specific to Z3 *)

outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
46
steplimitexceeded "Maximal allocation counts .* have been exceeded\\|(error \".*number of configured allocations exceeded\")"
47 48 49 50 51 52
timeout "interrupted by timeout"

(** Extra theories supported by Z3 *)

(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
53 54 55 56 57 58
  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
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
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
*)