src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Wed Feb 09 17:18:58 2011 +0100 (2011-02-09)
changeset 41742 11e862c68b40
parent 41741 839d1488045f
child 41744 a18e7bbca258
permissions -rw-r--r--
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
     1 (*  Title:      HOL/Tools/ATP/atp_systems.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Setup for supported ATPs.
     6 *)
     7 
     8 signature ATP_SYSTEMS =
     9 sig
    10   type failure = ATP_Proof.failure
    11 
    12   type atp_config =
    13     {exec: string * string,
    14      required_execs: (string * string) list,
    15      arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
    16      has_incomplete_mode: bool,
    17      proof_delims: (string * string) list,
    18      known_failures: (failure * string) list,
    19      default_max_relevant: int,
    20      explicit_forall: bool,
    21      use_conjecture_for_hypotheses: bool}
    22 
    23   datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
    24 
    25   (* for experimentation purposes -- do not use in production code *)
    26   val e_weight_method : e_weight_method Unsynchronized.ref
    27   val e_default_fun_weight : real Unsynchronized.ref
    28   val e_fun_weight_base : real Unsynchronized.ref
    29   val e_fun_weight_factor : real Unsynchronized.ref
    30   val e_default_sym_offs_weight : real Unsynchronized.ref
    31   val e_sym_offs_weight_base : real Unsynchronized.ref
    32   val e_sym_offs_weight_factor : real Unsynchronized.ref
    33 
    34   val eN : string
    35   val spassN : string
    36   val vampireN : string
    37   val sine_eN : string
    38   val snarkN : string
    39   val z3_atpN : string
    40   val remote_prefix : string
    41   val remote_atp :
    42     string -> string -> string list -> (string * string) list
    43     -> (failure * string) list -> int -> bool -> string * atp_config
    44   val add_atp : string * atp_config -> theory -> theory
    45   val get_atp : theory -> string -> atp_config
    46   val supported_atps : theory -> string list
    47   val is_atp_installed : theory -> string -> bool
    48   val refresh_systems_on_tptp : unit -> unit
    49   val setup : theory -> theory
    50 end;
    51 
    52 structure ATP_Systems : ATP_SYSTEMS =
    53 struct
    54 
    55 open ATP_Proof
    56 
    57 (* ATP configuration *)
    58 
    59 type atp_config =
    60   {exec: string * string,
    61    required_execs: (string * string) list,
    62    arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
    63    has_incomplete_mode: bool,
    64    proof_delims: (string * string) list,
    65    known_failures: (failure * string) list,
    66    default_max_relevant: int,
    67    explicit_forall: bool,
    68    use_conjecture_for_hypotheses: bool}
    69 
    70 val known_perl_failures =
    71   [(CantConnect, "HTTP error"),
    72    (NoPerl, "env: perl"),
    73    (NoLibwwwPerl, "Can't locate HTTP")]
    74 
    75 (* named ATPs *)
    76 
    77 val eN = "e"
    78 val spassN = "spass"
    79 val vampireN = "vampire"
    80 val z3_atpN = "z3_atp"
    81 val sine_eN = "sine_e"
    82 val snarkN = "snark"
    83 val remote_prefix = "remote_"
    84 
    85 structure Data = Theory_Data
    86 (
    87   type T = (atp_config * stamp) Symtab.table
    88   val empty = Symtab.empty
    89   val extend = I
    90   fun merge data : T = Symtab.merge (eq_snd op =) data
    91     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
    92 )
    93 
    94 fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
    95 
    96 
    97 (* E *)
    98 
    99 (* Give E an extra second to reconstruct the proof. Older versions even get two
   100    seconds, because the "eproof" script wrongly subtracted an entire second to
   101    account for the overhead of the script itself, which is in fact much
   102    lower. *)
   103 fun e_bonus () =
   104   if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
   105 
   106 val tstp_proof_delims =
   107   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
   108 
   109 datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
   110 
   111 val e_weight_method = Unsynchronized.ref E_Fun_Weight
   112 val e_default_fun_weight = Unsynchronized.ref 0.5
   113 val e_fun_weight_base = Unsynchronized.ref 0.0
   114 val e_fun_weight_factor = Unsynchronized.ref 40.0
   115 val e_default_sym_offs_weight = Unsynchronized.ref 0.0
   116 val e_sym_offs_weight_base = Unsynchronized.ref ~30.0
   117 val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0
   118 
   119 fun e_weight_method_case fw sow =
   120   case !e_weight_method of
   121     E_Auto => raise Fail "Unexpected \"E_Auto\""
   122   | E_Fun_Weight => fw
   123   | E_Sym_Offset_Weight => sow
   124 
   125 fun scaled_e_weight w =
   126   e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base)
   127   + w * e_weight_method_case (!e_fun_weight_factor) (!e_sym_offs_weight_factor)
   128   |> Real.ceil |> signed_string_of_int
   129 
   130 fun e_weight_arguments weights =
   131   if !e_weight_method = E_Auto orelse
   132      string_ord (getenv "E_VERSION", "1.2w") = LESS then
   133     "-xAutoDev"
   134   else
   135     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
   136     \--destructive-er-aggressive --destructive-er --presat-simplify \
   137     \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
   138     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
   139     \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^
   140     "(SimulateSOS, " ^
   141     scaled_e_weight (e_weight_method_case (!e_default_fun_weight)
   142                                           (!e_default_sym_offs_weight)) ^
   143     ",20,1.5,1.5,1" ^
   144     (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w)
   145                 |> implode) ^
   146     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
   147     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
   148     \FIFOWeight(PreferProcessed))'"
   149 
   150 val e_config : atp_config =
   151   {exec = ("E_HOME", "eproof"),
   152    required_execs = [],
   153    arguments = fn _ => fn timeout => fn weights =>
   154      "--tstp-in --tstp-out -l5 " ^ e_weight_arguments weights ^ " -tAutoDev \
   155      \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
   156    has_incomplete_mode = false,
   157    proof_delims = [tstp_proof_delims],
   158    known_failures =
   159      [(Unprovable, "SZS status: CounterSatisfiable"),
   160       (Unprovable, "SZS status CounterSatisfiable"),
   161       (TimedOut, "Failure: Resource limit exceeded (time)"),
   162       (TimedOut, "time limit exceeded"),
   163       (OutOfResources,
   164        "# Cannot determine problem status within resource limit"),
   165       (OutOfResources, "SZS status: ResourceOut"),
   166       (OutOfResources, "SZS status ResourceOut")],
   167    default_max_relevant = 500 (* FUDGE *),
   168    explicit_forall = false,
   169    use_conjecture_for_hypotheses = true}
   170 
   171 val e = (eN, e_config)
   172 
   173 
   174 (* SPASS *)
   175 
   176 (* The "-VarWeight=3" option helps the higher-order problems, probably by
   177    counteracting the presence of "hAPP". *)
   178 val spass_config : atp_config =
   179   {exec = ("ISABELLE_ATP", "scripts/spass"),
   180    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
   181    arguments = fn complete => fn timeout => fn _ =>
   182      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   183       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
   184      |> not complete ? prefix "-SOS=1 ",
   185    has_incomplete_mode = true,
   186    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   187    known_failures =
   188      known_perl_failures @
   189      [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
   190       (TimedOut, "SPASS beiseite: Ran out of time"),
   191       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   192       (MalformedInput, "Undefined symbol"),
   193       (MalformedInput, "Free Variable"),
   194       (SpassTooOld, "tptp2dfg"),
   195       (InternalError, "Please report this error")],
   196    default_max_relevant = 350 (* FUDGE *),
   197    explicit_forall = true,
   198    use_conjecture_for_hypotheses = true}
   199 
   200 val spass = (spassN, spass_config)
   201 
   202 
   203 (* Vampire *)
   204 
   205 val vampire_config : atp_config =
   206   {exec = ("VAMPIRE_HOME", "vampire"),
   207    required_execs = [],
   208    arguments = fn complete => fn timeout => fn _ =>
   209      (* This would work too but it's less tested: "--proof tptp " ^ *)
   210      "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
   211      " --thanks \"Andrei and Krystof\" --input_file"
   212      |> not complete ? prefix "--sos on ",
   213    has_incomplete_mode = true,
   214    proof_delims =
   215      [("=========== Refutation ==========",
   216        "======= End of refutation ======="),
   217       ("% SZS output start Refutation", "% SZS output end Refutation"),
   218       ("% SZS output start Proof", "% SZS output end Proof")],
   219    known_failures =
   220      [(Unprovable, "UNPROVABLE"),
   221       (IncompleteUnprovable, "CANNOT PROVE"),
   222       (TimedOut, "SZS status Timeout"),
   223       (Unprovable, "Satisfiability detected"),
   224       (Unprovable, "Termination reason: Satisfiable"),
   225       (VampireTooOld, "not a valid option"),
   226       (Interrupted, "Aborted by signal SIGINT")],
   227    default_max_relevant = 400 (* FUDGE *),
   228    explicit_forall = false,
   229    use_conjecture_for_hypotheses = true}
   230 
   231 val vampire = (vampireN, vampire_config)
   232 
   233 
   234 (* Z3 with TPTP syntax *)
   235 
   236 val z3_atp_config : atp_config =
   237   {exec = ("Z3_HOME", "z3"),
   238    required_execs = [],
   239    arguments = fn _ => fn timeout => fn _ =>
   240      "MBQI=true /p /t:" ^ string_of_int (to_secs 0 timeout),
   241    has_incomplete_mode = false,
   242    proof_delims = [],
   243    known_failures =
   244      [(Unprovable, "\nsat"),
   245       (IncompleteUnprovable, "\nunknown"),
   246       (ProofMissing, "\nunsat")],
   247    default_max_relevant = 250 (* FUDGE *),
   248    explicit_forall = true,
   249    use_conjecture_for_hypotheses = false}
   250 
   251 val z3_atp = (z3_atpN, z3_atp_config)
   252 
   253 
   254 (* Remote ATP invocation via SystemOnTPTP *)
   255 
   256 val systems = Synchronized.var "atp_systems" ([] : string list)
   257 
   258 fun get_systems () =
   259   case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   260     (output, 0) => split_lines output
   261   | (output, _) =>
   262     error (case extract_known_failure known_perl_failures output of
   263              SOME failure => string_for_failure "ATP" failure
   264            | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
   265 
   266 fun find_system name [] systems = find_first (String.isPrefix name) systems
   267   | find_system name (version :: versions) systems =
   268     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   269       NONE => find_system name versions systems
   270     | res => res
   271 
   272 fun get_system name versions =
   273   Synchronized.change_result systems
   274       (fn systems => (if null systems then get_systems () else systems)
   275                      |> `(find_system name versions))
   276 
   277 fun the_system name versions =
   278   case get_system name versions of
   279     SOME sys => sys
   280   | NONE => error ("System " ^ quote name ^
   281                    " is not available at SystemOnTPTP.")
   282 
   283 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   284 
   285 fun remote_config system_name system_versions proof_delims known_failures
   286                   default_max_relevant use_conjecture_for_hypotheses
   287                   : atp_config =
   288   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   289    required_execs = [],
   290    arguments = fn _ => fn timeout => fn _ =>
   291      " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
   292      ^ " -s " ^ the_system system_name system_versions,
   293    has_incomplete_mode = false,
   294    proof_delims = insert (op =) tstp_proof_delims proof_delims,
   295    known_failures =
   296      known_failures @ known_perl_failures @
   297      [(TimedOut, "says Timeout")],
   298    default_max_relevant = default_max_relevant,
   299    explicit_forall = true,
   300    use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
   301 
   302 fun remotify_config system_name system_versions
   303         ({proof_delims, known_failures, default_max_relevant,
   304           use_conjecture_for_hypotheses, ...} : atp_config) : atp_config =
   305   remote_config system_name system_versions proof_delims known_failures
   306                 default_max_relevant use_conjecture_for_hypotheses
   307 
   308 fun remote_atp name system_name system_versions proof_delims known_failures
   309                default_max_relevant use_conjecture_for_hypotheses =
   310   (remote_prefix ^ name,
   311    remote_config system_name system_versions proof_delims known_failures
   312                  default_max_relevant use_conjecture_for_hypotheses)
   313 fun remotify_atp (name, config) system_name system_versions =
   314   (remote_prefix ^ name, remotify_config system_name system_versions config)
   315 
   316 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   317 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   318 val remote_z3_atp =
   319   remote_atp z3_atpN "Z3---" ["2.18"] []
   320              [(IncompleteUnprovable, "SZS status Satisfiable"),
   321               (ProofMissing, "SZS status Unsatisfiable")]
   322              250 (* FUDGE *) false
   323 val remote_sine_e =
   324   remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
   325              600 (* FUDGE *) true
   326 val remote_snark =
   327   remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
   328              250 (* FUDGE *) true
   329 
   330 (* Setup *)
   331 
   332 fun add_atp (name, config) thy =
   333   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   334   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   335 
   336 fun get_atp thy name =
   337   the (Symtab.lookup (Data.get thy) name) |> fst
   338   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   339 
   340 val supported_atps = Symtab.keys o Data.get
   341 
   342 fun is_atp_installed thy name =
   343   let val {exec, required_execs, ...} = get_atp thy name in
   344     forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
   345   end
   346 
   347 fun refresh_systems_on_tptp () =
   348   Synchronized.change systems (fn _ => get_systems ())
   349 
   350 val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
   351             remote_sine_e, remote_snark]
   352 val setup = fold add_atp atps
   353 
   354 end;