Make or apply a

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

We will introduce clause-processor rules by way of the following example.
But note that the clause-processor utility is more general than this example
may suggest; for example, the second argument of

; Example (which we'll return to, below): (defthm correctness-of-note-fact-clause-processor (implies (and (pseudo-term-listp cl) (alistp a) (evl0 (conjoin-clauses (note-fact-clause-processor cl term)) a)) (evl0 (disjoin cl) a)) :rule-classes :clause-processor)

We begin this documentation with an introduction, focusing on the example
above, and then conclude with a detailed general discussion of
clause-processor rules. You might find it most useful simply to look at the
examples in community books directory

Also see define-trusted-clause-processor for documentation of an
analogous utility that does not require the clause-processor to be proved
correct. But please read the present documentation before reading about that
utility. Both utilities designate functions as ``clause-processors''. Such
functions must be executable — hence not constrained by virtue of being
introduced in the signature of an `encapsulate` — and must
respect stobj and output arity restrictions. For example, something
like

A `or`). For
example, if ACL2 prints a goal in the form *translated* terms; see term and
`termp`. For example, they do not contain calls of the macro

The recognizer for a clause is the function `term-listp` and the
recognizer for a list of clauses is `term-list-listp`.

Note that clause-processor simplifiers are similar to metafunctions, and similar efficiency considerations apply. See meta, in particular the discussion on how to ``make a metafunction maximally efficient.''

Unlike rules of class `meta`, rules of class

We begin with a simple illustrative example: a clause-processor that
assumes an alleged fact (named

(defun note-fact-clause-processor (cl term) (declare (xargs :guard t)) ; optional, for better efficiency (list (cons (list 'not term) cl) (list term)))

As with `meta` rules, we need to introduce a suitable
evaluator; see defevaluator if you want details. Since we expect to
reason about the function `not`, because of its role in

(defevaluator evl0 evl0-list ((not x) (if x y z)))

ACL2 can now prove the following theorem automatically. (This is the
example displayed at the outset of this documentation topic.) Of
course, `or` to its members), and

(defthm correctness-of-note-fact-clause-processor (implies (and (pseudo-term-listp cl) (alistp a) (evl0 (conjoin-clauses (note-fact-clause-processor cl term)) a)) (evl0 (disjoin cl) a)) :rule-classes :clause-processor)

Now let us submit a silly but illustrative example theorem to ACL2, to show
how a corresponding

ACL2 !>(thm (equal (car (cons x y)) x) :hints (("Goal" :clause-processor (note-fact-clause-processor clause '(equal a a))))) [Note: A hint was supplied of the goal above. Thanks!] We now apply the verified :CLAUSE-PROCESSOR function NOTE-FACT-CLAUSE- PROCESSOR to produce two new subgoals. Subgoal 2 (IMPLIES (EQUAL A A) (EQUAL (CAR (CONS X Y)) X)). But we reduce the conjecture to T, by the :executable-counterpart of IF and the simple :rewrite rule CAR-CONS. Subgoal 1 (EQUAL A A). But we reduce the conjecture to T, by primitive type reasoning. Q.E.D. Summary Form: ( THM ...) Rules: ((:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Proof succeeded. ACL2 !>

That concludes our introduction to clause-processor rules and hints. We turn now to detailed documentation.

The signature of a clause-processor function, `state`) while the other parameters and results are not stobjs
(see stobj). Note that there need not be input stobjs in [3] —
i.e.,

[1] ((CL-PROC cl) => cl-list) [2] ((CL-PROC cl hint) => cl-list) [3] ((CL-PROC cl hint st_1 ... st_k) => (mv erp cl-list st_i1 ... st_in)) [3+] ((CL-PROC cl hint st_1 ... st_k) => (mv erp cl-list st_i1 ... st_in d))

We call *clauses-result*. In [3] and [3+], we think
of the first component of the result as an error flag. Indeed, a proof will
instantly abort if that error flag is not

We next discuss the legal forms of

If a `rule-classes` specification includes
`world` to help prove the rule; see meta-extract for explanation of this
advanced feature.)

; General Form (omitting possible meta-extract hypotheses) (implies (and (pseudo-term-listp CL) (alistp A) (EVL (conjoin-clauses <CL-LIST>) B)) (EVL (disjoin CL) A))

Here

(clauses-result (CL-PROC CL HINT ...))

Logically, `cadr` if the `car`
is

In the above theorem, we are asked to prove

The clause-processor function,

Next we specify the legal forms for

But there are two additional general forms for

:clause-processor (:function F) :clause-processor (:function F :hint HINT)

The first of these

:clause-processor (CL-PROC clause)

Similarly the second of the

:clause-processor (CL-PROC clause HINT st_1 ... st_k)

Besides the ``

:clause-processor F

This expands to a basic form as follows, depending on

- If
F is a macro with one required argument or a function symbol with one argument:

:clause-processor (F clause) - If
F is a macro with two required arguments or a function symbol with two arguments:

:clause-processor (F clause nil) - If
F is a function symbol with inputs of the form [3] or [3+] above, that is, with input signature(nil nil st_1 ... st_k) :

:clause-processor (F clause nil st_1 ... st_k)

For examples of these syntactic forms, see community book

A `well-formedness-guarantee` has been provided with the `set-skip-meta-termp-checks` has been used with an active trust
tag to skip the check at the user's risk.

The proof also aborts when the clause-processor function returns at least
two values and the first value returned — the ``

If there is no error as above, but the

You can see all current

The following paper discusses ACL2 clause-processors at a high level suitable for a non-ACL2 audience:

M. Kaufmann, J S. Moore, S. Ray, and E. Reeber, ``Integrating External Deduction Tools with ACL2.''

Journal of Applied Logic(Special Issue: Empirically Successful Computerized Reasoning), Volume 7, Issue 1, March 2009, pp. 3–25. Also published online (DOI10.1016/j.jal.2007.07.002 ). Preliminary version in: Proceedings of the 6th International Workshop on the Implementation of Logics (IWIL 2006) (C. Benzmueller, B. Fischer, and G. Sutcliffe, editors), CEUR Workshop Proceedings Vol. 212, Phnom Penh, Cambodia, pp. 7–26, November 2006.

- Meta-extract
- Meta reasoning using valid terms extracted from context or world
- Set-skip-meta-termp-checks
- Skip output checks for meta functions and clause-processors
- Make-summary-data
- Return summary data from a clause-processor function
- Clause-processor-tools
- Noteworthy clause-processors
- Set-skip-meta-termp-checks!
- Skip output checks non-locally for meta functions and clause-processors