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 theexpr 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 subtermx from that matched expressions is assigned the value(intcons car cdr) , wherecar andcdr 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 itsintcar orintcdr 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 ofcdr in the:match field)) was successfully assigned a value.:ruletype may be:elim or:property , 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.- 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