drivers/simplify.drv

   1 (* Why driver for Simplify *)
   2
   3 prelude ";;; this is a prelude for Simplify"
   4
   5 printer "simplify"
   6 filename "%f-%t-%g.sx"
   7
   8 valid "\\bValid\\b"
   9 unknown "\\bInvalid\\b" ""
  10 time "why3cpulimit time : %s s"
  11
  12 (* Performed introductions depending on whether counterexamples are
  13    requested, as said by the meta "get_counterexmp". When this meta
  14    set, this transformation introduces the model variables that are
  15    still embedded in the goal. When it is not set, it removes all
  16    these unused-ce-related variables, even in the context.  *)
  17 transformation "counterexamples_dependent_intros"
  18
  19 transformation "inline_trivial"
  20 transformation "eliminate_builtin"
  21 transformation "eliminate_definition" (*_func*)
  22 transformation "eliminate_inductive"
  23 transformation "eliminate_if"
  24 transformation "eliminate_epsilon"
  25 transformation "eliminate_algebraic"
  26 transformation "eliminate_literal"
  27 transformation "eliminate_let"
  28
  29 transformation "simplify_formula"
  30 (*transformation "simplify_trivial_quantification"*)
  31
  32 transformation "remove_triggers"
  33 (*transformation "filter_trigger_no_predicate"*)
  34 (* predicate are *currently* translated to P(\x) = true, thus in a
  35 trigger they can't appear since = can't appear *)
  36 (*transformation "filter_trigger_builtin"*)
  37
  38 (* this is sound as long as int is the only kept type *)
  39 transformation "encoding_tptp"
  40
  41 theory BuiltIn
  42   syntax predicate (=)  "(EQ %1 %2)"
  43
  44   meta "encoding:base" type int
  45 end
  46
  47 theory int.Int
  48
  49   prelude ";;; this is a prelude for Simplify integer arithmetic"
  50
  51   syntax function zero "0"
  52   syntax function one  "1"
  53
  54   syntax function (+)  "(+ %1 %2)"
  55   syntax function (-)  "(- %1 %2)"
  56   syntax function (*)  "(* %1 %2)"
  57   syntax function (-_) "(- 0 %1)"
  58
  59   syntax predicate (<=) "(<= %1 %2)"
  60   syntax predicate (<)  "(< %1 %2)"
  61   syntax predicate (>=) "(>= %1 %2)"
  62   syntax predicate (>)  "(> %1 %2)"
  63
  64   remove prop MulComm.Comm
  65   remove prop MulAssoc.Assoc
  66   remove prop Unit_def_l
  67   remove prop Unit_def_r
  68   remove prop Inv_def_l
  69   remove prop Inv_def_r
  70   remove prop Assoc
  71   remove prop Mul_distr_l
  72   remove prop Mul_distr_r
  73   remove prop Comm
  74   remove prop Unitary
  75   remove prop Refl
  76   remove prop Trans
  77   remove prop Antisymm
  78   remove prop Total
  79   remove prop NonTrivialRing
  80   remove prop CompatOrderAdd
  81   remove prop ZeroLessOne
  82
  83 end
  84
  85 theory real.Real
  86
  87   remove prop ZeroLessOne
  88   remove prop NonTrivialRing
  89
  90 end