• Top
  • Documentation
  • Books
  • 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
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)