CBMC
smt_sorts.h File Reference

Data structure for smt sorts. More...

#include <util/irep.h>
#include <optional>
#include <type_traits>
#include "smt_sorts.def"
+ Include dependency graph for smt_sorts.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  smt_sortt
 
class  smt_sortt::storert< derivedt >
 Class for adding the ability to up and down cast smt_sortt to and from irept. More...
 
class  smt_bool_sortt
 
class  smt_bit_vector_sortt
 
class  smt_array_sortt
 
class  smt_sort_const_downcast_visitort
 

Macros

#define SORT_ID(the_id)   virtual void visit(const smt_##the_id##_sortt &) = 0;
 

Detailed Description

Data structure for smt sorts.

Note
All classes derived from smt_sortt, must be listed in smt_sorts.def.

Definition in file smt_sorts.h.

Macro Definition Documentation

◆ SORT_ID

#define SORT_ID (   the_id)    virtual void visit(const smt_##the_id##_sortt &) = 0;

Definition at line 103 of file smt_sorts.h.