41 std::vector<counterst::const_iterator> result;
47 [](counterst::const_iterator
a, counterst::const_iterator
b) ->
bool {
48 return a->second > b->second;
84 std::vector<framet> &
frames,
94 for(
auto &invariant : frame.invariants)
106 for(
auto &i : frame.invariants)
109 for(
auto &o : frame.obligations)
116 for(
auto entry : frequencies)
118 std::cout <<
"Freq " << entry->second <<
" " <<
format(entry->first)
125 for(
auto entry : frequencies)
127 if(entry->second == frequencies.front()->second)
132 if(
disjuncts.size() < frequencies.size())
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static std::ostream & yellow(std::ostream &)
static std::ostream & reset(std::ostream &)
static std::ostream & green(std::ostream &)
Base class for all expressions.
std::vector< exprt > operandst
std::map< exprt, std::size_t > counterst
void count_rec(const exprt &expr)
frequency_mapt(const exprt &expr)
std::vector< counterst::const_iterator > frequencies() const
void operator()(const exprt &expr)
void setup_rec(const exprt &expr)
const irep_idt & id() const
void generalization(std::vector< framet > &frames, const workt &dropped, const propertyt &property, const solver_optionst &solver_options)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...