drivers/yices.drv

   1
   2 (* Why3 driver for Yices (SMT-like syntax) *)
   3
   4 prelude ";;; this is a prelude for Yices "
   5
   6 printer "yices"
   7 filename "%f-%t-%g.ycs"
   8
   9 valid "\\bunsat\\b"
  10 unknown "\\bunknown\\b\\|\\bsat\\b" ""
  11 unknown "feature not supported: non linear problem" "non linear arith"
  12 time "why3cpulimit time : %s s"
  13
  14 (* Performed introductions depending on whether counterexamples are
  15    requested, as said by the meta "get_counterexmp". When this meta
  16    set, this transformation introduces the model variables that are
  17    still embedded in the goal. When it is not set, it removes all
  18    these unused-ce-related variables, even in the context.  *)
  19 transformation "counterexamples_dependent_intros"
  20
  21 transformation "inline_trivial"
  22 transformation "eliminate_builtin"
  23 transformation "eliminate_definition"
  24 transformation "eliminate_inductive"
  25 transformation "eliminate_epsilon"
  26 transformation "eliminate_algebraic"
  27 transformation "eliminate_literal"
  28
  29 transformation "simplify_formula"
  30 (*transformation "simplify_trivial_quantification"*)
  31
  32 transformation "discriminate"
  33 transformation "encoding_smt"
  34
  35 import "discrimination.gen"
  36
  37 theory BuiltIn
  38   syntax type int   "int"
  39   syntax type real  "real"
  40   syntax predicate (=)  "(= %1 %2)"
  41
  42   meta "encoding:kept" type int
  43
  44   (* could we do this? *)
  45   (* meta "eliminate_algebraic" "keep_enums" *)
  46 end
  47
  48 theory int.Int
  49
  50   prelude ";;; this is a prelude for Yices integer arithmetic"
  51
  52   syntax function zero "0"
  53   syntax function one  "1"
  54
  55   syntax function (+)  "(+ %1 %2)"
  56   syntax function (-)  "(- %1 %2)"
  57   syntax function (*)  "(* %1 %2)"
  58   syntax function (-_) "(- 0 %1)"
  59
  60   syntax predicate (<=) "(<= %1 %2)"
  61   syntax predicate (<)  "(< %1 %2)"
  62   syntax predicate (>=) "(>= %1 %2)"
  63   syntax predicate (>)  "(> %1 %2)"
  64
  65   remove prop MulComm.Comm
  66   remove prop MulAssoc.Assoc
  67   remove prop Unit_def_l
  68   remove prop Unit_def_r
  69   remove prop Inv_def_l
  70   remove prop Inv_def_r
  71   remove prop Assoc
  72   remove prop Mul_distr_l
  73   remove prop Mul_distr_r
  74   remove prop Comm
  75   remove prop Unitary
  76   remove prop Refl
  77   remove prop Trans
  78   remove prop Antisymm
  79   remove prop Total
  80   remove prop NonTrivialRing
  81   remove prop CompatOrderAdd
  82   remove prop ZeroLessOne
  83
  84 end
  85
  86
  87 theory real.Real
  88
  89   prelude ";;; this is a prelude for Yices real arithmetic"
  90
  91   syntax function zero "0"
  92   syntax function one  "1"
  93
  94   syntax function (+)  "(+ %1 %2)"
  95   syntax function (-)  "(- %1 %2)"
  96   syntax function (*)  "(* %1 %2)"
  97   (* Yices division doesn't accept anything else than constant on
  98   denominator so we don't use it (except for constant cf printer) *)
  99   (* syntax function (/)  "(/ %1 %2)" *)
 100   syntax function (-_) "(- 0 %1)"
 101   (* syntax function inv  "(/ 1 %1)" *)
 102
 103   syntax predicate (<=) "(<= %1 %2)"
 104   syntax predicate (<)  "(< %1 %2)"
 105   syntax predicate (>=) "(>= %1 %2)"
 106   syntax predicate (>)  "(> %1 %2)"
 107
 108   remove prop MulComm.Comm
 109   remove prop MulAssoc.Assoc
 110   remove prop Unit_def_l
 111   remove prop Unit_def_r
 112   remove prop Inv_def_l
 113   remove prop Inv_def_r
 114   remove prop Assoc
 115   remove prop Mul_distr_l
 116   remove prop Mul_distr_r
 117   remove prop Comm
 118   remove prop Unitary
 119   remove prop Inverse
 120   remove prop Refl
 121   remove prop Trans
 122   remove prop Antisymm
 123   remove prop Total
 124   remove prop NonTrivialRing
 125   remove prop CompatOrderAdd
 126   remove prop ZeroLessOne
 127
 128   meta "encoding:kept" type real
 129 end
 130
 131 theory Bool
 132   syntax type     bool  "bool"
 133   syntax function True  "true"
 134   syntax function False "false"
 135
 136   meta "encoding:kept" type bool
 137 end
 138
 139 theory bool.Bool
 140   syntax function andb  "(and %1 %2)"
 141   syntax function orb   "(or %1 %2)"
 142   syntax function notb  "(not %1)"
 143 end
 144
 145 theory HighOrd
 146   syntax type (->) "(-> %1 %2)"
 147   syntax function (@) "(%1 %2)"
 148
 149   meta "encoding:lskept" function (@)
 150 end
 151
 152 theory map.Map
 153   syntax function get    "(%1 %2)"
 154   syntax function ([])   "(%1 %2)"
 155   syntax function set    "(update %1 (%2) %3)"
 156   syntax function ([<-]) "(update %1 (%2) %3)"
 157
 158   meta "encoding:lskept" function get
 159   meta "encoding:lskept" function set
 160 end
 161
 162 theory map.Const
 163   meta "encoding:lskept" function const
 164 end