cprover
Loading...
Searching...
No Matches
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)
#define SORT_ID(the_id)
#define SORT_ID(the_id)
#define SORT_ID(the_id)

Macro Definition Documentation

◆ SORT_ID [1/4]

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

Definition at line 8 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 sub_classt * cast() const &

Definition at line 8 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 8 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 8 of file smt_sorts.cpp.