drivers/polypaver.drv

   1 (* Why3 driver for PolyPaver *)
   2 (* http://michalkonecny.github.io/polypaver/_site/ *)
   3
   4 printer "metitarski"
   5 filename "%f-%t-%g.tptp"
   6
   7 valid 0
   8 invalid 111
   9 timeout "Gave up on deciding conjecture: TIMED OUT"
  10 time "why3cpulimit time : %s s"
  11 unknown 1 "toto"
  12
  13 (* to be improved *)
  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 "inline_all"
  25 transformation "eliminate_definition"
  26 transformation "eliminate_inductive"
  27 transformation "eliminate_if"
  28 transformation "eliminate_epsilon"
  29 transformation "eliminate_algebraic"
  30 transformation "eliminate_literal"
  31 transformation "eliminate_let"
  32
  33 transformation "simplify_formula"
  34 transformation "simplify_unknown_lsymbols"
  35 transformation "simplify_trivial_quantification"
  36 transformation "introduce_premises"
  37 transformation "instantiate_predicate"
  38 transformation "abstract_unknown_lsymbols"
  39
  40 transformation "discriminate"
  41 transformation "encoding_tptp"
  42
  43 theory BuiltIn
  44   meta "encoding:base" type real
  45   syntax predicate (=)  "(%1 = %2)"
  46   meta "eliminate_algebraic" "no_index"
  47 end
  48
  49 import "discrimination.gen"
  50
  51 theory real.Real
  52
  53   syntax function zero "0.0"
  54   syntax function one  "1.0"
  55
  56   syntax function (+)   "(%1 + %2)"
  57   syntax function (-)   "(%1 - %2)"
  58   syntax function (-_)  "(-%1)"
  59   syntax function ( * ) "(%1 * %2)"
  60   syntax function (/)   "(%1 / %2)"
  61   syntax function inv   "(1/ %1)"
  62
  63   syntax predicate (<=) "(%1 <= %2)"
  64   syntax predicate (<)  "(%1 < %2)"
  65   syntax predicate (>=) "(%1 >= %2)"
  66   syntax predicate (>)  "(%1 > %2)"
  67
  68   meta "inline:no" predicate (<=)
  69   meta "inline:no" predicate (>=)
  70   meta "inline:no" predicate (>)
  71
  72   remove allprops
  73 end
  74
  75 theory real.Abs
  76   syntax function abs "abs(%1)"
  77   remove allprops
  78 end
  79
  80 theory real.Square
  81   syntax function sqr  "(%1)^2"
  82   syntax function sqrt "sqrt(%1)"
  83   remove allprops
  84 end
  85
  86 theory real.MinMax
  87   syntax function min "min(%1,%2)"
  88   syntax function max "max(%1,%2)"
  89   remove allprops
  90 end
  91
  92 theory real.ExpLog
  93   syntax function exp "exp(%1)"
  94   syntax function log "ln(%1)"
  95   remove allprops
  96 end
  97
  98 theory real.PowerReal
  99   syntax function pow "pow(%1,%2)"
 100   remove allprops
 101 end