Support for upcoming PolyPaver 0.3 in progress

http://michalkonecny.github.io/polypaver/_site/index.html

drivers/polypaver.drv

+(* Why3 driver for PolyPaver *)
+(* http://michalkonecny.github.io/polypaver/_site/ *)
+
+printer "metitarski"
+filename "%f-%t-%g.tptp"
+
+valid   "^SZS status Theorem"
+valid   "^SZS status Unsatisfiable"
+unknown "^SZS status CounterSatisfiable" ""
+unknown "^SZS status Satisfiable" ""
+timeout "^SZS status Timeout"
+unknown "^SZS status GaveUp" ""
+fail    "^SZS status Error" ""
+
+time "why3cpulimit time : %s s"
+
+(* to be improved *)
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "inline_all"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+transformation "eliminate_if"
+transformation "eliminate_let"
+
+transformation "simplify_formula"
+transformation "simplify_unknown_lsymbols"
+transformation "simplify_trivial_quantification"
+transformation "introduce_premises"
+transformation "instantiate_predicate"
+transformation "abstract_unknown_lsymbols"
+
+transformation "discriminate"
+transformation "encoding_tptp"
+
+theory BuiltIn
+  meta "encoding : base" type real
+  syntax predicate (=)  "(%1 = %2)"
+  meta "eliminate_algebraic" "no_index"
+end
+
+import "discrimination.gen"
+
+theory real.Real
+
+  syntax function zero "0.0"
+  syntax function one  "1.0"
+
+  syntax function (+)   "(%1 + %2)"
+  syntax function (-)   "(%1 - %2)"
+  syntax function (-_)  "(-%1)"
+  syntax function ( * ) "(%1 * %2)"
+  syntax function (/)   "(%1 / %2)"
+  syntax function inv   "(1/ %1)"
+
+  syntax predicate (<=) "(%1 <= %2)"
+  syntax predicate (<)  "(%1 < %2)"
+  syntax predicate (>=) "(%1 >= %2)"
+  syntax predicate (>)  "(%1 > %2)"
+
+  meta "inline : no" predicate (<=)
+  meta "inline : no" predicate (>=)
+  meta "inline : no" predicate (>)
+
+  remove allprops
+end
+
+theory real.Abs
+  syntax function abs "abs(%1)"
+  remove allprops
+end
+
+theory real.Square
+  syntax function sqr  "(%1)^2"
+  syntax function sqrt "sqrt(%1)"
+  remove allprops
+end
+
+theory real.MinMax
+  syntax function min "min(%1,%2)"
+  syntax function max "max(%1,%2)"
+  remove allprops
+end
+
+theory real.ExpLog
+  syntax function exp "exp(%1)"
+  syntax function log "ln(%1)"
+  remove allprops
+end
+
+theory real.PowerReal
+  syntax function pow "pow(%1,%2)"
+  remove allprops
+end

examples/tests-provers/polypaver.why

+
+theory Test
+
+  (*
+
+  Examples from http://michalkonecny.github.io/polypaver/_site/index.html
+
+*)
+
+  use import real.Real
+  use import real.ExpLog
+
+  goal g1:
+    forall a b:real.
+      -10.0 <= a <= 10.0 /\ -10.0 <= b <= 10.0 /\ b > a + 0.1 ->
+      exp a - exp b > (b-a) * exp ((a + b) / 2.0)
+
+end

share/provers-detection-data.conf

@@ -220,6 +220,16 @@ version_old = "2.2"
 command = "%l/why3-cpulimit %T %m -s %e --time %t %f"
 driver = "drivers/metitarski.drv"
 
+[ATP polypaver]
+name = "PolyPaver"
+exec = "polypaver"
+exec = "polypaver-0.3"
+version_switch = "--version"
+version_regexp = "PolyPaver \\([0-9.]+\\) (c)"
+version_ok = "0.3"
+command = "%l/why3-cpulimit %T %m -s %e -d 2 -m 10 --time=%t %f"
+driver = "drivers/polypaver.drv"
+
 [ATP spass]
 name = "Spass"
 exec = "SPASS"