smt_sorts.def File Reference

This set of definitions is used as part of the X-macro pattern. More...

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Detailed Description

This set of definitions is used as part of the X-macro pattern.

These define the set of sorts which are implemented and it is used to automate repetitive parts of the implementation. These include -

• The constant irep_idts used to identify each of the sort classes.
• The member functions of the smt_sort_const_downcast_visitort class.
• The type of sort checks required to implement smt_sortt::accept.

Definition in file smt_sorts.def.