From 19a1a07c9753b00541142c2c2ab66fed640d830f Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Wed, 21 Feb 2018 17:32:02 -0500 Subject: [PATCH 1/5] Added clean way to clear the list of current provers. The elements of prover [...] have one of the following forms, where s is a string: s (add s to the use-only list) +s (add include s to the include/exclude list) -s (add exclude s to the include/exclude list) The include/exclude list is ordered, so that later instructions can supersede earlier ones. The use-only list was not ordered, but now is. The relative order of the use-only and include/exclude lists is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover [+"Alt-Ergo" "Z3"] are equivalent. The semantics is that the use-only list is first interpreted (if it's empty, one starts with the current provers as the base), and only then are the instructions of the include/exclude list applied to it, in order. There was already the special use-only instruction "ALL". Now, there is also the use-only instruction "CLEAR", which clears the use-only list, but may be superseded by the use-only instructions that follow. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* a no-op *) prover [+"Z3"] (* adds just "Z3" to whatever current provers are *) prover [-"Z3"] (* removes just "Z3" from whatever current provers are *) prover ["ALL"] (* results in "Z3", "Alt-Ergo" *) prover ["CLEAR"] (* results in nothing *) prover ["CLEAR" +"Z3"] (* results in just "Z3" *) prover [+"Z3" "CLEAR"] (* results in just "Z3" *) prover ["CLEAR" "Z3"] (* result in just "Z3" *) prover ["Z3" "CLEAR"] (* results in nothing *) prover [-"Z3" "ALL"] (* results in "Alt-Ergo" *) prover [+"Z3" "ALL" -"Z3"] (* results in "Alt-Ergo" *) prover [-"Z3" "ALL" +"Z3"] (* results in "Z3", "Alt-Ergo" *) --- src/ecParser.mly | 4 +++- src/ecScope.ml | 12 ++++++++---- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index 136f7475ad..b89b1a5605 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -291,7 +291,9 @@ List.iter do1 os; oiter - (fun r -> pnames := Some { r with pp_add_rm = List.rev r.pp_add_rm }) + (fun r -> + pnames := Some { pp_use_only = List.rev r.pp_use_only; + pp_add_rm = List.rev r.pp_add_rm }) !pnames; { pprov_max = !mprovers; diff --git a/src/ecScope.ml b/src/ecScope.ml index 3c242b8abe..5d3d51808c 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -567,12 +567,16 @@ module Prover = struct match ppr.pprov_names with | None -> None, [] | Some pl -> - let do_uo s = - if s.pl_desc = "ALL" then all_provers () - else [check_prover_name s] in + let do_uo uo s = + match s.pl_desc with + | "ALL" -> all_provers () + | "CLEAR" -> [] + | _ -> + let x = check_prover_name s in + if List.exists ((=) x) uo then uo else x :: uo in let uo = if pl.pp_use_only = [] then None - else Some (List.flatten (List.map do_uo pl.pp_use_only)) in + else Some (List.fold_left do_uo [] pl.pp_use_only) in let do_ar (k,s) = k, check_prover_name s in uo, List.map do_ar pl.pp_add_rm in let verbose = omap (odfl 1) ppr.pprov_verbose in From f43dd302299156c48f1ac039827545d0bccb64c8 Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Thu, 22 Feb 2018 12:20:48 -0500 Subject: [PATCH 2/5] Reworking specification of current provers. All use-only instructions must come first. There are two "universal" use-only instructions: "" (all known provers), and "!" (no provers). It is illegal to mix ""/"!" with prover names (no point in doing so). As before, if the use-only part is empty, it means the currently known provers. The include/exclude instructions are processed in order, acting on the result of the use-only part. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* no-op *) prover [-"Z3"]. (* removes "Z3" from current provers *) prover [+"Z3"]. (* adds "Z3" to current provers *) prover [""]. (* results in "Z3", "Alt-Ergo" *) prover ["!"]. (* results in no provers *) prover ["Z3"]. (* results in "Z3" *) prover ["Z3" "Alt-Ergo"]. (* results in "Z3", "Alt-Ergo" *) prover ["!" +"Z3"]. (* results in "Z3" *) prover ["" -"Z3"]. (* results in "Alt-Ergo" *) --- src/ecParser.mly | 32 ++++++++++++++++++++++++-------- src/ecScope.ml | 4 ++-- 2 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index b89b1a5605..25c24cdc70 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -265,13 +265,31 @@ let iterate = ref None in let selected = ref None in + let is_universal p = unloc p = "" || unloc p = "!" in + + let ok_use_only pp p = + if pp.pp_add_rm <> [] + then let msg = "use-only elements must come at beginning" + in parse_error (loc p) (Some msg) + else if pp.pp_use_only <> [] && is_universal p + then let msg = "cannot add universal to non-empty use-only" + in parse_error (loc p) (Some msg) + else match pp.pp_use_only with + | [q] -> + if is_universal q + then let msg = "use-only part is already universal" + in parse_error (loc p) (Some msg) + else () + | _ -> () in + let add_prover (k, p) = let r = odfl empty_pprover_list !pnames in pnames := Some (match k with - | `Only -> { r with pp_use_only = p :: r.pp_use_only } - | `Include -> { r with pp_add_rm = (`Include, p) :: r.pp_add_rm } - | `Exclude -> { r with pp_add_rm = (`Exclude, p) :: r.pp_add_rm }) in + | `Only -> + (ok_use_only r p; { r with pp_use_only = p :: r.pp_use_only }) + | `Include -> { r with pp_add_rm = (`Include, p) :: r.pp_add_rm } + | `Exclude -> { r with pp_add_rm = (`Exclude, p) :: r.pp_add_rm }) in let do1 o = match o with @@ -290,11 +308,9 @@ List.iter do1 os; - oiter - (fun r -> - pnames := Some { pp_use_only = List.rev r.pp_use_only; - pp_add_rm = List.rev r.pp_add_rm }) - !pnames; + let _ = + let r = odfl empty_pprover_list !pnames in + pnames := Some { r with pp_add_rm = List.rev r.pp_add_rm } in { pprov_max = !mprovers; pprov_timeout = !timeout; diff --git a/src/ecScope.ml b/src/ecScope.ml index 5d3d51808c..2407ff377b 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -569,8 +569,8 @@ module Prover = struct | Some pl -> let do_uo uo s = match s.pl_desc with - | "ALL" -> all_provers () - | "CLEAR" -> [] + | "" -> all_provers () + | "!" -> [] | _ -> let x = check_prover_name s in if List.exists ((=) x) uo then uo else x :: uo in From d8a0e7efa1dbb507e11039c6ae82416456596749 Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Thu, 22 Feb 2018 12:44:03 -0500 Subject: [PATCH 3/5] Fixed poor spacing. --- src/ecParser.mly | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index 25c24cdc70..a7838920ee 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -287,7 +287,7 @@ pnames := Some (match k with | `Only -> - (ok_use_only r p; { r with pp_use_only = p :: r.pp_use_only }) + (ok_use_only r p; { r with pp_use_only = p :: r.pp_use_only }) | `Include -> { r with pp_add_rm = (`Include, p) :: r.pp_add_rm } | `Exclude -> { r with pp_add_rm = (`Exclude, p) :: r.pp_add_rm }) in From e5e94a40a6d7d5b9214357f0346ac9f993b478ee Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Thu, 22 Feb 2018 13:54:57 -0500 Subject: [PATCH 4/5] Fixed mistake wrt oiter. --- src/ecParser.mly | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index a7838920ee..93af2b5dd5 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -308,9 +308,9 @@ List.iter do1 os; - let _ = - let r = odfl empty_pprover_list !pnames in - pnames := Some { r with pp_add_rm = List.rev r.pp_add_rm } in + oiter + (fun r -> pnames := Some { r with pp_add_rm = List.rev r.pp_add_rm }) + !pnames; { pprov_max = !mprovers; pprov_timeout = !timeout; From 650baefe039a05023a0ea51cc78924aafcc62100 Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Tue, 27 Feb 2018 19:27:07 -0500 Subject: [PATCH 5/5] Fixed bug in SMT option matching. The third stage of filtering in the definition of option_matching had a bug, meaning that attempts to rely on it resulted in assertion failures. But that last stage - disambiguating from right to left - was arguably hard for users to predict, anyway. So, fixed the third stage, but left it out of algorithm. (If it's really desired, easy to put it back in, as now it'll work. But do we really think users will understand why, e.g., [prover x=1] means [prover maxlemmas=1] - because the x in maxlemmas comes earlier when working backward as opposed to the x in maxprovers?) This is how option disambiguation works: First filter-in those option names having the letters of the abbreviation abv in the correct order. Then work through the letters of abv in order, keeping only those option names in which each successive letter appears as early as possible --- src/ecParser.mly | 2 +- src/ecUtils.ml | 8 +++----- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index 93af2b5dd5..8762fbce6d 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3267,7 +3267,7 @@ smt_info: smt_info1: | t=word - { `MAXLEMMAS (Some t) } + { `MAXLEMMAS (Some t) } | TIMEOUT EQ t=word { `TIMEOUT t } diff --git a/src/ecUtils.ml b/src/ecUtils.ml index 7528a02879..bba47f8ad7 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -642,18 +642,16 @@ module String = struct then List.map fst matched else aux matched (i+1) end - in aux matched 0 let last_matching tomatch s = - first_matching (List.map rev tomatch) (rev s) + List.map rev (first_matching (List.map rev tomatch) (rev s)) end let option_matching tomatch s = match OptionMatching.all_matching tomatch s with - | [s] -> [s] | matched -> - match OptionMatching.first_matching matched s with - | [s] -> [s] | matched -> OptionMatching.last_matching matched s + | [s] -> [s] + | matched -> OptionMatching.first_matching matched s end (* -------------------------------------------------------------------- *)