14#ifndef CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
15#define CPROVER_GOTO_INSTRUMENT_WMM_DATA_DP_H
void dp_merge()
merge in N^3
void print(messaget &message)
std::set< datat > data_typet
bool dp(const abstract_eventt &e1, const abstract_eventt &e2) const
search in N^2
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write)
Class that provides messages with a built-in verbosity 'level'.
datat(irep_idt _id, source_locationt _loc, unsigned _eq_class)
bool operator==(const datat &d) const
datat(irep_idt _id, source_locationt _loc)
bool operator<(const datat &d2) const