		Search-engine friendly clone of the ACL2 documentation.

Verified

Smt-computed-hints

This document discusses how computed-hints are used in the architecture of Smtlink.

Smtlink uses ACL2::computed-hints and ACL2::clause-processor for controlling the several translation steps. To use Smtlink, the user first installs the computed hint, SMT::SMT-computed-hint. When the user uses :smtlink in ACL2::hints, it macro-expands into a :clause-processor hint. This applies the first clause-processor for parsing smt-hint. This clause-processor also add (SMT::hint-please some-hint) into the clause as the first in the disjunction. The SMT::SMT-computed-hint will recognize clauses that matches the form (('hint-please ) . term). It extracts the some-hint from the clause, and install below :computed-hint-replacement:

`(:computed-hint-replacement ((SMT-delayed-hint clause ',some-hint))
  :clause-processor (remove-hint-please clause))

This :computed-hint-replacement does two things: clearing up the SMT::hint-please disjunct from the clause with the hint :clause-processor (remove-hint-please clause), and install another computed-hint called SMT::SMT-delayed-hint for actually applying some-hint to the cleaned-up new subgoal.

We started out using just one computed-hint that recognizes SMT::hint-please and applies the hint. This results in a rewrite-loop that resembles the one described at ACL2::using-computed-hints-6. The problem is that, when a user supplies a :use hint, the computed-hint would generate a new subgoal that still contains the SMT::hint-please. The SMT::hint-please then triggers the computed-hint again, applying the :use hint, which generates a new subgoal that still contains the SMT::hint-please. This then triggers the computed-hint again ... you get the idea. To solve this problem, we add this one additional step of clause-processor to remove the SMT::hint-please disjunct from the clause. Then install another computed-hint called SMT::SMT-delayed-hint for running the real hints on the subgoal. Because this new subgoal doesn't contain SMT::hint-please, the SMT::SMT-computed-hint won't get in the way. It works fine even when the some-hint is again a :smtlink hint, allowing the user to use Smtlink inside of a Smtlink proof.

Definitions and Theorems

Function: my-split-kwd-alist

(defun my-split-kwd-alist (key kwd-alist)
 (declare (xargs :guard (and (symbolp key)
                             (true-listp kwd-alist))))
 (let ((acl2::__function__ 'my-split-kwd-alist))
  (declare (ignorable acl2::__function__))
  (b* ((kwd-alist (true-list-fix kwd-alist))
       ((unless (consp kwd-alist))
        (mv nil nil))
       ((if (eq key (car kwd-alist)))
        (mv nil kwd-alist))
       ((unless (consp (cdr kwd-alist)))
        (prog2$ (er hard?
                    'smt-computed-hints=>my-split-kwd-alist
                    "Something ~
  is wrong with the kwd-alist: ~q0"
                    kwd-alist)
                (mv nil nil)))
       ((mv pre post)
        (my-split-kwd-alist key (cddr kwd-alist))))
    (mv (cons (car kwd-alist)
              (cons (cadr kwd-alist) pre))
        post))))

Theorem: true-listp-of-my-split-kwd-alist.pre

(defthm true-listp-of-my-split-kwd-alist.pre
  (b* (((mv ?pre ?post)
        (my-split-kwd-alist key kwd-alist)))
    (true-listp pre))
  :rule-classes :rewrite)

Theorem: true-listp-of-my-split-kwd-alist.post

(defthm true-listp-of-my-split-kwd-alist.post
  (b* (((mv ?pre ?post)
        (my-split-kwd-alist key kwd-alist)))
    (true-listp post))
  :rule-classes :rewrite)

Function: treat-in-theory-hint

(defun treat-in-theory-hint (enabled kwd-alist)
 (declare (xargs :guard (and (true-listp enabled)
                             (true-listp kwd-alist))))
 (let ((acl2::__function__ 'treat-in-theory-hint))
  (declare (ignorable acl2::__function__))
  (b* ((kwd-alist (true-list-fix kwd-alist))
       ((mv pre post)
        (my-split-kwd-alist :in-theory kwd-alist)))
   (cond
    ((and (consp post)
          (consp (cdr post))
          (consp (cadr post))
          (equal (caadr post) 'enable))
     (append pre
             (cons ':in-theory
                   (cons (cons 'enable
                               (append enabled (cdadr post)))
                         (cddr post)))))
    ((and (consp post)
          (consp (cdr post))
          (consp (cadr post))
          (equal (caadr post) 'disable))
     (append
          pre
          (cons ':in-theory
                (cons (cons 'e/d
                            (cons enabled (cons (cdadr post) 'nil)))
                      (cddr post)))))
    ((and (consp post)
          (consp (cdr post))
          (consp (cadr post))
          (consp (cdadr post))
          (consp (cddadr post))
          (equal (caadr post) 'e/d))
     (append
         pre
         (cons ':in-theory
               (cons (cons 'e/d
                           (cons (append enabled (car (cdadr post)))
                                 (cons (cadr (cdadr post)) 'nil)))
                     (cddr post)))))
    (t (cons ':in-theory
             (cons (cons 'enable enabled)
                   kwd-alist)))))))

Theorem: true-listp-of-treat-in-theory-hint

(defthm true-listp-of-treat-in-theory-hint
  (b* ((new-kwd-alist (treat-in-theory-hint enabled kwd-alist)))
    (true-listp new-kwd-alist))
  :rule-classes :rewrite)

Function: treat-expand-hint

(defun treat-expand-hint (expand-lst kwd-alist)
  (declare (xargs :guard (and (true-listp expand-lst)
                              (true-listp kwd-alist))))
  (let ((acl2::__function__ 'treat-expand-hint))
    (declare (ignorable acl2::__function__))
    (b* ((kwd-alist (true-list-fix kwd-alist))
         ((mv pre post)
          (my-split-kwd-alist :expand kwd-alist)))
      (cond ((and (consp post) (consp (cdr post)))
             (append pre
                     (cons ':expand
                           (cons (append expand-lst (cadr post))
                                 post))))
            (t (cons ':expand
                     (append expand-lst kwd-alist)))))))

Theorem: true-listp-of-treat-expand-hint

(defthm true-listp-of-treat-expand-hint
  (b* ((new-kwd-alist (treat-expand-hint expand-lst kwd-alist)))
    (true-listp new-kwd-alist))
  :rule-classes :rewrite)

Function: extract-hint-wrapper

(defun extract-hint-wrapper (cl)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'extract-hint-wrapper))
    (declare (ignorable acl2::__function__))
    (cond ((endp cl) (mv nil nil))
          (t (b* ((lit cl))
               (case-match lit
                 ((('hint-please ('quote kwd-alist))
                   . term)
                  (mv term kwd-alist))
                 (& (extract-hint-wrapper (cdr cl)))))))))

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)))))))

Function: smt-delayed-hint

(defun smt-delayed-hint (cl kwd-alist)
  (declare (ignore cl))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'smt-delayed-hint))
    (declare (ignorable acl2::__function__))
    (cons ':computed-hint-replacement
          (cons '((smt-computed-hint clause))
                kwd-alist))))

Subtopics

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.
Smt-delayed-hint: SMT::SMT-delayed-hints applies the hints kwd-alist and install the smt-computed-hint back.