• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-counterexamples
        • Def-ctrex-rule
        • Fgl-counterexample-implementation-details
          • Cgraph
          • Cgraph-derive-assignments-for-vars
          • Cgraph-derive-assignments-obj
          • Cgraph-derive-assignments-bindings
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Def-fgl-param-thm
      • Fgl-rewrite-tracing
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fgl-counterexample-implementation-details

Cgraph-derive-assignments-for-vars

Signature

(cgraph-derive-assignments-for-vars 
     x vals assigns sts env$ cgraph 
     replimit &optional (logicman 'logicman) 
     (bvar-db 'bvar-db) 
     (state 'state)) 
 
  → 
(mv new-vals new-assigns new-sts)

Arguments

x — list of variables to derive values for.
    Guard (pseudo-var-list-p x).

vals — accumulator of variable values.
    Guard (obj-alist-p vals).

assigns — accumulator of object values.
    Guard (cgraph-alist-p assigns).

sts — accumulator of object derivstates.
    Guard (cgraph-derivstates-p sts).

env$ — Boolean assignment environment.

cgraph — Guard (cgraph-p cgraph).

replimit — Guard (posp replimit).

Returns

new-vals — Type (obj-alist-p new-vals).

new-assigns — Type (cgraph-alist-p new-assigns).

new-sts — Type (cgraph-derivstates-p new-sts).

Definitions and Theorems

Function: cgraph-derive-assignments-for-vars-fn

(defun cgraph-derive-assignments-for-vars-fn
       (x vals assigns sts env$
          cgraph replimit logicman bvar-db state)
 (declare (xargs :stobjs (env$ logicman bvar-db state)))
 (declare (xargs :guard (and (pseudo-var-list-p x)
                             (obj-alist-p vals)
                             (cgraph-alist-p assigns)
                             (cgraph-derivstates-p sts)
                             (cgraph-p cgraph)
                             (posp replimit))))
 (declare (xargs :guard (and (bfr-env$-p env$ (logicman->bfrstate))
                             (equal (bfr-nvars) (next-bvar bvar-db))
                             (lbfr-listp (cgraph-bfrlist cgraph)))))
 (let ((__function__ 'cgraph-derive-assignments-for-vars))
   (declare (ignorable __function__))
   (b* (((when (atom x))
         (mv (obj-alist-fix vals)
             (cgraph-alist-fix assigns)
             (cgraph-derivstates-fix sts)))
        (obj (g-var (car x)))
        ((mv assigns sts)
         (cgraph-derive-assignments-obj
              obj assigns sts env$ cgraph replimit))
        (pair (hons-get obj assigns))
        (vals (if pair (cons (cons (pseudo-var-fix (car x))
                                   (cgraph-value->val (cdr pair)))
                             vals)
                vals)))
     (cgraph-derive-assignments-for-vars
          (cdr x)
          vals
          assigns sts env$ cgraph replimit))))

Theorem: obj-alist-p-of-cgraph-derive-assignments-for-vars.new-vals

(defthm obj-alist-p-of-cgraph-derive-assignments-for-vars.new-vals
  (b* (((mv ?new-vals ?new-assigns ?new-sts)
        (cgraph-derive-assignments-for-vars-fn
             x vals assigns sts env$ cgraph
             replimit logicman bvar-db state)))
    (obj-alist-p new-vals))
  :rule-classes :rewrite)

Theorem: cgraph-alist-p-of-cgraph-derive-assignments-for-vars.new-assigns

(defthm
   cgraph-alist-p-of-cgraph-derive-assignments-for-vars.new-assigns
  (b* (((mv ?new-vals ?new-assigns ?new-sts)
        (cgraph-derive-assignments-for-vars-fn
             x vals assigns sts env$ cgraph
             replimit logicman bvar-db state)))
    (cgraph-alist-p new-assigns))
  :rule-classes :rewrite)

Theorem: cgraph-derivstates-p-of-cgraph-derive-assignments-for-vars.new-sts

(defthm
 cgraph-derivstates-p-of-cgraph-derive-assignments-for-vars.new-sts
 (b* (((mv ?new-vals ?new-assigns ?new-sts)
       (cgraph-derive-assignments-for-vars-fn
            x vals assigns sts env$ cgraph
            replimit logicman bvar-db state)))
   (cgraph-derivstates-p new-sts))
 :rule-classes :rewrite)

Theorem: cgraph-derive-assignments-for-vars-fn-of-pseudo-var-list-fix-x

(defthm
     cgraph-derive-assignments-for-vars-fn-of-pseudo-var-list-fix-x
  (equal (cgraph-derive-assignments-for-vars-fn
              (pseudo-var-list-fix x)
              vals assigns sts env$
              cgraph replimit logicman bvar-db state)
         (cgraph-derive-assignments-for-vars-fn
              x vals assigns sts env$ cgraph
              replimit logicman bvar-db state)))

Theorem: cgraph-derive-assignments-for-vars-fn-pseudo-var-list-equiv-congruence-on-x

(defthm
 cgraph-derive-assignments-for-vars-fn-pseudo-var-list-equiv-congruence-on-x
 (implies (pseudo-var-list-equiv x x-equiv)
          (equal (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$
                      cgraph replimit logicman bvar-db state)
                 (cgraph-derive-assignments-for-vars-fn
                      x-equiv vals assigns sts env$ cgraph
                      replimit logicman bvar-db state)))
 :rule-classes :congruence)

Theorem: cgraph-derive-assignments-for-vars-fn-of-obj-alist-fix-vals

(defthm cgraph-derive-assignments-for-vars-fn-of-obj-alist-fix-vals
  (equal (cgraph-derive-assignments-for-vars-fn
              x (obj-alist-fix vals)
              assigns sts env$
              cgraph replimit logicman bvar-db state)
         (cgraph-derive-assignments-for-vars-fn
              x vals assigns sts env$ cgraph
              replimit logicman bvar-db state)))

Theorem: cgraph-derive-assignments-for-vars-fn-obj-alist-equiv-congruence-on-vals

(defthm
 cgraph-derive-assignments-for-vars-fn-obj-alist-equiv-congruence-on-vals
 (implies (obj-alist-equiv vals vals-equiv)
          (equal (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$
                      cgraph replimit logicman bvar-db state)
                 (cgraph-derive-assignments-for-vars-fn
                      x vals-equiv assigns sts env$ cgraph
                      replimit logicman bvar-db state)))
 :rule-classes :congruence)

Theorem: cgraph-derive-assignments-for-vars-fn-of-cgraph-alist-fix-assigns

(defthm
  cgraph-derive-assignments-for-vars-fn-of-cgraph-alist-fix-assigns
  (equal (cgraph-derive-assignments-for-vars-fn
              x vals (cgraph-alist-fix assigns)
              sts env$
              cgraph replimit logicman bvar-db state)
         (cgraph-derive-assignments-for-vars-fn
              x vals assigns sts env$ cgraph
              replimit logicman bvar-db state)))

Theorem: cgraph-derive-assignments-for-vars-fn-cgraph-alist-equiv-congruence-on-assigns

(defthm
 cgraph-derive-assignments-for-vars-fn-cgraph-alist-equiv-congruence-on-assigns
 (implies (cgraph-alist-equiv assigns assigns-equiv)
          (equal (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$
                      cgraph replimit logicman bvar-db state)
                 (cgraph-derive-assignments-for-vars-fn
                      x vals assigns-equiv sts env$ cgraph
                      replimit logicman bvar-db state)))
 :rule-classes :congruence)

Theorem: cgraph-derive-assignments-for-vars-fn-of-cgraph-derivstates-fix-sts

(defthm
 cgraph-derive-assignments-for-vars-fn-of-cgraph-derivstates-fix-sts
 (equal (cgraph-derive-assignments-for-vars-fn
             x vals
             assigns (cgraph-derivstates-fix sts)
             env$
             cgraph replimit logicman bvar-db state)
        (cgraph-derive-assignments-for-vars-fn
             x vals assigns sts env$ cgraph
             replimit logicman bvar-db state)))

Theorem: cgraph-derive-assignments-for-vars-fn-cgraph-derivstates-equiv-congruence-on-sts

(defthm
 cgraph-derive-assignments-for-vars-fn-cgraph-derivstates-equiv-congruence-on-sts
 (implies (cgraph-derivstates-equiv sts sts-equiv)
          (equal (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$
                      cgraph replimit logicman bvar-db state)
                 (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts-equiv env$ cgraph
                      replimit logicman bvar-db state)))
 :rule-classes :congruence)

Theorem: cgraph-derive-assignments-for-vars-fn-of-cgraph-fix-cgraph

(defthm cgraph-derive-assignments-for-vars-fn-of-cgraph-fix-cgraph
  (equal (cgraph-derive-assignments-for-vars-fn
              x vals
              assigns sts env$ (cgraph-fix cgraph)
              replimit logicman bvar-db state)
         (cgraph-derive-assignments-for-vars-fn
              x vals assigns sts env$ cgraph
              replimit logicman bvar-db state)))

Theorem: cgraph-derive-assignments-for-vars-fn-cgraph-equiv-congruence-on-cgraph

(defthm
 cgraph-derive-assignments-for-vars-fn-cgraph-equiv-congruence-on-cgraph
 (implies (cgraph-equiv cgraph cgraph-equiv)
          (equal (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$
                      cgraph replimit logicman bvar-db state)
                 (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$ cgraph-equiv
                      replimit logicman bvar-db state)))
 :rule-classes :congruence)

Theorem: cgraph-derive-assignments-for-vars-fn-of-pos-fix-replimit

(defthm cgraph-derive-assignments-for-vars-fn-of-pos-fix-replimit
  (equal (cgraph-derive-assignments-for-vars-fn
              x vals assigns
              sts env$ cgraph (pos-fix replimit)
              logicman bvar-db state)
         (cgraph-derive-assignments-for-vars-fn
              x vals assigns sts env$ cgraph
              replimit logicman bvar-db state)))

Theorem: cgraph-derive-assignments-for-vars-fn-pos-equiv-congruence-on-replimit

(defthm
 cgraph-derive-assignments-for-vars-fn-pos-equiv-congruence-on-replimit
 (implies (acl2::pos-equiv replimit replimit-equiv)
          (equal (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$
                      cgraph replimit logicman bvar-db state)
                 (cgraph-derive-assignments-for-vars-fn
                      x vals assigns sts env$ cgraph
                      replimit-equiv logicman bvar-db state)))
 :rule-classes :congruence)