# HG changeset patch
# User blanchet
# Date 1429948086 -7200
# Node ID 90e88e521e0e3de914ab48bf889e88d4afc828dd
# Parent  02fd729f2883b2698cdb4d57bc01ef3156335041
made CVC4 support work also without unsat cores

diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/SMT.thy
--- 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
diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/Tools/SMT/cvc4_proof_parse.ML
--- 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;
diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/Tools/SMT/smt_solver.ML
--- 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 *)
diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/Tools/SMT/smt_systems.ML
--- 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 =
diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/Tools/SMT/verit_proof_parse.ML
--- 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
diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/Tools/SMT/z3_replay.ML
--- 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
diff -r 02fd729f2883 -r 90e88e521e0e src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- 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) =