• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
        • Svstmt-case
        • Svstmt-while
        • Svstmt-p
        • Svstmt-if
        • Svstmt-equiv
        • Svstmt-xcond
        • Svstmt-scope
        • Svstmt-assign
        • Svstmt-compile
          • Svstmt-compile.lisp
            • Svstate-merge-branches
            • Svex-alist-merge-branches
            • Svstmt-assign->subst
            • Svstack-merge-branches
            • Svstacks-compatible
            • Svjumpstate-merge-svstate-branches
            • Svjumpstate-svstate-compatible
            • Svstmt-lhs-check-masks
            • Svjumpstate
            • Svjumpstates-compatible
            • Svstmtlist-compile-top
            • Svjumpstate-sequence-svstates
            • Constraintlist-merge-branches
            • Svjumpstate-merge-branches
            • Svex-replace-range
            • Svex-svstmt-ite
            • Svstmt-process-write
            • Svjumpstate-sequence
            • Svstmt-process-writelist
            • Svstack-assign
            • Svstmt-writelist-var-sizes
            • Svstates-compatible
            • 4vec-replace-range
            • Svstmt-write-var-sizes
            • Make-empty-svjumpstate
            • Constraintlist-add-pathcond
            • Svjumpstate-pop-scope
            • Constraintlist-compose-svstack
            • Svstack-to-svex-alist
            • Svstack-filter-global-lhs-vars
            • Svjumpstate-vars
            • Svex-svstmt-or
            • Svex-svstmt-andc1
            • Svstate-push-scope
            • Svstate-pop-scope
            • Svstate-vars
            • Svstack-lookup
            • Svar-subtract-delay
            • Svstmt-initialize-locals
            • Svstack-fork
            • Svstack-clean
            • Svstack-nonempty-fix
            • Svstate-fork
            • Svstate-clean
            • Svstack-globalp
            • Svjumpstate-fork
            • Svar-delayed-member
            • Svjumpstate-levels
            • Svjumpstate-free
            • Svstate-free
            • Svstack-free
            • Svstack
            • Svar-size-alist
          • Svstate
        • Svstmt-constraints
        • Svstmt-jump
        • Svstmtlist
        • Svstmt-kind
        • Svstmt.lisp
        • Svstmt-fix
        • Svstmt-count
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svstmt-compile.lisp

Svex-svstmt-andc1

Signature

(svex-svstmt-andc1 a b) → or

Arguments

a — Guard (svex-p a).

b — Guard (svex-p b).

Returns

or — Type (svex-p or).

Definitions and Theorems

Function: svex-svstmt-andc1

(defun svex-svstmt-andc1 (a b)
  (declare (xargs :guard (and (svex-p a) (svex-p b))))
  (let ((__function__ 'svex-svstmt-andc1))
    (declare (ignorable __function__))
    (b* ((a (svex-fix a))
         (b (svex-fix b))
         ((when (svex-case a
                           :quote (2vec-p a.val)
                           :otherwise nil))
          (b* ((a (2vec->val (svex-quote->val a))))
            (if (eql a 0) b 0)))
         ((when (svex-case b
                           :quote (2vec-p b.val)
                           :otherwise nil))
          (b* ((b (2vec->val (svex-quote->val b))))
            (if (eql b 0)
                0
              (svex-call 'bitnot
                         (list (svex-call 'uor (list a))))))))
      (svex-call 'bitand
                 (list (svex-call 'bitnot
                                  (list (svex-call 'uor (list a))))
                       (svex-call 'uor (list b)))))))

Theorem: svex-p-of-svex-svstmt-andc1

(defthm svex-p-of-svex-svstmt-andc1
  (b* ((or (svex-svstmt-andc1 a b)))
    (svex-p or))
  :rule-classes :rewrite)

Theorem: vars-of-svex-svstmt-andc1

(defthm vars-of-svex-svstmt-andc1
  (b* ((common-lisp::?or (svex-svstmt-andc1 a b)))
    (implies (and (not (member v (svex-vars a)))
                  (not (member v (svex-vars b))))
             (not (member v (svex-vars or))))))

Theorem: svex-svstmt-andc1-of-svex-fix-a

(defthm svex-svstmt-andc1-of-svex-fix-a
  (equal (svex-svstmt-andc1 (svex-fix a) b)
         (svex-svstmt-andc1 a b)))

Theorem: svex-svstmt-andc1-svex-equiv-congruence-on-a

(defthm svex-svstmt-andc1-svex-equiv-congruence-on-a
  (implies (svex-equiv a a-equiv)
           (equal (svex-svstmt-andc1 a b)
                  (svex-svstmt-andc1 a-equiv b)))
  :rule-classes :congruence)

Theorem: svex-svstmt-andc1-of-svex-fix-b

(defthm svex-svstmt-andc1-of-svex-fix-b
  (equal (svex-svstmt-andc1 a (svex-fix b))
         (svex-svstmt-andc1 a b)))

Theorem: svex-svstmt-andc1-svex-equiv-congruence-on-b

(defthm svex-svstmt-andc1-svex-equiv-congruence-on-b
  (implies (svex-equiv b b-equiv)
           (equal (svex-svstmt-andc1 a b)
                  (svex-svstmt-andc1 a b-equiv)))
  :rule-classes :congruence)