Fgl-counterexamples
Generating counterexamples from SAT checks in FGL
When FGL calls a SAT solver and it returns a satisfying assignment,
what we actually have is an assignment for the Boolean variables associated
with various symbolic objects in the Boolean variable database. Often what we
really want is an assignment to the original variables of the theorem, or to
certain objects within our local context. This topic discusses FGL's method of
deriving a term-level counterexample from a Boolean-level counterexample.
Note that what we are trying to do is not always possible! The underlying
problem is undecidable, and it depends very much on the set of rules in use
whether there might be interdependencies among the Boolean variables such that
the satisfying assignment for the SAT problem can't be realized in terms of the
theorem variables. For example, if one Boolean variable is associated with
(logbitp 0 x) and assigned T but another variable is associated with
(intcar x) and assigned NIL, that assignment can't be realized
because the two expressions are equal. This topic as well as fgl-getting-bits-from-objects offer advice for avoiding these
interdependencies and ensuring that term-level counterexamples may be easily
derived from Boolean satisfying assignments.
The input to our computation is essentially an assignment of Boolean values
to various FGL objects, namely the ones associated with Boolean variables in
the Boolean variable database. More specifically, we have the bvar-db
mapping Boolean variables to FGL objects and an env, the satisfying
assignment for these Boolean variables; but we can view this as an assignment
of values to FGL objects instead, since the names of the Boolean variables are
interchangeable.
Sketch of Algorithm
We begin with an assignment a of values to FGL objects, derived from the
bvar-db and env. We want to extend this assignment so that
eventually it includes values for all the theorem variables that are
consistent, i.e. the evaluations of all the objects in a match their
associated values.
The primary way of extending a with new assignment pairs is to apply
certain rules that say how we may derive new assignments from existing ones.
These rules may be added by users. The following example rules illustrate two
common types:
(def-ctrex-rule intcar-intcdr-ctrex-elim
:match ((car (intcar x))
(cdr (intcdr x)))
:match-conds ((cdr-match cdr)
(car-match car))
:assign (let ((cdr (if cdr-match cdr (intcdr x)))
(car (if car-match car (intcar x))))
(intcons car cdr))
:assigned-var x
:ruletype :elim)
(def-ctrex-rule assoc-equal-ctrex-rule
:match ((pair (assoc-equal k x)))
:assign (put-assoc-equal k (cdr pair) x)
:assigned-var x
:ruletype :property)
The first rule says that if we have an assignment of a value to some object
matching (intcar x) (that is, a :g-apply FGL object whose function
symbol is intcar) and an assignment to some other object matching
(intcdr x) (that is, a :g-apply object whose function symbol is
intcdr and whose argument is the same as that of the intcar object),
then we can derive a value for x (the shared argument of the two objects),
namely the intcons of the two values. If we only have an assignment to
one or the other, intcar or intcdr, then the other part is defaulted
to the intcar/intcdr of any current value tentatively assigned to
x.
The second rule says that if we have an assignment of a value pair to
(assoc-equal k x), then we can modify x to accomodate that by setting
it to (put-assoc-equal k (cdr pair) x). The :property ruletype, as
distinguished from the :elim ruletype of the previous rule, implies that
this rule can be applied several times to update the assignment to a term
x; i.e. we can build up an alist given the values assigned to several
different keys.
Another method of adding pairs is to copy values on the basis of
equivalences that are assumed. That is, if (equiv x y) is assigned T
and y is assigned some value, then assign x that same value.
Subtopics
- Def-ctrex-rule
- Define a rule that helps FGL derive term-level counterexamples from Boolean assignments.
