verit.drv 3.11 KB
Newer Older
MARCHE Claude's avatar
docs  
MARCHE Claude committed
1 2 3 4 5 6 7 8 9
(* Why driver for SMT syntax *)

prelude ";;; this is a prelude for veriT"

printer "smtv1"
filename "%f-%t-%g.smt"

valid "^unsat"
unknown "^\\(unknown\\|sat\\)" "Unknown"
10
time "why3cpulimit time : %s s"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
11 12

(* À discuter *)
13
(*transformation "simplify_recursive_definition"*)
MARCHE Claude's avatar
docs  
MARCHE Claude committed
14 15 16 17 18
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
19
transformation "eliminate_algebraic_smt"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
20 21

transformation "simplify_formula"
22
(*transformation "simplify_trivial_quantification"*)
MARCHE Claude's avatar
docs  
MARCHE Claude committed
23 24

transformation "encoding_smt"
25
transformation "encoding_sort"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
26 27 28 29

theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
30
  syntax predicate (=)  "(= %1 %2)"
31 32

  meta "encoding : kept" type int
MARCHE Claude's avatar
docs  
MARCHE Claude committed
33 34 35 36 37 38
end

theory int.Int

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

39 40
  syntax function zero "0"
  syntax function one  "1"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
41

42 43 44 45
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
  syntax function (-_) "(- %1)"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
46

47 48 49 50
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65

  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
Andrei Paskevich's avatar
Andrei Paskevich committed
66
  remove prop ZeroLessOne
MARCHE Claude's avatar
docs  
MARCHE Claude committed
67 68 69 70 71 72 73 74

end


theory real.Real

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

75 76
  syntax function zero "0.0"
  syntax function one  "1.0"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
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)"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
84

85 86 87 88
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104

  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
Andrei Paskevich's avatar
Andrei Paskevich committed
105
  remove prop ZeroLessOne
MARCHE Claude's avatar
docs  
MARCHE Claude committed
106 107 108 109 110

  meta "encoding : kept" type real

end

111
theory Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
112
   syntax type bool      "bool"
113 114
   syntax function True  "true"
   syntax function False "false"
115 116 117 118
   meta "encoding : kept" type bool
end

theory bool.Bool
119 120 121 122
   syntax function andb  "(and %1 %2)"
   syntax function orb   "(or %1 %2)"
   syntax function xorb  "(xor %1 %2)"
   syntax function notb  "(not %1)"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
123 124 125 126
end


theory int.EuclideanDivision
127 128
   syntax function div "(div %1 %2)"
   syntax function mod "(mod %1 %2)"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
129 130 131 132 133 134 135 136 137 138 139 140
   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:
*)