• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
      • Aig-constructors
      • Aig-vars
      • Aig-sat
      • Bddify
      • Aig-substitution
      • Aig-other
        • Best-aig
        • Aig2c
        • Expr-to-aig
        • Aiger-write
        • Aig-random-sim
        • Aiger-read
        • Aig-print
        • Aig-cases
      • 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
  • Testing-utilities
  • Math

• Aig-other

Expr-to-aig

Convert an ACL2-like S-expression into an AIG.

(expr-to-aig expr) accepts S-expressions expr such as:

a
(not a)
(and a b c)

It currently accepts S-expressions composed of the following operators, all of which are assumed to be Boolean-valued (i.e., there's nothing four-valued going on here):

• not -- unary
• and, or, nand, nor -- variable arity
• iff, xor, implies -- binary
• if -- ternary

It constructs an AIG from the S-expression using the ordinary aig-constructors.

This can be useful for one-off debugging. We probably wouldn't recommend using it for anything serious, or trying to prove anything about it.

Definitions and Theorems

Function: expr-to-aig

(defun expr-to-aig (expr)
  (declare (xargs :guard t))
  (if (atom expr)
      expr
    (let ((fn (car expr)) (args (cdr expr)))
      (cond ((and (eq fn 'not) (= (len args) 1))
             (aig-not (expr-to-aig (car args))))
            ((eq fn 'and)
             (expr-to-aig-args 'and t args))
            ((eq fn 'or)
             (expr-to-aig-args 'or nil args))
            ((eq fn 'nand)
             (aig-not (expr-to-aig-args 'and t args)))
            ((eq fn 'nor)
             (aig-not (expr-to-aig-args 'or nil args)))
            ((and (eq fn 'iff) (= (len args) 2))
             (aig-iff (expr-to-aig (car args))
                      (expr-to-aig (cadr args))))
            ((and (eq fn 'xor) (= (len args) 2))
             (aig-xor (expr-to-aig (car args))
                      (expr-to-aig (cadr args))))
            ((and (eq fn 'implies) (= (len args) 2))
             (aig-or (aig-not (expr-to-aig (car args)))
                     (expr-to-aig (cadr args))))
            ((and (eq fn 'if) (= (len args) 3))
             (aig-ite (expr-to-aig (car args))
                      (expr-to-aig (cadr args))
                      (expr-to-aig (caddr args))))
            (t (prog2$ (er hard? 'expr-to-aig
                           "Malformed: ~x0~%" expr)
                       nil))))))

Function: expr-to-aig-args

(defun expr-to-aig-args (op final exprs)
  (declare (xargs :guard t))
  (if (atom exprs)
      final
    (let ((first (expr-to-aig (car exprs)))
          (rest (expr-to-aig-args op final (cdr exprs))))
      (case op
        (and (aig-and first rest))
        (or (aig-or first rest))))))