Itest?-query
Find counterexamples to an ACL2s statement.
General form
(itest?-query
stmt ;; The statement to find counterexamples to.
:num-counterexamples ... ;; Optional. If non-nil, the number of counterexamples to request from itest?.
:quiet ... ;; Optional. Whether or not to suppress all ACL2 printed output. Defaults to t.
:prover-step-limit ... ;; Optional. Sets the prover step limit. See @(see acl2s-query) for more information
;; about the default value.
)
=>
(list cts-found? itest?-res)
- Returns
- cts-found? is nil if no counterexamples were found, or t otherwise.
- itest?-res is a list list of the form (status cts wts), where
status is either nil, :falsifiable or :? and cts and wts are
assignments, with cts corresponding to counterexamples and wts to
witnesses returned by itest?. If cts-found? is nil (no counterexamples) and itest? proved
the conjecture, then itest?-res is of the form (nil nil
wts). If status is :falsifiable then cts is a
non-empty list. If status is :? then cts is nil,
and the conjecture was not proved.
The stmt argument should be an ACL2 expression. Be careful about symbol packages when using itest?-query when inside a different package - you may need to fully specify the name of an ACL2 function when calling it. See ACL2s-interface::ACL2s-interface-symbol-package-tips for more information.
When the :quiet option is set to t, itest?-query will attempt to suppress all ACL2 printed output while itest? is running. This temporarily overrides the current ACL2s-interface::quiet-mode.
itest?-query evaluates itest? inside of a with-prover-step-limit, where the step-limit is set to the value provided to :prover-step-limit, or ACL2's set prover-step-limit if that option is not provided. See set-prover-step-limit for more information about the prover step-limit. If you don't want to limit the number of prover steps permitted for itest?, set :prover-step-limit to nil.
:num-counterexamples allows one to request more counterexamples
from itest? than acl2s-defaults specifies. Note that
itest? will not always produce the number of counterexamples
requested. You may get more or less counterexamples. See test?
for a discussion of stopping conditions.
In some cases, itest? may produce counterexamples where some variables are assigned the value 'acl2::?. This indicates that itest? did not need to bind a value to those variables for the statement to evaluate to nil, given the other variable assignments.
See ACL2::test? for more information about ACL2s' counterexample generation facilities. itest? is essentially a slightly modified version of test? that provides more information programmatically.
Examples
(itest?-query '(implies (integerp x) (natp x)))
Returns
(T
(:FALSIFIABLE
(((X -371)) ((X -1)) ((X -945)) ((X -297)) ((X -850)) ((X -487)) ((X -201))
((X -18)) ((X -817)))
NIL)) (note that values for x may be different)
(itest?-query '(implies (natp x) (integerp x)))
Returns
(NIL (NIL NIL (((X 161)) ((X 5)) ((X 169)) ((X 8)) ((X 9)) ((X 417)))))
(itest?-query '(implies (true-listp x) (< (length x) 50)))
Returns
(NIL
(:? NIL
(((X '(0 0))) ((X '(ACL2S::ABA))) ((X '(ACL2S::A ACL2S::A))) ((X '(0)))
((X NIL)) ((X '(NIL NIL NIL NIL NIL))) ((X '(-1 (0 . T))))
((X '((NIL . T) (((T) T) (NIL) T))))))). This is an example of a case where counterexamples exist (i.e. a list of 50 0's) but
itest? cannot find any.
(itest?-query '(implies (and (natp x) (natp y) (natp z) (> x 0) (> y 0) (< z 100)) (/= z (+ (* x x) (* y y)))))
Returns
(T
(:FALSIFIABLE
(((Z 85) (Y 2) (X 9)) ((Z 41) (Y 4) (X 5)) ((Z 37) (Y 6) (X 1))
((Z 53) (Y 7) (X 2)) ((Z 37) (Y 1) (X 6)) ((Z 29) (Y 5) (X 2)))
(((Z 76249) (Y 260) (X 93)) ((Z 254137) (Y 484) (X 141))
((Z 13130) (Y 83) (X 79))))).
