equal
deleted
inserted
replaced
553 \opsmart{max\_relevant}{int\_or\_smart} |
553 \opsmart{max\_relevant}{int\_or\_smart} |
554 Specifies the maximum number of facts that may be returned by the relevance |
554 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 |
555 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 |
556 empirically found to be appropriate for the prover. A typical value would be |
557 300. |
557 300. |
|
558 |
|
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 |
558 \end{enum} |
571 \end{enum} |
559 |
572 |
560 \subsection{Output Format} |
573 \subsection{Output Format} |
561 \label{output-format} |
574 \label{output-format} |
562 |
575 |