		Search-engine friendly clone of the ACL2 documentation.

Call-graph

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 (identp from).; to — Guard (ident-optionp to).; call-graph — Guard (ident-ident-option-set-mapp 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 (identp from)
                         (ident-optionp to)
                         (ident-ident-option-set-mapp call-graph))))
 (let ((__function__ 'exists-call-pathp))
   (declare (ignorable __function__))
   (in to
       (call-graph-transitive-closure from call-graph))))