zenon.drv 847 Bytes
Newer Older
1 2 3 4 5 6
(* Why driver for first-order tptp provers *)

printer "tptp-fof"
filename "%f-%t-%g.p"

valid   "PROOF-FOUND"
7 8 9
timeout "Zenon error: could not find a proof within the time limit"
outofmemory "Zenon error: could not find a proof within the memory size limit"
unknown "NO-PROOF" "no proof found"
10 11 12 13 14 15 16 17 18 19
time "why3cpulimit time : %s s"

(* to be improved *)

transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
20
transformation "eliminate_literal"
21
transformation "eliminate_if"
Quentin Garchery's avatar
Quentin Garchery committed
22
transformation "eliminate_epsilon"
23 24
transformation "eliminate_let"

25
transformation "discriminate"
26 27 28 29 30 31 32
transformation "encoding_tptp"

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

33
import "discrimination.gen"