		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Constraintlist-add-pathcond

Signature
(constraintlist-add-pathcond cond negatedp constraints) → new-constraints
Arguments: cond — Guard (svex-p cond).; constraints — Guard (constraintlist-p constraints).
Returns: new-constraints — Type (constraintlist-p new-constraints).

Definitions and Theorems

Function: constraintlist-add-pathcond

(defun constraintlist-add-pathcond (cond negatedp constraints)
 (declare (xargs :guard (and (svex-p cond)
                             (constraintlist-p constraints))))
 (let ((__function__ 'constraintlist-add-pathcond))
   (declare (ignorable __function__))
   (if (atom constraints)
       nil
     (cons (change-constraint
                (car constraints)
                :cond (svcall bitor
                              (if negatedp cond
                                (svcall bitnot (svcall uor cond)))
                              (constraint->cond (car constraints))))
           (constraintlist-add-pathcond
                cond negatedp (cdr constraints))))))

Theorem: constraintlist-p-of-constraintlist-add-pathcond

(defthm constraintlist-p-of-constraintlist-add-pathcond
 (b* ((new-constraints
           (constraintlist-add-pathcond cond negatedp constraints)))
   (constraintlist-p new-constraints))
 :rule-classes :rewrite)

Theorem: vars-of-constraintlist-add-pathcond

(defthm vars-of-constraintlist-add-pathcond
 (b* ((?new-constraints
           (constraintlist-add-pathcond cond negatedp constraints)))
   (implies (and (not (member v (constraintlist-vars constraints)))
                 (not (member v (svex-vars cond))))
            (not (member v
                         (constraintlist-vars new-constraints))))))

Theorem: constraintlist-add-pathcond-of-svex-fix-cond

(defthm constraintlist-add-pathcond-of-svex-fix-cond
  (equal (constraintlist-add-pathcond (svex-fix cond)
                                      negatedp constraints)
         (constraintlist-add-pathcond cond negatedp constraints)))

Theorem: constraintlist-add-pathcond-svex-equiv-congruence-on-cond

(defthm constraintlist-add-pathcond-svex-equiv-congruence-on-cond
 (implies
  (svex-equiv cond cond-equiv)
  (equal
     (constraintlist-add-pathcond cond negatedp constraints)
     (constraintlist-add-pathcond cond-equiv negatedp constraints)))
 :rule-classes :congruence)

Theorem: constraintlist-add-pathcond-of-constraintlist-fix-constraints

(defthm
      constraintlist-add-pathcond-of-constraintlist-fix-constraints
 (equal
      (constraintlist-add-pathcond cond negatedp
                                   (constraintlist-fix constraints))
      (constraintlist-add-pathcond cond negatedp constraints)))

Theorem: constraintlist-add-pathcond-constraintlist-equiv-congruence-on-constraints

(defthm
 constraintlist-add-pathcond-constraintlist-equiv-congruence-on-constraints
 (implies
  (constraintlist-equiv constraints constraints-equiv)
  (equal
     (constraintlist-add-pathcond cond negatedp constraints)
     (constraintlist-add-pathcond cond negatedp constraints-equiv)))
 :rule-classes :congruence)