CBMC
Loading...
Searching...
No Matches
generalization.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generalization
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "generalization.h"
13
14#include <util/console.h>
15#include <util/format_expr.h>
16
17#include "solver.h"
18
19#include <algorithm>
20#include <iostream>
21#include <map>
22
24{
25public:
26 explicit frequency_mapt(const exprt &expr)
27 {
28 setup_rec(expr);
29 }
30
31 void operator()(const exprt &expr)
32 {
33 count_rec(expr);
34 }
35
36 using counterst = std::map<exprt, std::size_t>;
37
38 // return frequencies, highest to lowest
39 std::vector<counterst::const_iterator> frequencies() const
40 {
41 std::vector<counterst::const_iterator> result;
42 for(auto it = counters.begin(); it != counters.end(); it++)
43 result.push_back(it);
44 std::sort(
45 result.begin(),
46 result.end(),
47 [](counterst::const_iterator a, counterst::const_iterator b) -> bool {
48 return a->second > b->second;
49 });
50 return result;
51 }
52
53protected:
55
56 void count_rec(const exprt &expr)
57 {
58 if(expr.id() == ID_or)
59 {
60 for(auto &op : expr.operands())
61 count_rec(op);
62 }
63 else
64 {
65 auto it = counters.find(expr);
66 if(it != counters.end())
67 it->second++;
68 }
69 }
70
71 void setup_rec(const exprt &expr)
72 {
73 if(expr.id() == ID_or)
74 {
75 for(auto &op : expr.operands())
76 setup_rec(op);
77 }
78 else
79 counters.emplace(expr, 0);
80 }
81};
82
84 std::vector<framet> &frames,
85 const workt &dropped,
86 const propertyt &property,
88{
89 // Look at the frame where we've given up
90 auto &frame = frames[dropped.frame.index];
91
92 if(solver_options.verbose)
93 {
94 for(auto &invariant : frame.invariants)
95 {
96 std::cout << consolet::green << "GI " << format(invariant)
97 << consolet::reset << '\n';
98 }
99 }
100
101 // We generalize by dropping disjuncts.
102 // Look at the frequencies of the disjuncts in the proof obligation
103 // among the candidate invariant and the previous obligations.
105
106 for(auto &i : frame.invariants)
107 frequency_map(i);
108
109 for(auto &o : frame.obligations)
110 frequency_map(o);
111
112 const auto frequencies = frequency_map.frequencies();
113
114 if(solver_options.verbose)
115 {
116 for(auto entry : frequencies)
117 {
118 std::cout << "Freq " << entry->second << " " << format(entry->first)
119 << "\n";
120 }
121 }
122
123 // form disjunction of top ones
125 for(auto entry : frequencies)
126 {
127 if(entry->second == frequencies.front()->second)
128 disjuncts.push_back(entry->first);
129 }
130
131 // Does this actually strengthen the formula?
132 if(disjuncts.size() < frequencies.size())
133 {
135 frame.add_invariant(new_invariant);
136 if(solver_options.verbose)
137 std::cout << consolet::yellow << "NI " << format(new_invariant)
138 << consolet::reset << '\n';
139 }
140 else
141 {
142 // no, give up
143 }
144}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
static std::ostream & yellow(std::ostream &)
Definition console.cpp:136
static std::ostream & reset(std::ostream &)
Definition console.cpp:176
static std::ostream & green(std::ostream &)
Definition console.cpp:120
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
operandst & operands()
Definition expr.h:94
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
Definition irep.h:388
Console.
static format_containert< T > format(const T &o)
Definition format.h:37
void generalization(std::vector< framet > &frames, const workt &dropped, const propertyt &property, const solver_optionst &solver_options)
Generalization.
Equality Propagation.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:71