z3-realize.drv 2.41 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 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
(** Why3 driver for Z3 >= 4.3.2 *)

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

(* Counterexamples: set model parser *)
model_parser "smtv2"


import "smt-libv2.drv"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"

transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
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)
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"

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

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

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
Andrei Paskevich's avatar
Andrei Paskevich committed
49 50 51 52 53 54
  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
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
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
*)


(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
   have the same name for the function to_uint *)
theory bv.BV64
  syntax converter of_int "((_ int2bv 64) %1)"
  syntax function to_uint "(bv2int %1)"
end

theory bv.BV32
  syntax converter of_int "((_ int2bv 32) %1)"
  syntax function to_uint "(bv2int %1)"
end

theory bv.BV16
  syntax converter of_int "((_ int2bv 16) %1)"
  syntax function to_uint "(bv2int %1)"
end

theory bv.BV8
  syntax converter of_int "((_ int2bv 8) %1)"
  syntax function to_uint "(bv2int %1)"
end