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 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;                                                        \
  }

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.

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.