CBMC
smt_sorts.cpp File Reference
#include "smt_sorts.h"
#include <util/invariant.h>
#include "smt_sorts.def"
+ Include dependency graph for smt_sorts.cpp:

Go to the source code of this file.

Macros

#define SORT_ID(the_id)    const irep_idt ID_smt_##the_id##_sort{"smt_" #the_id "_sort"};
 
#define SORT_ID(the_id)
 
#define SORT_ID(the_id)
 
#define SORT_ID(the_id)
 

Functions

template<typename visitort >
void accept (const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
 

Macro Definition Documentation

◆ SORT_ID [1/4]

#define SORT_ID (   the_id)     const irep_idt ID_smt_##the_id##_sort{"smt_" #the_id "_sort"};

Definition at line 25 of file smt_sorts.cpp.

◆ SORT_ID [2/4]

#define SORT_ID (   the_id)
Value:
template <> \
const smt_##the_id##_sortt *smt_sortt::cast<smt_##the_id##_sortt>() const & \
{ \
return id() == ID_smt_##the_id##_sort \
? static_cast<const smt_##the_id##_sortt *>(this) \
: nullptr; \
}
const irep_idt & id() const
Definition: irep.h:384

Definition at line 25 of file smt_sorts.cpp.

◆ SORT_ID [3/4]

#define SORT_ID (   the_id)
Value:
template <> \
std::optional<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>() \
&& \
{ \
if(id() == ID_smt_##the_id##_sort) \
return {std::move(*static_cast<const smt_##the_id##_sortt *>(this))}; \
else \
return {}; \
}

Definition at line 25 of file smt_sorts.cpp.

◆ SORT_ID [4/4]

#define SORT_ID (   the_id)
Value:
if(id == ID_smt_##the_id##_sort) \
return visitor.visit(static_cast<const smt_##the_id##_sortt &>(sort));

Definition at line 25 of file smt_sorts.cpp.

Function Documentation

◆ accept()

template<typename visitort >
void accept ( const smt_sortt sort,
const irep_idt id,
visitort &&  visitor 
)

Definition at line 87 of file smt_sorts.cpp.