27 const std::string &prefix)
30 "memory_model::choice_"+prefix+std::to_string(
var_cnt++),
37 if(e1->source.thread_nr==e2->source.thread_nr)
52 for(address_mapt::const_iterator
57 const a_rect &a_rec=a_it->second;
59 for(event_listt::const_iterator
60 r_it=a_rec.
reads.begin();
61 r_it!=a_rec.
reads.end();
67 rf_some_operands.reserve(a_rec.
writes.size());
70 for(event_listt::const_iterator
82 w->source.thread_nr==
r->source.thread_nr;
88 std::make_pair(
r, w)]=s;
106 cond,
"rf-order",
r->source);
109 rf_some_operands.push_back(s);
117 if(rf_some_operands.empty())
119 else if(rf_some_operands.size()==1)
120 rf_some=rf_some_operands.front();
124 rf_some.
operands().swap(rf_some_operands);
symbol_exprt nondet_bool_symbol(const std::string &prefix)
void read_from(symex_target_equationt &equation)
exprt before(event_it e1, event_it e2, unsigned axioms)
API to expression classes.
bool po(event_it e1, event_it e2)
std::vector< exprt > operandst
choice_symbolst choice_symbols
virtual ~memory_model_baset()
memory_model_baset(const namespacet &_ns)
Memory models for partial order concurrency.
eventst::const_iterator event_it
Base class for all expressions.
void add_constraint(symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
Expression to hold a symbol (variable)