Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: options Sprache: Isabelle

Original von: Isabelle^©

(* :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) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.