Checking if a function call is a flextype related call. These calls will be translated directly to SMT solver, therefore won't need to be expanded.
(fncall-of-flextype fn-name fty-info) → flex?
There are five categories of flextype supported in Smtlink. Examples
are taken from
Supported functions for defprod:
Supported functions for deflist: (note Smtlink only support deflists that are true-listp)
Supported functions for defalist: (note Smtlink only support defalists that are true-listp)
Supported functions for defoption:
Function:
(defun fncall-of-flextype (fn-name fty-info) (declare (xargs :guard (and (symbolp fn-name) (fty-info-alist-p fty-info)))) (let ((acl2::__function__ 'fncall-of-flextype)) (declare (ignorable acl2::__function__)) (b* ((fn-name (symbol-fix fn-name)) (fty-info (fty-info-alist-fix fty-info)) (item (assoc-equal fn-name fty-info)) ((if item) t)) (fncall-of-flextype-special fn-name))))
Theorem:
(defthm fncall-of-flextype-conclusion (b* ((flex? (fncall-of-flextype fn-name fty-info))) (implies (and flex? (symbolp fn-name) (fty-info-alist-p fty-info)) (or (assoc-equal fn-name fty-info) (fncall-of-flextype-special fn-name)))) :rule-classes :rewrite)