An executable version of faig-purebool-list-p using SAT.
(faig-purebool-list-check x &key (config 'satlink::*default-config*)) → (mv fail purebool-list alist)
Function:
(defun faig-purebool-list-check-fn (x config) (declare (xargs :guard (satlink::config-p config))) (let ((__function__ 'faig-purebool-list-check)) (declare (ignorable __function__)) (b* ((aig (faig-purebool-list-aig x)) ((mv status alist) (aig-sat (aig-not aig) :config config)) ((when (eq status :sat)) (mv nil nil alist)) ((when (eq status :unsat)) (mv nil t nil))) (mv t nil nil))))
Theorem:
(defthm booleanp-of-faig-purebool-list-check.fail (b* (((mv ?fail ?purebool-list ?alist) (faig-purebool-list-check-fn x config))) (booleanp fail)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-of-faig-purebool-list-check.purebool-list (b* (((mv ?fail ?purebool-list ?alist) (faig-purebool-list-check-fn x config))) (booleanp purebool-list)) :rule-classes :type-prescription)
Theorem:
(defthm faig-purebool-list-check-correct (b* (((mv fail purebool-list ?alist) (faig-purebool-list-check x :config config))) (implies (not fail) (equal purebool-list (faig-purebool-list-p x)))))