Skip to content

Commit aed4d77

Browse files
kroeningkroening
authored
Merge pull request #7976 from diffblue/propt-interface
propt: change interface for solving under assumptions
2 parents 0ec6a1e + 9508799 commit aed4d77

33 files changed

+118
-197
lines changed

‎src/solvers/prop/prop.cpp

+8-1
Original file line numberDiff line numberDiff line change
@@ -38,8 +38,15 @@ bvt propt::new_variables(std::size_t width)
3838

3939
propt::resultt propt::prop_solve()
4040
{
41+
static const bvt empty_assumptions;
4142
++number_of_solver_calls;
42-
return do_prop_solve();
43+
return do_prop_solve(empty_assumptions);
44+
}
45+
46+
propt::resultt propt::prop_solve(const bvt &assumptions)
47+
{
48+
++number_of_solver_calls;
49+
return do_prop_solve(assumptions);
4350
}
4451

4552
std::size_t propt::get_number_of_solver_calls() const

‎src/solvers/prop/prop.h

+8-4
Original file line numberDiff line numberDiff line change
@@ -84,9 +84,11 @@ class propt
8484
// They overload this to return false and thus avoid some optimisations
8585
virtual bool cnf_handled_well() const { return true; }
8686

87-
// assumptions
88-
virtual void set_assumptions(const bvt &) { }
89-
virtual bool has_set_assumptions() const { return false; }
87+
// solving with assumptions
88+
virtual bool has_assumptions() const
89+
{
90+
return false;
91+
}
9092

9193
// variables
9294
virtual literalt new_variable()=0;
@@ -98,6 +100,7 @@ class propt
98100
virtual std::string solver_text() const = 0;
99101
enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
100102
resultt prop_solve();
103+
resultt prop_solve(const bvt &assumptions);
101104

102105
// satisfying assignment
103106
virtual tvt l_get(literalt a) const=0;
@@ -122,7 +125,8 @@ class propt
122125
std::size_t get_number_of_solver_calls() const;
123126

124127
protected:
125-
virtual resultt do_prop_solve() = 0;
128+
// solve under the given assumption
129+
virtual resultt do_prop_solve(const bvt &assumptions) = 0;
126130

127131
// to avoid a temporary for lcnf(...)
128132
bvt lcnf_bv;

‎src/solvers/prop/prop_conv_solver.cpp

+1-7
Original file line numberDiff line numberDiff line change
@@ -459,7 +459,7 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
459459

460460
log.statistics() << "Solving with " << prop.solver_text() << messaget::eom;
461461

462-
switch(prop.prop_solve())
462+
switch(prop.prop_solve(assumption_stack))
463463
{
464464
case propt::resultt::P_SATISFIABLE:
465465
return resultt::D_SATISFIABLE;
@@ -531,8 +531,6 @@ void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
531531
for(const auto &assumption : assumptions)
532532
assumption_stack.push_back(to_literal_expr(assumption).get_literal());
533533
context_size_stack.push_back(assumptions.size());
534-
535-
prop.set_assumptions(assumption_stack);
536534
}
537535

538536
void prop_conv_solvert::push()
@@ -543,17 +541,13 @@ void prop_conv_solvert::push()
543541

544542
assumption_stack.push_back(context_literal);
545543
context_size_stack.push_back(1);
546-
547-
prop.set_assumptions(assumption_stack);
548544
}
549545

550546
void prop_conv_solvert::pop()
551547
{
552548
// We remove the context from the stack.
553549
assumption_stack.resize(assumption_stack.size() - context_size_stack.back());
554550
context_size_stack.pop_back();
555-
556-
prop.set_assumptions(assumption_stack);
557551
}
558552

559553
// This method out-of-line because gcc-5.5.0-12ubuntu1 20171010 miscompiles it

‎src/solvers/refinement/bv_refinement_loop.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ bv_refinementt::bv_refinementt(const infot &info)
1616
config_(info)
1717
{
1818
// check features we need
19-
PRECONDITION(prop.has_set_assumptions());
19+
PRECONDITION(prop.has_assumptions());
2020
PRECONDITION(prop.has_set_to());
2121
PRECONDITION(prop.has_is_in_conflict());
2222
}
@@ -102,7 +102,7 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
102102
}
103103

104104
push(assumptions);
105-
propt::resultt result=prop.prop_solve();
105+
propt::resultt result = prop.prop_solve(assumption_stack);
106106
pop();
107107

108108
// clang-format off

‎src/solvers/sat/cnf_clause_list.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ class cnf_clause_listt:public cnft
7777
}
7878

7979
protected:
80-
resultt do_prop_solve() override
80+
resultt do_prop_solve(const bvt &) override
8181
{
8282
return resultt::P_ERROR;
8383
}

