equal
deleted
inserted
replaced
425 \postw |
425 \postw |
426 |
426 |
427 As their names suggest, the Skolem constants $\mathit{sym}.x$ and |
427 As their names suggest, the Skolem constants $\mathit{sym}.x$ and |
428 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$ |
428 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$ |
429 from \textit{sym}'s definition. |
429 from \textit{sym}'s definition. |
430 |
|
431 Although skolemization is a useful optimization, you can disable it by invoking |
|
432 Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details. |
|
433 |
430 |
434 \subsection{Natural Numbers and Integers} |
431 \subsection{Natural Numbers and Integers} |
435 \label{natural-numbers-and-integers} |
432 \label{natural-numbers-and-integers} |
436 |
433 |
437 Because of the axiom of infinity, the type \textit{nat} does not admit any |
434 Because of the axiom of infinity, the type \textit{nat} does not admit any |
2197 Specifies whether the values of Skolem constants should be displayed as part of |
2194 Specifies whether the values of Skolem constants should be displayed as part of |
2198 counterexamples. Skolem constants correspond to bound variables in the original |
2195 counterexamples. Skolem constants correspond to bound variables in the original |
2199 formula and usually help us to understand why the counterexample falsifies the |
2196 formula and usually help us to understand why the counterexample falsifies the |
2200 formula. |
2197 formula. |
2201 |
2198 |
2202 \nopagebreak |
|
2203 {\small See also \textit{skolemize} (\S\ref{optimizations}).} |
|
2204 |
|
2205 \opfalse{show\_datatypes}{hide\_datatypes} |
2199 \opfalse{show\_datatypes}{hide\_datatypes} |
2206 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should |
2200 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should |
2207 be displayed as part of counterexamples. Such subsets are sometimes helpful when |
2201 be displayed as part of counterexamples. Such subsets are sometimes helpful when |
2208 investigating whether a potential counterexample is genuine or spurious, but |
2202 investigating whether a potential counterexample is genuine or spurious, but |
2209 their potential for clutter is real. |
2203 their potential for clutter is real. |
2449 |
2443 |
2450 \nopagebreak |
2444 \nopagebreak |
2451 {\small See also \textit{debug} (\S\ref{output-format}) and |
2445 {\small See also \textit{debug} (\S\ref{output-format}) and |
2452 \textit{show\_consts} (\S\ref{output-format}).} |
2446 \textit{show\_consts} (\S\ref{output-format}).} |
2453 |
2447 |
2454 \optrue{skolemize}{dont\_skolemize} |
|
2455 Specifies whether the formula should be skolemized. For performance reasons, |
|
2456 (positive) $\forall$-quanti\-fiers that occur in the scope of a higher-order |
|
2457 (positive) $\exists$-quanti\-fier are left unchanged. |
|
2458 |
|
2459 \nopagebreak |
|
2460 {\small See also \textit{debug} (\S\ref{output-format}) and |
|
2461 \textit{show\_skolems} (\S\ref{output-format}).} |
|
2462 |
|
2463 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds} |
2448 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds} |
2464 Specifies whether Nitpick should use Kodkod's transitive closure operator to |
2449 Specifies whether Nitpick should use Kodkod's transitive closure operator to |
2465 encode non-well-founded ``linear inductive predicates,'' i.e., inductive |
2450 encode non-well-founded ``linear inductive predicates,'' i.e., inductive |
2466 predicates for which each the predicate occurs in at most one assumption of each |
2451 predicates for which each the predicate occurs in at most one assumption of each |
2467 introduction rule. Using the reflexive transitive closure is in principle |
2452 introduction rule. Using the reflexive transitive closure is in principle |