		Search-engine friendly clone of the ACL2 documentation.

Verified

Smt-extract

SMT-extract extracts type hypotheses from the clause. The SMT solver requires knowing type declarations.

Definitions and Theorems

Function: is-type-hyp-decl

(defun is-type-hyp-decl (expr)
  (declare (xargs :guard (pseudo-termp expr)))
  (let ((acl2::__function__ 'is-type-hyp-decl))
    (declare (ignorable acl2::__function__))
    (b* (((unless (equal (len expr) 3)) nil)
         (fn-name (car expr))
         ((unless (equal fn-name 'type-hyp))
          nil))
      t)))

Theorem: booleanp-of-is-type-hyp-decl

(defthm booleanp-of-is-type-hyp-decl
  (b* ((is-type-hyp? (is-type-hyp-decl expr)))
    (booleanp is-type-hyp?))
  :rule-classes :rewrite)

Function: extract-is-decl

(defun extract-is-decl (expr fty-info abs)
 (declare (xargs :guard (and (pseudo-termp expr)
                             (fty-info-alist-p fty-info)
                             (symbol-listp abs))))
 (let ((acl2::__function__ 'extract-is-decl))
   (declare (ignorable acl2::__function__))
   (b* (((if (is-type-hyp-decl expr)) t)
        ((unless (equal (len expr) 2)) nil)
        (fn-name (car expr))
        ((unless (symbolp fn-name)) nil)
        ((unless (or (member-equal fn-name (strip-cars *smt-types*))
                     (member-equal fn-name abs)
                     (typedecl-of-flextype fn-name fty-info)))
         nil)
        ((unless (and (symbolp (cadr expr)) (cadr expr)))
         nil))
     t)))

Theorem: booleanp-of-extract-is-decl

(defthm booleanp-of-extract-is-decl
  (b* ((is-decl? (extract-is-decl expr fty-info abs)))
    (booleanp is-decl?))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-append-of-pseudo-term-listp

(defthm pseudo-term-listp-of-append-of-pseudo-term-listp
  (implies (and (pseudo-term-listp x)
                (pseudo-term-listp y))
           (pseudo-term-listp (append x y))))

Function: extract-disjunct

(defun extract-disjunct (term fty-info abs)
 (declare (xargs :guard (and (pseudo-termp term)
                             (fty-info-alist-p fty-info)
                             (symbol-listp abs))))
 (let ((acl2::__function__ 'extract-disjunct))
  (declare (ignorable acl2::__function__))
  (b* ((term (pseudo-term-fix term)))
   (cond
     ((not (consp term)) (mv nil term))
     ((and (equal (car term) 'if)
           (equal (caddr term) ''t))
      (b* (((mv decl1 term1)
            (extract-disjunct (cadr term)
                              fty-info abs))
           ((mv decl2 term2)
            (extract-disjunct (cadddr term)
                              fty-info abs)))
        (mv (append decl1 decl2)
            (cond ((or (equal term1 ''t) (equal term2 ''t))
                   ''t)
                  ((equal term1 ''nil) term2)
                  ((equal term2 ''nil) term1)
                  (t (cons 'if
                           (cons term1
                                 (cons ''t (cons term2 'nil)))))))))
     ((equal (car term) 'not)
      (b* (((mv decl0 term0)
            (extract-conjunct (cadr term)
                              fty-info abs)))
        (mv decl0
            (cond ((equal term0 ''nil) ''t)
                  ((equal term0 ''t) ''nil)
                  (t (cons 'not (cons term0 'nil)))))))
     ((equal (car term) 'implies)
      (b* (((mv decl1 term1)
            (extract-conjunct (cadr term)
                              fty-info abs))
           ((mv decl2 term2)
            (extract-disjunct (caddr term)
                              fty-info abs)))
        (mv (append decl1 decl2)
            (cond ((or (equal term1 ''nil)
                       (equal term2 ''t))
                   ''t)
                  ((equal term1 ''t) term2)
                  ((equal term2 ''nil)
                   (cons 'not (cons term1 'nil)))
                  (t (cons 'implies
                           (cons term1 (cons term2 'nil))))))))
     (t (mv nil term))))))

Function: extract-conjunct

(defun extract-conjunct (term fty-info abs)
 (declare (xargs :guard (and (pseudo-termp term)
                             (fty-info-alist-p fty-info)
                             (symbol-listp abs))))
 (let ((acl2::__function__ 'extract-conjunct))
  (declare (ignorable acl2::__function__))
  (b* ((term (pseudo-term-fix term)))
   (cond
       ((not (consp term)) (mv nil term))
       ((and (equal (car term) 'if)
             (equal (cadddr term) ''nil))
        (b* (((mv decl1 term1)
              (extract-conjunct (cadr term)
                                fty-info abs))
             ((mv decl2 term2)
              (extract-conjunct (caddr term)
                                fty-info abs)))
          (mv (append decl1 decl2)
              (cond ((or (equal term1 ''nil)
                         (equal term2 ''nil))
                     ''nil)
                    ((equal term1 ''t) term2)
                    ((equal term2 ''t) term1)
                    (t (cons 'if
                             (cons term1 (cons term2 '('nil)))))))))
       ((equal (car term) 'not)
        (b* (((mv decl0 term0)
              (extract-disjunct (cadr term)
                                fty-info abs)))
          (mv decl0
              (cond ((equal term0 ''nil) ''t)
                    ((equal term0 ''t) ''nil)
                    (t (cons 'not (cons term0 'nil)))))))
       ((extract-is-decl term fty-info abs)
        (mv (list term) ''t))
       (t (mv nil term))))))

Theorem: return-type-of-extract-disjunct.decl-list

(defthm return-type-of-extract-disjunct.decl-list
  (b* (((mv ?decl-list ?theorem)
        (extract-disjunct term fty-info abs)))
    (pseudo-term-listp decl-list))
  :rule-classes :rewrite)

Theorem: return-type-of-extract-disjunct.theorem

(defthm return-type-of-extract-disjunct.theorem
  (b* (((mv ?decl-list ?theorem)
        (extract-disjunct term fty-info abs)))
    (pseudo-termp theorem))
  :rule-classes :rewrite)

Theorem: return-type-of-extract-conjunct.decl-list

(defthm return-type-of-extract-conjunct.decl-list
  (b* (((mv ?decl-list ?theorem)
        (extract-conjunct term fty-info abs)))
    (pseudo-term-listp decl-list))
  :rule-classes :rewrite)

Theorem: return-type-of-extract-conjunct.theorem

(defthm return-type-of-extract-conjunct.theorem
  (b* (((mv ?decl-list ?theorem)
        (extract-conjunct term fty-info abs)))
    (pseudo-termp theorem))
  :rule-classes :rewrite)

Function: smt-extract

(defun smt-extract (term fty-info abs)
  (declare (xargs :guard (and (pseudo-termp term)
                              (fty-info-alist-p fty-info)
                              (symbol-listp abs))))
  (let ((acl2::__function__ 'smt-extract))
    (declare (ignorable acl2::__function__))
    (b* (((mv decl-list theorem)
          (extract-disjunct term fty-info abs)))
      (mv decl-list theorem))))

Theorem: pseudo-term-listp-of-smt-extract.decl-list

(defthm pseudo-term-listp-of-smt-extract.decl-list
  (b* (((mv ?decl-list ?theorem)
        (smt-extract term fty-info abs)))
    (pseudo-term-listp decl-list))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-smt-extract.theorem

(defthm pseudo-termp-of-smt-extract.theorem
  (b* (((mv ?decl-list ?theorem)
        (smt-extract term fty-info abs)))
    (pseudo-termp theorem))
  :rule-classes :rewrite)

Subtopics

Extract: Functions for extracting type declarations from clause.