‎src/solvers/sat/dimacs_cnf.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ class dimacs_cnf_dumpt:public cnft
6666
}
6767

6868
protected:
69-
resultt do_prop_solve() override
69+
resultt do_prop_solve(const bvt &) override
7070
{
7171
return resultt::P_ERROR;
7272
}

‎src/solvers/sat/external_sat.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ void external_satt::set_assignment(literalt, bool)
3636
UNIMPLEMENTED;
3737
}
3838

39-
void external_satt::write_cnf_file(std::string cnf_file)
39+
void external_satt::write_cnf_file(std::string cnf_file, const bvt &assumptions)
4040
{
4141
log.status() << "Writing temporary CNF" << messaget::eom;
4242
std::ofstream out(cnf_file);
@@ -167,7 +167,7 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
167167
return resultt::P_ERROR;
168168
}
169169

170-
external_satt::resultt external_satt::do_prop_solve()
170+
external_satt::resultt external_satt::do_prop_solve(const bvt &assumptions)
171171
{
172172
// are we assuming 'false'?
173173
if(
@@ -179,7 +179,7 @@ external_satt::resultt external_satt::do_prop_solve()
179179

180180
// create a temporary file
181181
temporary_filet cnf_file("external-sat", ".cnf");
182-
write_cnf_file(cnf_file());
182+
write_cnf_file(cnf_file(), assumptions);
183183
auto output = execute_solver(cnf_file());
184184
return parse_result(output);
185185
}

‎src/solvers/sat/external_sat.h

+3-9
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ class external_satt : public cnf_clause_list_assignmentt
1212
public:
1313
explicit external_satt(message_handlert &message_handler, std::string cmd);
1414

15-
bool has_set_assumptions() const override final
15+
bool has_assumptions() const override final
1616
{
1717
return true;
1818
}
@@ -27,17 +27,11 @@ class external_satt : public cnf_clause_list_assignmentt
2727
bool is_in_conflict(literalt) const override;
2828
void set_assignment(literalt, bool) override;
2929

30-
void set_assumptions(const bvt &_assumptions) override
31-
{
32-
assumptions = _assumptions;
33-
}
34-
3530
protected:
3631
std::string solver_cmd;
37-
bvt assumptions;
3832

39-
resultt do_prop_solve() override;
40-
void write_cnf_file(std::string);
33+
resultt do_prop_solve(const bvt &assumptions) override;
34+
void write_cnf_file(std::string, const bvt &);
4135
std::string execute_solver(std::string);
4236
resultt parse_result(std::string);
4337
};

‎src/solvers/sat/pbs_dimacs_cnf.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -205,8 +205,10 @@ bool pbs_dimacs_cnft::pbs_solve()
205205
return satisfied;
206206
}
207207

208-
propt::resultt pbs_dimacs_cnft::do_prop_solve()
208+
propt::resultt pbs_dimacs_cnft::do_prop_solve(const bvt &assumptions)
209209
{
210+
PRECONDITION(assumptions.empty());
211+
210212
std::ofstream file("temp.cnf");
211213

212214
write_dimacs_cnf(file);

‎src/solvers/sat/pbs_dimacs_cnf.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ class pbs_dimacs_cnft:public dimacs_cnft
5858
}
5959

6060
protected:
61-
resultt do_prop_solve() override;
61+
resultt do_prop_solve(const bvt &assumptions) override;
6262

6363
std::set<int> assigned;
6464
};

‎src/solvers/sat/satcheck_booleforce.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -79,8 +79,9 @@ void satcheck_booleforce_baset::lcnf(const bvt &bv)
7979
clause_counter++;
8080
}
8181

82-
propt::resultt satcheck_booleforce_baset::do_prop_solve()
82+
propt::resultt satcheck_booleforce_baset::do_prop_solve(const bvt &assumptions)
8383
{
84+
PRECONDITION(assumptions.empty());
8485
PRECONDITION(status == SAT || status == INIT);
8586

8687
int result=booleforce_sat();

‎src/solvers/sat/satcheck_booleforce.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ class satcheck_booleforce_baset:public cnf_solvert
2626
void lcnf(const bvt &bv) override;
2727

2828
protected:
29-
resultt do_prop_solve() override;
29+
resultt do_prop_solve(const bvt &assumptions) override;
3030
};
3131

3232
class satcheck_booleforcet:public satcheck_booleforce_baset

‎src/solvers/sat/satcheck_cadical.cpp

+3-15
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
8585
clause_counter++;
8686
}
8787

