Aig-semantics
Functions related to the semantic meaning of AIGs, e.g., aig-eval and aig-equiv.
Subtopics
- Aig-eval
- (aig-eval x env) gives the semantics of aigs: it gives the
Boolean value of the AIG x under the environment env.
- Aig-alist-equiv
- We say the AIG Alists X and Y are equivalent when they bind
the same keys to equivalent AIGs, in the sense of aig-equiv.
- Aig-env-equiv
- We say the environments X and Y are equivalent when they
give equivalent values to variables looked up with aig-env-lookup.
- Aig-equiv
- We say the AIGs X and Y are equivalent when they always
evaluate to the same value, per aig-eval.
- Aig-eval-alist
- (aig-eval-alist x env) evaluates an AIG Alist (an alist binding keys
to AIGs).
- Aig-eval-list
- (aig-eval-list x env) evaluates a list of AIGs.
- Aig-eval-alists
- Evaluate a list of AIG Alists.
