Commit 8eb1d02d authored by MARCHE Claude's avatar MARCHE Claude

Metitarski: attempt for a new driver

parent 87041544
......@@ -284,7 +284,7 @@ Scheduled for 31 october 2013
*** Prouveur de Martin
*** examples de Frama-C/Jessie et Krakatoa
* Coq detection (et PVS) (CLAUDE, champ supplementaire compile_support = yes dans le prover-detection-data)
* DONE Coq detection (et PVS) (CLAUDE, champ supplementaire compile_support = yes dans le prover-detection-data)
** refuser de detecter Coq si on n'a pas compilé avec le support de Coq
(i.e. si Coq a ete installé apres)
......@@ -319,7 +319,7 @@ Scheduled for 31 october 2013
** Metitarski TODO: improve it (CLAUDE, GUILLAUME)
** others ?
* simplification de (a && false) ne devrait pas etre false
* DONE? simplification de (a && false) ne devrait pas etre false
......
......@@ -34,20 +34,32 @@ transformation "eliminate_let"
transformation "simplify_unknown_lsymbols"
transformation "discriminate"
transformation "encoding_metitarski"
(*
transformation "encoding_tptp"
transformation "encoding_sort"
*)
transformation "encoding_smt"
*)
theory BuiltIn
meta "encoding : kept" type int
meta "encoding : kept" type real
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
(*
meta "select_inst" "all"
meta "select_lskept" "all"
meta "select_lsinst" "all"
meta "select_kept" "all"
*)
end
import "discrimination.gen"
theory real.Real
meta "encoding : kept" type real
syntax function zero "0.0"
syntax function one "1.0"
......
......@@ -25,11 +25,11 @@
shape="ainfix >=ainfix *V0V0c0.0F">
<proof
prover="0"
timelimit="5"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
......@@ -42,11 +42,12 @@
shape="ainfix &gt;=asqrV0c0.0F">
<proof
prover="0"
timelimit="5"
timelimit="60"
memlimit="1000"
edited="metitarski-P-sqr_pos_1.tptp"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
</theory>
......@@ -66,11 +67,11 @@
shape="ainfix &gt;=asqrV0c0.0F">
<proof
prover="0"
timelimit="5"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
</theory>
......@@ -83,35 +84,35 @@
<goal
name="cos_bound"
locfile="../metitarski.why"
loclnum="30" loccnumb="7" loccnume="16"
loclnum="31" loccnumb="7" loccnume="16"
sum="1279f956936a79ace638c17c4f31378d"
proved="false"
expanded="true"
shape="ainfix &lt;=acosV0c1.0Aainfix &lt;=aprefix -c1.0acosV0F">
<proof
prover="0"
timelimit="5"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="2.34"/>
<result status="unknown" time="11.21"/>
</proof>
</goal>
<goal
name="cos_bound_harder"
locfile="../metitarski.why"
loclnum="33" loccnumb="7" loccnume="23"
loclnum="34" loccnumb="7" loccnume="23"
sum="9e730acb71ecc7a8fb46ef19c84a57db"
proved="true"
expanded="true"
shape="ainfix &lt;=acosV0c1.0Aainfix &lt;=c0.7acosV0Iainfix &lt;=V0c0.7Aainfix &lt;=aprefix -c0.7V0F">
<proof
prover="0"
timelimit="5"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.21"/>
<result status="valid" time="0.94"/>
</proof>
</goal>
</theory>
......
......@@ -77,8 +77,16 @@ let encoding_tptp env = Trans.seq [
forget_kept;
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env]
let encoding_metitarski env = Trans.seq [
Libencoding.monomorphise_goal;
(* forget_kept; *)
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env]
let () = register_env_transform "encoding_smt" encoding_smt
~desc:"Encode@ polymorphic@ types@ for@ provers@ with@ sorts."
let () = register_env_transform "encoding_tptp" encoding_tptp
~desc:"Encode@ polymorphic@ types@ for@ provers@ without@ sorts."
let () = register_env_transform "encoding_metitarski" encoding_metitarski
~desc:"Encode@ polymorphic@ types@ for@ prover@ metitarski."
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