drivers/alt_ergo_smt.drv

   1 (* Why3 driver for Alt-Ergo with SMT-lib V2 input format, including polymorphism *)
   2
   3 prelude ";;; this is a prelude for Alt-Ergo, Dolmen frontend"
   4 prelude "(set-logic ALL)"
   5 prelude "(set-info :smt-lib-version 2.6)"
   6
   7 import "smt-libv2.gen"
   8 filename "%f-%t-%g.psmt2"
   9 printer "smtv2.6par"
  10
  11 valid "^; File \".*\", line [0-9]+, characters [0-9]+-[0-9]+: ?Valid"
  12 unknown "^; File \".*\", line [0-9]+, characters [0-9]+-[0-9]+: ?I don't know" ""
  13 steplimitexceeded "^\\[Error\\]; Fatal Error: Steps limit reached"
  14
  15 steps "^; File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:.*(\\([0-9]+.?[0-9]*\\) steps)" 1
  16 steps "^\\[Error\\]; Fatal Error: Steps limit reached: \\([0-9]+.?[0-9]*\\)" 1
  17
  18 (* valid "^unsat" *)
  19 (* unknown "^\\(unknown\\|sat\\|Fail\\)" "" *)
  20 time "why3cpulimit time : %s s"
  21
  22 (* Performed introductions depending on whether counterexamples are
  23    requested, as said by the meta "get_counterexmp". When this meta
  24    set, this transformation introduces the model variables that are
  25    still embedded in the goal. When it is not set, it removes all
  26    these unused-ce-related variables, even in the context.  *)
  27 transformation "counterexamples_dependent_intros"
  28
  29 transformation "monomorphise_goal"
  30 transformation "inline_trivial"
  31 transformation "eliminate_builtin"
  32 transformation "remove_unused_keep_constants"
  33 transformation "eliminate_recursion"
  34 transformation "eliminate_inductive"
  35 transformation "eliminate_epsilon"
  36 transformation "eliminate_algebraic"
  37 transformation "eliminate_literal"
  38 transformation "split_premise_right"
  39 transformation "simplify_formula"
  40
  41
  42 theory BuiltIn
  43
  44   meta "eliminate_algebraic" "keep_enums"
  45   meta "eliminate_algebraic" "keep_recs"
  46
  47 end