Remove the iterate SMT option

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.
 

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

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

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

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;
     }
 

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;
 }
 

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;

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;

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;

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;

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   ; }

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;

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 ()

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) =