diff --git a/examples/MEE-CBC/CBC.eca b/examples/MEE-CBC/CBC.eca index 141b84ed52..919539f18a 100644 --- a/examples/MEE-CBC/CBC.eca +++ b/examples/MEE-CBC/CBC.eca @@ -502,23 +502,24 @@ section Reduce. /\ Compute.qs{2} = (DoubleQuery.qs `|` (fset1 (s + nth witness p i))){1}). wp; rnd (fun x => x + pi{2}); auto=> /> &1 &2 ge0_iP _ _ lt_i_szp. case: (mem DoubleQuery.qs{1} _)=> //=. - split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) + split=> [sR _|_]; 1:smt(addbA addbK addbC add0b). (* TODO: instantiate ring structure *) split=> [|_ r _]; 1:smt (dBlock_uffu). split=> [|_]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) - by split=> [|/#]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) - split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) + split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) + by split=> [|/#]; + split; [congr; congr; smt(addbA addbK addbC add0b) | smt()]. (* TODO: instantiate ring structure *) + split=> [sR _ |_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) split=> [|_ r _]; 1:smt (dBlock_uffu). split=> [|_]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) + split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) split. by move=> h; rewrite -addbA Block.subrr Block.addr0 /= /#. by move=> h; rewrite -addbA Block.subrr Block.addr0 /= /#. wp; rnd (fun x => x + pi{2}). - auto=> /> &2 szp_neq_0; split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) + auto=> /> &2 szp_neq_0; split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) split=> [|_ s _]; 1:smt (dBlock_uffu). split=> [|_]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) + split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) smt (size_ge0). qed. diff --git a/src/ec.ml b/src/ec.ml index 40a8b39e0d..1a1efc5dd4 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -269,11 +269,6 @@ let main () = ["-profile"] else [] in - let iterate = - if input.runo_provers.prvo_iterate then - ["-iterate"] - else [] in - let why3srv = input.runo_provers.prvo_why3server |> omap (fun server -> ["-server"; server]) @@ -311,7 +306,7 @@ let main () = List.flatten [ maxjobs; timeout; cpufactor; ppwidth; provers; quorum ; pragmas ; checkall; - profile; iterate; why3srv ; why3 ; + profile; why3srv ; why3 ; reloc ; noevict; boot ; idirs ; ] in @@ -527,7 +522,7 @@ let main () = Some [State.{ position = 0; goals = None; messages = [] }] else None in - { prvopts = {cmpopts.cmpo_provers with prvo_iterate = true} + { prvopts = cmpopts.cmpo_provers ; input = Some name ; terminal = terminal ; interactive = false @@ -556,7 +551,7 @@ let main () = lazy (T.from_channel ~name ~progress:`Silent ~lastgoals (open_in name)) in - { prvopts = {llmopts.llmo_provers with prvo_iterate = true} + { prvopts = llmopts.llmo_provers ; input = Some name ; terminal = terminal ; interactive = false @@ -594,7 +589,6 @@ let main () = prvo_ppwidth = None; prvo_checkall = false; prvo_profile = false; - prvo_iterate = false; prvo_why3server = None; } in @@ -742,7 +736,6 @@ let main () = EcCommands.cm_provers = state.prvopts.prvo_provers; EcCommands.cm_quorum = state.prvopts.prvo_quorum; EcCommands.cm_profile = state.prvopts.prvo_profile; - EcCommands.cm_iterate = state.prvopts.prvo_iterate; } in let checkproof = not state.docgen in diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 2b08923ea9..e90518ff08 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -846,7 +846,6 @@ type checkmode = { cm_provers : string list option; cm_quorum : int option; cm_profile : bool; - cm_iterate : bool; } let initial ~checkmode ~boot ~checkproof = @@ -858,7 +857,6 @@ let initial ~checkmode ~boot ~checkproof = EcScope.Prover.po_nprovers = Some checkmode.cm_nprovers; EcScope.Prover.po_provers = (checkmode.cm_provers, []); EcScope.Prover.po_quorum = checkmode.cm_quorum; - EcScope.Prover.pl_iterate = Some (checkmode.cm_iterate); } in let perv = (None, (mk_loc _dummy EcCoreLib.i_Pervasive, None), Some `Export) in diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 56440bfa96..7dab0b84b5 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -22,7 +22,6 @@ type checkmode = { cm_provers : string list option; cm_quorum : int option; cm_profile : bool; - cm_iterate : bool; } val initial : checkmode:checkmode -> boot:bool -> checkproof:bool -> EcScope.scope diff --git a/src/ecOptions.ml b/src/ecOptions.ml index d877ccde19..bd21a69aa0 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -65,7 +65,6 @@ and prv_options = { prvo_ppwidth : int option; prvo_checkall : bool; prvo_profile : bool; - prvo_iterate : bool; prvo_why3server : string option; } @@ -410,7 +409,6 @@ let specs = { `Spec ("pragmas" , `String, "Comma-separated list of pragmas"); `Spec ("pp-width" , `Int , "pretty-printing width"); `Spec ("profile" , `Flag , "Collect some profiling informations"); - `Spec ("iterate" , `Flag , "Force to iterate smt call"); `Spec ("server" , `String, "Connect to an external Why3 server"); ]); @@ -535,7 +533,6 @@ let prv_options_of_values ini values = end; prvo_checkall = get_flag "check-all" values; prvo_profile = get_flag "profile" values; - prvo_iterate = get_flag "iterate" values; prvo_why3server = get_string "why3server" values; } diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 0feb9f6162..a5c09b11d9 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -61,7 +61,6 @@ and prv_options = { prvo_ppwidth : int option; prvo_checkall : bool; prvo_profile : bool; - prvo_iterate : bool; prvo_why3server : string option; } diff --git a/src/ecParser.mly b/src/ecParser.mly index 65cd97b95f..8633c13125 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -152,7 +152,6 @@ type smt = [ | `ALL - | `ITERATE | `QUORUM of int | `MAXLEMMAS of int option | `MAXPROVERS of int @@ -198,7 +197,6 @@ "verbose" ; "lazy" ; "full" ; - "iterate" ; "dumpin" ; "selected" ; "debug" ] @@ -258,7 +256,6 @@ | "lazy" -> `VERSION (get_as_none s o; `Lazy) | "full" -> `VERSION (get_as_none s o; `Full) | "all" -> get_as_none s o; (`ALL) - | "iterate" -> get_as_none s o; (`ITERATE) | "selected" -> get_as_none s o; (`SELECTED) | "debug" -> get_as_none s o; (`DEBUG) | _ -> assert false @@ -274,7 +271,6 @@ let unwanted = ref None in let verbose = ref None in let version = ref None in - let iterate = ref None in let dumpin = ref None in let selected = ref None in let debug = ref None in @@ -318,7 +314,6 @@ | `UNWANTEDLEMMAS d -> unwanted := Some d | `VERBOSE v -> verbose := Some v | `VERSION v -> version := Some v - | `ITERATE -> iterate := Some true | `PROVER p -> List.iter add_prover p | `DUMPIN f -> dumpin := Some f | `SELECTED -> selected := Some true @@ -340,7 +335,6 @@ pprov_version = !version; plem_all = !all; plem_max = !mlemmas; - plem_iterate = !iterate; plem_wanted = !wanted; plem_unwanted = !unwanted; plem_dumpin = !dumpin; diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index fa83d6e698..9644cfde65 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -890,7 +890,6 @@ type pprover_infos = { pprov_version : [`Lazy | `Full] option; plem_all : bool option; plem_max : int option option; - plem_iterate : bool option; plem_wanted : pdbhint option; plem_unwanted : pdbhint option; plem_dumpin : string located option; @@ -908,7 +907,6 @@ let empty_pprover = { pprov_version = None; plem_all = None; plem_max = None; - plem_iterate = None; plem_wanted = None; plem_unwanted = None; plem_dumpin = None; diff --git a/src/ecProvers.ml b/src/ecProvers.ml index db618f2443..ccb56bbb24 100644 --- a/src/ecProvers.ml +++ b/src/ecProvers.ml @@ -401,7 +401,6 @@ type prover_infos = { pr_verbose : int; pr_all : bool; pr_max : int; - pr_iterate : bool; pr_wanted : hints; pr_unwanted : hints; pr_dumpin : string EcLocation.located option; @@ -418,7 +417,6 @@ let dft_prover_infos = { pr_quorum = 1; pr_verbose = 0; pr_all = false; - pr_iterate = false; pr_max = 50; pr_wanted = Hints.empty; pr_unwanted = Hints.empty; diff --git a/src/ecProvers.mli b/src/ecProvers.mli index 41481c73ce..d5a8572e93 100644 --- a/src/ecProvers.mli +++ b/src/ecProvers.mli @@ -49,7 +49,6 @@ type prover_infos = { pr_verbose : int; pr_all : bool; pr_max : int; - pr_iterate : bool; pr_wanted : hints; pr_unwanted : hints; pr_dumpin : string EcLocation.located option; diff --git a/src/ecScope.ml b/src/ecScope.ml index d0125b46fc..989174512f 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -641,7 +641,6 @@ module Prover = struct po_verbose : int option; pl_all : bool option; pl_max : int option; - pl_iterate : bool option; pl_wanted : EcProvers.hints option; pl_unwanted : EcProvers.hints option; pl_dumpin : string located option; @@ -659,7 +658,6 @@ module Prover = struct po_verbose = None; pl_all = None; pl_max = None; - pl_iterate = None; pl_wanted = None; pl_unwanted = None; pl_dumpin = None; @@ -700,7 +698,6 @@ module Prover = struct | None , None -> None | None , Some _ -> Some 0 end; - pl_iterate = ppr.plem_iterate; pl_wanted = omap (process_dbhint env) ppr.plem_wanted; pl_unwanted = omap (process_dbhint env) ppr.plem_unwanted; pl_dumpin = ppr.plem_dumpin; @@ -720,7 +717,6 @@ module Prover = struct let pr_verbose = max 0 (odfl dft.pr_verbose options.po_verbose) in let pr_all = odfl dft.pr_all options.pl_all in let pr_max = odfl dft.pr_max options.pl_max in - let pr_iterate = odfl dft.pr_iterate options.pl_iterate in let pr_wanted = odfl dft.pr_wanted options.pl_wanted in let pr_unwanted = odfl dft.pr_unwanted options.pl_unwanted in let pr_selected = odfl dft.pr_selected options.pl_selected in @@ -735,7 +731,7 @@ module Prover = struct in List.fold_left do_ar l (snd options.po_provers) in { pr_maxprocs; pr_provers ; pr_timelimit; pr_cpufactor; - pr_verbose ; pr_all ; pr_max ; pr_iterate ; + pr_verbose ; pr_all ; pr_max ; pr_wanted ; pr_unwanted; pr_selected ; pr_quorum ; pr_dumpin ; gn_debug ; } diff --git a/src/ecScope.mli b/src/ecScope.mli index f3548a3bd1..953041cc2b 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -246,7 +246,6 @@ module Prover : sig po_verbose : int option; pl_all : bool option; pl_max : int option; - pl_iterate : bool option; pl_wanted : EcProvers.hints option; pl_unwanted : EcProvers.hints option; pl_dumpin : string located option; diff --git a/src/ecSmt.ml b/src/ecSmt.ml index b0230936ae..2e523e770c 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -1644,43 +1644,8 @@ let select env pi hyps concl execute_task = else let rs = Frequency.f_ops_goal unwanted_ops hyps.h_local concl in let ri, other = init_relevant env pi rs in - if not pi.P.pr_iterate then begin - ignore (relevant_clause ri other); - (execute_task ri.toadd = Some true) - end else - let other, res = - if List.is_empty ri.toadd then - let other = relevant_clause ri other in - other, execute_task ri.toadd - else other, execute_task ri.toadd in - - match res with Some res -> res | None -> - let rec aux ml other i = - if i <= 0 then begin - ri.ri_max <- max_int; - ri.ri_p <- 0.; - ri.toadd <- []; - let other = relevant_clause ri other in - if List.is_empty ri.toadd then - (execute_task (List.fst other) = Some true) - else - match execute_task ri.toadd with - | None -> (execute_task (List.fst other) = Some true) - | Some res -> res - end else begin - ri.ri_max <- ml; - ri.toadd <- []; - let other = relevant_clause ri other in - let ml = min (2*ml+30) max_int in - if List.is_empty ri.toadd - then aux ml other (i-1) - else - match execute_task ri.toadd with - | None -> aux ml other (i-1) - | Some res -> res - end - - in aux pi.P.pr_max other 4 + ignore (relevant_clause ri other); + (execute_task ri.toadd = Some true) (* -------------------------------------------------------------------- *) let cnt = Counter.create () diff --git a/theories/datatypes/FMap.ec b/theories/datatypes/FMap.ec index 77709be247..5057af41f2 100644 --- a/theories/datatypes/FMap.ec +++ b/theories/datatypes/FMap.ec @@ -440,7 +440,7 @@ proof. by rewrite /filter /"_.[_]" filter_valE SmtMap.offunE. qed. lemma mem_filter (m : ('a,'b) fmap) (p : 'a -> 'b -> bool) x : x \in filter p m <=> x \in m /\ p x (oget m.[x]). -proof. smt(filterE). qed. +proof. by smt(filterE fmapP). qed. lemma get_filter (m : ('a,'b) fmap) (p : 'a -> 'b -> bool) x : x \in filter p m => (filter p m).[x] = m.[x]. @@ -690,7 +690,7 @@ proof. by case _ : (find P m) => // [x /find_some] /#. qed. lemma find_eq_none (p : 'a -> 'b -> bool) (m : ('a,'b) fmap): (forall x, x \in m => !p x (oget m.[x])) => find p m = None. -proof. by move=> np; apply contraT => /find_not_none /#. qed. +proof. by move=> np; apply contraT=> /find_not_none; smt(find_some). qed. (* -------------------------------------------------------------------- *) inductive find_spec (P : 'a -> 'b -> bool) (m : ('a, 'b) fmap) =