Skip to content

Commit 56da555

Browse files
kroeningkroening
committed
CHC solver: move solver_types.h methods into solver_types.cpp
This moves the body of the methods defined in the header file into a corresponding .cpp file.
1 parent 22c547a commit 56da555

File tree

4 files changed

+199
-166
lines changed

4 files changed

+199
-166
lines changed

‎src/cprover/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ SRC = address_taken.cpp \
2727
state_encoding_targets.cpp \
2828
solver.cpp \
2929
solver_progress.cpp \
30+
solver_types.cpp \
3031
variable_encoding.cpp \
3132
wcwidth.c \
3233
# Empty last line

‎src/cprover/solver.cpp‎

Lines changed: 0 additions & 166 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ Author: Daniel Kroening, dkr@amazon.com
2222
#include "bv_pointers_wide.h"
2323
#include "console.h"
2424
#include "counterexample_found.h"
25-
#include "free_symbols.h"
2625
#include "propagate.h"
2726
#include "report_properties.h"
2827
#include "report_traces.h"
@@ -35,171 +34,6 @@ Author: Daniel Kroening, dkr@amazon.com
3534
#include <map>
3635
#include <set>
3736

38-
frame_mapt build_frame_map(const std::vector<framet> &frames)
39-
{
40-
frame_mapt frame_map;
41-
42-
for(std::size_t i = 0; i < frames.size(); i++)
43-
frame_map[frames[i].symbol] = frame_reft(i);
44-
45-
return frame_map;
46-
}
47-
48-
void framet::add_invariant(exprt invariant)
49-
{
50-
if(invariant.id() == ID_and)
51-
{
52-
for(const auto &conjunct : to_and_expr(invariant).operands())
53-
add_invariant(conjunct);
54-
}
55-
else
56-
invariants.push_back(std::move(invariant));
57-
}
58-
59-
void framet::add_auxiliary(exprt invariant)
60-
{
61-
if(invariant.id() == ID_and)
62-
{
63-
for(const auto &conjunct : to_and_expr(invariant).operands())
64-
add_auxiliary(conjunct);
65-
}
66-
else
67-
auxiliaries.push_back(std::move(invariant));
68-
}
69-
70-
std::vector<framet> setup_frames(const std::vector<exprt> &constraints)
71-
{
72-
std::set<symbol_exprt> states_set;
73-
std::vector<framet> frames;
74-
75-
for(auto &c : constraints)
76-
{
77-
auto &location = c.source_location();
78-
free_symbols(c, [&states_set, &location, &frames](const symbol_exprt &s) {
79-
auto insert_result = states_set.insert(s);
80-
if(insert_result.second)
81-
frames.emplace_back(s, location, frame_reft(frames.size()));
82-
});
83-
}
84-
85-
return frames;
86-
}
87-
88-
void find_implications(
89-
const std::vector<exprt> &constraints,
90-
std::vector<framet> &frames)
91-
{
92-
const auto frame_map = build_frame_map(frames);
93-
94-
for(const auto &c : constraints)
95-
{
96-
// look for ∀ ς : state . Sxx(ς) ⇒ Syy(...)
97-
// and ∀ ς : state . Sxx(ς) ⇒ ...
98-
if(c.id() == ID_forall && to_forall_expr(c).where().id() == ID_implies)
99-
{
100-
auto &implication = to_implies_expr(to_forall_expr(c).where());
101-
102-
if(
103-
implication.rhs().id() == ID_function_application &&
104-
to_function_application_expr(implication.rhs()).function().id() ==
105-
ID_symbol)
106-
{
107-
auto &rhs_symbol = to_symbol_expr(
108-
to_function_application_expr(implication.rhs()).function());
109-
auto s_it = frame_map.find(rhs_symbol);
110-
if(s_it != frame_map.end())
111-
{
112-
frames[s_it->second.index].implications.emplace_back(
113-
implication.lhs(), to_function_application_expr(implication.rhs()));
114-
}
115-
}
116-
}
117-
}
118-
}
119-
120-
frame_reft
121-
find_frame(const frame_mapt &frame_map, const symbol_exprt &frame_symbol)
122-
{
123-
auto entry = frame_map.find(frame_symbol);
124-
125-
if(entry == frame_map.end())
126-
PRECONDITION(false);
127-
128-
return entry->second;
129-
}
130-
131-
std::vector<propertyt> find_properties(
132-
const std::vector<exprt> &constraints,
133-
const std::vector<framet> &frames)
134-
{
135-
const auto frame_map = build_frame_map(frames);
136-
std::vector<propertyt> properties;
137-
138-
for(const auto &c : constraints)
139-
{
140-
// look for ∀ ς : state . Sxx(ς) ⇒ ...
141-
if(c.id() == ID_forall && to_forall_expr(c).where().id() == ID_implies)
142-
{
143-
auto &implication = to_implies_expr(to_forall_expr(c).where());
144-
145-
if(
146-
implication.rhs().id() != ID_function_application &&
147-
implication.lhs().id() == ID_function_application &&
148-
to_function_application_expr(implication.lhs()).function().id() ==
149-
ID_symbol)
150-
{
151-
auto &lhs_symbol = to_symbol_expr(
152-
to_function_application_expr(implication.lhs()).function());
153-
auto lhs_frame = find_frame(frame_map, lhs_symbol);
154-
properties.emplace_back(
155-
c.source_location(), lhs_frame, implication.rhs());
156-
}
157-
}
158-
}
159-
160-
return properties;
161-
}
162-
163-
exprt property_predicate(const implies_exprt &src)
164-
{
165-
// Sxx(ς) ⇒ p(ς)
166-
return src.rhs();
167-
}
168-
169-
void dump(
170-
const std::vector<framet> &frames,
171-
const propertyt &property,
172-
bool values,
173-
bool implications)
174-
{
175-
for(const auto &f : frames)
176-
{
177-
std::cout << "FRAME: " << format(f.symbol) << '\n';
178-
179-
if(implications)
180-
{
181-
for(auto &c : f.implications)
182-
{
183-
std::cout << " implication: ";
184-
std::cout << format(c.lhs) << " -> " << format(c.rhs);
185-
std::cout << '\n';
186-
}
187-
}
188-
189-
if(values)
190-
{
191-
for(auto &i : f.invariants)
192-
std::cout << " invariant: " << format(i) << '\n';
193-
194-
for(auto &i : f.auxiliaries)
195-
std::cout << " auxiliary: " << format(i) << '\n';
196-
}
197-
198-
if(property.frame == f.ref)
199-
std::cout << " property: " << format(property.condition) << '\n';
200-
}
201-
}
202-
20337
bool is_subsumed(
20438
const std::vector<exprt> &a1,
20539
const std::vector<exprt> &a2,

‎src/cprover/solver_types.cpp‎

Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
/*******************************************************************\
2+
3+
Module: Solver Types
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Solver Types
11+
12+
#include "solver_types.h"
13+
14+
#include <util/format_expr.h>
15+
16+
#include "free_symbols.h"
17+
18+
#include <iostream>
19+
#include <set>
20+
21+
void framet::add_invariant(exprt invariant)
22+
{
23+
if(invariant.id() == ID_and)
24+
{
25+
for(const auto &conjunct : to_and_expr(invariant).operands())
26+
add_invariant(conjunct);
27+
}
28+
else
29+
invariants.push_back(std::move(invariant));
30+
}
31+
32+
void framet::add_auxiliary(exprt invariant)
33+
{
34+
if(invariant.id() == ID_and)
35+
{
36+
for(const auto &conjunct : to_and_expr(invariant).operands())
37+
add_auxiliary(conjunct);
38+
}
39+
else
40+
auxiliaries.push_back(std::move(invariant));
41+
}
42+
43+
frame_mapt build_frame_map(const std::vector<framet> &frames)
44+
{
45+
frame_mapt frame_map;
46+
47+
for(std::size_t i = 0; i < frames.size(); i++)
48+
frame_map[frames[i].symbol] = frame_reft(i);
49+
50+
return frame_map;
51+
}
52+
53+
std::vector<framet> setup_frames(const std::vector<exprt> &constraints)
54+
{
55+
std::set<symbol_exprt> states_set;
56+
std::vector<framet> frames;
57+
58+
for(auto &c : constraints)
59+
{
60+
auto &location = c.source_location();
61+
free_symbols(c, [&states_set, &location, &frames](const symbol_exprt &s) {
62+
auto insert_result = states_set.insert(s);
63+
if(insert_result.second)
64+
frames.emplace_back(s, location, frame_reft(frames.size()));
65+
});
66+
}
67+
68+
return frames;
69+
}
70+
71+
void find_implications(
72+
const std::vector<exprt> &constraints,
73+
std::vector<framet> &frames)
74+
{
75+
const auto frame_map = build_frame_map(frames);
76+
77+
for(const auto &c : constraints)
78+
{
79+
// look for ∀ ς : state . Sxx(ς) ⇒ Syy(...)
80+
// and ∀ ς : state . Sxx(ς) ⇒ ...
81+
if(c.id() == ID_forall && to_forall_expr(c).where().id() == ID_implies)
82+
{
83+
auto &implication = to_implies_expr(to_forall_expr(c).where());
84+
85+
if(
86+
implication.rhs().id() == ID_function_application &&
87+
to_function_application_expr(implication.rhs()).function().id() ==
88+
ID_symbol)
89+
{
90+
auto &rhs_symbol = to_symbol_expr(
91+
to_function_application_expr(implication.rhs()).function());
92+
auto s_it = frame_map.find(rhs_symbol);
93+
if(s_it != frame_map.end())
94+
{
95+
frames[s_it->second.index].implications.emplace_back(
96+
implication.lhs(), to_function_application_expr(implication.rhs()));
97+
}
98+
}
99+
}
100+
}
101+
}
102+
103+
frame_reft
104+
find_frame(const frame_mapt &frame_map, const symbol_exprt &frame_symbol)
105+
{
106+
auto entry = frame_map.find(frame_symbol);
107+
108+
if(entry == frame_map.end())
109+
PRECONDITION(false);
110+
111+
return entry->second;
112+
}
113+
114+
std::vector<propertyt> find_properties(
115+
const std::vector<exprt> &constraints,
116+
const std::vector<framet> &frames)
117+
{
118+
const auto frame_map = build_frame_map(frames);
119+
std::vector<propertyt> properties;
120+
121+
for(const auto &c : constraints)
122+
{
123+
// look for ∀ ς : state . Sxx(ς) ⇒ ...
124+
if(c.id() == ID_forall && to_forall_expr(c).where().id() == ID_implies)
125+
{
126+
auto &implication = to_implies_expr(to_forall_expr(c).where());
127+
128+
if(
129+
implication.rhs().id() != ID_function_application &&
130+
implication.lhs().id() == ID_function_application &&
131+
to_function_application_expr(implication.lhs()).function().id() ==
132+
ID_symbol)
133+
{
134+
auto &lhs_symbol = to_symbol_expr(
135+
to_function_application_expr(implication.lhs()).function());
136+
auto lhs_frame = find_frame(frame_map, lhs_symbol);
137+
properties.emplace_back(
138+
c.source_location(), lhs_frame, implication.rhs());
139+
}
140+
}
141+
}
142+
143+
return properties;
144+
}
145+
146+
exprt property_predicate(const implies_exprt &src)
147+
{
148+
// Sxx(ς) ⇒ p(ς)
149+
return src.rhs();
150+
}
151+
152+
void dump(
153+
const std::vector<framet> &frames,
154+
const propertyt &property,
155+
bool values,
156+
bool implications)
157+
{
158+
for(const auto &f : frames)
159+
{
160+
std::cout << "FRAME: " << format(f.symbol) << '\n';
161+
162+
if(implications)
163+
{
164+
for(auto &c : f.implications)
165+
{
166+
std::cout << " implication: ";
167+
std::cout << format(c.lhs) << " -> " << format(c.rhs);
168+
std::cout << '\n';
169+
}
170+
}
171+
172+
if(values)
173+
{
174+
for(auto &i : f.invariants)
175+
std::cout << " invariant: " << format(i) << '\n';
176+
177+
for(auto &i : f.auxiliaries)
178+
std::cout << " auxiliary: " << format(i) << '\n';
179+
}
180+
181+
if(property.frame == f.ref)
182+
std::cout << " property: " << format(property.condition) << '\n';
183+
}
184+
}

0 commit comments

Comments
 (0)