drivers/mathsat.drv

   1 (* Why driver for SMT2 syntax *)
   2
   3 prelude ";;; this is a prelude for MathSAT5"
   4 prelude "(set-logic AUFNIRA)"
   5
   6 printer "smtv2"
   7 filename "%f-%t-%g.smt2"
   8
   9 valid "^unsat"
  10 unknown "^\\(unknown\\|sat\\|Fail\\)" ""
  11 outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
  12 time "why3cpulimit time : %s s"
  13
  14
  15 (* Performed introductions depending on whether counterexamples are
  16    requested, as said by the meta "get_counterexmp". When this meta
  17    set, this transformation introduces the model variables that are
  18    still embedded in the goal. When it is not set, it removes all
  19    these unused-ce-related variables, even in the context.  *)
  20 transformation "counterexamples_dependent_intros"
  21
  22 transformation "inline_trivial"
  23 transformation "eliminate_builtin"
  24 transformation "eliminate_definition"
  25 transformation "eliminate_inductive"
  26 transformation "eliminate_epsilon"
  27 transformation "eliminate_algebraic"
  28 transformation "eliminate_literal"
  29
  30 transformation "simplify_formula"
  31 (*transformation "simplify_trivial_quantification"*)
  32
  33 transformation "discriminate"
  34 transformation "encoding_smt"
  35
  36 theory BuiltIn
  37   syntax type int   "Int"
  38   syntax type real  "Real"
  39   syntax predicate (=)  "(= %1 %2)"
  40
  41   meta "encoding:kept" type int
  42 end
  43
  44 theory int.Int
  45
  46   prelude ";;; this is a prelude for Z3 integer arithmetic"
  47
  48   syntax function zero "0"
  49   syntax function one  "1"
  50
  51   syntax function (+)  "(+ %1 %2)"
  52   syntax function (-)  "(- %1 %2)"
  53   syntax function (*)  "(* %1 %2)"
  54   syntax function (-_) "(- %1)"
  55
  56   syntax predicate (<=) "(<= %1 %2)"
  57   syntax predicate (<)  "(< %1 %2)"
  58   syntax predicate (>=) "(>= %1 %2)"
  59   syntax predicate (>)  "(> %1 %2)"
  60
  61   remove prop MulComm.Comm
  62   remove prop MulAssoc.Assoc
  63   remove prop Unit_def_l
  64   remove prop Unit_def_r
  65   remove prop Inv_def_l
  66   remove prop Inv_def_r
  67   remove prop Assoc
  68   remove prop Mul_distr_l
  69   remove prop Mul_distr_r
  70   remove prop Comm
  71   remove prop Unitary
  72   remove prop Refl
  73   remove prop Trans
  74   remove prop Antisymm
  75   remove prop Total
  76   remove prop NonTrivialRing
  77   remove prop CompatOrderAdd
  78   remove prop ZeroLessOne
  79
  80 end
  81
  82
  83 theory real.Real
  84
  85   prelude ";;; this is a prelude for Z3 real arithmetic"
  86
  87   syntax function zero "0.0"
  88   syntax function one  "1.0"
  89
  90   syntax function (+)  "(+ %1 %2)"
  91   syntax function (-)  "(- %1 %2)"
  92   syntax function (*)  "(* %1 %2)"
  93   syntax function (/)  "(/ %1 %2)"
  94   syntax function (-_) "(- %1)"
  95   syntax function inv  "(/ 1.0 %1)"
  96
  97   syntax predicate (<=) "(<= %1 %2)"
  98   syntax predicate (<)  "(< %1 %2)"
  99   syntax predicate (>=) "(>= %1 %2)"
 100   syntax predicate (>)  "(> %1 %2)"
 101
 102   remove prop MulComm.Comm
 103   remove prop MulAssoc.Assoc
 104   remove prop Unit_def_l
 105   remove prop Unit_def_r
 106   remove prop Inv_def_l
 107   remove prop Inv_def_r
 108   remove prop Assoc
 109   remove prop Mul_distr_l
 110   remove prop Mul_distr_r
 111   remove prop Comm
 112   remove prop Unitary
 113   remove prop Inverse
 114   remove prop Refl
 115   remove prop Trans
 116   remove prop Antisymm
 117   remove prop Total
 118   remove prop NonTrivialRing
 119   remove prop CompatOrderAdd
 120   remove prop ZeroLessOne
 121
 122   meta "encoding:kept" type real
 123
 124 end
 125
 126 theory Bool
 127   syntax type     bool  "Bool"
 128   syntax function True  "true"
 129   syntax function False "false"
 130   meta "encoding:kept" type bool
 131 end
 132
 133 theory bool.Bool
 134   syntax function andb  "(and %1 %2)"
 135   syntax function orb   "(or %1 %2)"
 136   syntax function xorb  "(xor %1 %2)"
 137   syntax function notb  "(not %1)"
 138   syntax function implb "(=> %1 %2)"
 139 end
 140
 141 theory bool.Ite
 142   syntax function ite "(ite %1 %2 %3)"
 143   meta "encoding:lskept" function ite
 144 end
 145
 146 (* needs to be checked
 147 theory int.EuclideanDivision
 148   syntax function div "(div %1 %2)"
 149   syntax function mod "(mod %1 %2)"
 150   remove prop Mod_bound
 151   remove prop Div_mod
 152   remove prop Mod_1
 153   remove prop Div_1
 154 end
 155 *)
 156
 157 theory real.FromInt
 158   syntax function from_int "(to_real %1)"
 159   remove prop Zero
 160   remove prop One
 161   remove prop Add
 162   remove prop Sub
 163   remove prop Mul
 164   remove prop Neg
 165 end
 166
 167 (*
 168 theory real.Truncate
 169   syntax function floor "(to_int %1)"
 170   remove prop Floor_down
 171   remove prop Floor_monotonic
 172 end
 173 *)
 174
 175 theory HighOrd
 176   syntax type     (->) "(Array %1 %2)"
 177   syntax function (@) "(select %1 %2)"
 178
 179   meta "encoding:lskept" function (@)
 180 end
 181
 182 theory map.Map
 183   syntax function get "(select %1 %2)"
 184   syntax function set "(store %1 %2 %3)"
 185
 186   meta "encoding:lskept" function get
 187   meta "encoding:lskept" function set
 188 end
 189
 190 theory map.Const
 191   meta "encoding:lskept" function const
 192 (*  syntax function const "(const[%t0] %1)" *)
 193 end