Prove/cgen
top-level API function for Cgen/testing.
Introduction
This is the main API function to test/check a form for counterexamples with
the full power of prove (and hints), i.e. prove/cgen actually calls
prove as a subfunction. You can accomplish the same thing using thm,
defthm with the acl2s defaults parameter testing-enabled set to T,
but this function gives the user/caller more control: the user is responsible
to pass cgen-state (use make-cgen-state to construct one), that
provides the context for cgen/testing; the results and statistics
summarizing Cgen/testing are collected in cgen-state and this is returned to
the caller.
General Form:
(prove/cgen form hints cgen-state state) => (mv erp cgen-state state)
The erp part of result is nil, if call to prove was
successful, it is :falsifiable if there is at least one
counterexample (not necessarily top-level), it is t if there was a error
in trans-eval call of prove (usually a hard/raw lisp error), it is :?
otherwise, which points out that we could neither prove nor disprove the
conjecture under consideration
Example
For an example of the use of prove/cgen, you can study the
implementation of the test? macro itself found in cgen/top.lisp. To see
the structure of cgen-state, you can study the
print-testing-summary-fn function which deconstructs it and prints its
information in a human-readable form.
