z3_smtv1.drv 3.14 KB
Newer Older
1 2 3 4
(* Why driver for SMT syntax *)

prelude ";;; this is a prelude for Z3"

Andrei Paskevich's avatar
Andrei Paskevich committed
5
printer "smtv1"
6 7 8 9 10 11 12 13
filename "%f-%t-%g.smt"

valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
time "why3cpulimit time : %s s"


(* À discuter *)
14
(*transformation "simplify_recursive_definition"*)
15 16 17 18 19 20 21 22 23
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"

transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
Andrei Paskevich's avatar
Andrei Paskevich committed
24

25
transformation "encoding_smt"
Andrei Paskevich's avatar
Andrei Paskevich committed
26
transformation "encoding_sort"
27 28 29 30

theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
31
  syntax predicate (=)  "(= %1 %2)"
32 33 34 35 36 37 38 39

  meta "encoding : kept" type int
end

theory int.Int

  prelude ";;; this is a prelude for Z3 integer arithmetic"

40 41
  syntax function zero "0"
  syntax function one  "1"
42

43 44 45 46
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
  syntax function (-_) "(- %1)"
47

48 49 50 51
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd

end


theory real.Real

  prelude ";;; this is a prelude for Z3 real arithmetic"

75 76
  syntax function zero "0.0"
  syntax function one  "1.0"
77

78 79 80 81 82 83
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
  syntax function (/)  "(/ %1 %2)"
  syntax function (-_) "(- %1)"
  syntax function inv  "(/ 1.0 %1)"
84

85 86 87 88
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Inverse
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd

  meta "encoding : kept" type real

end

(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
   syntax type bool   "bool"
114 115 116 117 118 119
   syntax function True  "true"
   syntax function False "false"
   syntax function andb  "(and %1 %2)"
   syntax function orb   "(or %1 %2)"
   syntax function xorb  "(xor %1 %2)"
   syntax function notb  "(not %1)"
120 121 122 123 124 125
   meta cloned "encoding_decorate : kept" type bool
end
*)


theory int.EuclideanDivision
126 127
   syntax function div "(div %1 %2)"
   syntax function mod "(mod %1 %2)"
128 129 130 131 132 133 134 135 136 137 138 139
   remove prop Mod_bound
   remove prop Div_mod
   remove prop Mod_1
   remove prop Div_1
end

(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)