4v-sexpr-to-faig
Translation from 4v-sexprs into a faigs.
It is often useful to be able to convert a sexpr into a faig, since then you can apply AIG/FAIG based tools such as ABC, sat solvers,
the bddify algorithm, and so forth to sexpr-based models. For instance,
we use this conversion to implement an efficient gl symbolic counterpart
for 4v-sexpr-eval, which is used in practically all of our GL-based
hardware proofs.
Signature: (4v-sexpr-to-faig x onoff &key (optimize 't)) builds an faig.
x is the sexpr you want to convert into an FAIG.
onoff argument should be an alist that assigns an initial FAIG for
every variable of x. Commonly the onoff alist should bind each
variable v to some pair of fresh variables like (v1 . v0), i.e.,
v1 is the onset variable and v0 is the offset variable for v,
but other uses are also possible. It is beneficial for onoff to be a fast
alist, but it will be made fast if necessary.
optimize is an optional flag that defaults to t. When
optimization is allowed, we convert the sexpr in a smarter way that is
generally faster and produces smaller FAIGs which may be easier for other tools
to analyze. You almost certainly want optimization unless you are doing
certain kinds of fragile AIG decomposition where you really want AIGs that are
exactly the same. (If that sounds like nonsense, then you want
optimization.)
The basic idea of the optimization is to take advantage of the fact that
many sexpr operations are actually "three-valued," i.e., they never produce
Z. For instance, when we are converting a sexpr like (NOT (AND A B)) into
an faig, since we know the result of an AND gate is never Z, it
suffices to use t-aig-not instead of f-aig-not. There are
similar reductions for many gates; see faig-constructors for some
details.
You might regard 4v-sexpr-to-faig as a somewhat low-level function.
Its correctness theorem is rather elaborate and to make use of it you generally
need to construct an onoff alist that sensibly accomplishes your goal. A
good starting place and example might be 4v-sexpr-eval-by-faig, which
generates an appropriate onoff so that it can carry out a 4v-sexpr-eval computation using FAIG evaluation as the engine.
Function: 4v-sexpr-to-faig-fn1
(defun 4v-sexpr-to-faig-fn1 (x onoff optimizep)
"Assumes ONOFF is fast."
(declare (xargs :guard t))
(if optimizep (4v-sexpr-to-faig-opt x onoff)
(4v-sexpr-to-faig-plain x onoff)))
Function: 4v-sexpr-to-faig-fn
(defun 4v-sexpr-to-faig-fn (x onoff optimizep)
"Assumes ONOFF is fast."
(declare (xargs :guard t))
(with-fast-alist onoff
(if optimizep (4v-sexpr-to-faig-opt x onoff)
(4v-sexpr-to-faig-plain x onoff))))
Theorem: 4v-sexpr-to-faig-fn1-removal
(defthm 4v-sexpr-to-faig-fn1-removal
(equal (4v-sexpr-to-faig-fn1 x onoff optimizep)
(4v-sexpr-to-faig-fn x onoff optimizep)))
Theorem: consp-of-4v-sexpr-to-faig-fn
(defthm consp-of-4v-sexpr-to-faig-fn
(consp (4v-sexpr-to-faig-fn x onoff optimize))
:rule-classes :type-prescription)
Theorem: faig-eval-of-4v-sexpr-to-faig
(defthm faig-eval-of-4v-sexpr-to-faig
(equal (faig-eval (4v-sexpr-to-faig-fn x onoff optimize)
env)
(faig-eval (4v-sexpr-to-faig-plain x onoff)
env)))
Subtopics
- 4v-and-faig-operations-commute
- Lemmas showing that equivalence of 4v-operations to faig-constructors.
- 4v-sexpr-to-faig-plain
- Non-optimized conversion from sexprs into faigs.
- 4v-sexpr-to-faig-opt
- Optimized conversion from sexprs into faigs.
- Sfaig
- A simplified version of 4v-sexpr-to-faig that constructs its
own onoff list out of the variables of the sexpr.
- 4v->faig-const
- Convert a 4vp into a faig-const-p.
- 4v-sexpr-to-faig-list
- Convert a sexpr list into a faig list.
- Faig-const-fix
- Identity for FAIG constants, or constant X otherwise.
- Faig-const->4v
- Convert a faig-const-p into a 4vp.
- 4v-sexpr-to-faig-alist
- Convert a sexpr alist into an faig alist.
- Faig-const-<=
- Lattice ordering for FAIG constants.
- Faig-const-p
- Recognizer for constant faigs.
