|
(* :mode=isabelle-options: *)
section "Automatically tried tools"
public option auto_time_start : real = 1.0
-- "initial delay for automatically tried tools (seconds)"
public option auto_time_limit : real = 2.0
-- "time limit for automatically tried tools (seconds > 0)"
public option auto_nitpick : bool = false
-- "run Nitpick automatically"
public option auto_sledgehammer : bool = false
-- "run Sledgehammer automatically"
public option auto_methods : bool = false
-- "try standard proof methods automatically"
public option auto_quickcheck : bool = true
-- "run Quickcheck automatically"
public option auto_solve_direct : bool = true
-- "run solve_direct automatically"
section "Miscellaneous Tools"
public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire"
-- "provers for Sledgehammer (separated by blanks)"
public option sledgehammer_timeout : int = 30
-- "provers will be interrupted after this time (in seconds)"
public option vampire_noncommercial : string = "unknown"
-- "status of Vampire activation for noncommercial use (yes, no, unknown)"
public option MaSh : string = "sml"
-- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
public option kodkod_scala : bool = true
-- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
public option kodkod_max_threads : int = 0
-- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)"
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
