• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
          • Svtv-data
          • Defsvtv$
          • Svtv-run
          • Defsvtv-phasewise
          • Svtv
          • Svtv-spec
          • Defsvtv
          • Process.lisp
            • Svtv-compile
            • Defsvtv-events
            • Svtv-compile-lazy
            • Svtv-compile-phase
            • Svtv-compile-phases-lazy
            • Svtv-allphases-inputs
            • Svtv-phase-inputs
            • Svtv-inalist-resolve-unassigned
            • Svtv-simplify-outs/states
              • Svtv-collect-inmap
              • Svar-boolmasks-limit-to-bound-vars
              • Svtv-overrides->assigns
              • Svtv-non-override-test-input-vars
              • Svtv-outputs->outalist
              • Svtv-run-squash-dontcares
              • Svtv-inputs->assigns
              • Svtv-phase-var-assigns
              • Defsvtv-fn
              • Svtv-entries->overrideconds
              • Svtv-entries->vars
              • Svtv-easy-bindings-main
              • Svtv-collect-masks
              • Svtv-baseentry-svex
              • Svtv-init-states
              • Lhs->mask
              • Svtv-easy-bindings-svtv-vars
              • Svtv-autoins-aux
              • Svtv-autohyps-aux
              • Svtv-autobinds-aux
              • Svtv-autoins
              • Svtv-autohyps
              • Svtv-autobinds
              • Fast-alist-free-list
              • Defsvtv-default-names
            • Svtv-doc
            • Svtv-chase$
            • Svtv-versus-stv
            • Svtv-debug-fsm
            • Structure.lisp
            • Svtv-debug
            • Def-pipeline-thm
            • Expand.lisp
            • Def-cycle-thm
            • Svtv-utilities
            • Svtv-debug$
            • Defsvtv$-phasewise
          • Svex-decomposition-methodology
          • Sv-versus-esim
          • Svex-decomp
          • Svex-compose-dfs
          • Svex-compilation
          • Moddb
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Process.lisp

    Svtv-simplify-outs/states

    Signature
    (svtv-simplify-outs/states outs nextstates simplify) 
      → 
    (mv simp-outs simp-states)
    Arguments
    outs — Guard (svex-alist-p outs).
    nextstates — Guard (svex-alist-p nextstates).
    Returns
    simp-outs — Type (svex-alist-p simp-outs).
    simp-states — Type (svex-alist-p simp-states).

    Definitions and Theorems

    Function: svtv-simplify-outs/states

    (defun svtv-simplify-outs/states (outs nextstates simplify)
      (declare (xargs :guard (and (svex-alist-p outs)
                                  (svex-alist-p nextstates))))
      (let ((__function__ 'svtv-simplify-outs/states))
        (declare (ignorable __function__))
        (b* ((outs (svex-alist-fix outs))
             (nextstates (svex-alist-fix nextstates))
             ((unless simplify) (mv outs nextstates))
             (alist (append outs nextstates))
             (simp-alist (svex-alist-normalize-concats
                              (svex-alist-rewrite-fixpoint alist
                                                           :verbosep t)
                              :verbosep t))
             (outs-len (len outs))
             (simp-outs (take outs-len simp-alist))
             (simp-states (nthcdr outs-len simp-alist)))
          (mv simp-outs simp-states))))

    Theorem: svex-alist-p-of-svtv-simplify-outs/states.simp-outs

    (defthm svex-alist-p-of-svtv-simplify-outs/states.simp-outs
      (b* (((mv ?simp-outs ?simp-states)
            (svtv-simplify-outs/states outs nextstates simplify)))
        (svex-alist-p simp-outs))
      :rule-classes :rewrite)

    Theorem: svex-alist-p-of-svtv-simplify-outs/states.simp-states

    (defthm svex-alist-p-of-svtv-simplify-outs/states.simp-states
      (b* (((mv ?simp-outs ?simp-states)
            (svtv-simplify-outs/states outs nextstates simplify)))
        (svex-alist-p simp-states))
      :rule-classes :rewrite)

    Theorem: svtv-simplify-outs/states-of-svex-alist-fix-outs

    (defthm svtv-simplify-outs/states-of-svex-alist-fix-outs
      (equal (svtv-simplify-outs/states (svex-alist-fix outs)
                                        nextstates simplify)
             (svtv-simplify-outs/states outs nextstates simplify)))

    Theorem: svtv-simplify-outs/states-svex-alist-equiv-congruence-on-outs

    (defthm
          svtv-simplify-outs/states-svex-alist-equiv-congruence-on-outs
     (implies
       (svex-alist-equiv outs outs-equiv)
       (equal
            (svtv-simplify-outs/states outs nextstates simplify)
            (svtv-simplify-outs/states outs-equiv nextstates simplify)))
     :rule-classes :congruence)

    Theorem: svtv-simplify-outs/states-of-svex-alist-fix-nextstates

    (defthm svtv-simplify-outs/states-of-svex-alist-fix-nextstates
      (equal (svtv-simplify-outs/states outs (svex-alist-fix nextstates)
                                        simplify)
             (svtv-simplify-outs/states outs nextstates simplify)))

    Theorem: svtv-simplify-outs/states-svex-alist-equiv-congruence-on-nextstates

    (defthm
     svtv-simplify-outs/states-svex-alist-equiv-congruence-on-nextstates
     (implies
       (svex-alist-equiv nextstates nextstates-equiv)
       (equal
            (svtv-simplify-outs/states outs nextstates simplify)
            (svtv-simplify-outs/states outs nextstates-equiv simplify)))
     :rule-classes :congruence)