• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
        • Litp
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Cnf

Env$

A bit array that serves as the environment for eval-formula.

Definitions and Theorems

Definition: env$p

(defabsstobj env$
             :foundation acl2::bitarr$c
             :recognizer (env$p :logic acl2::bitarr$ap
                                :exec acl2::bitarr$cp)
             :creator (create-env$ :logic acl2::create-bitarr$a
                                   :exec acl2::create-bitarr$c)
             :exports ((env$-length :logic acl2::bits$a-length
                                    :exec acl2::bits$c-length
                                    :protect nil)
                       (env$-get :logic acl2::bits$ai
                                 :exec acl2::bits$ci
                                 :protect nil)
                       (env$-set :logic acl2::update-bits$ai
                                 :exec acl2::update-bits$ci
                                 :protect nil)
                       (env$-resize :logic acl2::resize-bits$a
                                    :exec acl2::resize-bits$c
                                    :protect nil))
             :congruent-to bitarr)

Definition: create-env$

(defabsstobj env$
             :foundation acl2::bitarr$c
             :recognizer (env$p :logic acl2::bitarr$ap
                                :exec acl2::bitarr$cp)
             :creator (create-env$ :logic acl2::create-bitarr$a
                                   :exec acl2::create-bitarr$c)
             :exports ((env$-length :logic acl2::bits$a-length
                                    :exec acl2::bits$c-length
                                    :protect nil)
                       (env$-get :logic acl2::bits$ai
                                 :exec acl2::bits$ci
                                 :protect nil)
                       (env$-set :logic acl2::update-bits$ai
                                 :exec acl2::update-bits$ci
                                 :protect nil)
                       (env$-resize :logic acl2::resize-bits$a
                                    :exec acl2::resize-bits$c
                                    :protect nil))
             :congruent-to bitarr)

Definition: env$-length

(defabsstobj env$
             :foundation acl2::bitarr$c
             :recognizer (env$p :logic acl2::bitarr$ap
                                :exec acl2::bitarr$cp)
             :creator (create-env$ :logic acl2::create-bitarr$a
                                   :exec acl2::create-bitarr$c)
             :exports ((env$-length :logic acl2::bits$a-length
                                    :exec acl2::bits$c-length
                                    :protect nil)
                       (env$-get :logic acl2::bits$ai
                                 :exec acl2::bits$ci
                                 :protect nil)
                       (env$-set :logic acl2::update-bits$ai
                                 :exec acl2::update-bits$ci
                                 :protect nil)
                       (env$-resize :logic acl2::resize-bits$a
                                    :exec acl2::resize-bits$c
                                    :protect nil))
             :congruent-to bitarr)

Definition: env$-get

(defabsstobj env$
             :foundation acl2::bitarr$c
             :recognizer (env$p :logic acl2::bitarr$ap
                                :exec acl2::bitarr$cp)
             :creator (create-env$ :logic acl2::create-bitarr$a
                                   :exec acl2::create-bitarr$c)
             :exports ((env$-length :logic acl2::bits$a-length
                                    :exec acl2::bits$c-length
                                    :protect nil)
                       (env$-get :logic acl2::bits$ai
                                 :exec acl2::bits$ci
                                 :protect nil)
                       (env$-set :logic acl2::update-bits$ai
                                 :exec acl2::update-bits$ci
                                 :protect nil)
                       (env$-resize :logic acl2::resize-bits$a
                                    :exec acl2::resize-bits$c
                                    :protect nil))
             :congruent-to bitarr)

Definition: env$-set

(defabsstobj env$
             :foundation acl2::bitarr$c
             :recognizer (env$p :logic acl2::bitarr$ap
                                :exec acl2::bitarr$cp)
             :creator (create-env$ :logic acl2::create-bitarr$a
                                   :exec acl2::create-bitarr$c)
             :exports ((env$-length :logic acl2::bits$a-length
                                    :exec acl2::bits$c-length
                                    :protect nil)
                       (env$-get :logic acl2::bits$ai
                                 :exec acl2::bits$ci
                                 :protect nil)
                       (env$-set :logic acl2::update-bits$ai
                                 :exec acl2::update-bits$ci
                                 :protect nil)
                       (env$-resize :logic acl2::resize-bits$a
                                    :exec acl2::resize-bits$c
                                    :protect nil))
             :congruent-to bitarr)

Definition: env$-resize

(defabsstobj env$
             :foundation acl2::bitarr$c
             :recognizer (env$p :logic acl2::bitarr$ap
                                :exec acl2::bitarr$cp)
             :creator (create-env$ :logic acl2::create-bitarr$a
                                   :exec acl2::create-bitarr$c)
             :exports ((env$-length :logic acl2::bits$a-length
                                    :exec acl2::bits$c-length
                                    :protect nil)
                       (env$-get :logic acl2::bits$ai
                                 :exec acl2::bits$ci
                                 :protect nil)
                       (env$-set :logic acl2::update-bits$ai
                                 :exec acl2::update-bits$ci
                                 :protect nil)
                       (env$-resize :logic acl2::resize-bits$a
                                    :exec acl2::resize-bits$c
                                    :protect nil))
             :congruent-to bitarr)