drivers/spass_types.drv

   1 (* Why driver for SPASS with types (>= 3.8) *)
   2
   3 printer "dfg"
   4 filename "%f-%t-%g.dfg"
   5
   6 valid   "Proof found"
   7 invalid "Completion found"
   8 timeout "Ran out of time"
   9 timeout "CPU time limit exceeded"
  10 outofmemory "Out of Memory"
  11 unknown "No Proof Found" ""
  12 fail    "Failure.*" "\"\\0\""
  13
  14 time "why3cpulimit time : %s s"
  15
  16 (* to be improved *)
  17
  18 (* Performed introductions depending on whether counterexamples are
  19    requested, as said by the meta "get_counterexmp". When this meta
  20    set, this transformation introduces the model variables that are
  21    still embedded in the goal. When it is not set, it removes all
  22    these unused-ce-related variables, even in the context.  *)
  23 transformation "counterexamples_dependent_intros"
  24
  25 transformation "inline_trivial"
  26
  27 transformation "eliminate_builtin"
  28 transformation "eliminate_definition"
  29 transformation "eliminate_inductive"
  30 transformation "eliminate_if"
  31 transformation "eliminate_epsilon"
  32 transformation "eliminate_algebraic"
  33 transformation "eliminate_literal"
  34 transformation "eliminate_let"
  35
  36 transformation "discriminate"
  37
  38 theory BuiltIn
  39   syntax predicate (=)  "equal(%1, %2)"
  40   meta "eliminate_algebraic" "no_index"
  41 end
  42
  43 import "discrimination.gen"