Commit d3625e5c authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'bugfix/v0.87'

parents ca0251f6 3608ecd5
......@@ -20,6 +20,8 @@ ifeq ($(BENCH),yes)
endif
MLWUTIL=Nat
MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
Firstorder_formula_impl Firstorder_formula_list_impl \
Firstorder_tableau_impl Unification FormulaTransformations \
......@@ -28,9 +30,10 @@ MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
MLWIMPL=$(MLWTYPES) ProverMain ProverTest
BD=build
MLUTIL=$(patsubst %,$(BD)/%__Nat,$(MLWUTIL))
MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLWTYPES))
MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLWIMPL))
MLALL=$(MLTYPES) $(MLIMPL)
MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
ML=$(patsubst %,%.ml,$(MLALL))
CMX=$(patsubst %,%.cmx,$(MLALL))
OCAMLC=ocamlopt.opt
......
......@@ -307,8 +307,8 @@ module Impl
&& eval rho.unifier y = Var_fo_term y
&& st tm rho.unifier = Var_fo_term y
&& is_fo_term_free_var_in_fo_term y (st tm rho.unifier)) && y >= 0 } ;
let by = BA.get rhob y in
match by with
let by' = BA.get rhob y in
match by' with
| Nil -> bottomvar rhob rho y ;
if x = y
then raise UnificationFailure
......@@ -902,18 +902,18 @@ module Impl
assert { st bxm rhoi' = sc rhobm rhoi' x
= rhoi' x = st t1m rhoi' && st bxm rhoi' = st t1m rhoi' } ;
res
| _ -> let by = BA.get rhob y in
match by with
| Cons (Assign by) _ -> (*checkit rho y it2 ;*)
let bym = by.model_fo_term_field in
| _ -> let by' = BA.get rhob y in
match by' with
| Cons (Assign by') _ -> (*checkit rho y it2 ;*)
let bym = by'.model_fo_term_field in
let rhobm = rho.unifier_base_model in
let rhoi = rho.unifier in
assert { sdata_inv (Assign by) } ;
assert { sdata_inv (Assign by') } ;
assert { bym = rhobm y (*/\ mem y fv*) } ;
assert { st bym rhoi = sc rhobm rhoi y = rhoi y = st t2m rhoi
&& forall s:func int (fo_term int int).
st bym (sc rhoi s) = st t2m (sc rhoi s) } ;
let res = unification_term t1 by lv rhob rho lp (*fv s it1 (it2-1)*) in
let res = unification_term t1 by' lv rhob rho lp (*fv s it1 (it2-1)*) in
let rhoi' = res.final_unifier.unifier in
assert { st bym rhoi' = sc rhobm rhoi' y
= rhoi' y = st t2m rhoi' && st bym rhoi' = st t2m rhoi' } ;
......
......@@ -2,37 +2,38 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Isabelle" version="2015" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC4" version="1.2" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="2" name="Zenon" version="0.8.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="4" name="Eprover" version="1.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="2.19" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC3" version="2.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="8" name="Eprover" version="1.4" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="9" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="10" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="11" name="Simplify" version="1.5.4" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="12" name="Yices" version="1.0.38" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="13" name="Zenon" version="0.7.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="14" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="15" name="Metis" version="2.3" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="16" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="17" name="Alt-Ergo" version="0.95.2" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="18" name="PVS" version="6.0" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="19" name="veriT" version="201310" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="20" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="21" name="CVC4" version="1.3" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="22" name="Vampire" version="0.6" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="24" name="veriT" version="201410" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="27" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="0" name="Isabelle" version="2015" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="60" steplimit="1" memlimit="1000"/>
<prover id="2" name="Zenon" version="0.8.0" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="4" name="Eprover" version="1.6" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="5" name="Z3" version="2.19" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="CVC3" version="2.2" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="8" name="Eprover" version="1.4" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="9" name="Spass" version="3.7" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="10" name="Z3" version="4.3.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="11" name="Simplify" version="1.5.4" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="12" name="Yices" version="1.0.38" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="13" name="Zenon" version="0.7.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="14" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="15" name="Metis" version="2.3" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="16" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="17" name="Alt-Ergo" version="0.95.2" timelimit="60" steplimit="1" memlimit="1000"/>
<prover id="18" name="PVS" version="6.0" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="19" name="veriT" version="201310" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="20" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="21" name="CVC4" version="1.3" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="22" name="Vampire" version="0.6" timelimit="3" steplimit="1" memlimit="1000"/>
<prover id="23" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="24" name="veriT" version="201410" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="27" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="29" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../genealogy.why" expanded="true">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
<goal name="Child_is_son_or_daughter">
<proof prover="0" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="6.55"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -59,6 +60,7 @@
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="27" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="Sibling_sym">
<proof prover="0" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="7.12"/></proof>
......@@ -86,6 +88,7 @@
<proof prover="25"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="Sibling_is_brother_or_sister">
<proof prover="0" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="7.32"/></proof>
......@@ -111,6 +114,7 @@
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.01"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="Grandparent_is_grandfather_or_grandmother">
<proof prover="0" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="7.48"/></proof>
......@@ -137,6 +141,7 @@
<proof prover="25"><result status="valid" time="0.00" steps="38"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="36"/></proof>
</goal>
<goal name="Grandfather_male">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......@@ -163,6 +168,7 @@
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="Grandmother_female">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -189,6 +195,7 @@
<proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.00"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="Only_two_grandfathers">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -215,6 +222,7 @@
<proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="26"><result status="valid" time="0.02"/></proof>
<proof prover="28"><result status="valid" time="0.01"/></proof>
<proof prover="29"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
</theory>
</file>
......
[ATP alt-ergo-prv]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-1.30"
exec = "alt-ergo-1.20.prv"
exec = "alt-ergo-1.10.prv"
exec = "alt-ergo-1.00.prv"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$"
version_ok = "1.30"
version_ok = "1.20.prv"
version_old = "1.10.prv"
version_old = "1.00.prv"
......
......@@ -168,6 +168,8 @@ module Translate = struct
open Decl
let type_unit = ML.Ttuple []
let rec type_ info ty = match ty.ty_node with
| Tyvar v ->
ML.Tvar v.tv_name
......@@ -458,7 +460,10 @@ module Translate = struct
| _ -> assert false
let pv_name pv = pv.pv_vs.vs_name
let pvty info pv = vsty info pv.pv_vs
let pvty info pv =
if pv.pv_ghost then (pv.pv_vs.vs_name, type_unit)
else vsty info pv.pv_vs
let lv_name = function
| LetV pv -> pv_name pv
......@@ -473,12 +478,20 @@ module Translate = struct
| _ -> true
let filter_ghost_params =
(* removal of ghost does not work
let dummy = create_pvsymbol (Ident.id_fresh "") ity_unit in
fun args ->
match List.filter (fun v -> not v.Mlw_ty.pv_ghost) args with
| [] -> [dummy]
| l -> l
*)
fun args -> args (* filtering ghost happens in pvty *)
(*
List.map
(fun v -> if v.Mlw_ty.pv_ghost then
create_pvsymbol (Ident.id_fresh "") ity_unit
else v)
*)
let rec expr info e =
assert (not e.e_ghost);
match e.e_node with
......@@ -499,6 +512,7 @@ module Translate = struct
let n = Number.compute_int (get_int_constant e1) in
let e1 = ML.Esyntax (BigInt.to_string n, []) in
ML.Esyntax (s, [e1])
(*
| Eapp (e, v, _) when v.pv_ghost ->
(* ghost parameters are ignored *)
begin
......@@ -506,10 +520,13 @@ module Translate = struct
| Eapp _ -> expr info e
| _ -> ML.Eapp (expr info e, [ML.enop])
end
*)
| Eapp (e, v, _) ->
ML.Eapp (expr info e, [ML.Eident (pv_name v)])
| Elet ({ let_expr = e1 }, e2) when e1.e_ghost ->
expr info e2
| Elet ({ let_sym = lv; let_expr = e1 }, e2) when e1.e_ghost ->
(* TODO: remove superflous let *)
ML.Elet (lv_name lv, ML.enop, expr info e2)
| Elet ({ let_sym = LetV pv }, e2) when ity_equal pv.pv_ity ity_mark ->
expr info e2
| Elet ({ let_sym = LetV pv; let_expr = e1 }, e2) when is_underscore pv ->
......
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