Recognizer for fgl-satlink-monolithic-sat-config structures.
(fgl-satlink-monolithic-sat-config-p x) → *
Function:
(defun fgl-satlink-monolithic-sat-config-p (x) (declare (xargs :guard t)) (let ((__function__ 'fgl-satlink-monolithic-sat-config-p)) (declare (ignorable __function__)) (and (consp x) (eq (car x) :fgl-satlink-config) (mbe :logic (and (alistp (cdr x)) (equal (strip-cars (cdr x)) '(ignore-pathcond ignore-constraint satlink-config-override transform transform-config-override conjoin))) :exec (fty::alist-with-carsp (cdr x) '(ignore-pathcond ignore-constraint satlink-config-override transform transform-config-override conjoin))) (b* ((ignore-pathcond (cdr (std::da-nth 0 (cdr x)))) (ignore-constraint (cdr (std::da-nth 1 (cdr x)))) (?satlink-config-override (cdr (std::da-nth 2 (cdr x)))) (transform (cdr (std::da-nth 3 (cdr x)))) (?transform-config-override (cdr (std::da-nth 4 (cdr x)))) (acl2::?conjoin (cdr (std::da-nth 5 (cdr x))))) (and (booleanp ignore-pathcond) (booleanp ignore-constraint) (booleanp transform))))))
Theorem:
(defthm consp-when-fgl-satlink-monolithic-sat-config-p (implies (fgl-satlink-monolithic-sat-config-p x) (consp x)) :rule-classes :compound-recognizer)