psyche.drv 2.13 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 49 50 51 52
(* Why driver for Psyche *)

prelude "(set-logic FO)"

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

valid "^PROVABLE"
invalid "^NOT PROVABLE"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"

(* À discuter *)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"

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

transformation "discriminate"
transformation "encoding_smt"

theory BuiltIn
  syntax type real  "Real"
  syntax predicate (=)  "(= %1 %2)"
  meta "eliminate_algebraic" "no_index"
end

theory real.Real

  prelude ";;; this is a prelude for smt-lib v2 real arithmetic"

  syntax function zero "0"
  syntax function one  "1"

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function ( * )  "(* %1 %2)"
  syntax function (/)  "(/ %1 %2)"
  syntax function (-_) "(- %1)"
  syntax function inv  "(/ 1 %1)"

  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"

Andrei Paskevich's avatar
Andrei Paskevich committed
53 54 55 56 57 58 59
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
60 61
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
62
  remove prop Comm
63 64 65 66 67 68 69 70 71 72
  remove prop Unitary
  remove prop Inverse
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

73
  meta "encoding:kept" type real
74 75 76 77 78

end

(*
theory Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
79 80 81 82
  syntax type     bool  "Bool"
  syntax function True  "true"
  syntax function False "false"
  meta "encoding:kept" type bool
83 84 85
end

theory bool.Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
86 87 88 89 90
  syntax function andb  "(and %1 %2)"
  syntax function orb   "(or %1 %2)"
  syntax function xorb  "(xor %1 %2)"
  syntax function notb  "(not %1)"
  syntax function implb "(=> %1 %2)"
91 92 93 94
end

theory bool.Ite
  syntax function ite "(ite %1 %2 %3)"
95
  meta "encoding:lskept" function ite
96 97 98 99
end
*)

import "discrimination.gen"