Evaluate a term and return its result, logically obtained by reading the state's oracle.
Note: for many purposes you may be able to use magic-ev-fncall
(oracle-eval term alist state) --> (mv error val state)
NOTE: Oracle-eval will not operate as intended until the form
In the logic, this function reads from the ACL2 oracle twice, to obtain the error message, if any, and the value. In the execution, we instead evaluate the term and return its result. We believe this is sound.
The term can involve free variables that appear in the alist, and can also take state, but it must return a single non-stobj value. Therefore, it cannot modify state.
Oracle-eval is a constrained function, and as such has no execution
semantics itself. Instead, an executable version is attached to it
(see defattach). By default, this executable version doesn't do
anything interesting, because a trust tag is necessary to allow
oracle-eval to function as intended. Running
(encapsulate (((oracle-eval * * state) => (mv * * state))) (local (value-triple :elided)) (defthm state-p1-of-oracle-eval (implies (state-p1 state) (state-p1 (mv-nth 2 (oracle-eval term alist state))))))
(defthm state-p1-of-oracle-eval (implies (state-p1 state) (state-p1 (mv-nth 2 (oracle-eval term alist state)))))