False-counterexamples
Occasionally, GL will abort a proof after printing:
False counterexample! See :xdoc gl::false-counterexamples.
Most of the time, you might think of GL as an "exact" system where we have
an explicit Boolean function representation of every bit in all the objects in
your conjecture. Ideally, this should allow GL to either prove your theorem or
find a counterexample.
This isn't always the case. Sometimes GL represents objects more abstractly.
For example, GL tends not to support operations on non-integer rational
numbers. If it runs into a call of (* 1/3 x), it may represent the result
abstractly, as a term-like symbolic object:
(:g-apply binary-* 1/3 (:g-integer ...))
(assuming x is represented as a :g-integer object). This sort of
abstraction can help to avoid creating potentially very-expensive symbolic
objects, and is an important part of GL's term-level-reasoning.
This kind of abstraction can be contagious. For example, if we are trying
to prove (not (equal (* 1/3 x) 'not-a-number)), then using the
:g-apply representation for the * subterm will likely cause GL to
also use a :g-apply representation for the whole term. But now, how is GL
supposed to give this to a SAT solver?
When GL finds a :g-apply object in a Boolean context, such as an IF
test or a theorem's hypothesis or conclusion, it will create a fresh Boolean
variable to represent that term. But if, say, that term is something like
(:g-apply equal (:g-apply binary-* 1/3 ...)
not-a-number)
which is always false, then this Boolean variable is too general, and by
replacing the term with the Boolean variable, GL has lost track of the fact
that the term is actually always false. This generally leads to false
counterexamples.
Dealing with False Counterexamples
The first things to check for when you encounter a false counterexample:
- Missing :g-bindings: When a variable is omitted from the
:g-bindings form, a warning is printed and the missing variable is
assigned a :g-var object. A :g-var can represent any ACL2 object,
without restriction. Symbolic counterparts typically produce :g-apply
objects when called on :g-var arguments, and this can easily lead to false
counterexamples.
- The stack depth limit, or "clock", was exhausted. This may happen when
symbolically executing a recursive function if the termination condition can't
be detected, though this is often caused by previous introduction of an
unexpected G-APPLY object.
- An unsupported primitive was called. For example, as of August 2013 we do
not yet support UNARY-/, so any call of UNARY-/ encountered during symbolic
execution will return a G-APPLY of UNARY-/ to the input argument. It may be
that you can avoid calling such functions by installing an alternate definition.
- A primitive was called on an unsupported type of symbolic object. For
example, the symbolic counterparts for most arithmetic primitives will produce
a G-APPLY object if an input seems like it might represent a non-integer
rational. Since symbolic operations on rationals are absurdly expensive, we
simply don't implement them for the most part.
It is common to use GL in such a way that G-VAR forms are not used, and
G-APPLY forms are unwelcome if they appear at all; when they do, they typically
result in a symbolic execution failure of some sort. However, there are ways
of using GL in which G-VAR and G-APPLY forms are expected to exist; see term-level-reasoning. If you are not expecting GL to create G-APPLY objects
but you are encountering false counterexamples, we suggest using the following
form to determine why a G-APPLY object is first being created:
(gl::break-on-g-apply)
Then when GL::G-APPLY is called in order to create the form, (BREAK$)
will be called. Usually this will allow you to look at the backtrace and
determine in what context the first G-APPLY object is being created.
Alternatively, if you are expecting some G-APPLY forms to be created but
unexpected ones are cropping up, you can make the break conditional
on the function symbol being applied:
(gl::break-on-g-apply :allowed-fns (foo bar))
