		Search-engine friendly clone of the ACL2 documentation.

Call-graphs

Exists-call-pathp

Check for the existence of a call path from the destination to the target.

Signature
(exists-call-pathp from to call-graph) → *
Arguments: from — Guard (qualified-identp from).; to — Guard (qualified-ident-optionp to).; call-graph — Guard (call-graphp call-graph).

That is, the function checks whether to is in from's transitive closure. See call-graph-transitive-closure.

Definitions and Theorems

Function: exists-call-pathp

(defun exists-call-pathp (from to call-graph)
  (declare (xargs :guard (and (qualified-identp from)
                              (qualified-ident-optionp to)
                              (call-graphp call-graph))))
  (let ((__function__ 'exists-call-pathp))
    (declare (ignorable __function__))
    (in to
        (call-graph-transitive-closure from call-graph))))