spass_types.drv 809 Bytes
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
(* Why driver for SPASS with types (>= 3.8) *)

printer "dfg"
filename "%f-%t-%g.dfg"

valid   "Proof found"
invalid "Completion found"
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
fail    "Failure.*" "\"\\0\""

time "why3cpulimit time : %s s"

(* to be improved *)

transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
24
transformation "eliminate_literal"
25
transformation "eliminate_epsilon"
26 27 28
transformation "eliminate_if"
transformation "eliminate_let"

29 30
transformation "discriminate"

31 32 33 34 35
theory BuiltIn
  syntax predicate (=)  "equal(%1, %2)"
  meta "eliminate_algebraic" "no_index"
end

36
import "discrimination.gen"