alt_ergo_smt2.drv 2.64 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(* Why driver for Alt-Ergo with SMT-lib2 input format *)

prelude ";;; this is a prelude for Alt-Ergo"

printer "smtv2"
filename "%f-%t-%g.smt2"

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

12
(*transformation "simplify_recursive_definition"*)
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
transformation "inline_trivial"

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

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

theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
28 29

  syntax predicate (=)  "(= %1 %2)"
30 31 32 33 34 35 36 37

  meta "encoding : kept" type int
end

theory int.Int

  prelude ";;; this is a prelude for Alt-Ergo integer arithmetic"

38 39
  syntax function zero "0"
  syntax function one  "1"
40

41 42 43 44
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
  syntax function (-_) "(- %1)"
45

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

  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 Total
  remove prop Antisymm
  remove prop NonTrivialRing
  remove prop CompatOrderAdd

end

theory int.EuclideanDivision

70 71
  syntax function div "(div %1 %2)"
  syntax function mod "(mod %1 %2)"
72 73 74 75 76 77 78

end

theory real.Real

  prelude ";;; this is a prelude for Alt-Ergo real arithmetic"

79 80
  syntax function zero "0.0"
  syntax function one  "1.0"
81

82 83 84 85 86 87
  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)"
88

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

  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 Total
  remove prop Antisymm
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd

end


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