		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Svexlist-eval-integer-listp-with-transforms

Signature
(svexlist-eval-integer-listp-with-transforms x env symbolic-params transforms &key tracked-alist) → *
Arguments: x — Guard (svexlist-p x).; env — Guard (svex-env-p env).; symbolic-params — Guard (alistp symbolic-params).

Definitions and Theorems

Function: svexlist-eval-integer-listp-with-transforms-fn

(defun svexlist-eval-integer-listp-with-transforms-fn
       (x env symbolic-params
          transforms tracked-alist)
  (declare (xargs :guard (and (svexlist-p x)
                              (svex-env-p env)
                              (alistp symbolic-params))))
  (declare (ignorable symbolic-params
                      transforms tracked-alist))
  (let ((__function__ 'svexlist-eval-integer-listp-with-transforms))
    (declare (ignorable __function__))
    (integer-listp (svexlist-eval x env))))

Theorem: unequiv-implies-equal-svexlist-eval-integer-listp-with-transforms-fn-3

(defthm
 unequiv-implies-equal-svexlist-eval-integer-listp-with-transforms-fn-3
 (implies (fgl::unequiv symbolic-params symbolic-params-equiv)
          (equal (svexlist-eval-integer-listp-with-transforms-fn
                      x env symbolic-params
                      transforms tracked-alist)
                 (svexlist-eval-integer-listp-with-transforms-fn
                      x env symbolic-params-equiv
                      transforms tracked-alist)))
 :rule-classes (:congruence))

Theorem: unequiv-implies-equal-svexlist-eval-integer-listp-with-transforms-fn-4

(defthm
 unequiv-implies-equal-svexlist-eval-integer-listp-with-transforms-fn-4
 (implies (fgl::unequiv transforms transforms-equiv)
          (equal (svexlist-eval-integer-listp-with-transforms-fn
                      x env symbolic-params
                      transforms tracked-alist)
                 (svexlist-eval-integer-listp-with-transforms-fn
                      x env symbolic-params
                      transforms-equiv tracked-alist)))
 :rule-classes (:congruence))

Theorem: unequiv-implies-equal-svexlist-eval-integer-listp-with-transforms-fn-5

(defthm
 unequiv-implies-equal-svexlist-eval-integer-listp-with-transforms-fn-5
 (implies (fgl::unequiv tracked-alist tracked-alist-equiv)
          (equal (svexlist-eval-integer-listp-with-transforms-fn
                      x env symbolic-params
                      transforms tracked-alist)
                 (svexlist-eval-integer-listp-with-transforms-fn
                      x env symbolic-params
                      transforms tracked-alist-equiv)))
 :rule-classes (:congruence))

Theorem: svexlist-eval-integer-listp-with-transforms-fgl

(defthm svexlist-eval-integer-listp-with-transforms-fgl
 (equal
  (svexlist-eval-integer-listp-with-transforms
       x env symbolic-params transforms
       :tracked-alist tracked-alist)
  (b*
   ((orig-x x)
    (env (make-fast-alist (svex-env-fix env)))
    (svars (svexlist-vars-for-symbolic-eval x env symbolic-params))
    (x (svexlist-x-out-unused-vars
            x svars
            (symbolic-params-x-out-cond symbolic-params)))
    (x (maybe-svexlist-rewrite-fixpoint
            x
            (cdr (assoc :simplify symbolic-params))))
    (boolmasks
     (make-fast-alist
      (hons-copy
         (ec-call (svar-boolmasks-fix
                       (cdr (assoc :boolmasks symbolic-params)))))))
    ((unless (svex-env-check-boolmasks boolmasks env))
     (b*
      ((?ign
           (cw "ERROR: some bits assumed to be Boolean were not~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (integer-listp (svexlist-eval orig-x env)))))
    ((mv err x-a4vecs hint-a4vecs)
     (time$
      (svexlist->a4vecs-for-varlist-with-subexprs x svars boolmasks)
      :msg "; svex->aigs: ~st sec, ~sa bytes.~%"))
    ((when err)
     (b* ((?ign (cw "ERROR gathering AIG bits for variables: ~@0~%"
                    err)))
       (fgl::abort-rewrite
            (integer-listp (svexlist-eval orig-x env)))))
    ((mv ?err aig-env)
     (time$
         (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env)
         :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env (make-fast-alist aig-env))
    (?ign (fast-alist-free env))
    (x-eval
         (time$ (a4veclist-eval x-a4vecs aig-env)
                :msg "; a4veclist-eval x: ~st sec, ~sa bytes.~%"))
    (hint-eval
         (time$ (a4veclist-eval hint-a4vecs aig-env)
                :msg "; a4veclist-eval sub: ~st sec, ~sa bytes.~%"))
    (evals-integer-listp (integer-listp x-eval))
    ((mv hint-upper hint-lower)
     (4veclist-separate-upper-lower hint-eval))
    ((mv iso-ok hint-upper hint-lower)
     (fgl::fgl-make-isomorphic iso-ok hint-upper hint-lower))
    ((unless iso-ok)
     (b*
      ((?ign
        (cw
         "ERROR: the equivalence hint objects couldn't be made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (integer-listp (svexlist-eval orig-x env)))))
    (len1
     (fgl::syntax-bind
      len1
      (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-upper)))))
    (len2
     (fgl::syntax-bind
      len2
      (fgl::g-concrete (len (fgl::fgl-object-bfrlist hint-lower)))))
    ((unless (fgl::syntax-bind lens-equal (equal len1 len2)))
     (b*
      ((?ign
        (cw
         "ERROR: the number of BFR objects in the ~
                                 equivalence hint objects wasn't equal after ~
                                 they were made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (integer-listp (svexlist-eval orig-x env))))))
   (fgl::fgl-simplify-ordered
    evals-integer-listp transforms
    :tracked-obj
    (cons
     (cons
       :evals-equivalent-equiv-classes (cons hint-upper hint-lower))
     tracked-alist)))))

Theorem: svexlist-eval-integer-listp-with-transforms-fgl-extreme-2

(defthm svexlist-eval-integer-listp-with-transforms-fgl-extreme-2
 (equal
  (svexlist-eval-integer-listp-with-transforms
       x env symbolic-params transforms
       :tracked-alist tracked-alist)
  (b*
   ((orig-x x)
    (env (make-fast-alist (svex-env-fix env)))
    (svars (svexlist-vars-for-symbolic-eval x env symbolic-params))
    (x (svexlist-x-out-unused-vars
            x svars
            (symbolic-params-x-out-cond symbolic-params)))
    (x (maybe-svexlist-rewrite-fixpoint
            x
            (cdr (assoc :simplify symbolic-params))))
    (boolmasks
     (make-fast-alist
      (hons-copy
         (ec-call (svar-boolmasks-fix
                       (cdr (assoc :boolmasks symbolic-params)))))))
    ((unless (and (svex-env-check-boolmasks boolmasks env)))
     (b*
      ((?ign
           (cw "ERROR: some bits assumed to be Boolean were not~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (integer-listp (svexlist-eval orig-x env))))))
    ((mv err x-a4vecs hint-a4vecs)
     (time$
      (svexlist->a4vecs-for-varlist-with-subexprs x svars boolmasks)
      :msg "; svex->aigs: ~st sec, ~sa bytes.~%"))
    ((when err)
     (b* ((?ign (cw "ERROR gathering AIG bits for variables: ~@0~%"
                    err)))
       (fgl::abort-rewrite
            (and (integer-listp (svexlist-eval orig-x env))))))
    ((mv ?err aig-env)
     (time$
         (svexlist->a4vec-aig-env-for-varlist x svars boolmasks env)
         :msg "; env -> aig env: ~st sec, ~sa bytes.~%"))
    (aig-env (make-fast-alist aig-env))
    (?ign (fast-alist-free env))
    ((mv upper-aigs lower-aigs)
     (a4veclist-separate-upper-lower (append hint-a4vecs)))
    ((mv x-eval & & upper-eval lower-eval)
     (eval-collection-of-a4vecs-and-aigs
          x-a4vecs
          nil nil upper-aigs lower-aigs aig-env))
    (integer-listp (integer-listp x-eval))
    ((mv iso-ok upper-eval lower-eval)
     (time$
          (fgl::fgl-make-isomorphic iso-ok upper-eval lower-eval)))
    ((unless iso-ok)
     (b*
      ((?ign
        (cw
         "ERROR: the equivalence hint objects couldn't be made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (integer-listp (svexlist-eval orig-x env))))))
    (len1
     (fgl::syntax-bind
      len1
      (fgl::g-concrete (len (fgl::fgl-object-bfrlist upper-eval)))))
    (len2
     (fgl::syntax-bind
      len2
      (fgl::g-concrete (len (fgl::fgl-object-bfrlist lower-eval)))))
    ((unless (fgl::syntax-bind lens-equal (equal len1 len2)))
     (b*
      ((?ign
        (cw
         "ERROR: the number of BFR objects in the ~
                                 equivalence hint objects wasn't equal after ~
                                 they were made isomorphic!~%"))
       (?foo (break$)))
      (fgl::abort-rewrite
           (and (integer-listp (svexlist-eval orig-x env)))))))
   (fgl::fgl-simplify-ordered
    integer-listp transforms
    :tracked-obj
    (cons
     (cons
       :evals-equivalent-equiv-classes (cons upper-eval lower-eval))
     tracked-alist)))))