Attach/modify metadata for a defdata type
(defdata-attach pos :enumerator nth-small-pos-testing) (defdata-attach imem :enum/acc imem-custom-enum2)
(defdata-attach typename [:enum/test enum-fn] [:equiv eq-rel] [:equiv-fixer eq-fix-fn] [:constraint ... ] [:sampling constant-list] [overridable metadata] )
Defdata-attach can be used to attach custom test enumerators for certain types. This provides a method to customize Cgen's test data generation capability for certain scenarios.
(Advanced) Type refinement : User can attach rules that specify (to Cgen) how to refine/expand a variable of this type when certain additional constraints match (or subterm-match). For those who are familar with dest-elim rules, the :rule field has a similar form. For example:
(defdata-attach imemory :constraint (mget a x) ;x is the variable of this type :constraint-variable x :rule (implies (and (natp a) ;additional hyps (instp x.a) (imemoryp x1)) (equal x (mset a x.a x1))) ;refine/expand :meta-precondition (or (variablep a) (fquotep a)) :match-type :subterm-match)
Warning: Other optional keyword arguments are currently unsupported and the use of :override-ok can be unsound.