drivers/verit.drv

   1 (* Why3 driver for veriT solver *)
   2
   3 prelude ";;; this is a prelude for veriT"
   4 prelude "(set-logic AUFLIRA)"
   5 (* A  : Array
   6    UF : Uninterpreted Function
   7    LIRA : Linear Integer Reals Arithmetic
   8 *)
   9
  10 import "smt-libv2.gen"
  11 filename "%f-%t-%g.smt2"
  12 printer "smtv2"
  13 import "discrimination.gen"
  14
  15 (* specific message from veriT 201310 *)
  16 unknown "non-linear reasoning desactivated" ""
  17 (* specific message from veriT 201410 *)
  18 unknown "error : Non linear expression with non-linear reasoning disabled" ""
  19
  20 (* Performed introductions depending on whether counterexamples are
  21    requested, as said by the meta "get_counterexmp". When this meta
  22    set, this transformation introduces the model variables that are
  23    still embedded in the goal. When it is not set, it removes all
  24    these unused-ce-related variables, even in the context.  *)
  25 transformation "counterexamples_dependent_intros"
  26
  27 transformation "inline_trivial"
  28
  29 transformation "eliminate_builtin"
  30 transformation "eliminate_definition"
  31 transformation "eliminate_inductive"
  32 transformation "eliminate_epsilon"
  33 transformation "eliminate_algebraic"
  34 transformation "eliminate_literal"
  35
  36 transformation "simplify_formula"
  37 (*transformation "simplify_trivial_quantification"*)
  38
  39 transformation "encoding_smt"
  40 transformation "encoding_sort"
  41
  42 (*
  43 disabled: veriT seems more efficient with the axiomatic version
  44 theory int.EuclideanDivision
  45   syntax function div "(div %1 %2)"
  46   syntax function mod "(mod %1 %2)"
  47   remove prop Mod_bound
  48   remove prop Div_mod
  49   remove prop Mod_1
  50   remove prop Div_1
  51 end
  52 *)