		Search-engine friendly clone of the ACL2 documentation.

Ubdds

Bdd-sat-dfs

(bdd-sat-dfs x) finds a satisfying assignment for the UBDD x, if one exists. It works even if x is not a well-formed UBDD, but it might be slow in that case.

Definitions and Theorems

Function: bdd-sat-dfs

(defun
 bdd-sat-dfs (x)
 (declare (xargs :guard t))
 (if (atom x)
     nil
     (let* ((a (car x)) (d (cdr x)))
           (cond ((and (atom a) a) '(t))
                 ((and (atom d) d) '(nil))
                 (t (let ((rec1 (bdd-sat-dfs a)))
                         (if rec1 (cons t rec1)
                             (let ((rec2 (bdd-sat-dfs d)))
                                  (and rec2 (cons nil rec2))))))))))

Theorem: bdd-sat-dfs-produces-satisfying-assign

(defthm bdd-sat-dfs-produces-satisfying-assign
        (implies (bdd-sat-dfs x)
                 (eval-bdd x (bdd-sat-dfs x))))

Theorem: bdd-sat-dfs-not-satisfying-when-nil

(defthm bdd-sat-dfs-not-satisfying-when-nil
        (implies (and (consp x) (not (bdd-sat-dfs x)))
                 (not (eval-bdd x vars))))

Theorem: bdd-sat-dfs-correct

(defthm bdd-sat-dfs-correct
        (implies (eval-bdd x vars)
                 (eval-bdd x (bdd-sat-dfs x))))