Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik