6#define OPTION_ID(the_id) \
7 const irep_idt ID_smt_option_##the_id{"smt_option_" #the_id};
6#define OPTION_ID(the_id) \ …
8#include "smt_options.def"
23 return !(*
this == other);
37template <
typename visitort>
40#define OPTION_ID(the_id) \
41 if(id == ID_smt_option_##the_id) \
42 return visitor.visit(static_cast<const smt_option_##the_id##t &>(option));
45#include "smt_options.def"
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
bool operator==(const irept &other) const
void set(const irep_idt &name, const irep_idt &value)
smt_option_produce_modelst(bool setting)
void accept(smt_option_const_downcast_visitort &) const
bool operator==(const smt_optiont &) const
bool operator!=(const smt_optiont &) const
void accept(const smt_optiont &option, const irep_idt &id, visitort &&visitor)
#define UNREACHABLE
This should be used to mark dead code.