drivers/vampire_4_5_1.drv

   1 (* Why driver for Vampire *)
   2
   3 valid   "Refutation found"
   4 unknown "Time limit reached" "Time out"
   5 unknown "Refutation not found" ""
   6 outofmemory "Memory limit exceeded"
   7
   8 import "smt-libv2.gen"
   9 filename "%f-%t-%g.smt2"
  10 printer "smtv2.6"
  11
  12 import "discrimination.gen"
  13 theory BuiltIn
  14   meta "select_alginst_default" "local"
  15   meta "eliminate_algebraic" "keep_mono"
  16 end
  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 transformation "eliminate_builtin"
  27 transformation "detect_polymorphism"
  28 transformation "eliminate_definition_conditionally"
  29 transformation "eliminate_inductive"
  30 transformation "eliminate_epsilon"
  31 transformation "eliminate_literal"
  32
  33 transformation "simplify_formula"
  34
  35 transformation "eliminate_projections_sums"
  36 transformation "discriminate_if_poly"
  37 transformation "eliminate_algebraic_if_poly"
  38 transformation "encoding_smt_if_poly"