88-
propt::resultt satcheck_cadicalt::do_prop_solve()
88+
propt::resultt satcheck_cadicalt::do_prop_solve(const bvt &assumptions)
8989
{
9090
INVARIANT(status != statust::ERROR, "there cannot be an error");
9191

@@ -105,7 +105,8 @@ propt::resultt satcheck_cadicalt::do_prop_solve()
105105
}
106106

107107
for(const auto &a : assumptions)
108-
solver->assume(a.dimacs());
108+
if(!a.is_true())
109+
solver->assume(a.dimacs());
109110

110111
switch(solver->solve())
111112
{
@@ -144,19 +145,6 @@ satcheck_cadicalt::~satcheck_cadicalt()
144145
delete solver;
145146
}
146147

147-
void satcheck_cadicalt::set_assumptions(const bvt &bv)
148-
{
149-
// We filter out 'true' assumptions which cause spurious results with CaDiCaL.
150-
assumptions.clear();
151-
for(const auto &assumption : bv)
152-
{
153-
if(!assumption.is_true())
154-
{
155-
assumptions.push_back(assumption);
156-
}
157-
}
158-
}
159-
160148
bool satcheck_cadicalt::is_in_conflict(literalt a) const
161149
{
162150
return solver->failed(a.dimacs());

‎src/solvers/sat/satcheck_cadical.h

+3-6
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,7 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
3131
void lcnf(const bvt &bv) override;
3232
void set_assignment(literalt a, bool value) override;
3333

34-
void set_assumptions(const bvt &_assumptions) override;
35-
bool has_set_assumptions() const override
34+
bool has_assumptions() const override
3635
{
3736
return true;
3837
}
@@ -43,12 +42,10 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
4342
bool is_in_conflict(literalt a) const override;
4443

4544
protected:
46-
resultt do_prop_solve() override;
45+
resultt do_prop_solve(const bvt &assumptions) override;
4746

4847
// NOLINTNEXTLINE(readability/identifiers)
49-
CaDiCaL::Solver * solver;
50-
51-
bvt assumptions;
48+
CaDiCaL::Solver *solver;
5249
};
5350

5451
#endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H

‎src/solvers/sat/satcheck_glucose.cpp

+13-14
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,17 @@ void convert(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
3232
}
3333
}
3434

35+
void convert_assumptions(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
36+
{
37+
dest.capacity(bv.size());
38+
39+
for(const auto &literal : bv)
40+
{
41+
if(!literal.is_true())
42+
dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
43+
}
44+
}
45+
3546
template<typename T>
3647
tvt satcheck_glucose_baset<T>::l_get(literalt a) const
3748
{
@@ -153,7 +164,7 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
153164
}
154165

155166
template <typename T>
156-
propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
167+
propt::resultt satcheck_glucose_baset<T>::do_prop_solve(const bvt &assumptions)
157168
{
158169
PRECONDITION(status != statust::ERROR);
159170

@@ -189,7 +200,7 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
189200
else
190201
{
191202
Glucose::vec<Glucose::Lit> solver_assumptions;
192-
convert(assumptions, solver_assumptions);
203+
convert_assumptions(assumptions, solver_assumptions);
193204

194205
if(solver->solve(solver_assumptions))
195206
{
@@ -262,18 +273,6 @@ bool satcheck_glucose_baset<T>::is_in_conflict(literalt a) const
262273
return false;
263274
}
264275

265-
template<typename T>
266-
void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
267-
{
268-
assumptions=bv;
269-
270-
for(const auto &literal : assumptions)
271-
{
272-
INVARIANT(
273-
!literal.is_constant(), "assumption literals must not be constant");
274-
}
275-
}
276-
277276
template class satcheck_glucose_baset<Glucose::Solver>;
278277
template class satcheck_glucose_baset<Glucose::SimpSolver>;
279278

‎src/solvers/sat/satcheck_glucose.h

+2-6
Original file line numberDiff line numberDiff line change
@@ -41,14 +41,11 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
4141
void lcnf(const bvt &bv) override;
4242
void set_assignment(literalt a, bool value) override;
4343

44-
// extra MiniSat feature: solve with assumptions
45-
void set_assumptions(const bvt &_assumptions) override;
46-
4744
// extra MiniSat feature: default branching decision
4845
void set_polarity(literalt a, bool value);
4946

5047
bool is_in_conflict(literalt a) const override;
51-
bool has_set_assumptions() const override
48+
bool has_assumptions() const override
5249
{
5350
return true;
5451
}
@@ -58,12 +55,11 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
5855
}
5956

6057
protected:
61-
resultt do_prop_solve() override;
58+
resultt do_prop_solve(const bvt &assumptions) override;
6259

6360
std::unique_ptr<T> solver;
6461

6562
void add_variables();
66-
bvt assumptions;
6763
};
6864

6965
class satcheck_glucose_no_simplifiert:

0 commit comments

Comments
 (0)