		Search-engine friendly clone of the ACL2 documentation.

Cgraph

Ctrex-rule

Internal structure of a counterexample generation rule

This is a product type introduced by defprod.

Fields

name — symbolp
match — pseudo-term: Pattern to be matched in order to trigger this rule
unify-subst — fgl-object-bindings: Initial substitution for unifying with match -- usually nil
target — pseudo-term: Term representing the object that will be assigned a value based on this rule
deps — cmr::pseudo-term-subst: Substitution giving the dependencies of the rule
dep-success-vars — cmr::pseudo-term-subst: Pairs such as (a-success . a) where a is one of the keys of deps. Vars such as a-success may then be used in the success/priority/value formulas.
success — pseudo-term: Term evaluated to determine whether the formula was successful
priority — pseudo-term: Term evaluated to determine the priority of the formula application
value — pseudo-term: Term evaluated to compute the value of the target
order — natp: Relative ordering, for determining which formulas to evaluate first/last -- use constants *ctrex-order-first*, *ctrex-order-mid*, *ctrex-order-last*.
ruletype — ctrex-ruletype-p

As discussed in cgraph, this is the format in which a rule is stored. This rule has one match pattern, determining the objects on which the rule triggers. A rule definition form may create more than one ctrex-rule (of the same name) to accomodate different patterns that might match.

Subtopics

Ctrex-rule-fix: Fixing function for ctrex-rule structures.
Make-ctrex-rule: Basic constructor macro for ctrex-rule structures.
Ctrex-rule-p: Recognizer for ctrex-rule structures.
Ctrex-rule-equiv: Basic equivalence relation for ctrex-rule structures.
Ctrex-rule->dep-success-vars: Get the dep-success-vars field from a ctrex-rule.
Change-ctrex-rule: Modifying constructor for ctrex-rule structures.
Ctrex-rule->unify-subst: Get the unify-subst field from a ctrex-rule.
Ctrex-rule->ruletype: Get the ruletype field from a ctrex-rule.
Ctrex-rule->priority: Get the priority field from a ctrex-rule.
Ctrex-rule->value: Get the value field from a ctrex-rule.
Ctrex-rule->target: Get the target field from a ctrex-rule.
Ctrex-rule->success: Get the success field from a ctrex-rule.
Ctrex-rule->match: Get the match field from a ctrex-rule.
Ctrex-rule->deps: Get the deps field from a ctrex-rule.
Ctrex-rule->order: Get the order field from a ctrex-rule.
Ctrex-rule->name: Get the name field from a ctrex-rule.