Def-ctrex-rule
Define a rule that helps FGL derive term-level counterexamples from Boolean assignments.
This form defines an informal rule that FGL may use to help derive
assignments for theorem variables from the Boolean assignments returned by SAT
solvers. During this process (see fgl-counterexamples), various FGL objects
are assigned concrete values, and we use these values to derive further assignments.
A counterexample rule tells how to derive a new assignment from some
existing assignments. An example:
(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)
The rule is stored under an arbitrary name, the first argument. The rest of the arguments:
- :match gives a list of bindings (var expr). When applying the
rule, one or more of the expr entries must be matched against an object
with an existing assignment. For example, to apply the above rule we must have
an assignment of a value to some term matching (intcar x), (intcdr
x), or both. These assignments may come from three origins -- 1. the term
may be one that is assigned a Boolean variable in the Boolean variable
database (see fgl-getting-bits-from-objects); 2. the term may be contain
no variables and thus be evaluated under the Boolean assignment; 3. the term
may be given an assignment by applying other counterexample rules.
- :assigned-var and :assign respectively give the term to be
assigned the value and the value. In the above case, the subterm x from
that matched expressions is assigned the value (intcons car cdr), where
car and cdr are the values assigned for the respective expressions,
if they were assigned. If not, x may have been tentatively assigned a
value by a previous rule and its intcar or intcdr may be
preserved.
- :match-conds provide variables that say whether a value was determined
for the given variable. In this case, cdr-match will be true if
(intcdr x) (the binding of cdr in the :match field)) was
successfully assigned a value.
- :ruletype may be :elim, :property, or :fixup, signifying how the rule
is intended to be used. An :elim rule should be applied once when as many
of the match expressions as possible have been assigned values; at that point,
we apply the rule and compute the final value for the subexpression. A
:property rule may be applied to several different matching expressions in
order to compute a value for the same subexpression. A :fixup rule is placed
last in the order and is intended to fix up a previously assigned value.
- An additional keyword :assign-cond must (if provided) be a term, which
will be evaluated in the same way as :assign. If it evaluates to a
non-nil value, then the value is assigned; if not, the rule does not
provide an assignment.
An example of a property rule:
(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)
This is a suitable property rule, but not an elim rule, because it may match
many assignments to (assoc-equal k x) for different k in order to
compute a value for x.
