added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)

--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Feb 24 11:23:34 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Feb 24 11:23:35 2012 +0100
@@ -99,8 +99,9 @@
 Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
 the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
 the SMT solvers Z3 \cite{z3} is used by default, and you can tell Sledgehammer
-to try CVC3 \cite{cvc3} and Yices \cite{yices} as well; these are run either
-locally or on a server at the TU M\"unchen.
+to try Alt-Ergo \cite{alt-ergo}, CVC3 \cite{cvc3}, and Yices \cite{yices} as
+well; these are run either locally or (for CVC3 and Z3) on a server at the TU
+M\"unchen.
 
 The problem passed to the automatic provers consists of your current goal
 together with a heuristic selection of hundreds of facts (theorems) from the
@@ -152,10 +153,11 @@
 \cite{sutcliffe-2000}. If you want better performance, you should at least
 install E and SPASS locally.
 
-Among the SMT solvers, CVC3, Yices, and Z3 can be run locally, and CVC3 and Z3
-can be run remotely on a TU M\"unchen server. If you want better performance and
-get the ability to replay proofs that rely on the \emph{smt} proof method
-without an Internet connection, you should at least install Z3 locally.
+Among the SMT solvers, Alt-Ergo, CVC3, Yices, and Z3 can be run locally, and
+CVC3 and Z3 can be run remotely on a TU M\"unchen server. If you want better
+performance and get the ability to replay proofs that rely on the \emph{smt}
+proof method without an Internet connection, you should at least install Z3
+locally.
 
 There are three main ways to install automatic provers on your machine:
 
@@ -204,14 +206,14 @@
 \texttt{SATALLAX\_VERSION}, \texttt{SPASS\_VERSION}, or
 \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``1.4'').
 
