• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
        • Schemalg
        • Restrict
        • Expdata
        • Casesplit
        • Simplify-term
        • Simplify-defun-sk
        • Parteval
        • Solve
        • Wrap-output
        • Propagate-iso
        • Simplify
        • Finite-difference
        • Drop-irrelevant-params
        • Copy-function
        • Lift-iso
        • Rename-params
        • Utilities
          • Defaults-table
          • Xdoc::apt-constructors
          • Input-processors
            • Process-input-old-soft-io-sel-mod
            • Process-input-new/wrapper-names
            • Process-input-select-old-soft-io
            • Process-input-old-to-new-name
            • Process-input-old-if-new-name
            • Process-input-old-to-wrapper-name
            • Process-input-wrapper-enable
            • Process-input-wrapper-to-old-name
            • Process-input-old-to-new-enable
            • Process-input-old-to-wrapper-enable
            • Process-input-old-if-new-enable
            • Process-input-new-name
            • Process-input-new-to-old-name
            • Process-input-wrapper-to-old-enable
            • Process-input-verify-guards
            • Process-input-new-enable
            • Process-input-new-to-old-enable
          • Transformation-table
          • Find-base-cases
          • Untranslate-specifier-utilities
          • Print-specifier-utilities
          • Hints-specifier-utilities
        • Simplify-term-programmatic
        • Simplify-defun-sk-programmatic
        • Simplify-defun-programmatic
        • Simplify-defun+
        • Common-options
        • Common-concepts
      • Acre
      • Milawa
      • Smtlink
      • Aleobft
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • C
      • Java
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Riscv
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Bigmems
      • Builtins
      • Axe
      • Execloader
      • Solidity
      • Leo
      • Paco
      • Concurrent-programs
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Utilities

Input-processors

Utilities to process inputs that are common to multiple APT transformations.

Subtopics

Process-input-old-soft-io-sel-mod
Process the old input of an APT transformation, when that input must denote a SOFT shallow pop-refinement specification of a certain form.
Process-input-new/wrapper-names
Process the :new-name and :wrapper-name inputs.
Process-input-select-old-soft-io
Process the input of an APT transformation that selects an input of the function variable call in a SOFT shallow pop-refinement specification of a certain form.
Process-input-old-to-new-name
Process the :old-to-new-name input of an APT transformation.
Process-input-old-if-new-name
Process the :old-if-new-name input of an APT transformation.
Process-input-old-to-wrapper-name
Process the :old-to-wrapper-name input of an APT transformation.
Process-input-wrapper-enable
Process the :wrapper-enable input of an APT transformation.
Process-input-wrapper-to-old-name
Process the :wrapper-to-old-name input of an APT transformation.
Process-input-old-to-new-enable
Process the :old-to-new-enable input of an APT transformation.
Process-input-old-to-wrapper-enable
Process the :old-to-wrapper-enable input of an APT transformation.
Process-input-old-if-new-enable
Process the :old-if-new-enable input of an APT transformation.
Process-input-new-name
Process the :new-name input of an APT transformation.
Process-input-new-to-old-name
Process the :new-to-old-name input of an APT transformation.
Process-input-wrapper-to-old-enable
Process the :wrapper-to-old-enable input of an APT transformation.
Process-input-verify-guards
Process the :verify-guards input of an APT transformation.
Process-input-new-enable
Process the :new-enable input of an APT transformation.
Process-input-new-to-old-enable
Process the :new-to-old-enable input of an APT transformation.