Skip to content

Commit 5af9fed

Browse files
peterschrammelpeterschrammel
committed
Clang-format
1 parent 3266c51 commit 5af9fed

File tree

2 files changed

+52
-54
lines changed

2 files changed

+52
-54
lines changed

‎src/goto-checker/solver_factory.cpp

Lines changed: 42 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -35,34 +35,35 @@ smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const
3535
// we shouldn't get here if this option isn't set
3636
PRECONDITION(options.get_bool_option("smt2"));
3737

38-
smt2_dect::solvert s=smt2_dect::solvert::GENERIC;
38+
smt2_dect::solvert s = smt2_dect::solvert::GENERIC;
3939

4040
if(options.get_bool_option("boolector"))
41-
s=smt2_dect::solvert::BOOLECTOR;
41+
s = smt2_dect::solvert::BOOLECTOR;
4242
else if(options.get_bool_option("cprover-smt2"))
4343
s = smt2_dect::solvert::CPROVER_SMT2;
4444
else if(options.get_bool_option("mathsat"))
45-
s=smt2_dect::solvert::MATHSAT;
45+
s = smt2_dect::solvert::MATHSAT;
4646
else if(options.get_bool_option("cvc3"))
47-
s=smt2_dect::solvert::CVC3;
47+
s = smt2_dect::solvert::CVC3;
4848
else if(options.get_bool_option("cvc4"))
49-
s=smt2_dect::solvert::CVC4;
49+
s = smt2_dect::solvert::CVC4;
5050
else if(options.get_bool_option("yices"))
51-
s=smt2_dect::solvert::YICES;
51+
s = smt2_dect::solvert::YICES;
5252
else if(options.get_bool_option("z3"))
53-
s=smt2_dect::solvert::Z3;
53+
s = smt2_dect::solvert::Z3;
5454
else if(options.get_bool_option("generic"))
55-
s=smt2_dect::solvert::GENERIC;
55+
s = smt2_dect::solvert::GENERIC;
5656

5757
return s;
5858
}
5959

