drivers/dreal.drv

   1 (** Why3 driver for dreal 21.4.06.2* *)
   2
   3 prelude ";; produced by dreal.drv ;;"
   4
   5 printer "smtv2"
   6
   7 filename "%f-%t-%g.smt2"
   8 unknown "delta-sat with delta = .*" ""
   9 time "why3cpulimit time : %s s"
  10 valid "^unsat$"
  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_definition"
  21 transformation "eliminate_builtin"
  22 transformation "eliminate_inductive"
  23 transformation "eliminate_epsilon"
  24 transformation "eliminate_algebraic"
  25 transformation "eliminate_literal"
  26 transformation "simplify_formula"
  27 transformation "simplify_trivial_quantification"
  28 transformation "encoding_smt"
  29 transformation "simplify_computations"
  30 transformation "introduce_premises"
  31 transformation "instantiate_predicate"
  32 transformation "keep_only_arithmetic"
  33 transformation "abstract_unknown_lsymbols"
  34 transformation "eliminate_unknown_lsymbols"
  35 transformation "eliminate_unknown_types"
  36 transformation "eliminate_big_constants"
  37
  38 prelude "(set-logic QF_NRA)"
  39
  40 theory BuiltIn
  41   syntax type int   "Int"
  42   syntax type real  "Real"
  43   syntax predicate (=)  "(= %1 %2)"
  44
  45   meta "encoding:kept" type int
  46   meta "encoding:ignore_polymorphism_ls" predicate (=)
  47 end
  48
  49 theory int.Int
  50   syntax function zero "0"
  51   syntax function one  "1"
  52
  53   syntax function (+)  "(+ %1 %2)"
  54   syntax function (-)  "(- %1 %2)"
  55   syntax function (*)  "(* %1 %2)"
  56   syntax function (-_) "(- %1)"
  57
  58   syntax predicate (<=) "(<= %1 %2)"
  59   syntax predicate (<)  "(< %1 %2)"
  60   syntax predicate (>=) "(>= %1 %2)"
  61   syntax predicate (>)  "(> %1 %2)"
  62
  63   remove allprops
  64 end
  65
  66 theory int.Abs
  67   syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
  68
  69   remove allprops
  70 end
  71
  72
  73 theory real.Real
  74   syntax function zero "0.0"
  75   syntax function one  "1.0"
  76
  77   syntax function (+)  "(+ %1 %2)"
  78   syntax function (-)  "(- %1 %2)"
  79   syntax function (*)  "(* %1 %2)"
  80   syntax function (/)  "(/ %1 %2)"
  81   syntax function (-_) "(- %1)"
  82   syntax function inv  "(/ 1.0 %1)"
  83
  84   syntax predicate (<=) "(<= %1 %2)"
  85   syntax predicate (<)  "(< %1 %2)"
  86   syntax predicate (>=) "(>= %1 %2)"
  87   syntax predicate (>)  "(> %1 %2)"
  88
  89   remove allprops
  90
  91   meta "encoding:kept" type real
  92 end
  93
  94 theory real.Abs
  95   syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
  96
  97   remove allprops
  98 end
  99
 100 theory real.MinMax
 101   syntax function min "(min %1 %2)"
 102   syntax function max "(max %1 %2)"
 103   remove allprops
 104 end
 105
 106 theory real.FromInt
 107   remove allprops
 108 end
 109
 110 theory real.Truncate
 111   syntax function truncate "(ite (>= %1 0.0) \
 112                                  (to_int %1) \
 113                                  (- (to_int (- %1))))"
 114   syntax function floor "(to_int %1)"
 115   syntax function ceil "(- (to_int (- %1)))"
 116   remove allprops
 117 end
 118
 119 theory real.Square
 120   syntax function sqrt "(sqrt %1)"
 121   syntax function sqr "(pow %1 2)"
 122   remove allprops
 123 end
 124
 125 theory real.ExpLog
 126   syntax function exp "(exp %1)"
 127   syntax function log "(log %1)"
 128   remove allprops
 129 end
 130
 131 theory real.PowerReal
 132   syntax function pow "(^ %1 %2)"
 133   remove allprops
 134 end
 135
 136 theory real.Trigonometry
 137   syntax function cos "(cos %1)"
 138   syntax function sin "(sin %1)"
 139   syntax function tan "(tan %1)"
 140   syntax function atan "(atan %1)"
 141
 142   remove prop Pythagorean_identity
 143   remove prop Cos_le_one
 144   remove prop Sin_le_one
 145   remove prop Cos_0
 146   remove prop Sin_0
 147   remove prop Cos_neg
 148   remove prop Sin_neg
 149   remove prop Cos_sum
 150   remove prop Sin_sum
 151   remove prop Tan_atan
 152 end
 153
 154 theory real.Hyperbolic
 155   syntax function cosh "(cosh %1)"
 156   syntax function sinh "(sinh %1)"
 157   syntax function tanh "(tanh %1)"
 158 end
 159
 160 theory ieee_float.GenericFloat
 161   remove allprops
 162 end