drivers/psyche.drv

   1 (* Why driver for Psyche *)
   2
   3 prelude "(set-logic FO)"
   4
   5 printer "smtv2"
   6 filename "%f-%t-%g.smt2"
   7
   8 valid "^PROVABLE"
   9 invalid "^NOT PROVABLE"
  10 timeout "interrupted by timeout"
  11 time "why3cpulimit time : %s s"
  12
  13 (* Performed introductions depending on whether counterexamples are
  14    requested, as said by the meta "get_counterexmp". When this meta
  15    set, this transformation introduces the model variables that are
  16    still embedded in the goal. When it is not set, it removes all
  17    these unused-ce-related variables, even in the context.  *)
  18 transformation "counterexamples_dependent_intros"
  19
  20 transformation "inline_trivial"
  21 transformation "eliminate_builtin"
  22 transformation "eliminate_definition"
  23 transformation "eliminate_inductive"
  24 transformation "eliminate_epsilon"
  25 transformation "eliminate_algebraic"
  26 transformation "eliminate_literal"
  27
  28 transformation "simplify_formula"
  29 (*transformation "simplify_trivial_quantification"*)
  30
  31 transformation "discriminate"
  32 transformation "encoding_smt"
  33
  34 theory BuiltIn
  35   syntax type real  "Real"
  36   syntax predicate (=)  "(= %1 %2)"
  37   meta "eliminate_algebraic" "no_index"
  38 end
  39
  40 theory real.Real
  41
  42   prelude ";;; this is a prelude for smt-lib v2 real arithmetic"
  43
  44   syntax function zero "0"
  45   syntax function one  "1"
  46
  47   syntax function (+)  "(+ %1 %2)"
  48   syntax function (-)  "(- %1 %2)"
  49   syntax function ( * )  "(* %1 %2)"
  50   syntax function (/)  "(/ %1 %2)"
  51   syntax function (-_) "(- %1)"
  52   syntax function inv  "(/ 1 %1)"
  53
  54   syntax predicate (<=) "(<= %1 %2)"
  55   syntax predicate (<)  "(< %1 %2)"
  56   syntax predicate (>=) "(>= %1 %2)"
  57   syntax predicate (>)  "(> %1 %2)"
  58
  59   remove prop MulComm.Comm
  60   remove prop MulAssoc.Assoc
  61   remove prop Unit_def_l
  62   remove prop Unit_def_r
  63   remove prop Inv_def_l
  64   remove prop Inv_def_r
  65   remove prop Assoc
  66   remove prop Mul_distr_l
  67   remove prop Mul_distr_r
  68   remove prop Comm
  69   remove prop Unitary
  70   remove prop Inverse
  71   remove prop Refl
  72   remove prop Trans
  73   remove prop Antisymm
  74   remove prop Total
  75   remove prop NonTrivialRing
  76   remove prop CompatOrderAdd
  77   remove prop ZeroLessOne
  78
  79   meta "encoding:kept" type real
  80
  81 end
  82
  83 (*
  84 theory Bool
  85   syntax type     bool  "Bool"
  86   syntax function True  "true"
  87   syntax function False "false"
  88   meta "encoding:kept" type bool
  89 end
  90
  91 theory bool.Bool
  92   syntax function andb  "(and %1 %2)"
  93   syntax function orb   "(or %1 %2)"
  94   syntax function xorb  "(xor %1 %2)"
  95   syntax function notb  "(not %1)"
  96   syntax function implb "(=> %1 %2)"
  97 end
  98
  99 theory bool.Ite
 100   syntax function ite "(ite %1 %2 %3)"
 101   meta "encoding:lskept" function ite
 102 end
 103 *)
 104
 105 import "discrimination.gen"