6060
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
6161
{
62-
auto solver=util_make_unique<solvert>();
62+
auto solver = util_make_unique<solvert>();
6363

64-
if(options.get_bool_option("beautify") ||
65-
!options.get_bool_option("sat-preprocessor")) // no simplifier
64+
if(
65+
options.get_bool_option("beautify") ||
66+
!options.get_bool_option("sat-preprocessor")) // no simplifier
6667
{
6768
// simplifier won't work with beautification
6869
solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
@@ -76,9 +77,9 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
7677

7778
auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
7879

79-
if(options.get_option("arrays-uf")=="never")
80+
if(options.get_option("arrays-uf") == "never")
8081
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
81-
else if(options.get_option("arrays-uf")=="always")
82+
else if(options.get_option("arrays-uf") == "always")
8283
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
8384

8485
solver->set_prop_conv(std::move(bv_pointers));
@@ -91,19 +92,18 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
9192
no_beautification();
9293
no_incremental_check();
9394

94-
auto prop=util_make_unique<dimacs_cnft>();
95+
auto prop = util_make_unique<dimacs_cnft>();
9596
prop->set_message_handler(message_handler);
9697

97-
std::string filename=options.get_option("outfile");
98+
std::string filename = options.get_option("outfile");
9899

99100
auto bv_dimacs = util_make_unique<bv_dimacst>(ns, *prop, filename);
100101
return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
101102
}
102103

103104
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
104105
{
105-
std::unique_ptr<propt> prop=[this]() -> std::unique_ptr<propt>
106-
{
106+
std::unique_ptr<propt> prop = [this]() -> std::unique_ptr<propt> {
107107
// We offer the option to disable the SAT preprocessor
108108
if(options.get_bool_option("sat-preprocessor"))
109109
{
@@ -116,21 +116,20 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
116116
prop->set_message_handler(message_handler);
117117

118118
bv_refinementt::infot info;
119-
info.ns=&ns;
120-
info.prop=prop.get();
119+
info.ns = &ns;
120+
info.prop = prop.get();
121121
info.output_xml = output_xml_in_refinement;
122122

123123
// we allow setting some parameters
124124
if(options.get_bool_option("max-node-refinement"))
125-
info.max_node_refinement=
125+
info.max_node_refinement =
126126
options.get_unsigned_int_option("max-node-refinement");
127127

128-
info.refine_arrays=options.get_bool_option("refine-arrays");
129-
info.refine_arithmetic=options.get_bool_option("refine-arithmetic");
128+
info.refine_arrays = options.get_bool_option("refine-arrays");
129+
info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
130130

131131
return util_make_unique<solvert>(
132-
util_make_unique<bv_refinementt>(info),
133-
std::move(prop));
132+
util_make_unique<bv_refinementt>(info), std::move(prop));
134133
}
135134

136135
/// the string refinement adds to the bit vector refinement specifications for
@@ -140,17 +139,17 @@ std::unique_ptr<solver_factoryt::solvert>
140139
solver_factoryt::get_string_refinement()
141140
{
142141
string_refinementt::infot info;
143-
info.ns=&ns;
144-
auto prop=util_make_unique<satcheck_no_simplifiert>();
142+
info.ns = &ns;
143+
auto prop = util_make_unique<satcheck_no_simplifiert>();
145144
prop->set_message_handler(message_handler);
146-
info.prop=prop.get();
147-
info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
145+
info.prop = prop.get();
146+
info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
148147
info.output_xml = output_xml_in_refinement;
149148
if(options.get_bool_option("max-node-refinement"))
150-
info.max_node_refinement=
149+
info.max_node_refinement =
151150
options.get_unsigned_int_option("max-node-refinement");
152-
info.refine_arrays=options.get_bool_option("refine-arrays");
153-
info.refine_arithmetic=options.get_bool_option("refine-arithmetic");
151+
info.refine_arrays = options.get_bool_option("refine-arrays");
152+
info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
154153

155154
return util_make_unique<solvert>(
156155
util_make_unique<string_refinementt>(info), std::move(prop));
@@ -161,11 +160,11 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
161160
{
162161
no_beautification();
163162

164-
const std::string &filename=options.get_option("outfile");
163+
const std::string &filename = options.get_option("outfile");
165164

166-
if(filename=="")
165+
if(filename == "")
167166
{
168-
if(solver==smt2_dect::solvert::GENERIC)
167+
if(solver == smt2_dect::solvert::GENERIC)
169168
{
170169
throw invalid_command_line_argument_exceptiont(
171170
"required filename not provided",
@@ -181,11 +180,11 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
181180
solver);
182181

183182
if(options.get_bool_option("fpa"))
184-
smt2_dec->use_FPA_theory=true;
183+
smt2_dec->use_FPA_theory = true;
185184

186185
return util_make_unique<solvert>(std::move(smt2_dec));
187186
}
188-
else if(filename=="-")
187+
else if(filename == "-")
189188
{
190189
auto smt2_conv = util_make_unique<smt2_convt>(
191190
ns,
@@ -196,19 +195,19 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
196195
std::cout);
197196

198197
if(options.get_bool_option("fpa"))
199-
smt2_conv->use_FPA_theory=true;
198+
smt2_conv->use_FPA_theory = true;
200199

201200
smt2_conv->set_message_handler(message_handler);
202201

203202
return util_make_unique<solvert>(std::move(smt2_conv));
204203
}
205204
else
206205
{
207-
#ifdef _MSC_VER
208-
auto out=util_make_unique<std::ofstream>(widen(filename));
209-
#else
210-
auto out=util_make_unique<std::ofstream>(filename);
211-
#endif
206+
#ifdef _MSC_VER
207+
auto out = util_make_unique<std::ofstream>(widen(filename));
208+
#else
209+
auto out = util_make_unique<std::ofstream>(filename);
210+
#endif
212211

213212
if(!*out)
214213
{
@@ -225,7 +224,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
225224
*out);
226225

227226
if(options.get_bool_option("fpa"))
228-
smt2_conv->use_FPA_theory=true;
227+
smt2_conv->use_FPA_theory = true;
229228

230229
smt2_conv->set_message_handler(message_handler);
231230

‎src/goto-checker/solver_factory.h

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,12 @@ Author: Daniel Kroening, Peter Schrammel
1818

1919
#include <util/options.h>
2020

21+
#include <goto-symex/symex_target_equation.h>
2122
#include <solvers/prop/prop.h>
2223
#include <solvers/prop/prop_conv.h>
2324
#include <solvers/sat/cnf.h>
2425
#include <solvers/sat/satcheck.h>
2526
#include <solvers/smt2/smt2_dec.h>
26-
#include <goto-symex/symex_target_equation.h>
2727

2828
class solver_factoryt
2929
{
@@ -50,19 +50,18 @@ class solver_factoryt
5050
{
5151
}
5252

53-
explicit solvert(std::unique_ptr<prop_convt> p):prop_conv_ptr(std::move(p))
53+
explicit solvert(std::unique_ptr<prop_convt> p)
54+
: prop_conv_ptr(std::move(p))
5455
{
5556
}
5657

57-
solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2):
58-
prop_ptr(std::move(p2)),
59-
prop_conv_ptr(std::move(p1))
58+
solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<propt> p2)
59+
: prop_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
6060
{
6161
}
6262

63-
solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2):
64-
ofstream_ptr(std::move(p2)),
65-
prop_conv_ptr(std::move(p1))
63+
solvert(std::unique_ptr<prop_convt> p1, std::unique_ptr<std::ofstream> p2)
64+
: ofstream_ptr(std::move(p2)), prop_conv_ptr(std::move(p1))
6665
{
6766
}
6867

@@ -80,17 +79,17 @@ class solver_factoryt
8079

8180
void set_prop_conv(std::unique_ptr<prop_convt> p)
8281
{
83-
prop_conv_ptr=std::move(p);
82+
prop_conv_ptr = std::move(p);
8483
}
8584

8685
void set_prop(std::unique_ptr<propt> p)
8786
{
88-
prop_ptr=std::move(p);
87+
prop_ptr = std::move(p);
8988
}
9089

9190
void set_ofstream(std::unique_ptr<std::ofstream> p)
9291
{
93-
ofstream_ptr=std::move(p);
92+
ofstream_ptr = std::move(p);
9493
}
9594

9695
// the objects are deleted in the opposite order they appear below

0 commit comments

Comments
 (0)