		Search-engine friendly clone of the ACL2 documentation.

Bfr-to-param-space

Perhaps strengthen a BFR under some hypothesis.

Signature
(bfr-to-param-space p x) → *

The general idea here is to use the hypothesis in order to strengthen the variables that are going to be used while symbolically simulating the conclusion. The BFR p is a representation of the hypothesis, and x is some BFR, typically a variable, that our hypothesis might tell us something about.

In BDD mode, we use BDD parameterization to produce a new BDD that is similar to x but that may be collapsed in cases where p is false. In AIG mode, we do something much lighter weight, and essentially just look for variables that we happen to know are true or false.

Definitions and Theorems

Function: bfr-to-param-space

(defun bfr-to-param-space (p x)
 (declare (xargs :guard t))
 (let ((__function__ 'bfr-to-param-space))
  (declare (ignorable __function__))
  (bfr-case
       :bdd (acl2::to-param-space p x)
       :aig (acl2::aig-restrict
                 x
                 (acl2::aig-extract-iterated-assigns-alist p 10)))))

Subtopics

Bfr-to-param-space-weak: Same as bfr-to-param-space for BDDs, but don't bother to do anything if we're working with AIGs.
Bfr-from-param-space