# HG changeset patch
# User blanchet
# Date 1402585323 -7200
# Node ID a40edeaa01b11ec834f1e4e4a884ce9ac6fe933f
# Parent  7e2658f2e77d7f577ede66815e6728addcc62db1
don't ask proof-disabled solvers to do proofs

diff -r 7e2658f2e77d -r a40edeaa01b1 src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/SMT2.thy	Thu Jun 12 17:02:03 2014 +0200
@@ -393,4 +393,11 @@
 hide_type (open) symb_list pattern
 hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod
 
+declare [[smt2_solver = cvc3]]
+
+lemma "2 + 2 = (4::int)"
+using [[smt2_trace]]
+apply smt2
+done
+
 end
diff -r 7e2658f2e77d -r a40edeaa01b1 src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -20,6 +20,7 @@
      avail: unit -> bool,
      command: unit -> string list,
      options: Proof.context -> string list,
+     smt_options: (string * string) list,
      default_max_relevant: int,
      outcome: string -> string list -> outcome * string list,
      parse_proof: (Proof.context -> SMT2_Translate.replay_data ->
@@ -118,7 +119,7 @@
 
 in
 
-fun invoke name command ithms ctxt =
+fun invoke name command smt_options ithms ctxt =
   let
     val options = SMT2_Config.solver_options_of ctxt
     val comments = [space_implode " " options]
@@ -126,7 +127,7 @@
     val (str, replay_data as {context = ctxt', ...}) =
       ithms
       |> tap (trace_assms ctxt)
-      |> SMT2_Translate.translate ctxt comments
+      |> SMT2_Translate.translate ctxt smt_options comments
       ||> tap trace_replay_data
   in (run_solver ctxt' name (make_command command options) str, replay_data) end
 
@@ -148,6 +149,7 @@
    avail: unit -> bool,
    command: unit -> string list,
    options: Proof.context -> string list,
+   smt_options: (string * string) list,
    default_max_relevant: int,
    outcome: string -> string list -> outcome * string list,
    parse_proof: (Proof.context -> SMT2_Translate.replay_data ->
@@ -172,6 +174,7 @@
 
 type solver_info = {
   command: unit -> string list,
+  smt_options: (string * string) list,
   default_max_relevant: int,
   parse_proof: Proof.context -> SMT2_Translate.replay_data ->
     ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
@@ -207,11 +210,12 @@
   val cfalse = Thm.cterm_of @{theory} @{prop False}
 in
 
-fun add_solver ({name, class, avail, command, options, default_max_relevant, outcome,
+fun add_solver ({name, class, avail, command, options, smt_options, default_max_relevant, outcome,
     parse_proof = parse_proof0, replay = replay0} : solver_config) =
   let
     fun solver oracle = {
       command = command,
+      smt_options = smt_options,
       default_max_relevant = default_max_relevant,
       parse_proof = parse_proof (outcome name) parse_proof0,
       replay = replay (outcome name) replay0 oracle}
@@ -236,8 +240,9 @@
 fun apply_solver_and_replay ctxt thms0 =
   let
     val thms = map (check_topsort ctxt) thms0
-    val (name, {command, replay, ...}) = name_and_info_of ctxt
-    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms) ctxt
+    val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt
+    val (output, replay_data) =
+      invoke name command smt_options (SMT2_Normalize.normalize ctxt thms) ctxt
   in replay ctxt replay_data output end
 
 
@@ -259,8 +264,9 @@
     val thms = conjecture :: prems @ facts
     val thms' = map (check_topsort ctxt) thms
 
-    val (name, {command, parse_proof, ...}) = name_and_info_of ctxt
-    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms') ctxt
+    val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt
+    val (output, replay_data) =
+      invoke name command smt_options (SMT2_Normalize.normalize ctxt thms') ctxt
   in
     parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
   end
diff -r 7e2658f2e77d -r a40edeaa01b1 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -31,11 +31,10 @@
     " failed -- enable tracing using the " ^ quote (Config.name_of SMT2_Config.trace) ^
     " option for details"))
 
-fun on_first_nontrivial_line test_outcome solver_name lines =
+fun on_first_line test_outcome solver_name lines =
   let
-    val empty_line = (fn "" => true | s => String.isPrefix "***" s)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, ls) = split_first (snd (take_prefix empty_line lines))
+    val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines))
   in (test_outcome solver_name l, ls) end
 
 
@@ -44,7 +43,7 @@
 local
   fun cvc3_options ctxt = [
     "-seed", string_of_int (Config.get ctxt SMT2_Config.random_seed),
-    "-lang", "smt2", "-output-lang", "presentation",
+    "-lang", "smt2",
     "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]
 in
 
@@ -54,8 +53,9 @@
   avail = make_avail "CVC3",
   command = make_command "CVC3",
   options = cvc3_options,
+  smt_options = [],
   default_max_relevant = 400 (* FUDGE *),
-  outcome = on_first_nontrivial_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = NONE,
   replay = NONE }
 
@@ -122,8 +122,9 @@
   avail = make_avail "Z3_NEW",
   command = z3_make_command "Z3_NEW",
   options = z3_options,
+  smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 350 (* FUDGE *),
-  outcome = on_first_nontrivial_line (outcome_of "unsat" "sat" "unknown"),
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = SOME Z3_New_Replay.parse_proof,
   replay = SOME Z3_New_Replay.replay }
 
diff -r 7e2658f2e77d -r a40edeaa01b1 src/HOL/Tools/SMT2/smt2_translate.ML
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -24,7 +24,7 @@
   type config = {
     logic: term list -> string,
     has_datatypes: bool,
-    serialize: string list -> sign -> sterm list -> string }
+    serialize: (string * string) list -> string list -> sign -> sterm list -> string }
   type replay_data = {
     context: Proof.context,
     typs: typ Symtab.table,
@@ -34,7 +34,8 @@
 
   (*translation*)
   val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
-  val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data
+  val translate: Proof.context -> (string * string) list -> string list -> (int * thm) list ->
+    string * replay_data
 end;
 
 structure SMT2_Translate: SMT2_TRANSLATE =
@@ -65,7 +66,7 @@
 type config = {
   logic: term list -> string,
   has_datatypes: bool,
-  serialize: string list -> sign -> sterm list -> string }
+  serialize: (string * string) list -> string list -> sign -> sterm list -> string }
 
 type replay_data = {
   context: Proof.context,
@@ -472,7 +473,7 @@
         "for solver class " ^ quote (SMT2_Util.string_of_class cs)))
   end
 
-fun translate ctxt comments ithms =
+fun translate ctxt smt_options comments ithms =
   let
     val {logic, has_datatypes, serialize} = get_config ctxt
 
@@ -513,7 +514,7 @@
   in
     (ts4, tr_context)
     |-> intermediate logic dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2
-    |>> uncurry (serialize comments)
+    |>> uncurry (serialize smt_options comments)
     ||> replay_data_of ctxt2 rewrite_rules ithms
   end
 
diff -r 7e2658f2e77d -r a40edeaa01b1 src/HOL/Tools/SMT2/smtlib2_interface.ML
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -128,10 +128,10 @@
 fun assert_name_of_index i = assert_prefix ^ string_of_int i
 fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
 
-fun serialize comments {logic, sorts, dtyps, funcs} ts =
+fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
   Buffer.empty
   |> fold (Buffer.add o enclose "; " "\n") comments
-  |> Buffer.add "(set-option :produce-proofs true)\n"
+  |> 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)
   |> (if null dtyps then I