--- a/src/HOL/SMT.thy Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/SMT.thy Mon Feb 07 15:26:22 2022 +0100
@@ -676,18 +676,19 @@
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
solvers are fully trusted without additional checks. The following
option can cause the SMT solver to run in proof-producing mode, giving
-a checkable certificate. This is currently only implemented for Z3.
+a checkable certificate. This is currently implemented only for veriT and
+Z3.
\<close>
declare [[smt_oracle = false]]
text \<open>
-Each SMT solver provides several commandline options to tweak its
+Each SMT solver provides several command-line options to tweak its
behaviour. They can be passed to the solver by setting the following
options.
\<close>
-declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
+declare [[cvc4_options = ""]]
declare [[verit_options = ""]]
declare [[z3_options = ""]]
--- a/src/HOL/Tools/SMT/smt_config.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Feb 07 15:26:22 2022 +0100
@@ -115,7 +115,7 @@
|> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
(Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
(Thm.declaration_attribute o K o set_solver_options o pair name))
- ("additional command line options for SMT solver " ^ quote name))
+ ("additional command-line options for SMT solver " ^ quote name))
fun all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt)))
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Feb 07 15:26:22 2022 +0100
@@ -21,7 +21,7 @@
command: unit -> string list,
options: Proof.context -> string list,
smt_options: (string * string) list,
- good_slices: (int * string) list,
+ good_slices: ((int * string) * string list) list,
outcome: string -> string list -> outcome * string list,
parse_proof: (Proof.context -> SMT_Translate.replay_data ->
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
@@ -30,11 +30,11 @@
(*registry*)
val add_solver: solver_config -> theory -> theory
- val good_slices: Proof.context -> string -> (int * string) list
+ val good_slices: Proof.context -> string -> ((int * string) * string list) list
(*filter*)
val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list ->
- int -> Time.time -> parsed_proof
+ int -> Time.time -> string list -> parsed_proof
(*tactic*)
val smt_tac: Proof.context -> thm list -> int -> tactic
@@ -124,9 +124,9 @@
in
-fun invoke name command smt_options ithms ctxt =
+fun invoke name command options smt_options ithms ctxt =
let
- val options = SMT_Config.solver_options_of ctxt
+ val options = options @ SMT_Config.solver_options_of ctxt
val comments = [space_implode " " options]
val (str, replay_data as {context = ctxt', ...}) =
@@ -155,7 +155,7 @@
command: unit -> string list,
options: Proof.context -> string list,
smt_options: (string * string) list,
- good_slices: (int * string) list,
+ good_slices: ((int * string) * string list) list,
outcome: string -> string list -> outcome * string list,
parse_proof: (Proof.context -> SMT_Translate.replay_data ->
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
@@ -180,7 +180,7 @@
type solver_info = {
command: unit -> string list,
smt_options: (string * string) list,
- good_slices: (int * string) list,
+ good_slices: ((int * string) * string list) list,
parse_proof: Proof.context -> SMT_Translate.replay_data ->
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
parsed_proof,
@@ -252,13 +252,13 @@
val thms = map (check_topsort ctxt) thms0
val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt
val (output, replay_data) =
- invoke name command smt_options (SMT_Normalize.normalize ctxt thms) ctxt
+ invoke name command [] smt_options (SMT_Normalize.normalize ctxt thms) ctxt
in replay ctxt replay_data output end
(* filter (for Sledgehammer) *)
-fun smt_filter ctxt0 goal xfacts i time_limit =
+fun smt_filter ctxt0 goal xfacts i time_limit options =
let
val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit)
@@ -276,7 +276,7 @@
val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt
val (output, replay_data) =
- invoke name command smt_options (SMT_Normalize.normalize ctxt thms') ctxt
+ invoke name command options smt_options (SMT_Normalize.normalize ctxt thms') ctxt
in
parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
end
--- a/src/HOL/Tools/SMT/smt_systems.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Mon Feb 07 15:26:22 2022 +0100
@@ -96,12 +96,13 @@
smt_options = [(":produce-unsat-cores", "true")],
good_slices =
(* FUDGE *)
- [(512, meshN),
- (64, meshN),
- (1024, meshN),
- (256, mepoN),
- (32, meshN),
- (128, meshN)],
+ [((512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+ ((64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+ ((1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+ ((256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+ ((32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+ ((128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+ ((256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
replay = NONE }
@@ -140,12 +141,12 @@
smt_options = [(":produce-proofs", "true")],
good_slices =
(* FUDGE *)
- [(1024, meshN),
- (512, mashN),
- (64, meshN),
- (128, meshN),
- (256, mepoN),
- (32, meshN)],
+ [((1024, meshN), []),
+ ((512, mashN), []),
+ ((64, meshN), []),
+ ((128, meshN), []),
+ ((256, mepoN), []),
+ ((32, meshN), [])],
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"),
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = SOME Verit_Replay.replay }
@@ -181,12 +182,12 @@
smt_options = [(":produce-proofs", "true")],
good_slices =
(* FUDGE *)
- [(1024, meshN),
- (512, mepoN),
- (64, meshN),
- (256, meshN),
- (128, mashN),
- (32, meshN)],
+ [((1024, meshN), []),
+ ((512, mepoN), []),
+ ((64, meshN), []),
+ ((256, meshN), []),
+ ((128, mashN), []),
+ ((32, meshN), [])],
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME Z3_Replay.parse_proof,
replay = SOME Z3_Replay.replay }
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 07 15:26:22 2022 +0100
@@ -314,9 +314,11 @@
original @ shifted_once @ shifted_twice
end
- fun adjust_extra (format0, type_enc0, lam_trans0, uncurried_aliases0, extra_extra0) =
- (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans,
- the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
+ fun adjust_extra (ATP_Slice (format0, type_enc0, lam_trans0, uncurried_aliases0,
+ extra_extra0)) =
+ ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans,
+ the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
+ | adjust_extra (extra as SMT_Slice _) = extra
fun adjust_slice ((num_facts0, fact_filter0), extra) =
let
@@ -324,7 +326,7 @@
val max_facts = max_facts |> the_default num_facts0
val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
in
- ((num_facts, fact_filter), Option.map adjust_extra extra)
+ ((num_facts, fact_filter), adjust_extra extra)
end
val provers = distinct (op =) schedule
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 07 15:26:22 2022 +0100
@@ -63,7 +63,11 @@
factss : (string * fact list) list,
found_proof : string -> unit}
- type prover_slice = base_slice * atp_slice option
+ datatype prover_slice_extra =
+ ATP_Slice of atp_slice
+ | SMT_Slice of string list
+
+ type prover_slice = base_slice * prover_slice_extra
type prover_result =
{outcome : atp_failure option,
@@ -176,7 +180,11 @@
factss : (string * fact list) list,
found_proof : string -> unit}
-type prover_slice = base_slice * atp_slice option
+datatype prover_slice_extra =
+ ATP_Slice of atp_slice
+| SMT_Slice of string list
+
+type prover_slice = base_slice * prover_slice_extra
type prover_result =
{outcome : atp_failure option,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 07 15:26:22 2022 +0100
@@ -111,7 +111,7 @@
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val ((good_max_facts, good_fact_filter), SOME (good_format, good_type_enc, good_lam_trans,
+ val ((good_max_facts, good_fact_filter), ATP_Slice (good_format, good_type_enc, good_lam_trans,
good_uncurried_aliases, extra)) = slice
val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 07 15:26:22 2022 +0100
@@ -63,9 +63,9 @@
fun get_slices ctxt name =
let val thy = Proof_Context.theory_of ctxt in
if is_atp name then
- map (apsnd SOME) (#good_slices (get_atp thy name ()) ctxt)
+ map (apsnd ATP_Slice) (#good_slices (get_atp thy name ()) ctxt)
else if is_smt_prover ctxt name then
- map (rpair NONE) (SMT_Solver.good_slices ctxt name)
+ map (apsnd SMT_Slice) (SMT_Solver.good_slices ctxt name)
else
error ("No such prover: " ^ name)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Feb 04 10:48:49 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 07 15:26:22 2022 +0100
@@ -70,7 +70,7 @@
not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT])
fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances,
- type_enc, slices, timeout, ...} : params) state goal i facts =
+ type_enc, slices, timeout, ...} : params) state goal i facts options =
let
val run_timeout = slice_timeout slices timeout
val (higher_order, nat_as_int) =
@@ -100,7 +100,7 @@
val birth = Timer.checkRealTimer timer
val filter_result as {outcome, ...} =
- SMT_Solver.smt_filter ctxt goal facts i run_timeout
+ SMT_Solver.smt_filter ctxt goal facts i run_timeout options
handle exn =>
if Exn.is_interrupt exn orelse debug then
Exn.reraise exn
@@ -121,13 +121,13 @@
let
val ctxt = Proof.context_of state
- val ((best_max_facts, best_fact_filter), _) = slice
+ val ((best_max_facts, best_fact_filter), SMT_Slice options) = slice
val effective_fact_filter = fact_filter |> the_default best_fact_filter
val facts = take best_max_facts (facts_of_filter effective_fact_filter factss)
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
- smt_filter name params state goal subgoal facts
+ smt_filter name params state goal subgoal facts options
val used_facts =
(case fact_ids of
NONE => map fst used_from