Improved support for metitarski (contrib by Piotr Trojanek)

drivers/metitarski.drv

 (* Why driver for MetiTarski *)
 
-valid   "Proof found"
-invalid "Completion found"
-timeout "Ran out of time"
-timeout "CPU time limit exceeded"
-outofmemory "Out of Memory"
-unknown "No Proof Found" ""
-fail    "Failure.*" "\"\\0\""
-
-import "tptp.gen"
+(* TODO:
+ * real.FromInt
+ * real.Truncate
+ * real.PowerInt    (incomplete)
+ * real.Hyperbolic
+ * real.Polar       (should work as is)
+ *)
+
+printer "tptp-fof"
+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 "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_if"
+transformation "eliminate_let"
+
+transformation "simplify_unknown_lsymbols"
+transformation "discriminate"
+(*
+transformation "encoding_tptp"
+transformation "encoding_sort"
+*)
+transformation "encoding_smt"
+
+theory BuiltIn
+  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)"
+
+  (* These follow from Metitarski's axioms. *)
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc
+  remove prop CommutativeGroup.Unit_def_l
+  remove prop CommutativeGroup.Unit_def_r
+  remove prop CommutativeGroup.Inv_def_l
+  remove prop CommutativeGroup.Inv_def_r
+  remove prop Assoc.Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Inverse
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop ZeroLessOne
+
+  remove prop add_div
+  remove prop sub_div
+  remove prop neg_div
+  remove prop assoc_mul_div
+  remove prop assoc_div_mul
+  remove prop assoc_div_div
+  remove prop CompatOrderMult
+end
+
+prelude "%%% this is a prelude for Metitarski"
+prelude "include('Axioms/general.ax')."
+
+theory real.Abs
+  prelude "%%% this is a prelude for Metitarski absolute value"
+
+  syntax function abs "abs(%1)"
+
+  prelude "include('Axioms/abs.ax')."
+  prelude "include('Axioms/abs2.ax')."
+
+  (* These follow from Metitarski's axioms. *)
+  remove prop Abs_le
+  remove prop Abs_pos
+  remove prop Abs_sum
+  remove prop Abs_prod
+  remove prop triangular_inequality
+end
+
+theory real.Square
+  prelude "%%% this is a prelude for Metitarski square"
+
+  prelude "include('Axioms/sqrt-general.ax')."
+
+  syntax function sqr  "(%1)^2"
+
+  (* This follows from Metitarski's general axioms. *)
+  remove prop Sqrt_positive
+  remove prop Sqrt_le
+end
+
+theory real.Trigonometry
+  prelude "%%% this is a prelude for Metitarski trigonometry"
+
+  prelude "include('Axioms/pi.ax')."
+
+  remove prop Pi_interval
+
+  prelude "include('Axioms/tan.ax')."
+  prelude "include('Axioms/arctan-lower.ax')."
+  prelude "include('Axioms/arctan-upper.ax')."
+
+  syntax function atan  "arctan(%1)"
+  syntax function tan  "tan(%1)"
+
+  (* These follow from Metitarski's base axioms. *)
+  prelude "include('Axioms/cos.ax')."
+  prelude "include('Axioms/sin.ax')."
+
+  remove prop Cos_0
+  remove prop Sin_0
+
+  (* These follow from Metitarski's auxiliary axioms. *)
+  prelude "include('Axioms/cos-constant.ax')."
+  prelude "include('Axioms/sin-constant.ax')."
+
+  remove prop Cos_le_one
+  remove prop Sin_le_one
+end
+
+theory real.MinMax
+  prelude "%%% this is a prelude for Metitarski min-max"
+
+  prelude "include('Axioms/minmax.ax')."
+
+  syntax function min "min(%1,%2)"
+  syntax function max "max(%1,%2)"
+
+  remove prop Max_is_ge
+  remove prop Max_is_some
+  remove prop Min_is_le
+  remove prop Min_is_some
+end
+
+theory real.PowerInt
+  syntax function power "%1^%2"
+
+  prelude "%%% this is a prelude for Metitarski power function"
+
+  prelude "include('Axioms/pow.ax')."
+
+  (* These follow from Metitarski's axioms. *)
+end
+
+theory real.ExpLog
+  syntax function exp "exp(%1)"
+  syntax function log "ln(%1)"
+
+  prelude "%%% this is a prelude for Metitarski exp/log"
+
+  prelude "include('Axioms/exp-general.ax')."
+  prelude "include('Axioms/ln-general.ax')."
+
+  (* These follow from Metitarski's axioms. *)
+  remove prop Log_one
+  remove prop Exp_zero
+end
+
+theory real.PowerReal
+  syntax function pow "pow(%1,%2)"
+
+  prelude "include('Axioms/pow.ax')."
+
+  (* These follow from Metitarski's axioms. *)
+  remove prop Pow_one_y
+  remove prop Pow_exp_log
+end
+
+theory int.Int
+
+  syntax function zero "0"
+  syntax function one  "1"
+
+  syntax function (+)  "(%1 + %2)"
+  syntax function (-)  "(%1 - %2)"
+  syntax function (*)  "(%1 * %2)"
+  syntax function (-_) "(-%1)"
+
+  syntax predicate (<=) "(%1 <= %2)"
+  syntax predicate (<)  "(%1 < %2)"
+  syntax predicate (>=) "(%1 >= %2)"
+  syntax predicate (>)  "(%1 > %2)"
+
+  (* These follow from Metitarski's axioms. *)
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc
+  remove prop CommutativeGroup.Unit_def_l
+  remove prop CommutativeGroup.Unit_def_r
+  remove prop CommutativeGroup.Inv_def_l
+  remove prop CommutativeGroup.Inv_def_r
+  remove prop Assoc.Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+  remove prop ZeroLessOne
+
+end

examples/logic/lagrange_inequality/why3session.xml

@@ -23,10 +23,14 @@
   version="8.4pl2"/>
  <prover
   id="5"
+  name="MetiTarski"
+  version="2.2"/>
+ <prover
+  id="6"
   name="Z3"
   version="3.2"/>
  <prover
-  id="6"
+  id="7"
   name="Z3"
   version="4.3.1"/>
  <file
@@ -48,7 +52,7 @@
     expanded="true"
     shape="ainfix &gt;=anorm2V0V1c0.0F">
     <proof
-     prover="6"
+     prover="7"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -65,7 +69,7 @@
     expanded="true"
     shape="ainfix =ainfix *anorm2V0V1anorm2V2V3ainfix +asqradotV0V1V2V3asqrainfix -ainfix *V0V3ainfix *V1V2F">
     <proof
-     prover="6"
+     prover="7"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -97,7 +101,7 @@
      <result status="valid" time="0.80"/>
     </proof>
     <proof
-     prover="6"
+     prover="7"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -130,7 +134,7 @@
      <result status="valid" time="0.01"/>
     </proof>
     <proof
-     prover="6"
+     prover="7"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -155,6 +159,14 @@
      archived="false">
      <result status="valid" time="1.78"/>
     </proof>
+    <proof
+     prover="5"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.04"/>
+    </proof>
    </goal>
    <goal
     name="CauchySchwarz"
@@ -190,7 +202,7 @@
     expanded="true"
     shape="ainfix &lt;=anorm2ainfix +V0V2ainfix +V1V3asqrainfix +anormV0V1anormV2V3F">
     <proof
-     prover="5"
+     prover="6"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -198,7 +210,7 @@
      <result status="valid" time="0.01"/>
     </proof>
     <proof
-     prover="6"
+     prover="7"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -238,6 +250,14 @@
      archived="false">
      <result status="valid" time="0.01"/>
     </proof>
+    <proof
+     prover="5"
+     timelimit="5"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.05"/>
+    </proof>
    </goal>
    <goal
     name="triangle"

plugins/tptp/tptp_printer.ml

@@ -120,7 +120,7 @@ and print_fmla info fmt f = match f.t_node with
         | Tand -> "&" | Tor -> "|" | Timplies -> "=>" | Tiff -> "<=>" in
       fprintf fmt "(%a@ %s %a)" (print_fmla info) f1 s (print_fmla info) f2
   | Tnot f ->
-      fprintf fmt "~@ (%a)" (print_fmla info) f
+      fprintf fmt "~@ %a" (print_fmla info) f
   | Ttrue ->
       fprintf fmt "$true"
   | Tfalse ->