		Search-engine friendly clone of the ACL2 documentation.

Bfr-reasoning

Bfr-eval-cp

The actual clause processor for bfr-reasoning.

Signature
(bfr-eval-cp clause hints) → *

Definitions and Theorems

Function: bfr-eval-cp

(defun bfr-eval-cp (clause hints)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-eval-cp))
    (declare (ignorable __function__))
    (let* ((bfr-terms (car hints))
           (patterns (cadr hints))
           (eval-patterns (caddr hints))
           (vals (bfr-eval-vals clause eval-patterns))
           (clause (instantiate-equals-with-bfr-evals
                        clause vals bfr-terms patterns)))
      (list clause))))

Theorem: bfr-eval-cp-correct

(defthm bfr-eval-cp-correct
  (implies
       (and (pseudo-term-listp clause)
            (alistp a)
            (bfr-cp-ev (conjoin-clauses (bfr-eval-cp clause hints))
                       a))
       (bfr-cp-ev (disjoin clause) a))
  :rule-classes :clause-processor)

Subtopics

Instantiate-equals-with-bfr-evals
Instantiate-bfr-evals
Collect-bfr-eval-vals
Bfr-eval-vals