		Search-engine friendly clone of the ACL2 documentation.

Network

Aignet-lit-fix

(aignet-lit-fix x aignet) fixes the literal x to be a valid literal for this AIG network.

Signature
(aignet-lit-fix x aignet) → fix
Arguments: x — Guard (litp x).; aignet — Guard (node-listp aignet).
Returns: fix — Type (litp fix).

If x is a valid literal in the sense of aignet-litp, it is returned unchanged:

Theorem: aignet-lit-fix-when-aignet-litp

(defthm aignet-lit-fix-when-aignet-litp
  (implies (aignet-litp x aignet)
           (equal (aignet-lit-fix x aignet)
                  (lit-fix x))))

Otherwise we adjust it to refer to the constant node, which is unconditionally valid.

Definitions and Theorems

Function: aignet-lit-fix

(defun aignet-lit-fix (x aignet)
  (declare (xargs :guard (and (litp x) (node-listp aignet))))
  (let ((__function__ 'aignet-lit-fix))
    (declare (ignorable __function__))
    (make-lit (aignet-id-fix (lit->var x) aignet)
              (lit->neg x))))

Theorem: litp-of-aignet-lit-fix

(defthm litp-of-aignet-lit-fix
  (b* ((fix (aignet-lit-fix x aignet)))
    (litp fix))
  :rule-classes :type-prescription)

Theorem: aignet-litp-of-aignet-lit-fix

(defthm aignet-litp-of-aignet-lit-fix
  (aignet-litp (aignet-lit-fix x aignet)
               aignet))

Theorem: aignet-lit-fix-when-aignet-litp

(defthm aignet-lit-fix-when-aignet-litp
  (implies (aignet-litp x aignet)
           (equal (aignet-lit-fix x aignet)
                  (lit-fix x))))

Theorem: lit->var-of-aignet-lit-fix

(defthm lit->var-of-aignet-lit-fix
  (equal (lit->var (aignet-lit-fix x aignet))
         (aignet-id-fix (lit->var x) aignet)))

Theorem: lit->neg-of-aignet-lit-fix

(defthm lit->neg-of-aignet-lit-fix
  (equal (lit->neg (aignet-lit-fix x aignet))
         (lit->neg x)))

Theorem: aignet-lit-fix-of-lit-fix-x

(defthm aignet-lit-fix-of-lit-fix-x
  (equal (aignet-lit-fix (lit-fix x) aignet)
         (aignet-lit-fix x aignet)))

Theorem: aignet-lit-fix-lit-equiv-congruence-on-x

(defthm aignet-lit-fix-lit-equiv-congruence-on-x
  (implies (lit-equiv x x-equiv)
           (equal (aignet-lit-fix x aignet)
                  (aignet-lit-fix x-equiv aignet)))
  :rule-classes :congruence)

Theorem: aignet-lit-fix-of-node-list-fix-aignet

(defthm aignet-lit-fix-of-node-list-fix-aignet
  (equal (aignet-lit-fix x (node-list-fix aignet))
         (aignet-lit-fix x aignet)))

Theorem: aignet-lit-fix-node-list-equiv-congruence-on-aignet

(defthm aignet-lit-fix-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (aignet-lit-fix x aignet)
                  (aignet-lit-fix x aignet-equiv)))
  :rule-classes :congruence)