		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Process-hint

Signature
(process-hint cl user-hint) → subgoal-lst
Arguments: cl — Guard (pseudo-term-listp cl).
Returns: subgoal-lst — Type (pseudo-term-list-listp subgoal-lst).

Definitions and Theorems

Function: process-hint

(defun process-hint (cl user-hint)
 (declare (xargs :guard (pseudo-term-listp cl)))
 (let ((acl2::__function__ 'process-hint))
  (declare (ignorable acl2::__function__))
  (b*
   ((cl (pseudo-term-list-fix cl))
    ((unless (smtlink-hint-syntax-p user-hint))
     (prog2$
      (cw
       "User provided Smtlink hint can't be applied because of ~
    syntax error in the hints: ~q0Therefore proceed without Smtlink...~%"
       user-hint)
      (list cl)))
    (combined-hint (combine-hints user-hint (smt-hint)))
    (next-cp (cdr (assoc-equal 'process-hint
                               *smt-architecture*)))
    ((if (null next-cp)) (list cl))
    (cp-hint
     (cons
      ':clause-processor
      (cons
           (cons next-cp
                 (cons 'clause
                       (cons (cons 'quote (cons combined-hint 'nil))
                             'nil)))
           'nil)))
    (subgoal-lst (cons (cons 'hint-please
                             (cons (cons 'quote (cons cp-hint 'nil))
                                   'nil))
                       cl)))
   (list subgoal-lst))))

Theorem: pseudo-term-list-listp-of-process-hint

(defthm pseudo-term-list-listp-of-process-hint
  (b* ((subgoal-lst (process-hint cl user-hint)))
    (pseudo-term-list-listp subgoal-lst))
  :rule-classes :rewrite)