		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Combine-hints

Combining user-hints into smt-hint.

Signature
(combine-hints user-hint hint) → combined-hint
Arguments: user-hint — Guard (smtlink-hint-syntax-p user-hint).; hint — Guard (smtlink-hint-p hint).
Returns: combined-hint — Type (smtlink-hint-p combined-hint).

Definitions and Theorems

Function: combine-hints

(defun combine-hints (user-hint hint)
 (declare (xargs :guard (and (smtlink-hint-syntax-p user-hint)
                             (smtlink-hint-p hint))))
 (let ((acl2::__function__ 'combine-hints))
  (declare (ignorable acl2::__function__))
  (b*
   ((hint (smtlink-hint-fix hint))
    (user-hint (smtlink-hint-syntax-fix user-hint))
    ((unless (consp user-hint)) hint)
    ((cons option (cons second rest))
     user-hint)
    ((smtlink-hint h) hint)
    (fast-funcs (make-alist-fn-lst h.functions))
    (new-hint
     (case option
      (:functions
       (with-fast-alist
            fast-funcs
            (merge-functions
                 second
                 (change-smtlink-hint hint
                                      :fast-functions fast-funcs))))
      (:hypotheses (merge-hypothesis second hint))
      (:main-hint (merge-main-hint second hint))
      (:abstract (set-abstract-types second hint))
      (:fty (set-fty-types second hint))
      (:int-to-rat (set-int-to-rat second hint))
      (:smt-fname (set-fname second hint))
      (:smt-dir (set-smt-dir second hint))
      (:rm-file (set-rm-file second hint))
      (:custom-p (set-custom-p second hint))
      (:smt-solver-params (set-smt-solver-params second hint))
      (t (set-wrld-len second hint)))))
   (combine-hints rest new-hint))))

Theorem: smtlink-hint-p-of-combine-hints

(defthm smtlink-hint-p-of-combine-hints
  (b* ((combined-hint (combine-hints user-hint hint)))
    (smtlink-hint-p combined-hint))
  :rule-classes :rewrite)