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.
Generally, a value for one term-like object suggests a value for some
subterm object, as in the rules above. However, if an object is composed of
subterms that can be assigned values, then that parent object can be computed
directly from these subterm values.
More details on the implementation of the derivation of counterexamples can
be found under the cgraph topic.
Counterexamples can be derived and run from SAT calls during rewriting. The
following functions can be used inside a syntaxp, syntax-interp,
or syntax-bind form:
- interp-st-run-ctrex: After a satisfiability call produces a SAT
result, fetch the satisfying assignment from the solver (for the given sat-config),
turn the satisfying assignment into a term-level counterexample and
evaluate the top-level goal on that counterexample.
- interp-st-sat-counterexample: Fetch the satisfying assignment from
the SAT solver (for the given sat-config) and store it in the FGL interpreter
state. This must be done before the deriving the counterexample using the
functions below; on the other hand, it is not a prerequisite for
interp-st-run-ctrex.
- interp-st-counterex-bindings: Derive a counterexample from the
latest satisfiable SAT check (if any), and evaluate the given symbolic object
bindings under that counterexample. Additionally returns the counterexample's
assignment of top-level theorem variables.
- interp-st-counterex-bindings/print-errors: like
interp-st-counterex-bindings but also summarizes any counterexample
derivation errors.
- interp-st-counterex-stack-bindings/print-errors: like
interp-st-counterex-bindings/print-errors but uses the bindings of the top stack
frame (i.e. the rewrite rule from which this function is called).
- interp-st-counterex-prev-stack-bindings/print-errors: like
interp-st-counterex-stack-bindings/print-errors but uses the bindings of
the next-to-top stack frame (i.e. the caller of the rewrite rule from which
this function is called).
Counterexample derivation, as well as running the goal term after the
counterexample is derived, uses an evaluator function called
magitastic-ev. This evaluator allows function definitions to be overridden
for the purpose of running counterexamples, by adding entries to a table. This
can be used to speed up counterexample generation or cheat to work around
abstractions that don't allow the production of top-level counterexamples.
Subtopics
- Def-ctrex-rule
- Define a rule that helps FGL derive term-level counterexamples from Boolean assignments.
- Fgl-counterexample-implementation-details
- Parent topic for implementation specifics of FGL counterexample generation
