Commit 04189cd4 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'negative_literals' into new_system

parents e16f23b8 e515b07c
......@@ -24,6 +24,8 @@ transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "eliminate_literal"
transformation "eliminate_negative_constants"
transformation "simplify_formula"
......@@ -34,4 +36,3 @@ theory BuiltIn
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
......@@ -7,7 +7,7 @@
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../12475.why" expanded="true">
<theory name="Stmt" sum="f2e23bc6c52360c346f78a5be969b6b4" expanded="true">
<theory name="Stmt" sum="875cae0dd4a2795d1efc5e3e1180b734" expanded="true">
<goal name="toto" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="3" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -12,7 +12,7 @@
<file name="../agatha.why" expanded="true">
<theory name="Agatha" sum="65caf34afba9724ec20c2e4ca302503d" expanded="true">
<goal name="Diff1" expanded="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="4"><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.00" steps="5"/></proof>
......@@ -21,7 +21,7 @@
<proof prover="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Diff2" expanded="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="4"><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.01" steps="6"/></proof>
......@@ -30,7 +30,7 @@
<proof prover="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Diff3" expanded="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01" steps="7"/></proof>
......@@ -39,7 +39,7 @@
<proof prover="10"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Enigma" expanded="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="0"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
......
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="9" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
......@@ -16,8 +16,8 @@
</theory>
<theory name="Example" sum="befcd266c1f484dfa381084b8131ba5c" expanded="true">
<goal name="G1">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.02"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -27,19 +27,19 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G2">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.02"/></proof>
<proof prover="9"><result status="valid" time="0.06"/></proof>
<proof prover="10" timelimit="10"><result status="valid" time="0.03" steps="45"/></proof>
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="1.32"/></proof>
<proof prover="12"><result status="valid" time="2.09"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="G5b">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></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.01"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -49,8 +49,8 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5c">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
......@@ -59,30 +59,30 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.05"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.47"/></proof>
<proof prover="12"><result status="valid" time="0.73"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="G3">
<proof prover="6" timelimit="9"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.03"/></proof>
<proof prover="9"><result status="valid" time="0.07"/></proof>
<proof prover="11"><result status="valid" time="0.17"/></proof>
<proof prover="12"><result status="valid" time="0.85"/></proof>
<proof prover="11"><result status="valid" time="0.34"/></proof>
<proof prover="12"><result status="valid" time="1.31"/></proof>
</goal>
<goal name="G4">
<proof prover="2"><result status="valid" time="0.53"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.82"/></proof>
<proof prover="6" timelimit="7"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.07"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.83"/></proof>
<proof prover="11"><result status="valid" time="0.13"/></proof>
<proof prover="12"><result status="valid" time="1.37"/></proof>
<proof prover="13"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
......@@ -90,7 +90,7 @@
</theory>
<theory name="Example2" sum="ab79d277a8f71ff7d72600bdefbe809e" expanded="true">
<goal name="G1">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="6"><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.00"/></proof>
......@@ -107,7 +107,7 @@
<proof prover="13" memlimit="1000"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="G5b">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><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>
<proof prover="9"><result status="valid" time="0.00"/></proof>
......@@ -116,7 +116,7 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5c">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><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.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......@@ -125,7 +125,7 @@
<proof prover="13"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G5">
<proof prover="5"><result status="valid" time="0.00"/></proof>
<proof prover="0"><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.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
......@@ -135,8 +135,8 @@
</goal>
<goal name="G3">
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.03"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.14"/></proof>
<proof prover="9"><result status="valid" time="0.14"/></proof>
<proof prover="11"><result status="valid" time="0.04"/></proof>
<proof prover="12"><result status="valid" time="0.00"/></proof>
</goal>
......
......@@ -5,9 +5,9 @@
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../real.why" expanded="true">
<theory name="CosineSingle" sum="97f9e06974199fb947370814aa2ff134" expanded="true">
<theory name="CosineSingle" sum="7dae6c2648a23c62f67c4fd7bc4654d3" expanded="true">
<goal name="MethodError" expanded="true">
<proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="1.82"/></proof>
<proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="1.31"/></proof>
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
</theory>
......
......@@ -98,7 +98,7 @@
</theory>
<theory name="HdTlNoOpt" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="NthHdTl" sum="3d14df5fb64a9db0c86e94f99cbc6759">
<theory name="NthHdTl" sum="2df5f3b79d8ce9a9de7c60035dab5135">
<goal name="Nth_tl">
<proof prover="6"><result status="valid" time="0.00" steps="21"/></proof>
</goal>
......@@ -153,7 +153,7 @@
<proof prover="6"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="mem_decomp.1.2" expl="2.">
<proof prover="3"><result status="valid" time="0.83"/></proof>
<proof prover="3"><result status="valid" time="0.59"/></proof>
</goal>
</transf>
</goal>
......@@ -345,7 +345,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="63"/></proof>
</goal>
<goal name="rev_append_sorted_incr.1.7" expl="7.">
<proof prover="6"><result status="valid" time="1.58" steps="2697"/></proof>
<proof prover="6"><result status="valid" time="0.94" steps="2697"/></proof>
</goal>
<goal name="rev_append_sorted_incr.1.8" expl="8.">
<proof prover="4"><result status="valid" time="1.59"/></proof>
......@@ -377,7 +377,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="rev_append_sorted_decr.1.7" expl="7.">
<proof prover="6"><result status="valid" time="1.47" steps="2409"/></proof>
<proof prover="6"><result status="valid" time="1.13" steps="2409"/></proof>
</goal>
<goal name="rev_append_sorted_decr.1.8" expl="8.">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -462,7 +462,7 @@
<proof prover="6"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="Permut_length">
<proof prover="7" edited="list_Permut_Permut_length_2.v"><result status="valid" time="2.14"/></proof>
<proof prover="7" edited="list_Permut_Permut_length_2.v"><result status="valid" time="1.54"/></proof>
</goal>
</theory>
<theory name="Distinct" sum="12ed45bbf4afe5f5deaa62646cbf49f3">
......
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coq-interval.why" expanded="true">
<theory name="P" sum="c76b54c1e6453d33af15a42fd9489845" expanded="true">
<theory name="P" sum="7f6fe6b31b02a544c60045c0aec7b149" expanded="true">
<goal name="pow_eps2_max_int" expanded="true">
<proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="1.21"/></proof>
<proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="0.80"/></proof>
</goal>
</theory>
</file>
......
......@@ -17,7 +17,7 @@
<proof prover="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="P3" sum="6c869b810ccce7e54679d67b1e628afa" expanded="true">
<theory name="P3" sum="6963eeaec55244f198b193c068311ae7" expanded="true">
<goal name="cos_bound" expanded="true">
<proof prover="1"><result status="timeout" time="5.20"/></proof>
</goal>
......@@ -42,9 +42,9 @@
<proof prover="1"><result status="unknown" time="0.23"/></proof>
</goal>
</theory>
<theory name="PolyPaverExamples" sum="610ebe5089f186069f185ce34e8d16b6" expanded="true">
<theory name="PolyPaverExamples" sum="a06fb800674a994e8bf9b744d8665392" expanded="true">
<goal name="g1" expanded="true">
<proof prover="1"><result status="unknown" time="0.24"/></proof>
<proof prover="1"><result status="unknown" time="0.39"/></proof>
</goal>
</theory>
</file>
......
......@@ -45,7 +45,7 @@ let deref_id ~loc id =
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (mixfix ~loc "[]<-", [a; i; v]))
let constant ~loc s =
mk_expr ~loc (Econst (Number.ConstInt (Number.int_const_dec s)))
mk_expr ~loc (Econst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec s})))
let len ~loc =
Qident (mk_id ~loc "len")
let break ~loc =
......
......@@ -307,7 +307,7 @@ term_arg: mk_term(term_arg_) { $1 }
term_arg_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst (Number.ConstInt ((Number.int_const_dec $1))) }
| INTEGER { Tconst (Number.(ConstInt { ic_negative = false ; ic_abs = int_const_dec $1})) }
| NONE { Ttuple [] }
| TRUE { Ttrue }
| FALSE { Tfalse }
......
......@@ -94,11 +94,13 @@ let print_type info fmt ty = try print_type info fmt ty
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = false;
Number.negative_int_support = Number.Number_default;
Number.dec_int_support = Number.Number_default;
Number.hex_int_support = Number.Number_unsupported;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
Number.def_int_support = Number.Number_unsupported;
Number.negative_real_support = Number.Number_default;
Number.dec_real_support = Number.Number_default;
Number.hex_real_support = Number.Number_unsupported;
Number.frac_real_support = Number.Number_custom
......
......@@ -285,7 +285,7 @@ let rec ty denv env impl { e_loc = loc; e_node = n } = match n with
| Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
let t_int_const s =
t_const (Number.ConstInt (Number.int_const_dec s)) ty_int
t_const (Number.(ConstInt { ic_negative = false; ic_abs = int_const_dec s})) ty_int
(* unused
let t_real_const r = t_const (Number.ConstReal r)
......@@ -308,8 +308,8 @@ let rec term denv env impl { e_loc = loc; e_node = n } = match n with
find_dobj ~loc denv env impl s
| Enum (Nint s) -> t_int_const s
| Enum (Nreal (i,f,e)) ->
t_const (Number.ConstReal
(Number.real_const_dec i (Opt.get_def "0" f) e)) ty_real
t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec i (Opt.get_def "0" f) e})) ty_real
| Enum (Nrat (n,d)) ->
let n = t_int_const n and d = t_int_const d in
let frac = ns_find_ls denv.th_rat.th_export ["frac"] in
......
......@@ -524,25 +524,26 @@ let rec tr_positive p = match kind_of_term p with
| _ ->
raise NotArithConstant
let const_of_big_int b =
let const_of_big_int is_neg b =
Term.t_const
(Number.ConstInt (Number.int_const_dec (Big_int.string_of_big_int b)))
(Number.(ConstInt { ic_negative = is_neg ;
ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
ty_int
(* translates a closed Coq term t:Z or R into a FOL term of type int or real *)
let rec tr_arith_constant dep t = match kind_of_term t with
| Construct _ when is_global coq_Z0 t -> Term.t_nat_const 0
| App (f, [|a|]) when is_global coq_Zpos f ->
const_of_big_int (tr_positive a)
const_of_big_int false (tr_positive a)
| App (f, [|a|]) when is_global coq_Zneg f ->
let t = const_of_big_int (tr_positive a) in
let fs = why_constant_int dep ["prefix -"] in
Term.fs_app fs [t] Ty.ty_int
const_of_big_int true (tr_positive a)
| Const _ when is_global coq_R0 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "0" "0" None))
Term.t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec "0" "0" None }))
ty_real
| Const _ when is_global coq_R1 t ->
Term.t_const (Number.ConstReal (Number.real_const_dec "1" "0" None))
Term.t_const (Number.(ConstReal { rc_negative = false ;
rc_abs = real_const_dec "1" "0" None}))
ty_real
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
(* let ta = tr_arith_constant a in *)
......
......@@ -254,6 +254,7 @@ let syntax_arguments_typed =
let syntax_range_literal s fmt c =
let f s b e fmt =
let v = Number.compute_int_literal c.Number.ic_abs in
let base = match s.[e-1] with
| 'x' -> 16
| 'd' -> 10
......@@ -267,8 +268,20 @@ let syntax_range_literal s fmt c =
else
None
in
let v = Number.compute_int c in
Number.print_in_base base digits fmt v
if base = 10 then begin
if c.Number.ic_negative then fprintf fmt "-";
Number.print_in_base base digits fmt v
end
else
let v =
if c.Number.ic_negative then
match digits with
| Some d ->
BigInt.sub (BigInt.pow_int_pos base d) v
| None -> failwith ("number of digits must be given for printing negative literals in base " ^ string_of_int base)
else v
in
Number.print_in_base base digits fmt v
in
global_substitute_fmt opt_search_forward_literal_format f s fmt
......@@ -287,9 +300,10 @@ let syntax_float_literal s fp fmt c =
else
None
in
let e,m = Number.compute_float c fp in
let e,m = Number.compute_float c.Number.rc_abs fp in
let sg = if c.Number.rc_negative then BigInt.one else BigInt.zero in
match s.[b] with
| 's' -> Number.print_in_base base digits fmt BigInt.zero
| 's' -> Number.print_in_base base digits fmt sg
| 'e' -> Number.print_in_base base digits fmt e
| 'm' -> Number.print_in_base base digits fmt m
| _ -> assert false
......
......@@ -822,7 +822,13 @@ let fs_app fs tl ty = t_app fs tl (Some ty)
let ps_app ps tl = t_app ps tl None
let t_nat_const n =
t_const (Number.ConstInt (Number.int_const_dec (string_of_int n))) ty_int
assert (n >= 0);
let a =
Number.{ic_negative = false ; ic_abs = int_const_dec (string_of_int n)}
in
t_const (Number.ConstInt a) ty_int
let t_bigint_const n = t_const (Number.const_of_big_int n) Ty.ty_int
exception InvalidLiteralType of ty
......@@ -831,14 +837,14 @@ let check_literal c ty =
| Tyapp (ts,[]) -> ts
| _ -> raise (InvalidLiteralType ty) in
match c with
| Number.ConstInt c when not (ts_equal ts ts_int) ->
| Number.ConstInt n when not (ts_equal ts ts_int) ->
begin match ts.ts_def with
| Range ir -> Number.check_range c ir
| Range ir -> Number.(check_range n ir)
| _ -> raise (InvalidLiteralType ty)
end
| Number.ConstReal c when not (ts_equal ts ts_real) ->
| Number.ConstReal x when not (ts_equal ts ts_real) ->
begin match ts.ts_def with
| Float fp -> Number.check_float c fp
| Float fp -> Number.(check_float x.Number.rc_abs fp)
| _ -> raise (InvalidLiteralType ty)
end
| _ -> ()
......
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