		Search-engine friendly clone of the ACL2 documentation.

Base-api

Aignet-add-and

(aignet-add-and f0 f1 aignet) adds an new AND gate node to the aignet with the given fanin literals.

Note: this is a very low level function. It is often better to use routines like aignet-hash-and, aignet-hash-or, etc., which can do some simplifications to produce smaller aig networks.

Logically this is just:

(cons (gate-node (aignet-lit-fix f0 aignet)
                 (aignet-lit-fix f1 aignet))
      aignet)

The aignet-lit-fixes ensure that well-formedness of the network is preserved unconditionally.

In the execution we update the necessary arrays, counts, etc.

Function: aignet-add-and^

(defun aignet$a::aignet-add-and^ (f0 f1 aignet)
  (declare
       (xargs :guard (and (litp f0)
                          (litp f1)
                          (aignet$a::aignet-well-formedp aignet))))
  (declare (xargs :guard (and (aignet$a::id-existsp (lit->var f0)
                                                    aignet)
                              (aignet$a::id-existsp (lit->var f1)
                                                    aignet)
                              (< (aignet$a::num-fanins aignet)
                                 536870911))))
  (let ((__function__ 'aignet$a::aignet-add-and^))
    (declare (ignorable __function__))
    (cons (and-node (aignet-lit-fix f0 aignet)
                    (aignet-lit-fix f1 aignet))
          (node-list-fix aignet))))