# HG changeset patch
# User blanchet
# Date 1416389475 -3600
# Node ID 627a93f6718295e365040ae37ebecdc8c9591371
# Parent  cc5e345753541c91b6859b3f035cc637f4fb3a02
parse CVC4 unsat cores

diff -r cc5e34575354 -r 627a93f67182 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Nov 19 10:31:15 2014 +0100
+++ b/src/HOL/SMT.thy	Wed Nov 19 10:31:15 2014 +0100
@@ -159,6 +159,7 @@
 ML_file "Tools/SMT/z3_isar.ML"
 ML_file "Tools/SMT/smt_solver.ML"
 ML_file "Tools/SMT/cvc4_interface.ML"
+ML_file "Tools/SMT/cvc4_proof_parse.ML"
 ML_file "Tools/SMT/verit_proof.ML"
 ML_file "Tools/SMT/verit_isar.ML"
 ML_file "Tools/SMT/verit_proof_parse.ML"
diff -r cc5e34575354 -r 627a93f67182 src/HOL/Tools/SMT/cvc4_proof_parse.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/cvc4_proof_parse.ML	Wed Nov 19 10:31:15 2014 +0100
@@ -0,0 +1,43 @@
+(*  Title:      HOL/Tools/SMT/cvc4_proof_parse.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+CVC4 proof (actually, unsat core) parsing.
+*)
+
+signature CVC4_PROOF_PARSE =
+sig
+  val parse_proof: SMT_Translate.replay_data ->
+    ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
+    SMT_Solver.parsed_proof
+end;
+
+structure CVC4_Proof_Parse: CVC4_PROOF_PARSE =
+struct
+
+fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output =
+  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 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 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
+
+end;
diff -r cc5e34575354 -r 627a93f67182 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Nov 19 10:31:15 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Wed Nov 19 10:31:15 2014 +0100
@@ -85,10 +85,10 @@
   avail = make_avail "CVC4",
   command = make_command "CVC4",
   options = cvc4_options,
-  smt_options = [],
+  smt_options = [(":produce-unsat-cores", "true")],
   default_max_relevant = 400 (* FUDGE *),
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
-  parse_proof = NONE,
+  parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
   replay = NONE }
 
 end
diff -r cc5e34575354 -r 627a93f67182 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Nov 19 10:31:15 2014 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Nov 19 10:31:15 2014 +0100
@@ -139,18 +139,23 @@
     (space_implode "\n  " (map sdatatype dtyps)))
 
 fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
-  Buffer.empty
-  |> fold (Buffer.add o enclose "; " "\n") comments
-  |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
-  |> Buffer.add logic
-  |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
-  |> fold sdtyp (AList.coalesce (op =) dtyps)
-  |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
-      (sort (fast_string_ord o pairself fst) funcs)
-  |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"
-      (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts)
-  |> Buffer.add "(check-sat)\n(get-proof)\n"
-  |> Buffer.content
+  let
+    val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true")
+  in
+    Buffer.empty
+    |> fold (Buffer.add o enclose "; " "\n") comments
+    |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
+    |> Buffer.add logic
+    |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
+    |> fold sdtyp (AList.coalesce (op =) dtyps)
+    |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
+        (sort (fast_string_ord o pairself fst) funcs)
+    |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"
+        (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts)
+    |> Buffer.add "(check-sat)\n"
+    |> Buffer.add (if unsat_core then "(get-unsat-core)\n" else "(get-proof)\n")
+    |> Buffer.content
+  end
 
 (* interface *)