• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
        • Aig-constructors
        • Aig-vars
        • Aig-sat
        • Bddify
        • Aig-substitution
          • Aig-partial-eval
          • Aig-restrict
          • Aig-compose
          • Aig-restrict-alist
          • Aig-partial-eval-alist
          • Aig-compose-alist
          • Aig-restrict-alists
          • Aig-compose-alists
          • Aig-restrict-list
          • Aig-partial-eval-list
          • Aig-compose-list
        • Aig-other
        • Aig-semantics
        • Aig-and-count
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Aig

Aig-substitution

AIG operations for carrying out substitutions, compositions, and partial evaluations.

Subtopics

Aig-partial-eval
(aig-partial-eval x env) evaluates x, an AIG, under the partial environment env, producing a new AIG as a result.
Aig-restrict
(aig-restrict x sigma) performs variable substitution throughout the AIG x, replacing any variables bound in sigma with their corresponding values.
Aig-compose
(aig-compose x sigma) performs variable substitution throughout the AIG x, unconditionally replacing every variable in x with its binding in sigma.
Aig-restrict-alist
(aig-restrict-alist x sigma) substitutes into an AIG Alist (an alist binding keys to AIGs).
Aig-partial-eval-alist
(aig-partial-eval-alist x env) partially evaluates an AIG Alist (an alist binding keys to AIGs).
Aig-compose-alist
(aig-compose-alist x sigma) composes into an AIG Alist (an alist binding keys to AIGs).
Aig-restrict-alists
(aig-restrict-alists x sigma) substitutes into a list of AIG Alists.
Aig-compose-alists
(aig-compose-alists x sigma) composes into a list of AIG Alists.
Aig-restrict-list
(aig-restrict-list x sigma) substitutes into a list of AIGs.
Aig-partial-eval-list
(aig-partial-eval-list x env) partially evaluates a list of AIGs.
Aig-compose-list
(aig-compose-list x sigma) composes into a list of AIGs.