Constraint-info
Obtaining the constraint on a function symbol
See constraints for relevant background.
Constraint-info is a rather technical system utility, and detailed
documentation may be found in comments in the ACL2 source code, in particular
in the definition of constraint-info. Here we give only an overview of
this utility.
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 x origins), as
follows. When flg is nil, x is a term and origins is a
single origin token such as (DEFUN FN), indicating the source of
the constraint, x, on fn. When flg is non-nil it is a
function name, and usually x is a list of terms and origins is an
equally long list of corresponding origin tokens; but there is a special case
if the constraints are unknown, as can be the case with use of partial-encapsulate.
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 x1 origin1)
(constraint-info 'f1 wrld)
(list flg1 x1 origin1))
'f2
(mv-let (flg2 x2 origin2)
(constraint-info 'f2 wrld)
(list flg2 x2 origin2))
'f3
(mv-let (flg3 x3 origin3)
(constraint-info 'f3 wrld)
(list flg3 x3 origin3))
'f4
(mv-let (flg4 x4 origin4)
(constraint-info 'f4 wrld)
(list flg4 x4 origin4))))
(RESULT F1
(F1 ((EQUAL (F4 X) (F3 X))
(EQUAL (F1 X) (F4 X)))
((DEFUN F4) (THEOREM F1-PROP)))
F2
(NIL (EQUAL (F2 X) (F1 X)) (DEFUN F2))
F3
(F1 ((EQUAL (F4 X) (F3 X))
(EQUAL (F1 X) (F4 X)))
((DEFUN F4) (THEOREM F1-PROP)))
F4
(F1 ((EQUAL (F4 X) (F3 X))
(EQUAL (F1 X) (F4 X)))
((DEFUN F4) (THEOREM F1-PROP))))
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.
