made CVC4 support work also without unsat cores
authorblanchet
Sat Apr 25 09:48:06 2015 +0200 (2015-04-25 ago)
changeset 6020190e88e521e0e
parent 60200 02fd729f2883
child 60202 a95023a21725
made CVC4 support work also without unsat cores
src/HOL/SMT.thy
src/HOL/Tools/SMT/cvc4_proof_parse.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_systems.ML
src/HOL/Tools/SMT/verit_proof_parse.ML
src/HOL/Tools/SMT/z3_replay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
     1.1 --- a/src/HOL/SMT.thy	Fri Apr 24 23:05:33 2015 +0200
     1.2 +++ b/src/HOL/SMT.thy	Sat Apr 25 09:48:06 2015 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4  *}
     1.5  
     1.6  method_setup moura = {*
     1.7 - Scan.succeed (SIMPLE_METHOD' o moura_tac)
     1.8 +  Scan.succeed (SIMPLE_METHOD' o moura_tac)
     1.9  *} "solve skolemization goals, especially those arising from Z3 proofs"
    1.10  
    1.11  hide_fact (open) choices bchoices
     2.1 --- a/src/HOL/Tools/SMT/cvc4_proof_parse.ML	Fri Apr 24 23:05:33 2015 +0200
     2.2 +++ b/src/HOL/Tools/SMT/cvc4_proof_parse.ML	Sat Apr 25 09:48:06 2015 +0200
     2.3 @@ -15,29 +15,32 @@
     2.4  struct
     2.5  
     2.6  fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output =
     2.7 -  let
     2.8 -    val num_ll_defs = length ll_defs
     2.9 +  if exists (String.isPrefix "(error \"This build of CVC4 doesn't have proof support") output then
    2.10 +    {outcome = NONE, fact_ids = NONE, atp_proof = K []}
    2.11 +  else
    2.12 +    let
    2.13 +      val num_ll_defs = length ll_defs
    2.14  
    2.15 -    val id_of_index = Integer.add num_ll_defs
    2.16 -    val index_of_id = Integer.add (~ num_ll_defs)
    2.17 +      val id_of_index = Integer.add num_ll_defs
    2.18 +      val index_of_id = Integer.add (~ num_ll_defs)
    2.19  
    2.20 -    val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output
    2.21 -    val used_assm_js =
    2.22 -      map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
    2.23 -        used_assert_ids
    2.24 +      val used_assert_ids = map_filter (try SMTLIB_Interface.assert_index_of_name) output
    2.25 +      val used_assm_js =
    2.26 +        map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
    2.27 +          used_assert_ids
    2.28  
    2.29 -    val conjecture_i = 0
    2.30 -    val prems_i = conjecture_i + 1
    2.31 -    val num_prems = length prems
    2.32 -    val facts_i = prems_i + num_prems
    2.33 +      val conjecture_i = 0
    2.34 +      val prems_i = conjecture_i + 1
    2.35 +      val num_prems = length prems
    2.36 +      val facts_i = prems_i + num_prems
    2.37  
    2.38 -    val fact_ids' =
    2.39 -      map_filter (fn j =>
    2.40 -        let val (i, _) = nth assms j in
    2.41 -          try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
    2.42 -        end) used_assm_js
    2.43 -  in
    2.44 -    {outcome = NONE, fact_ids = fact_ids', atp_proof = fn () => []}
    2.45 -  end
    2.46 +      val fact_ids' =
    2.47 +        map_filter (fn j =>
    2.48 +          let val (i, _) = nth assms j in
    2.49 +            try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
    2.50 +          end) used_assm_js
    2.51 +    in
    2.52 +      {outcome = NONE, fact_ids = SOME fact_ids', atp_proof = K []}
    2.53 +    end
    2.54  
    2.55  end;
     3.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Apr 24 23:05:33 2015 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Sat Apr 25 09:48:06 2015 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5    type parsed_proof =
     3.6      {outcome: SMT_Failure.failure option,
     3.7 -     fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list,
     3.8 +     fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option,
     3.9       atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
    3.10  
    3.11    type solver_config =
    3.12 @@ -140,7 +140,7 @@
    3.13  
    3.14  type parsed_proof =
    3.15    {outcome: SMT_Failure.failure option,
    3.16 -   fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list,
    3.17 +   fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option,
    3.18     atp_proof: unit -> (term, string) ATP_Proof.atp_step list}
    3.19  
    3.20  type solver_config =
    3.21 @@ -195,7 +195,7 @@
    3.22        (Unsat, lines) =>
    3.23          (case parse_proof0 of
    3.24            SOME pp => pp outer_ctxt replay_data xfacts prems concl lines
    3.25 -        | NONE => {outcome = NONE, fact_ids = [], atp_proof = K []})
    3.26 +        | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []})
    3.27      | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
    3.28  
    3.29    fun replay outcome replay0 oracle outer_ctxt
    3.30 @@ -270,7 +270,7 @@
    3.31    in
    3.32      parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
    3.33    end
    3.34 -  handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = [], atp_proof = K []}
    3.35 +  handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = NONE, atp_proof = K []}
    3.36  
    3.37  
    3.38  (* SMT tactic *)
     4.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Fri Apr 24 23:05:33 2015 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Sat Apr 25 09:48:06 2015 +0200
     4.3 @@ -27,10 +27,13 @@
     4.4      " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
     4.5      " option for details"))
     4.6  
     4.7 +fun is_blank_or_error_line "" = true
     4.8 +  | is_blank_or_error_line s = String.isPrefix "(error " s
     4.9 +
    4.10  fun on_first_line test_outcome solver_name lines =
    4.11    let
    4.12      val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    4.13 -    val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines))
    4.14 +    val (l, ls) = split_first (snd (take_prefix is_blank_or_error_line lines))
    4.15    in (test_outcome solver_name l, ls) end
    4.16  
    4.17  fun on_first_non_unsupported_line test_outcome solver_name lines =
    4.18 @@ -59,7 +62,6 @@
    4.19  
    4.20  end
    4.21  
    4.22 -
    4.23  (* CVC4 *)
    4.24  
    4.25  val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
    4.26 @@ -68,6 +70,7 @@
    4.27    fun cvc4_options ctxt = [
    4.28      "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    4.29      "--lang=smt2",
    4.30 +    "--continued-execution",
    4.31      "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
    4.32  
    4.33    fun select_class ctxt =
     5.1 --- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Fri Apr 24 23:05:33 2015 +0200
     5.2 +++ b/src/HOL/Tools/SMT/verit_proof_parse.ML	Sat Apr 25 09:48:06 2015 +0200
     5.3 @@ -70,7 +70,7 @@
     5.4      val fact_helper_ids' =
     5.5        map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
     5.6    in
     5.7 -    {outcome = NONE, fact_ids = fact_ids',
     5.8 +    {outcome = NONE, fact_ids = SOME fact_ids',
     5.9       atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
    5.10         fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
    5.11    end
     6.1 --- a/src/HOL/Tools/SMT/z3_replay.ML	Fri Apr 24 23:05:33 2015 +0200
     6.2 +++ b/src/HOL/Tools/SMT/z3_replay.ML	Sat Apr 25 09:48:06 2015 +0200
     6.3 @@ -206,7 +206,7 @@
     6.4      val fact_helper_ids' =
     6.5        map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
     6.6    in
     6.7 -    {outcome = NONE, fact_ids = fact_ids',
     6.8 +    {outcome = NONE, fact_ids = SOME fact_ids',
     6.9       atp_proof = fn () => Z3_Isar.atp_proof_of_z3_proof ctxt ll_defs rewrite_rules prems concl
    6.10         fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
    6.11    end
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Apr 24 23:05:33 2015 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sat Apr 25 09:48:06 2015 +0200
     7.3 @@ -126,7 +126,7 @@
     7.4                reraise exn
     7.5              else
     7.6                {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
     7.7 -               fact_ids = [], atp_proof = K []}
     7.8 +               fact_ids = NONE, atp_proof = K []}
     7.9  
    7.10          val death = Timer.checkRealTimer timer
    7.11          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    7.12 @@ -189,8 +189,10 @@
    7.13  
    7.14      val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
    7.15        smt_filter_loop name params state goal subgoal factss
    7.16 -    val used_named_facts = map snd fact_ids
    7.17 -    val used_facts = sort_wrt fst (map fst used_named_facts)
    7.18 +    val used_facts =
    7.19 +      (case fact_ids of
    7.20 +        NONE => map fst used_from
    7.21 +      | SOME ids => sort_wrt fst (map (fst o snd) ids))
    7.22      val outcome = Option.map failure_of_smt_failure outcome
    7.23  
    7.24      val (preferred_methss, message) =