Smt-computed-hint
SMT::SMT-computed-hint extract the actual hints from the
SMT::hint-please disjunct, apply the SMT::remove-hint-please
clause-processor, and install the smt-delayed-hint for
applying the actual hints.
- Signature
(smt-computed-hint cl) → *
Definitions and Theorems
Function: smt-computed-hint
(defun smt-computed-hint (cl)
(declare (xargs :guard t))
(let ((acl2::__function__ 'smt-computed-hint))
(declare (ignorable acl2::__function__))
(b* (((mv & kwd-alist)
(extract-hint-wrapper cl)))
(cons
':computed-hint-replacement
(cons
(cons (cons 'smt-delayed-hint
(cons 'clause
(cons (cons 'quote (cons kwd-alist 'nil))
'nil)))
'nil)
'(:clause-processor (remove-hint-please clause)))))))
