--- a/src/HOL/SMT.thy Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/SMT.thy Sat Apr 25 09:48:06 2015 +0200
@@ -49,7 +49,7 @@
*}
method_setup moura = {*
- Scan.succeed (SIMPLE_METHOD' o moura_tac)
+ Scan.succeed (SIMPLE_METHOD' o moura_tac)
*} "solve skolemization goals, especially those arising from Z3 proofs"
hide_fact (open) choices bchoices
--- a/src/HOL/Tools/SMT/cvc4_proof_parse.ML Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/Tools/SMT/cvc4_proof_parse.ML Sat Apr 25 09:48:06 2015 +0200
@@ -15,29 +15,32 @@
struct
fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output =
- let
- val num_ll_defs = length ll_defs
+ if exists (String.isPrefix "(error \"This build of CVC4 doesn't have proof support") output then
+ {outcome = NONE, fact_ids = NONE, atp_proof = K []}
+ else
+ let
+ val num_ll_defs = length ll_defs
- val id_of_index = Integer.add num_ll_defs
- val index_of_id = Integer.add (~ num_ll_defs)
+ val id_of_index = Integer.add num_ll_defs
+ val index_of_id = Integer.add (~ num_ll_defs)
- val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output
- val used_assm_js =
- map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
- used_assert_ids
+ val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output
+ val used_assm_js =
+ map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
+ used_assert_ids
- val conjecture_i = 0
- val prems_i = conjecture_i + 1
- val num_prems = length prems
- val facts_i = prems_i + num_prems
+ val conjecture_i = 0
+ val prems_i = conjecture_i + 1
+ val num_prems = length prems
+ val facts_i = prems_i + num_prems
- val fact_ids' =
- map_filter (fn j =>
- let val (i, _) = nth assms j in
- try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
- end) used_assm_js
- in
- {outcome = NONE, fact_ids = fact_ids', atp_proof = fn () => []}
- end
+ val fact_ids' =
+ map_filter (fn j =>
+ let val (i, _) = nth assms j in
+ try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
+ end) used_assm_js
+ in
+ {outcome = NONE, fact_ids = SOME fact_ids', atp_proof = K []}
+ end
end;
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sat Apr 25 09:48:06 2015 +0200
@@ -11,7 +11,7 @@
type parsed_proof =
{outcome: SMT_Failure.failure option,
- fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list,
+ fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option,
atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
type solver_config =
@@ -140,7 +140,7 @@
type parsed_proof =
{outcome: SMT_Failure.failure option,
- fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list,
+ fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option,
atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
type solver_config =
@@ -195,7 +195,7 @@
(Unsat, lines) =>
(case parse_proof0 of
SOME pp => pp outer_ctxt replay_data xfacts prems concl lines
- | NONE => {outcome = NONE, fact_ids = [], atp_proof = K []})
+ | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []})
| (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
fun replay outcome replay0 oracle outer_ctxt
@@ -270,7 +270,7 @@
in
parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
end
- handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = [], atp_proof = K []}
+ handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = NONE, atp_proof = K []}
(* SMT tactic *)
--- a/src/HOL/Tools/SMT/smt_systems.ML Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Sat Apr 25 09:48:06 2015 +0200
@@ -27,10 +27,13 @@
" failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
" option for details"))
+fun is_blank_or_error_line "" = true
+ | is_blank_or_error_line s = String.isPrefix "(error " s
+
fun on_first_line test_outcome solver_name lines =
let
val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
- val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines))
+ val (l, ls) = split_first (snd (take_prefix is_blank_or_error_line lines))
in (test_outcome solver_name l, ls) end
fun on_first_non_unsupported_line test_outcome solver_name lines =
@@ -59,7 +62,6 @@
end
-
(* CVC4 *)
val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
@@ -68,6 +70,7 @@
fun cvc4_options ctxt = [
"--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
"--lang=smt2",
+ "--continued-execution",
"--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
fun select_class ctxt =
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML Sat Apr 25 09:48:06 2015 +0200
@@ -70,7 +70,7 @@
val fact_helper_ids' =
map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
in
- {outcome = NONE, fact_ids = fact_ids',
+ {outcome = NONE, fact_ids = SOME fact_ids',
atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
end
--- a/src/HOL/Tools/SMT/z3_replay.ML Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_replay.ML Sat Apr 25 09:48:06 2015 +0200
@@ -206,7 +206,7 @@
val fact_helper_ids' =
map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
in
- {outcome = NONE, fact_ids = fact_ids',
+ {outcome = NONE, fact_ids = SOME fact_ids',
atp_proof = fn () => Z3_Isar.atp_proof_of_z3_proof ctxt ll_defs rewrite_rules prems concl
fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Apr 24 23:05:33 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sat Apr 25 09:48:06 2015 +0200
@@ -126,7 +126,7 @@
reraise exn
else
{outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
- fact_ids = [], atp_proof = K []}
+ fact_ids = NONE, atp_proof = K []}
val death = Timer.checkRealTimer timer
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
@@ -189,8 +189,10 @@
val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
smt_filter_loop name params state goal subgoal factss
- val used_named_facts = map snd fact_ids
- val used_facts = sort_wrt fst (map fst used_named_facts)
+ val used_facts =
+ (case fact_ids of
+ NONE => map fst used_from
+ | SOME ids => sort_wrt fst (map (fst o snd) ids))
val outcome = Option.map failure_of_smt_failure outcome
val (preferred_methss, message) =