474 \item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3 |
474 \item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3 |
475 as an ATP'' runs on Geoff Sutcliffe's Miami servers. |
475 as an ATP'' runs on Geoff Sutcliffe's Miami servers. |
476 \end{enum} |
476 \end{enum} |
477 |
477 |
478 By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever |
478 By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever |
479 the SMT module's \emph{smt\_solver} configuration option is set to) in |
479 the SMT module's \textit{smt\_solver} configuration option is set to) in |
480 parallel---either locally or remotely, depending on the number of processor |
480 parallel---either locally or remotely, depending on the number of processor |
481 cores available. For historical reasons, the default value of this option can be |
481 cores available. For historical reasons, the default value of this option can be |
482 overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu |
482 overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu |
483 in Proof General. |
483 in Proof General. |
484 |
484 |
534 Specifies whether full-type information is encoded in ATP problems. Enabling |
534 Specifies whether full-type information is encoded in ATP problems. Enabling |
535 this option can prevent the discovery of type-incorrect proofs, but it also |
535 this option can prevent the discovery of type-incorrect proofs, but it also |
536 tends to slow down the ATPs significantly. For historical reasons, the default |
536 tends to slow down the ATPs significantly. For historical reasons, the default |
537 value of this option can be overridden using the option ``Sledgehammer: Full |
537 value of this option can be overridden using the option ``Sledgehammer: Full |
538 Types'' from the ``Isabelle'' menu in Proof General. |
538 Types'' from the ``Isabelle'' menu in Proof General. |
|
539 |
|
540 \opfalse{full\_types}{partial\_types} |
|
541 Specifies whether full-type information is encoded in ATP problems. Enabling |
|
542 this option can prevent the discovery of type-incorrect proofs, but it also |
|
543 tends to slow down the ATPs significantly. For historical reasons, the default |
|
544 value of this option can be overridden using the option ``Sledgehammer: Full |
|
545 Types'' from the ``Isabelle'' menu in Proof General. |
|
546 |
|
547 \opfalse{monomorphize}{dont\_monomorphize} |
|
548 Specifies whether the relevant facts should be monomorphized---i.e., whether |
|
549 their type variables should be instantiated with relevant ground types. |
|
550 Monomorphization is always performed for SMT solvers, irrespective of this |
|
551 option. Monomorphization can simplify reasoning but also leads to larger fact |
|
552 bases, which can slow down the ATPs. |
|
553 |
|
554 \opdefault{monomorphize\_limit}{int}{\upshape 4} |
|
555 Specifies the maximum number of iterations for the monomorphization fixpoint |
|
556 construction. The higher this limit is, the more monomorphic instances are |
|
557 potentially generated. |
|
558 |
|
559 \opdefault{type\_sys}{string}{smart} |
|
560 Specifies the type system to use in ATP problems. The option can take the |
|
561 following values: |
|
562 |
|
563 \begin{enum} |
|
564 \item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with |
|
565 its type. |
|
566 |
|
567 % NOT YET IMPLEMENTED: |
|
568 %\item[$\bullet$] \textbf{\textit{preds}:} Types are represented by predicates. |
|
569 |
|
570 \item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names. |
|
571 This value is available only if \textit{monomorphize} is enabled and |
|
572 \textit{full\_types} is enabled. |
|
573 |
|
574 \item[$\bullet$] \textbf{\textit{const\_args}:} Constants are annotated with |
|
575 their type parameters, which are passed as extra arguments. This value is not |
|
576 available if \textit{full\_types} is enabled. |
|
577 |
|
578 \item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the |
|
579 ATP. |
|
580 |
|
581 \item[$\bullet$] \textbf{\textit{smart}:} This is the same as |
|
582 \textit{tags} if \textit{full\_types} is enabled; otherwise, this is the |
|
583 same as \textit{mangled} if \textit{monomorphize} is enabled and |
|
584 \textit{const\_args} otherwise. |
|
585 \end{enum} |
|
586 |
|
587 For SMT solvers, the type system is always \textit{mangled}. |
539 \end{enum} |
588 \end{enum} |
540 |
589 |
541 \subsection{Relevance Filter} |
590 \subsection{Relevance Filter} |
542 \label{relevance-filter} |
591 \label{relevance-filter} |
543 |
592 |
554 Specifies the maximum number of facts that may be returned by the relevance |
603 Specifies the maximum number of facts that may be returned by the relevance |
555 filter. If the option is set to \textit{smart}, it is set to a value that was |
604 filter. If the option is set to \textit{smart}, it is set to a value that was |
556 empirically found to be appropriate for the prover. A typical value would be |
605 empirically found to be appropriate for the prover. A typical value would be |
557 300. |
606 300. |
558 |
607 |
559 \opfalse{monomorphize}{dont\_monomorphize} |
|
560 Specifies whether the relevant facts should be monomorphized---i.e., whether |
|
561 their type variables should be instantiated with relevant ground types. |
|
562 Monomorphization is always performed for SMT solvers, irrespective of this |
|
563 option. Monomorphization can simplify reasoning but also leads to larger fact |
|
564 bases, which can slow down the ATPs. |
|
565 |
|
566 \opdefault{monomorphize\_limit}{int}{\upshape 4} |
|
567 Specifies the maximum number of iterations for the monomorphization fixpoint |
|
568 construction. The higher this limit is, the more monomorphic instances are |
|
569 potentially generated. |
|
570 |
|
571 \end{enum} |
608 \end{enum} |
572 |
609 |
573 \subsection{Output Format} |
610 \subsection{Output Format} |
574 \label{output-format} |
611 \label{output-format} |
575 |
612 |