• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
          • Add-io-pairs-details
          • Show-io-pairs
          • Get-io-pairs
          • Merge-io-pairs
          • Remove-io-pairs
            • Add-io-pair
            • Deinstall-io-pairs
            • Install-io-pairs
          • Defalist
          • Defmapappend
          • Returns-specifiers
          • Defarbrec
          • Define-sk
          • Defines
          • Error-value-tuples
          • Defmax-nat
          • Defmin-int
          • Deftutorial
          • Extended-formals
          • Defrule
          • Defval
          • Defsurj
          • Defiso
          • Defconstrained-recognizer
          • Deffixer
          • Defmvtypes
          • Defconsts
          • Defthm-unsigned-byte-p
          • Support
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Add-io-pairs

    Remove-io-pairs

    Remove input-output pairs

    For relevant background, see add-io-pairs, which modifies a function by looking up the result for specified input-output pairs. The utility remove-io-pairs removes all such pairs for the specified function symbols.

    General Forms:
    (remove-io-pairs fn1 ... fnk)
    (remove-io-pairs :all)

    where the arguments are not evaluated. The use of :all specifies that all I/O pairs are to be removed for all function symbols; otherwise, all I/O pairs are removed only for the specified function symbols. A warning is printed for each input fni that does not currently have any I/O pairs.

    Remark. As add-io-pairs actually memoizes functions, remove-io-pairs unmemoizes the specified functions. For a utility that unmemoizes while preserving I/O pairs for possible re-installation later, see deinstall-io-pairs.