		Search-engine friendly clone of the ACL2 documentation.

Smtlink-hint

Smtlink-hint-p

Recognizer for smtlink-hint structures.

Signature
(smtlink-hint-p x) → *

Definitions and Theorems

Function: smtlink-hint-p

(defun smtlink-hint-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'smtlink-hint-p))
  (declare (ignorable acl2::__function__))
  (and
   (mbe
    :logic
    (and (alistp x)
         (equal (strip-cars x)
                '(functions hypotheses main-hint let-binding
                            symbols abs fty fty-info fty-types
                            int-to-rat smt-dir rm-file smt-fname
                            smt-params fast-functions type-decl-list
                            expanded-clause-w/-hint expanded-g/type
                            smt-cnf wrld-fn-len custom-p)))
    :exec (fty::alist-with-carsp
               x
               '(functions hypotheses main-hint let-binding
                           symbols abs fty fty-info fty-types
                           int-to-rat smt-dir rm-file smt-fname
                           smt-params fast-functions type-decl-list
                           expanded-clause-w/-hint expanded-g/type
                           smt-cnf wrld-fn-len custom-p)))
   (b* ((functions (cdr (std::da-nth 0 x)))
        (hypotheses (cdr (std::da-nth 1 x)))
        (main-hint (cdr (std::da-nth 2 x)))
        (let-binding (cdr (std::da-nth 3 x)))
        (symbols (cdr (std::da-nth 4 x)))
        (abs (cdr (std::da-nth 5 x)))
        (fty (cdr (std::da-nth 6 x)))
        (fty-info (cdr (std::da-nth 7 x)))
        (fty-types (cdr (std::da-nth 8 x)))
        (int-to-rat (cdr (std::da-nth 9 x)))
        (smt-dir (cdr (std::da-nth 10 x)))
        (rm-file (cdr (std::da-nth 11 x)))
        (smt-fname (cdr (std::da-nth 12 x)))
        (smt-params (cdr (std::da-nth 13 x)))
        (fast-functions (cdr (std::da-nth 14 x)))
        (type-decl-list (cdr (std::da-nth 15 x)))
        (expanded-clause-w/-hint (cdr (std::da-nth 16 x)))
        (expanded-g/type (cdr (std::da-nth 17 x)))
        (smt-cnf (cdr (std::da-nth 18 x)))
        (wrld-fn-len (cdr (std::da-nth 19 x)))
        (custom-p (cdr (std::da-nth 20 x))))
     (and (func-listp functions)
          (hint-pair-listp hypotheses)
          (true-listp main-hint)
          (let-binding-p let-binding)
          (symbol-listp symbols)
          (symbol-listp abs)
          (symbol-listp fty)
          (fty-info-alist-p fty-info)
          (fty-types-p fty-types)
          (booleanp int-to-rat)
          (stringp smt-dir)
          (booleanp rm-file)
          (stringp smt-fname)
          (true-listp smt-params)
          (func-alistp fast-functions)
          (pseudo-termp type-decl-list)
          (hint-pair-p expanded-clause-w/-hint)
          (pseudo-termp expanded-g/type)
          (smtlink-config-p smt-cnf)
          (natp wrld-fn-len)
          (booleanp custom-p))))))

Theorem: consp-when-smtlink-hint-p

(defthm consp-when-smtlink-hint-p
  (implies (smtlink-hint-p x) (consp x))
  :rule-classes :compound-recognizer)