12 #ifndef CPROVER_MUSKETEER_FENCE_INSERTER_H 13 #define CPROVER_MUSKETEER_FENCE_INSERTER_H 99 unsigned const_constraints_number,
100 unsigned const_unique);
112 std::set<event_idt>
po;
184 if(copy.find(
"::")==std::string::npos)
186 return copy.substr(copy.find_last_of(
"::")+1);
191 std::list<std::string>::const_iterator it,
192 std::list<std::string>::const_iterator end,
196 #endif // CPROVER_MUSKETEER_FENCE_INSERTER_H std::map< unsigned, edget > & map_to_e
normal variables used almost every time
The type of an expression.
std::map< edget, unsigned > & map_from_e
fence_insertert(instrumentert &instr)
const std::string & id2string(const irep_idt &d)
const_graph_visitort const_graph_visitor
to retrieve the concrete graph edges involved in the (abstract) cycles
std::string to_string(fence_typet f) const
unsigned col_to_var(unsigned u) const
virtual void process_cycles_selection()
std::list< std::set< event_idt > > powr_constraints
typet get_type(const irep_idt &id)
event_grapht::critical_cyclet::delayt edget
typet type_component(std::list< std::string >::const_iterator it, std::list< std::string >::const_iterator end, const typet &type)
fence_insertert(instrumentert &instr, memory_modelt _model)
std::map< edget, fence_typet > fenced_edges
unsigned add_invisible_edge(const edget &e)
std::map< edget, unsigned > map_from_e
const memory_modelt model
unsigned add_edge(const edget &e)
static std::string remove_extra(std::string copy)
fence_typet col_to_fence(unsigned u) const
virtual unsigned fence_cost(fence_typet e) const
event_grapht::critical_cyclet::delayt edget
virtual bool filter_cycles(unsigned cycle_id) const
std::list< std::set< event_idt > > porr_constraints
unsigned var_fence_to_col(fence_typet f, unsigned var) const
cycles visitor for computing edges involved for fencing
void mip_fill_matrix(ilpt &ilp, unsigned &i, unsigned const_constraints_number, unsigned const_unique)
graph visitor for computing edges involved for fencing
std::list< std::set< event_idt > > com_constraints
instrumentert & instrumenter
void compute_fence_options()
static std::string remove_extra(const irep_idt &id)
void mip_set_var(ilpt &ilp, unsigned &i)
cycles_visitort cycles_visitor
std::list< std::set< event_idt > > porw_constraints
void mip_set_cst(ilpt &ilp, unsigned &i)
std::map< unsigned, edget > map_to_e
std::map< unsigned, float > freq_table
unsigned add_edge(const edget &e)
std::size_t constraints_number
number of constraints
std::list< std::set< event_idt > > poww_constraints