Read-ACL2-oracle
Pop the oracle field of the state
ACL2 has a mutable `state' that contains a number of fields; see
state. One of these fields is a list, called the acl2-oracle
field. There are no constraints on the elements of this list; thus, you will
not be able to prove anything about those elements. However, as a
convenience, ACL2 permits you to evaluate the form (read-acl2-oracle
state), which returns the multiple value (mv nil nil state).
The ACL2 implementation uses read-acl2-oracle, but you will likely
find this function to be useless unless you do advanced, scurrilous things
using trust tags (see defttag).
The following definition is the logical definition of
read-acl2-oracle, but as explained above does not really characterize its
behavior under the hood.
Function: read-acl2-oracle
(defun read-acl2-oracle (state-state)
(declare (xargs :guard (state-p1 state-state)))
(mv (null (acl2-oracle state-state))
(car (acl2-oracle state-state))
(update-acl2-oracle (cdr (acl2-oracle state-state))
state-state)))
