merge

--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Oct 26 16:59:19 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Oct 26 20:09:38 2010 +0200
@@ -64,9 +64,12 @@
 fun z3_on_last_line solver_name lines =
   let
     fun junk l =
-      String.isPrefix "WARNING" l orelse
-      String.isPrefix "ERROR" l orelse
-      forall Symbol.is_ascii_blank (Symbol.explode l)
+      if String.isPrefix "WARNING: Out of allocated virtual memory" l
+      then raise SMT_Solver.SMT SMT_Solver.Out_Of_Memory
+      else
+        String.isPrefix "WARNING" l orelse
+        String.isPrefix "ERROR" l orelse
+        forall Symbol.is_ascii_blank (Symbol.explode l)
   in
     the_default ("", []) (try (swap o split_last) (filter_out junk lines))
     |>> outcome_of "unsat" "sat" "unknown" solver_name

--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 16:59:19 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 20:09:38 2010 +0200
@@ -9,8 +9,9 @@
   datatype failure =
     Counterexample of bool * term list |
     Time_Out |
+    Out_Of_Memory |
     Other_Failure of string
-  val string_of_failure: Proof.context -> failure -> string
+  val string_of_failure: Proof.context -> string -> failure -> string
   exception SMT of failure
 
   type interface = {
@@ -44,7 +45,8 @@
   val select_certificates: string -> Context.generic -> Context.generic
 
   (*solvers*)
-  type solver = bool -> Proof.context -> (int * thm) list -> int list * thm
+  type solver = bool option -> Proof.context -> (int * thm) list ->
+    int list * thm
   val add_solver: solver_config -> theory -> theory
   val set_solver_options: string -> string -> Context.generic ->
     Context.generic
@@ -56,7 +58,8 @@
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
-    {outcome: failure option, used_facts: 'a list, run_time_in_msecs: int}
+    {outcome: failure option, used_facts: 'a list,
+    run_time_in_msecs: int option}
 
   (*tactic*)
   val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
@@ -73,9 +76,10 @@
 datatype failure =
   Counterexample of bool * term list |
   Time_Out |
+  Out_Of_Memory |
   Other_Failure of string
 
-fun string_of_failure ctxt (Counterexample (real, ex)) =
+fun string_of_failure ctxt _ (Counterexample (real, ex)) =
       let
         val msg = (if real then "C" else "Potential c") ^ "ounterexample found"
       in
@@ -83,8 +87,9 @@
         else Pretty.string_of (Pretty.big_list (msg ^ ":")
           (map (Syntax.pretty_term ctxt) ex))
       end
-  | string_of_failure _ Time_Out = "Time out."
-  | string_of_failure _ (Other_Failure msg) = msg
+  | string_of_failure _ name Time_Out = name ^ " timed out."
+  | string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory."
+  | string_of_failure _ _ (Other_Failure msg) = msg
 
 exception SMT of failure
 
@@ -162,23 +167,28 @@
 
 local
 
-fun choose (force_remote, env_var, is_remote, name) =
+fun choose (rm, env_var, is_remote, name) =
   let
+    val force_local = (case rm of SOME false => true | _ => false)
+    val force_remote = (case rm of SOME true => true | _ => false)
     val lsolver = get_local_solver env_var
     val remote_url = getenv "REMOTE_SMT_URL"
+    val trace = if is_some rm then K () else tracing
   in
     if not force_remote andalso is_some lsolver
     then 
-     (tracing ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
+     (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
       [the lsolver])
-    else if is_remote
+    else if not force_local andalso is_remote
     then
-     (tracing ("Invoking remote SMT solver " ^ quote name ^ " at " ^
+     (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^
         quote remote_url ^ " ...");
       [getenv "REMOTE_SMT", name])
     else if force_remote
-    then error ("SMT solver " ^ quote name ^ " is not remotely available.")
-    else error ("Undefined Isabelle environment variable: " ^ quote env_var)
+    then error ("The SMT solver " ^ quote name ^ " is not remotely available.")
+    else error ("The SMT solver " ^ quote name ^ " has not been found " ^
+      "on this computer. Please set the Isabelle environment variable " ^
+      quote env_var ^ ".")
   end
 
 fun make_cmd solver args problem_path proof_path = space_implode " " (
@@ -218,6 +228,9 @@
 
 end
 
+fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o
+  Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd))
+
 fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
   let
     fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
@@ -237,6 +250,7 @@
       "arguments:" :: args
   in
     irules
+    |> tap (trace_assms ctxt)
     |> SMT_Translate.translate translate_config ctxt comments
     ||> tap (trace_recon_data ctxt)
     |>> run_solver ctxt cmd args
@@ -270,14 +284,14 @@
     else ()
   end
 
-fun gen_solver name info force_remote ctxt irules =
+fun gen_solver name info rm ctxt irules =
   let
     val {env_var, is_remote, options, more_options, interface, reconstruct} =
       info
     val {extra_norm, translate} = interface
     val (with_datatypes, translate') =
       set_has_datatypes (Config.get ctxt datatypes) translate
-    val cmd = (force_remote, env_var, is_remote, name)
+    val cmd = (rm, env_var, is_remote, name)
   in
     (irules, ctxt)
     |-> SMT_Normalize.normalize extra_norm with_datatypes
@@ -294,7 +308,7 @@
 
 (* solver store *)
 
-type solver = bool -> Proof.context -> (int * thm) list -> int list * thm
+type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
 
 type solver_info = {
   env_var: string,
@@ -401,17 +415,17 @@
   | TVar (_, []) => true
   | _ => false))
 
-fun smt_solver force_remote ctxt irules =
+fun smt_solver rm ctxt irules =
   (* without this test, we would run into problems when atomizing the rules: *)
   if exists (has_topsort o Thm.prop_of o snd) irules
   then raise SMT (Other_Failure "proof state contains the universal sort {}")
-  else solver_of (Context.Proof ctxt) force_remote ctxt irules
+  else solver_of (Context.Proof ctxt) rm ctxt irules
 
-fun smt_filter rm time_limit st xrules i =
+fun smt_filter run_remote time_limit st xrules i =
   let
-    val {context, facts, goal} = Proof.goal st
+    val {facts, goal, ...} = Proof.goal st
     val ctxt =
-      context
+      Proof.context_of st
       |> Config.put timeout (Time.toSeconds time_limit)
       |> Config.put oracle false
       |> Config.put filter_only true
@@ -420,13 +434,14 @@
       |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt
       |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
     val irs = map (pair ~1) (Thm.assume cprop :: facts)
+    val rm = SOME run_remote
   in
     split_list xrules
     ||> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I
     |-> map_filter o try o nth
-    |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs= ~1})
+    |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
   end
-  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs= ~1}
+  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE}
   (* FIXME: measure runtime *)
 
 
@@ -438,8 +453,9 @@
   THEN' Tactic.rtac @{thm ccontr}
   THEN' SUBPROOF (fn {context=cx, prems, ...} =>
     let
-      fun solve () = snd (smt_solver false cx (map (pair ~1) (rules @ prems)))
-      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx)
+      fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems)))
+      val name = solver_name_of (Context.Proof cx)
+      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name)
     in
       (if pass_exns then SOME (solve ())
        else (SOME (solve ()) handle SMT fail => (trace fail; NONE)))