Commit c656dc97 authored by MARCHE Claude's avatar MARCHE Claude

example prover: upgrade alt-ergo version

parent 811b80c8
......@@ -4347,8 +4347,8 @@ module Impl
(const (Var_fo_term (-1)) : int -> (fo_term int int))
identity identity))
(identity) (identity)) ;
let mrv0 = rename_symbol mv0 identity in
let mrv1 = rename_fo_term_list mv1 identity identity in
let ghost mrv0 = rename_symbol mv0 identity in
let ghost mrv1 = rename_fo_term_list mv1 identity identity in
let resv0 =
{ nlrepr_symbol_field = v0 ;
nlfree_var_symbol_set_abstraction_symbol_field = fv0 ;
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -4,62 +4,62 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Firstorder_symbol_impl.mlw" proved="true">
<theory name="Logic" proved="true">
<goal name="VC nlsize_positive_lemma_symbol" expl="VC for nlsize_positive_lemma_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="6"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="17"/></proof>
</goal>
<goal name="VC shiftb_compose_lemma_symbol" expl="VC for shiftb_compose_lemma_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.08" steps="130"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="144"/></proof>
</goal>
<goal name="VC nlmodel_subst_commutation_lemma_symbol" expl="VC for nlmodel_subst_commutation_lemma_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="VC nlmodel_rename_commutation_lemma_symbol" expl="VC for nlmodel_rename_commutation_lemma_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.04" steps="35"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="32"/></proof>
</goal>
<goal name="VC bound_depth_of_symbol_in_symbol_nonnegative" expl="VC for bound_depth_of_symbol_in_symbol_nonnegative" proved="true">
<proof prover="7"><result status="valid" time="0.04" steps="19"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="31"/></proof>
</goal>
<goal name="VC model_equal_symbol" expl="VC for model_equal_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.04" steps="49"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="50"/></proof>
</goal>
</theory>
<theory name="Impl" proved="true">
<goal name="VC bind_var_symbol_in_symbol" expl="VC for bind_var_symbol_in_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.10" steps="93"/></proof>
<proof prover="2"><result status="valid" time="0.10" steps="210"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_symbol" expl="VC for unbind_var_symbol_in_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.16" steps="137"/></proof>
<proof prover="2"><result status="valid" time="0.16" steps="189"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_symbol" expl="VC for subst_base_symbol_in_symbol" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC subst_base_symbol_in_symbol.0" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_symbol.1" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="4"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_symbol.2" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.04" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_symbol.3" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_symbol.4" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="18"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_symbol.5" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="42"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="71"/></proof>
</goal>
</transf>
</goal>
<goal name="VC construct_symbol" expl="VC for construct_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.06" steps="102"/></proof>
<proof prover="2"><result status="valid" time="0.06" steps="183"/></proof>
</goal>
<goal name="VC destruct_symbol" expl="VC for destruct_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.04" steps="46"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="84"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol" expl="VC for nlsubst_symbol_in_symbol" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -68,40 +68,40 @@
<goal name="VC nlsubst_symbol_in_symbol.0.0" expl="precondition" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC nlsubst_symbol_in_symbol.0.0.0" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.12" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.12" steps="11"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.1" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="14"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.2" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="13"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.3" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="18"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.4" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.04" steps="15"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="10"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.5" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.06" steps="13"/></proof>
<proof prover="2"><result status="valid" time="0.06" steps="11"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.6" expl="precondition" proved="true">
<proof prover="7"><result status="valid" time="0.05" steps="12"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="12"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.7" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC nlsubst_symbol_in_symbol.7.0" expl="assertion" proved="true">
<proof prover="7"><result status="valid" time="0.08" steps="124"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="91"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.7.1" expl="assertion" proved="true">
<proof prover="7"><result status="valid" time="0.21" steps="99"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="231"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.7.2" expl="assertion" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="48"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="54"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.7.3" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
......@@ -116,13 +116,13 @@
<goal name="VC nlsubst_symbol_in_symbol.8.0" expl="postcondition" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC nlsubst_symbol_in_symbol.8.0.0" expl="VC for nlsubst_symbol_in_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.03" steps="26"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.8.0.1" expl="VC for nlsubst_symbol_in_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.05" steps="49"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="72"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.8.0.2" expl="VC for nlsubst_symbol_in_symbol" proved="true">
<proof prover="7"><result status="valid" time="0.11" steps="64"/></proof>
<proof prover="2"><result status="valid" time="0.11" steps="23"/></proof>
</goal>
<goal name="VC nlsubst_symbol_in_symbol.8.0.3" expl="VC for nlsubst_symbol_in_symbol" proved="true">
<proof prover="0"><result status="valid" time="0.16"/></proof>
......
......@@ -2018,8 +2018,8 @@ module Impl
(const (Var_fo_term (-1)) : int -> (fo_term int int))
identity identity))
(identity) (identity)) ;
let mrv0 = rename_fo_term mv0 identity identity in
let mrv1 = rename_fo_term_list mv1 identity identity in
let ghost mrv0 = rename_fo_term mv0 identity identity in
let ghost mrv1 = rename_fo_term_list mv1 identity identity in
let resv0 =
{ nlrepr_fo_term_field = v0 ;
nlfree_var_symbol_set_abstraction_fo_term_field = fv0 ;
......@@ -2176,8 +2176,8 @@ module Impl
(const (Var_fo_term (-1)) : int -> (fo_term int int))
identity identity))
(identity) (identity)) ;
let mrv0 = rename_symbol mv0 identity in
let mrv1 = rename_fo_term_list mv1 identity identity in
let ghost mrv0 = rename_symbol mv0 identity in
let ghost mrv1 = rename_fo_term_list mv1 identity identity in
let resv0 =
{ nlrepr_symbol_field = v0 ;
nlfree_var_symbol_set_abstraction_symbol_field = fv0 ;
......
......@@ -62,19 +62,15 @@ module Spec
()
end
let rec function rename_fo_term_list (t:fo_term_list 'b0 'b3) (s0:'b0 -> 'c0)
(s3:'b3 -> 'c3) : fo_term_list 'c0 'c3
variant { t }
=
function rename_fo_term_list (t:fo_term_list 'b0 'b3) (s0:'b0 -> 'c0)
(s3:'b3 -> 'c3) : fo_term_list 'c0 'c3 =
match t with | FONil -> FONil
| FOCons v0 v1 ->
FOCons (rename_fo_term v0 s0 s3) (rename_fo_term_list v1 s0 s3)
end
with function rename_fo_term (t:fo_term 'b0 'b3) (s0:'b0 -> 'c0) (s3:'b3 -> 'c3) :
fo_term 'c0 'c3
variant { t }
=
with rename_fo_term (t:fo_term 'b0 'b3) (s0:'b0 -> 'c0) (s3:'b3 -> 'c3) :
fo_term 'c0 'c3 =
match t with | Var_fo_term v0 -> Var_fo_term (s3 v0)
| App v0 v1 -> App (rename_symbol v0 s0) (rename_fo_term_list v1 s0 s3)
end
......
......@@ -2,26 +2,26 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Functions.mlw" proved="true">
<theory name="Func" proved="true">
<goal name="update_eq" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="update_neq" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC compose_associative" expl="VC for compose_associative" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC identity_neutral" expl="VC for identity_neutral" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="100"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC const_compose_left" expl="VC for const_compose_left" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC const_compose_right" expl="VC for const_compose_right" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -2,17 +2,17 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Nat.mlw" proved="true">
<theory name="Nat" proved="true">
<goal name="VC nat_to_int_nonnegative" expl="VC for nat_to_int_nonnegative" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="VC add_nat_simulate_add_int" expl="VC for add_nat_simulate_add_int" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="42"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="74"/></proof>
</goal>
<goal name="one_nat_value" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,20 +2,20 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Predicates.mlw" proved="true">
<theory name="Pred" proved="true">
<goal name="pupdate_eq" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="pupdate_neq" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC pcompose_associative" expl="VC for pcompose_associative" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="VC identity_neutral" expl="VC for identity_neutral" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</theory>
</file>
......
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