Skip to content

Commit 8842667

Browse files
tautschnigtautschnig
authored
Merge pull request #4044 from tautschnig/propt-message-handler
Require a message handler when constructing a propt [blocks: #3800]
2 parents 23290f4 + 89641a2 commit 8842667

28 files changed

+112
-73
lines changed

‎jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Author: Jesse Sigal, [email protected]
66
77
\*******************************************************************/
88

9+
#include <testing-utils/message.h>
910
#include <testing-utils/use_catch.h>
1011

1112
#include <java_bytecode/java_bytecode_language.h>
@@ -154,7 +155,7 @@ std::string create_info(std::vector<exprt> &lemmas, const namespacet &ns)
154155
/// \return SAT solver result
155156
decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
156157
{
157-
satcheck_no_simplifiert sat_check;
158+
satcheck_no_simplifiert sat_check(null_message_handler);
158159
bv_refinementt::infot info;
159160
info.ns = &ns;
160161
info.prop = &sat_check;

‎src/goto-instrument/accelerate/scratch_program.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ class scratch_programt:public goto_programt
4545
path_storage(),
4646
options(get_default_options()),
4747
symex(mh, symbol_table, equation, options, path_storage),
48-
satcheck(util_make_unique<satcheckt>()),
48+
satcheck(util_make_unique<satcheckt>(mh)),
4949
satchecker(ns, *satcheck),
5050
z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
5151
checker(&z3) // checker(&satchecker)

‎src/solvers/flattening/bv_minimize.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,8 @@ class bv_minimizing_dect:public bv_pointerst
4848
return "Bit vector minimizing SAT";
4949
}
5050

51-
explicit bv_minimizing_dect(const namespacet &_ns):
52-
bv_pointerst(_ns, satcheck)
51+
bv_minimizing_dect(const namespacet &_ns, message_handlert &message_handler)
52+
: bv_pointerst(_ns, satcheck), satcheck(message_handler)
5353
{
5454
}
5555

‎src/solvers/prop/prop.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,9 @@ Author: Daniel Kroening, [email protected]
2424
class propt
2525
{
2626
public:
27-
propt() { }
27+
explicit propt(message_handlert &message_handler) : log(message_handler)
28+
{
29+
}
2830

2931
virtual ~propt() { }
3032

‎src/solvers/qbf/qbf_quantor.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/invariant.h>
1515

16-
qbf_quantort::qbf_quantort()
16+
qbf_quantort::qbf_quantort(message_handlert &message_handler)
17+
: qdimacs_cnft(message_handler)
1718
{
1819
}
1920

‎src/solvers/qbf/qbf_quantor.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
class qbf_quantort:public qdimacs_cnft
1616
{
1717
public:
18-
qbf_quantort();
18+
explicit qbf_quantort(message_handlert &message_handler);
1919
virtual ~qbf_quantort();
2020

2121
virtual const std::string solver_text();

‎src/solvers/qbf/qbf_qube.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ Author: CM Wintersteiger
1313

1414
#include <util/invariant.h>
1515

16-
qbf_qubet::qbf_qubet()
16+
qbf_qubet::qbf_qubet(message_handlert &message_handler)
17+
: qdimacs_cnft(message_handler)
1718
{
1819
// skizzo crashes on broken lines
1920
break_lines=false;

‎src/solvers/qbf/qbf_qube.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: CM Wintersteiger
1515
class qbf_qubet:public qdimacs_cnft
1616
{
1717
public:
18-
qbf_qubet();
18+
explicit qbf_qubet(message_handlert &message_handler);
1919
virtual ~qbf_qubet();
2020

2121
virtual const std::string solver_text();

‎src/solvers/qbf/qbf_qube_core.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,8 @@ Author: CM Wintersteiger
1515
#include <util/arith_tools.h>
1616
#include <util/invariant.h>
1717

18-
qbf_qube_coret::qbf_qube_coret() : qdimacs_coret()
18+
qbf_qube_coret::qbf_qube_coret(message_handlert &message_handler)
19+
: qdimacs_coret(message_handler)
1920
{
2021
break_lines=false;
2122
qbf_tmp_file="qube.qdimacs";

‎src/solvers/qbf/qbf_qube_core.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ class qbf_qube_coret:public qdimacs_coret
2323
assignmentt assignment;
2424

2525
public:
26-
qbf_qube_coret();
26+
explicit qbf_qube_coret(message_handlert &message_handler);
2727
virtual ~qbf_qube_coret();
2828

2929
virtual const std::string solver_text();

‎src/solvers/qbf/qbf_skizzo.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/invariant.h>
1515

16-
qbf_skizzot::qbf_skizzot()
16+
qbf_skizzot::qbf_skizzot(message_handlert &message_handler)
17+
: qdimacs_cnft(message_handler)
1718
{
1819
// skizzo crashes on broken lines
1920
break_lines=false;

‎src/solvers/qbf/qbf_skizzo.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
class qbf_skizzot:public qdimacs_cnft
1616
{
1717
public:
18-
qbf_skizzot();
18+
explicit qbf_skizzot(message_handlert &message_handler);
1919
virtual ~qbf_skizzot();
2020

2121
virtual const std::string solver_text();

‎src/solvers/qbf/qdimacs_cnf.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,10 @@ Author: Daniel Kroening, [email protected]
1818
class qdimacs_cnft:public dimacs_cnft
1919
{
2020
public:
21-
qdimacs_cnft() { }
21+
explicit qdimacs_cnft(message_handlert &message_handler)
22+
: dimacs_cnft(message_handler)
23+
{
24+
}
2225
virtual ~qdimacs_cnft() { }
2326

2427
virtual void write_qdimacs_cnf(std::ostream &out);

‎src/solvers/qbf/qdimacs_core.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,11 @@ Author: CM Wintersteiger
1919
class qdimacs_coret:public qdimacs_cnft
2020
{
2121
public:
22+
explicit qdimacs_coret(message_handlert &message_handler)
23+
: qdimacs_cnft(message_handler)
24+
{
25+
}
26+
2227
virtual tvt l_get(literalt a) const=0;
2328
virtual bool is_in_core(literalt l) const=0;
2429

‎src/solvers/refinement/refine_arrays.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ void bv_refinementt::arrays_overapproximated()
4343
std::list<lazy_constraintt>::iterator it=lazy_array_constraints.begin();
4444
while(it!=lazy_array_constraints.end())
4545
{
46-
satcheck_no_simplifiert sat_check;
46+
satcheck_no_simplifiert sat_check(get_message_handler());
4747
bv_pointerst solver(ns, sat_check);
4848
solver.unbounded_array=bv_pointerst::unbounded_arrayt::U_ALL;
4949

‎src/solvers/sat/cnf.h

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,10 @@ class cnft:public propt
1919
public:
2020
// For CNF, we don't use index 0 as a matter of principle,
2121
// so we'll start counting variables at 1.
22-
cnft():_no_variables(1) { }
22+
explicit cnft(message_handlert &message_handler)
23+
: propt(message_handler), _no_variables(1)
24+
{
25+
}
2326
virtual ~cnft() { }
2427

2528
virtual literalt land(literalt a, literalt b) override;
@@ -66,7 +69,8 @@ class cnft:public propt
6669
class cnf_solvert:public cnft
6770
{
6871
public:
69-
cnf_solvert():status(statust::INIT), clause_counter(0)
72+
explicit cnf_solvert(message_handlert &message_handler)
73+
: cnft(message_handler), status(statust::INIT), clause_counter(0)
7074
{
7175
}
7276

‎src/solvers/sat/cnf_clause_list.h

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,10 @@ Author: Daniel Kroening, [email protected]
2323
class cnf_clause_listt:public cnft
2424
{
2525
public:
26-
cnf_clause_listt() { }
26+
explicit cnf_clause_listt(message_handlert &message_handler)
27+
: cnft(message_handler)
28+
{
29+
}
2730
virtual ~cnf_clause_listt() { }
2831

2932
virtual void lcnf(const bvt &bv);
@@ -82,6 +85,11 @@ class cnf_clause_listt:public cnft
8285
class cnf_clause_list_assignmentt:public cnf_clause_listt
8386
{
8487
public:
88+
explicit cnf_clause_list_assignmentt(message_handlert &message_handler)
89+
: cnf_clause_listt(message_handler)
90+
{
91+
}
92+
8593
typedef std::vector<tvt> assignmentt;
8694

8795
assignmentt &get_assignment()

‎src/solvers/sat/dimacs_cnf.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,15 +15,11 @@ Author: Daniel Kroening, [email protected]
1515
#include <iostream>
1616
#include <sstream>
1717

18-
dimacs_cnft::dimacs_cnft():break_lines(false)
18+
dimacs_cnft::dimacs_cnft(message_handlert &message_handler)
19+
: cnf_clause_listt(message_handler), break_lines(false)
1920
{
2021
}
2122

22-
dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
23-
{
24-
log.set_message_handler(message_handler);
25-
}
26-
2723
void dimacs_cnft::set_assignment(literalt, bool)
2824
{
2925
UNIMPLEMENTED;
@@ -35,7 +31,10 @@ bool dimacs_cnft::is_in_conflict(literalt) const
3531
return false;
3632
}
3733

38-
dimacs_cnf_dumpt::dimacs_cnf_dumpt(std::ostream &_out):out(_out)
34+
dimacs_cnf_dumpt::dimacs_cnf_dumpt(
35+
std::ostream &_out,
36+
message_handlert &message_handler)
37+
: cnft(message_handler), out(_out)
3938
{
4039
}
4140

‎src/solvers/sat/dimacs_cnf.h

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
1717
class dimacs_cnft:public cnf_clause_listt
1818
{
1919
public:
20-
dimacs_cnft();
2120
explicit dimacs_cnft(message_handlert &);
2221
virtual ~dimacs_cnft() { }
2322

@@ -43,7 +42,7 @@ class dimacs_cnft:public cnf_clause_listt
4342
class dimacs_cnf_dumpt:public cnft
4443
{
4544
public:
46-
explicit dimacs_cnf_dumpt(std::ostream &_out);
45+
dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
4746
virtual ~dimacs_cnf_dumpt() { }
4847

4948
virtual const std::string solver_text()

‎src/solvers/sat/pbs_dimacs_cnf.h

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,13 @@ Author: Alex Groce
1919
class pbs_dimacs_cnft:public dimacs_cnft
2020
{
2121
public:
22-
pbs_dimacs_cnft():
23-
optimize(false),
24-
maximize(false),
25-
binary_search(false),
26-
goal(0),
27-
opt_sum(0)
22+
explicit pbs_dimacs_cnft(message_handlert &message_handler)
23+
: dimacs_cnft(message_handler),
24+
optimize(false),
25+
maximize(false),
26+
binary_search(false),
27+
goal(0),
28+
opt_sum(0)
2829
{
2930
}
3031

‎src/solvers/sat/satcheck_glucose.cpp

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -215,9 +215,11 @@ void satcheck_glucose_baset<T>::set_assignment(literalt a, bool value)
215215
}
216216
}
217217

218-
template<typename T>
219-
satcheck_glucose_baset<T>::satcheck_glucose_baset(T *_solver):
220-
solver(_solver)
218+
template <typename T>
219+
satcheck_glucose_baset<T>::satcheck_glucose_baset(
220+
T *_solver,
221+
message_handlert &message_handler)
222+
: cnf_solvert(message_handler), solver(_solver)
221223
{
222224
}
223225

@@ -254,13 +256,19 @@ void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
254256
INVARIANT(!it->is_constant(), "assumption literals must not be constant");
255257
}
256258

257-
satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert():
258-
satcheck_glucose_baset<Glucose::Solver>(new Glucose::Solver)
259+
satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(
260+
message_handlert &message_handler)
261+
: satcheck_glucose_baset<Glucose::Solver>(
262+
new Glucose::Solver,
263+
message_handler)
259264
{
260265
}
261266

262-
satcheck_glucose_simplifiert::satcheck_glucose_simplifiert():
263-
satcheck_glucose_baset<Glucose::SimpSolver>(new Glucose::SimpSolver)
267+
satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(
268+
message_handlert &message_handler)
269+
: satcheck_glucose_baset<Glucose::SimpSolver>(
270+
new Glucose::SimpSolver,
271+
message_handler)
264272
{
265273
}
266274

‎src/solvers/sat/satcheck_glucose.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ template<typename T>
2727
class satcheck_glucose_baset:public cnf_solvert
2828
{
2929
public:
30-
explicit satcheck_glucose_baset(T *);
30+
satcheck_glucose_baset(T *, message_handlert &message_handler);
3131
virtual ~satcheck_glucose_baset();
3232

3333
virtual resultt prop_solve();
@@ -57,15 +57,15 @@ class satcheck_glucose_no_simplifiert:
5757
public satcheck_glucose_baset<Glucose::Solver>
5858
{
5959
public:
60-
satcheck_glucose_no_simplifiert();
60+
explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
6161
virtual const std::string solver_text();
6262
};
6363

6464
class satcheck_glucose_simplifiert:
6565
public satcheck_glucose_baset<Glucose::SimpSolver>
6666
{
6767
public:
68-
satcheck_glucose_simplifiert();
68+
explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
6969
virtual const std::string solver_text();
7070
virtual void set_frozen(literalt a);
7171
bool is_eliminated(literalt a) const;

‎src/solvers/sat/satcheck_minisat2.cpp

Lines changed: 11 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -293,9 +293,11 @@ void satcheck_minisat2_baset<T>::set_assignment(literalt a, bool value)
293293
}
294294
}
295295

296-
template<typename T>
297-
satcheck_minisat2_baset<T>::satcheck_minisat2_baset(T *_solver):
298-
solver(_solver), time_limit_seconds(0)
296+
template <typename T>
297+
satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
298+
T *_solver,
299+
message_handlert &message_handler)
300+
: cnf_solvert(message_handler), solver(_solver), time_limit_seconds(0)
299301
{
300302
}
301303

@@ -336,28 +338,20 @@ void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
336338
}
337339
}
338340

339-
satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert():
340-
satcheck_minisat2_baset<Minisat::Solver>(new Minisat::Solver)
341-
{
342-
}
343-
344341
satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(
345342
message_handlert &message_handler)
346-
: satcheck_minisat_no_simplifiert()
347-
{
348-
log.set_message_handler(message_handler);
349-
}
350-
351-
satcheck_minisat_simplifiert::satcheck_minisat_simplifiert():
352-
satcheck_minisat2_baset<Minisat::SimpSolver>(new Minisat::SimpSolver)
343+
: satcheck_minisat2_baset<Minisat::Solver>(
344+
new Minisat::Solver,
345+
message_handler)
353346
{
354347
}
355348

356349
satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(
357350
message_handlert &message_handler)
358-
: satcheck_minisat_simplifiert()
351+
: satcheck_minisat2_baset<Minisat::SimpSolver>(
352+
new Minisat::SimpSolver,
353+
message_handler)
359354
{
360-
log.set_message_handler(message_handler);
361355
}
362356

363357
void satcheck_minisat_simplifiert::set_frozen(literalt a)

0 commit comments

Comments
 (0)