Macro to generate linear rules about the sizes in bits of C integer types.
Each theorem says that the size in bits of the first type has the specified relation with the size in bits of the second type.
Note that we also allow equalities, not just inequalities. Linear rules may use equalities in ACL2.
Macro:
(defmacro def-integer-bits-linear-rule (type1 rel type2 &key name disable) (declare (xargs :guard (and (member-eq type1 '(char short int long llong)) (member-eq type2 '(char short int long llong)) (member-eq rel '(= < > <= >=)) (symbolp name) (booleanp disable)))) (b* ((type1-bits (pack type1 '-bits)) (type2-bits (pack type2 '-bits)) (name (or name (pack type1-bits '- rel '- type2-bits))) (type1-string (str::cat "@('" (str::downcase-string (symbol-name type1)) "')")) (type2-string (str::cat "@('" (str::downcase-string (symbol-name type2)) "')"))) (cons (if disable 'defruled 'defrule) (cons name (cons ':parents (cons (cons type1-bits (cons type2-bits 'nil)) (cons ':short (cons (str::cat "Relation between " type1-string " and " type2-string " bit sizes.") (cons (cons rel (cons (cons type1-bits 'nil) (cons (cons type2-bits 'nil) 'nil))) (cons ':rule-classes (cons (cons (cons ':linear (cons ':trigger-terms (cons (cons (cons type1-bits 'nil) (cons (cons type2-bits 'nil) 'nil)) 'nil))) 'nil) (cons ':enable (cons (cons type1-bits (cons type2-bits 'nil)) 'nil)))))))))))))