Cgen
Counterexample Generation a.k.a Disproving for ACL2
Using Cgen
Cgen is available and enabled in all ACL2 Sedan session modes except Compatible.
If it is not already available, you can use Cgen simply be submitting the following
commands:
(include-book "acl2s/cgen/top" :dir :system :ttags :all)
(acl2s-defaults :set testing-enabled t)
Introduction
Cgen is a powerful debugging facility that can be used to test/check
formulas for counterexamples automatically. It is implemented as a set of
books, tightly coupled with the defdata framework. Thus for the most
profitable use of Cgen, one should specify all type-like monadic predicates
using defdata or at least register such predicates as defdata types using
register-type. When Cgen is in effect via the testing-enabled
parameter, every checkpoint subgoal arising in event contexts such as thm,
defthm and verify-guards is checked (searched) for
counterexamples. So although you can integrate Cgen seamlessly in your
interactive proof workflow, we recommend the use of the specially designed
macro, test?.
To prove use thm, to disprove use test?
One can use test? as a drop-in replacement for thm
to disprove conjectures. test? guarantees that
counterexamples are printed in terms of the top goal's
variables. See test? for more details and examples.
More Powerful Theorem Proving
Cgen also defeats false generalizations. We have seen many
examples where defthms succeed with testing-enabled because
Cgen falsified a bad generalization, thereby causing ACL2 to
backtrack and modify its proof search path.
Example
Examine the proof output to see the backtracking.
(acl2s-defaults :set testing-enabled t) ;try first with nil
(defthm no-duplicates-remove
(implies (and (true-listp list)
(no-duplicatesp list))
(no-duplicatesp (remove x list))))
Control Parameters
The Cgen library can be configured via a collection of parameters using the
acl2s-defaults macro using the :get or :set keyword
arguments. In particular, see num-trials, verbosity-level,
testing-enabled. All the control parameters are package-agnostic.
Advanced Notes
The API functions/macros for Cgen library reside in the ACL2S package. Use
list (*acl2s-exports*) to import these symbols into your own
package.
More details
To understand more about how testing works, please refer to the following
paper
Subtopics
- Defdata
- A Data Definition Framework
- Test?
- Test/Check a conjecture for counterexamples.
- ACL2s-defaults
- Getting and setting defaults for various parameters in Cgen (ACL2 Sedan)
- Prove/cgen
- top-level API function for Cgen/testing.
- Register-type
- Register a name as a defdata type
- With-timeout
- Evaluate form with a timeout (in seconds)
- Defdata-attach
- Attach/modify metadata for a defdata type
- Testing-enabled
- Testing enable/disable flag
- 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
- 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
- Test-then-skip-proofs
- The ACL2s version of skip-proofs.
- 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
- Cgen::flush
- Flush/Reset the Cgen state globals to sane values.
- Backtrack-bad-generalizations
- Specify whether to check for and then backtrack from bad generalizations.
- Use-fixers
- Specify whether fixers are to be used.
- Thm-no-test
- A version of thm with testing disabled.
- Defthmd-no-test
- A version of defthmd with testing disabled.
- Defthm-no-test
- A version of defthm with testing disabled.
