z3_432.drv 3.21 KB
Newer Older
1 2 3 4 5 6 7
(** 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"
8
import "smt-libv2-bv.gen"
9 10 11 12
import "discrimination.gen"

transformation "inline_trivial"
transformation "eliminate_builtin"
13
(* temporarily disabled: too much experimental
14
transformation "detect_polymorphism"
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 63 64 65
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
*)
66 67 68


(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
69 70
   have the same name for the function to_uint *)
theory bv.BV64
71
  syntax converter of_int "((_ int2bv 64) %1)"
72 73 74 75
  syntax function to_uint "(bv2int %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds
76

77 78 79 80 81 82 83 84
  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
85 86
end

87
theory bv.BV32
88
  syntax converter of_int "((_ int2bv 32) %1)"
89 90 91 92
  syntax function to_uint "(bv2int %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds
93

94 95 96 97 98 99 100 101
  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
102 103
end

104
theory bv.BV16
105
  syntax converter of_int "((_ int2bv 16) %1)"
106 107 108 109
  syntax function to_uint "(bv2int %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds
110

111 112 113 114 115 116 117 118
  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
119 120
end

121
theory bv.BV8
122
  syntax converter of_int "((_ int2bv 8) %1)"
123 124 125 126
  syntax function to_uint "(bv2int %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds
127

128 129 130 131 132 133 134 135
  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
136
end