Commit 01efbbd2 authored by MARCHE Claude's avatar MARCHE Claude

Improved Metitarski printer and driver. Example my_cosine.mlw now works

parent 834aa65f
......@@ -161,10 +161,6 @@ Release Notes (details in file CHANGES):
* plusieurs drivers acceptés sur la ligne de commande (AP)
* solve issues with metitarski
. DONE theory PowerReal
. crashes when applied on a WP (see examples/my_cosine.mlw)
* clean up the support for SMTLIB bitvectors: there are 2 theories in the stdlib: thoeries/bv.why and modules/bitvectors.mlw
-> not anymore, but more cleaning can be done: no need to separate all theories in drivers for Z3 and CVC4, since the same theory can be put several times in a driver (or imported sub-drivers)
......@@ -174,6 +170,10 @@ Release Notes (details in file CHANGES):
== DONE ==
* solve issues with metitarski
. DONE theory PowerReal
. DONE crashes when applied on a WP (see examples/my_cosine.mlw)
* determine which is the minumum version of Ocaml to compile, and then
updated configure.in and the manual
-> vérification compilation avec OCaml 3.12 -> Claude va le faire
......
......@@ -42,7 +42,7 @@ theory int.Int
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function ( * ) "(%1 * %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "dummy"
......@@ -86,7 +86,7 @@ theory real.Real
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function ( * ) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function (-_) "(-%1)"
syntax function inv "(1.0 / %1)"
......
......@@ -34,7 +34,13 @@ 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"
......
......@@ -2,19 +2,17 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="4000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="3" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="MetiTarski" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="6" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<prover id="7" name="CVC3" version="2.2" timelimit="3" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="9" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="11" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="12" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="13" name="Coq" version="8.4pl5" timelimit="5" memlimit="4000"/>
<file name="../lagrange_inequality.why" expanded="true">
<theory name="LagrangeInequality" sum="5e115a67d12d3b9e0cb091836baf8f27" expanded="true">
<goal name="norm2_pos">
......@@ -33,11 +31,10 @@
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="3.19"/></proof>
<proof prover="12"><result status="valid" time="2.49"/></proof>
</goal>
<goal name="norm_pos">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
......@@ -46,13 +43,12 @@
<proof prover="12"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sqr_le_sqrt">
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="2.67"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
<proof prover="13" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="1.53"/></proof>
</goal>
<goal name="CauchySchwarz">
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="2.55"/></proof>
<proof prover="6"><result status="valid" time="0.22"/></proof>
<proof prover="13" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.36"/></proof>
</goal>
</theory>
<theory name="TriangleInequality" sum="c1ce71fbadfa600580a354699d029b51" expanded="true">
......@@ -64,14 +60,12 @@
<goal name="sqr_sqrt_le">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="4"><result status="valid" time="0.05"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="10"><result status="valid" time="0.05" steps="11"/></proof>
</goal>
<goal name="triangle">
<proof prover="0" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="2.13"/></proof>
<proof prover="13" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.91"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,7 +2,6 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
......@@ -12,31 +11,37 @@
<prover id="7" name="Z3" version="3.2" timelimit="3" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="9" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="10" name="Coq" version="8.4pl5" timelimit="5" memlimit="1000"/>
<prover id="11" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<file name="../triangle_inequality.why" expanded="true">
<theory name="CauchySchwarzInequality" sum="029d2a2da0bd5b8c118724b66181542e" expanded="true">
<goal name="norm2_pos">
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="p_expr">
<proof prover="5" timelimit="30"><result status="valid" time="0.01"/></proof>
<proof prover="3" timelimit="30"><result status="highfailure" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="p_pos">
<proof prover="1"><result status="valid" time="0.02" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="5" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="mul_div_simpl">
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="p_val_part">
<metas>
......@@ -244,15 +249,15 @@
<ip_library name="real"/>
<ip_qualid name="Sqrt_le"/>
</pr_pos>
<pr_pos name="norm2_pos" id="2836"
<pr_pos name="norm2_pos" id="2852"
ip_theory="CauchySchwarzInequality">
<ip_qualid name="norm2_pos"/>
</pr_pos>
<pr_pos name="p_expr" id="2862"
<pr_pos name="p_expr" id="2878"
ip_theory="CauchySchwarzInequality">
<ip_qualid name="p_expr"/>
</pr_pos>
<pr_pos name="p_pos" id="2873"
<pr_pos name="p_pos" id="2889"
ip_theory="CauchySchwarzInequality">
<ip_qualid name="p_pos"/>
</pr_pos>
......@@ -374,18 +379,18 @@
<meta_arg_pr id="2575"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2836"/>
<meta_arg_pr id="2852"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2862"/>
<meta_arg_pr id="2878"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="2873"/>
<meta_arg_pr id="2889"/>
</meta>
<goal name="p_val_part">
<transf name="eliminate_builtin">
<goal name="p_val_part.1" expl="1.">
<proof prover="2" timelimit="45"><result status="valid" time="32.03"/></proof>
<proof prover="1" timelimit="45"><result status="valid" time="46.41" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -395,54 +400,62 @@
</goal>
<goal name="p_val_part_pos">
<proof prover="1"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="p_val_part_pos_aux">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="CauchySchwarz_aux_non_null">
<proof prover="0" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="1.24"/></proof>
<proof prover="10" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="1.24"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="norm_null">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="1"><result status="timeout" time="5.01"/></proof>
<proof prover="11"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="CauchySchwarz_aux_null">
<proof prover="1"><result status="valid" time="0.06" steps="18"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="5" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.28"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="CauchySchwarz_aux">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="5" obsolete="true"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="norm_pos">
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="5" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sqr_le_sqrt">
<proof prover="1"><result status="valid" time="0.03" steps="18"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="CauchySchwarz">
<proof prover="0" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.47"/></proof>
<proof prover="10" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.47"/></proof>
</goal>
</theory>
<theory name="TriangleInequality" sum="0e6e449288baab6d459040c11cfc2eb5" expanded="true">
......@@ -452,12 +465,13 @@
</goal>
<goal name="sqr_sqrt_le">
<proof prover="1"><result status="valid" time="0.04" steps="17"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="5" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="11"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="triangle">
<proof prover="0" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="1.27"/></proof>
<proof prover="10" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="1.27"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,12 +4,14 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="8" memlimit="1000"/>
<prover id="1" name="Gappa" version="1.1.1" timelimit="2" memlimit="0"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<file name="../my_cosine.mlw" expanded="true">
<theory name="M" sum="0c66613577f8d2343f3cd0096f576e85" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="1. assertion" expanded="true">
<proof prover="0" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="valid" time="3.46"/></proof>
<proof prover="2" edited="my_cosine-M-WP_parameter_my_cosine_1.tptp"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="2. precondition" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
......@@ -19,13 +19,15 @@ open Term
open Decl
open Printer
let bls = ["true";"false"]
let ident_printer =
let san = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer [] ~sanitizer:san
create_ident_printer bls ~sanitizer:san
let pr_printer =
let san = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer [] ~sanitizer:san
create_ident_printer bls ~sanitizer:san
let print_symbol fmt id =
let san = String.uncapitalize in
......
......@@ -48,7 +48,7 @@ let () =
])))
~desc:"Same@ as@ simplify_trivial_quantification_in_goal,@ but@ instead@ \
of@ substituting@ quantified@ variables,@ substitute@ applications@ \
of@ non-buit-in@ symbols.@ Used@ by@ the@ Gappa@ pretty-printer."
of@ non-built-in@ symbols.@ Used@ by@ the@ Gappa@ pretty-printer."
(* patterns (TODO: add a parser and generalize it out of Gappa) *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment