		Search-engine friendly clone of the ACL2 documentation.

ACL2s-defaults

Getting and setting defaults for various parameters in Cgen (ACL2 Sedan)

Examples

(acl2s-defaults :set num-trials 1000)
(acl2s-defaults :get cgen-local-timeout)
(acl2s-defaults :get testing-enabled)
(acl2s-defaults :set num-counterexamples 3)

The following parameters are available for control via acl2s-defaults. These are stored in the constant *acl2s-parameters* and are package-agnostic.

num-trials
verbosity-level
num-counterexamples
num-witnesses
sampling-method
backtrack-limit
search-strategy
testing-enabled
cgen-timeout
cgen-local-timeout
cgen-single-test-timeout
print-cgen-summary
use-fixers
num-print-counterexamples
num-print-witnesses

Subtopics

Defdata-aliasing-enabled: Enable Defdata aliasing
Cgen-single-test-timeout: Cgen/Testing timeout for single, individual tests (in seconds)
Verbosity-level: Control verbosity of Cgen
Testing-enabled: Testing enable/disable flag
Search-strategy: Specify the search strategy to be used.
Num-print-counterexamples: Number of Counterexamples to be printed
Cgen-timeout: test?/prover timeout (in seconds)
Cgen-local-timeout: Cgen/Testing timeout (in seconds)
Num-witnesses: Number of Witnesses to be shown
Num-trials: Max number of tries to find counterexamples
Num-print-witnesses: Number of Witnesses to be printed
Sampling-method: Specify sampling method to be used to instantiate variables
Recursively-fix: Specify whether unsatisfied but fixable constraints are to be recursively fixed.
Num-counterexamples: Number of Counterexamples to be searched
Backtrack-limit: Maximum number of backtracks allowed (per variable)
Print-cgen-summary: Print summary for Cgen
Backtrack-bad-generalizations: Specify whether to check for and then backtrack from bad generalizations.
Use-fixers: Specify whether fixers are to be used.