• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
        • Saving-event-data
        • Trans-eval
        • System-utilities-non-built-in
        • Get-event-data
        • Untranslate
        • Constraint-info
      • Stobj
      • State
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Loop$-primer
      • Fast-alists
      • Defconst
      • Defmacro
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Irrelevant-formals
      • Efficiency
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Oracle-eval
      • Defmacro-untouchable
      • Primitive
      • <<
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• System-utilities
• Constraint

Constraint-info

Obtaining the constraint on a function symbol

For a function symbol, fn, and a logical world, wrld — for example, the current world, (w state) — evaluation of the form (constraint-info fn wrld) returns (mv flg c), where c is the list of constraints on fn (implicitly conjoined), and flg is nil if fn is a defined function and otherwise is a function symbol with that same list of constraints (possibly fn itself). See constraint for relevant background.

We illustrate with the following example.

(encapsulate
  (((f1 *) => *)
   ((f3 *) => *))
  (local (defun f1 (x) x))
  (defun f2 (x) (f1 x))
  (local (defun f3 (x) x))
  (defun f4 (x) (f3 x))
  (defthm f1-prop (equal (f1 x) (f4 x))))

Then we can see the results of constraint-info on each introduced function symbol, as follows.

ACL2 !>(let ((wrld (w state)))
          (list
           'result
           'f1 (mv-let (flg1 c1) (constraint-info 'f1 wrld) (list flg1 c1))
           'f2 (mv-let (flg2 c2) (constraint-info 'f2 wrld) (list flg2 c2))
           'f3 (mv-let (flg3 c3) (constraint-info 'f3 wrld) (list flg3 c3))
           'f4 (mv-let (flg4 c4) (constraint-info 'f4 wrld) (list flg4 c4))))
(RESULT F1
        (F1 ((EQUAL (F4 X) (F3 X))
             (EQUAL (F1 X) (F4 X))))
        F2 (NIL (EQUAL (F2 X) (F1 X)))
        F3
        (F1 ((EQUAL (F4 X) (F3 X))
             (EQUAL (F1 X) (F4 X))))
        F4
        (F1 ((EQUAL (F4 X) (F3 X))
             (EQUAL (F1 X) (F4 X)))))
ACL2 !>

Notice that the flag (first result) for f2 is nil, because even though the definition of f2 is lexically inside the encapsulate, it doesn't affect the constraints because it can be safely moved to just after the encapsulate. However, the definition of f4 does affect (or ``infect''; see subversive-recursions) the constraints: it can't be moved to after the encapsulate because of the defthm after it.

Also see constraint. For more details, see comments in the definition of constraint-info in the ACL2 source code.