-Similarly, if you want to build CVC3, or found a
+Similarly, if you want to build Alt-Ergo or CVC3, or found a
 Yices or Z3 executable somewhere (e.g.,
 \url{http://yices.csl.sri.com/download.shtml} or
 \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html}),
 set the environment variable \texttt{CVC3\_\allowbreak SOLVER},
 \texttt{YICES\_SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of
 the executable, \emph{including the file name}. Sledgehammer has been tested
-with CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 3.2.
+with Alt-Ergo 0.93, CVC3 2.2, Yices 1.0.28, and Z3 3.0 to 3.2.
 Since the SMT solvers' output formats are somewhat unstable, other
 versions of the solvers might not work well with Sledgehammer. Ideally,
 also set \texttt{CVC3\_VERSION}, \texttt{YICES\_VERSION}, or
@@ -311,7 +313,7 @@
 \label{hints}
 
 This section presents a few hints that should help you get the most out of
-Sledgehammer. Frequently (and infrequently) asked questions are answered in
+Sledgehammer. Frequently asked questions are answered in
 \S\ref{frequently-asked-questions}.
 
 %\newcommand\point[1]{\medskip\par{\sl\bfseries#1}\par\nopagebreak}
@@ -770,6 +772,14 @@
 The following local provers are supported:
 
 \begin{enum}
+\item[\labelitemi] \textbf{\textit{alt\_ergo}:} Alt-Ergo is a polymorphic
+SMT solver developed by Bobot et al.\ \cite{alt-ergo}.
+It supports the TPTP polymorphic typed first-order format (TFF1) via Why3
+\cite{why3}. It is included for experimental purposes. To use Alt-Ergo, set the
+environment variable \texttt{WHY3\_HOME} to the directory that contains the
+\texttt{why3} executable. Sledgehammer has been tested with Alt-Ergo 0.93 and an
+unidentified development version of Why3.
+
 \item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
@@ -812,7 +822,7 @@
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
 Sledgehammer has been tested with versions 0.6, 1.0, and 1.8.
-%Vampire 1.8 supports the TPTP typed first-order format (TFF0).
+Versions above 1.8 support the TPTP typed first-order format (TFF0).
 
 \item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
 SRI \cite{yices}. To use Yices, set the environment variable
@@ -1057,14 +1067,18 @@
 $\const{t\_}\tau(t)$.
 
 \item[\labelitemi] \textbf{\textit{mono\_native} (sound):} Exploits native
-first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
-falls back on \textit{mono\_guards}. The problem is monomorphized.
+first-order types if the prover supports the TFF0, TFF1, or THF0 syntax;
+otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized.
 
 \item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits
 native higher-order types if the prover supports the THF0 syntax; otherwise,
 falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
 monomorphized.
 
+\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native
+polymorphic first-order types if the prover supports the TFF1 syntax; otherwise,
+falls back on \textit{mono\_native}.
+
 \item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\

--- a/doc-src/manual.bib	Fri Feb 24 11:23:34 2012 +0100
+++ b/doc-src/manual.bib	Fri Feb 24 11:23:35 2012 +0100
@@ -301,6 +301,27 @@
   author = "Jasmin Christian Blanchette and Tobias Nipkow",
   crossref = {itp2010}}
 
+@inproceedings{why3,
+  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
+  title = {{Why3}: Shepherd Your Herd of Provers},
+  editor = "K. Rustan M. Leino and Micha\l{} Moskal",
+  booktitle = {Boogie 2011},
+  pages = "53--64",
+  year = 2011
+}
+
+@inproceedings{alt-ergo,
+  author = {Fran\c{c}ois Bobot and Sylvain Conchon and Evelyne Contejean and St\'ephane Lescuyer},
+  title = {Implementing Polymorphism in {SMT} Solvers},
+  booktitle = {SMT '08},
+  pages = "1--5",
+  publisher = "ACM",
+  series = "ICPS",
+  year = 2008,
+  editor = {Clark Barrett and Leonardo de Moura}}
+% /BPR
+% and Domagoj Babic and Amit Goel
+
 @inproceedings{boehme-nipkow-2010,
   author={Sascha B\"ohme and Tobias Nipkow},
   title={Sledgehammer: Judgement Day},
@@ -813,7 +834,6 @@
   author    = {Konstantin Korovin and
                Christoph Sticksel},
   title     = {{iP}rover-{E}q: An Instantiation-Based Theorem Prover with Equality},
-  year      = {2010},
   pages     = {196--202},
   booktitle={Automated Reasoning: IJCAR 2010},
   editor={J. Giesl and R. H\"ahnle},

--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Feb 24 11:23:34 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Feb 24 11:23:35 2012 +0100
@@ -752,6 +752,9 @@
           end
       in add 0 |> apsnd SOME end
 
+fun avoid_clash_with_alt_ergo_type_vars s =
+  if is_tptp_variable s then s else s ^ "_"
+
 fun avoid_clash_with_dfg_keywords s =
   let val n = String.size s in
     if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
@@ -766,8 +769,12 @@
   let
     val empty_pool =
       if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
-    val nice_name =
-      nice_name (case format of DFG _ => avoid_clash_with_dfg_keywords | _ => I)
+    val avoid_clash =
+      case format of
+        TFF (TPTP_Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
+      | DFG _ => avoid_clash_with_dfg_keywords
+      | _ => I
+    val nice_name = nice_name avoid_clash
     fun nice_type (AType (name, tys)) =
         nice_name name ##>> pool_map nice_type tys #>> AType
       | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Feb 24 11:23:34 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Feb 24 11:23:35 2012 +0100
@@ -2653,10 +2653,10 @@
        (aritiesN,
         map (formula_line_for_arity_clause format type_enc) arity_clauses),
        (helpersN, helper_lines),
+       (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
        (conjsN,
         map (formula_line_for_conjecture ctxt polym_constrs format mono
-                                         type_enc) conjs),
-       (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
+                                         type_enc) conjs)]
     val problem =
       problem
       |> (case format of

--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Feb 24 11:23:34 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Feb 24 11:23:35 2012 +0100
@@ -37,14 +37,14 @@
   val e_default_sym_offs_weight : real Config.T
   val e_sym_offs_weight_base : real Config.T
   val e_sym_offs_weight_span : real Config.T
+  val alt_ergoN : string
+  val dummy_thfN : string
   val eN : string
   val e_sineN : string
   val e_tofofN : string
   val iproverN : string
   val iprover_eqN : string
   val leo2N : string
-  val dummy_tff1N : string
-  val dummy_thfN : string
   val satallaxN : string
   val snarkN : string
   val spassN : string
@@ -127,14 +127,14 @@
 
 (* named ATPs *)
 
+val alt_ergoN = "alt_ergo"
+val dummy_thfN = "dummy_thf" (* experimental *)
 val eN = "e"
 val e_sineN = "e_sine"
 val e_tofofN = "e_tofof"
 val iproverN = "iprover"
 val iprover_eqN = "iprover_eq"
 val leo2N = "leo2"
-val dummy_tff1N = "dummy_tff1" (* experimental *)
-val dummy_thfN = "dummy_thf" (* experimental *)
 val satallaxN = "satallax"
 val snarkN = "snark"
 val spassN = "spass"
@@ -162,6 +162,31 @@
 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
 
 
+(* Alt-Ergo *)
+
+val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit)
+
+val alt_ergo_config : atp_config =
+  {exec = ("WHY3_HOME", "why3"),
+   required_execs = [],
+   arguments =
+     fn _ => fn _ => fn _ => fn timeout => fn _ =>
+        "--format tff1 --prover alt-ergo --timelimit " ^
+        string_of_int (to_secs 1 timeout),
+   proof_delims = [],
+   known_failures =
+     [(ProofMissing, ": Valid"),
+      (TimedOut, ": Timeout"),
+      (GaveUp, ": Unknown")],
+   conj_sym_kind = Hypothesis,
+   prem_kind = Hypothesis,
+   best_slices = fn _ =>
+     (* FUDGE *)
+     [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))]}
+
+val alt_ergo = (alt_ergoN, alt_ergo_config)
+
+
 (* E *)
 
 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
@@ -340,8 +365,6 @@
 
 val spass_new_H2 = "-Heuristic=2"
 val spass_new_H2SOS = "-Heuristic=2 -SOS"
-val spass_new_Red2 = "-RFRew=2 -RBRew=2 -RTaut=2"
-val spass_new_Sorts0 = "-Sorts=0"
 val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
 val spass_new_H2NuVS0Red2 =
   "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
@@ -457,10 +480,6 @@
                         if is_format_higher_order format then keep_lamsN
                         else combsN, false), "")))]}
 
-val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
-val dummy_tff1_config = dummy_config dummy_tff1_format "poly_native"
-val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
-
 val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
 val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
 val dummy_thf = (dummy_thfN, dummy_thf_config)
@@ -598,7 +617,7 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, leo2, dummy_tff1, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
+  [alt_ergo, e, leo2, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
    remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
    remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
    remote_waldmeister]