CBMC
smt_logics.cpp File Reference
#include "smt_logics.h"
#include "smt_logics.def"
+ Include dependency graph for smt_logics.cpp:

Go to the source code of this file.

Macros

#define LOGIC_ID(the_id, the_name)    const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
 
#define LOGIC_ID(the_id, the_name)
 
#define LOGIC_ID(the_id, the_name)
 

Functions

template<typename visitort >
void accept (const smt_logict &logic, const irep_idt &id, visitort &&visitor)
 

Macro Definition Documentation

◆ LOGIC_ID [1/3]

#define LOGIC_ID (   the_id,
  the_name 
)     const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};

Definition at line 45 of file smt_logics.cpp.

◆ LOGIC_ID [2/3]

#define LOGIC_ID (   the_id,
  the_name 
)
Value:
if(id == ID_smt_logic_##the_id) \
return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));

Definition at line 45 of file smt_logics.cpp.

◆ LOGIC_ID [3/3]

#define LOGIC_ID (   the_id,
  the_name 
)
Value:
smt_logic_##the_id##t::smt_logic_##the_id##t() \
: smt_logict{ID_smt_logic_##the_id} \
{ \
}

Definition at line 45 of file smt_logics.cpp.

Function Documentation

◆ accept()

template<typename visitort >
void accept ( const smt_logict logic,
const irep_idt id,
visitort &&  visitor 
)

Definition at line 23 of file smt_logics.cpp.