1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, Mathias Preiner, Alex Ozdemir |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* SAT Solver. |
14 |
|
* |
15 |
|
* Implementation of the cryptominisat for cvc5 (bit-vectors). |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "prop/cryptominisat.h" |
19 |
|
|
20 |
|
#ifdef CVC5_USE_CRYPTOMINISAT |
21 |
|
|
22 |
|
#include "base/check.h" |
23 |
|
#include "util/statistics_registry.h" |
24 |
|
|
25 |
|
#include <cryptominisat5/cryptominisat.h> |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace prop { |
29 |
|
|
30 |
|
using CMSatVar = unsigned; |
31 |
|
|
32 |
|
// helper functions |
33 |
|
namespace { |
34 |
|
|
35 |
9950 |
CMSat::Lit toInternalLit(SatLiteral lit) |
36 |
|
{ |
37 |
9950 |
if (lit == undefSatLiteral) |
38 |
|
{ |
39 |
|
return CMSat::lit_Undef; |
40 |
|
} |
41 |
9950 |
return CMSat::Lit(lit.getSatVariable(), lit.isNegated()); |
42 |
|
} |
43 |
|
|
44 |
30 |
SatLiteral toSatLiteral(CMSat::Lit lit) |
45 |
|
{ |
46 |
30 |
if (lit == CMSat::lit_Undef) |
47 |
|
{ |
48 |
|
return undefSatLiteral; |
49 |
|
} |
50 |
30 |
return SatLiteral(lit.var(), lit.sign()); |
51 |
|
} |
52 |
|
|
53 |
165 |
SatValue toSatLiteralValue(CMSat::lbool res) |
54 |
|
{ |
55 |
165 |
if (res == CMSat::l_True) return SAT_VALUE_TRUE; |
56 |
129 |
if (res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN; |
57 |
129 |
Assert(res == CMSat::l_False); |
58 |
129 |
return SAT_VALUE_FALSE; |
59 |
|
} |
60 |
|
|
61 |
3872 |
void toInternalClause(SatClause& clause, |
62 |
|
std::vector<CMSat::Lit>& internal_clause) |
63 |
|
{ |
64 |
13772 |
for (unsigned i = 0; i < clause.size(); ++i) |
65 |
|
{ |
66 |
9900 |
internal_clause.push_back(toInternalLit(clause[i])); |
67 |
|
} |
68 |
3872 |
Assert(clause.size() == internal_clause.size()); |
69 |
3872 |
} |
70 |
|
|
71 |
|
} // helper functions |
72 |
|
|
73 |
13 |
CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry& registry, |
74 |
13 |
const std::string& name) |
75 |
13 |
: d_solver(new CMSat::SATSolver()), |
76 |
|
d_numVariables(0), |
77 |
|
d_okay(true), |
78 |
26 |
d_statistics(registry, name) |
79 |
|
{ |
80 |
13 |
} |
81 |
|
|
82 |
13 |
void CryptoMinisatSolver::init() |
83 |
|
{ |
84 |
13 |
d_true = newVar(); |
85 |
13 |
d_false = newVar(); |
86 |
|
|
87 |
26 |
std::vector<CMSat::Lit> clause(1); |
88 |
13 |
clause[0] = CMSat::Lit(d_true, false); |
89 |
13 |
d_solver->add_clause(clause); |
90 |
|
|
91 |
13 |
clause[0] = CMSat::Lit(d_false, true); |
92 |
13 |
d_solver->add_clause(clause); |
93 |
13 |
} |
94 |
|
|
95 |
26 |
CryptoMinisatSolver::~CryptoMinisatSolver() {} |
96 |
|
|
97 |
|
ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, |
98 |
|
bool rhs, |
99 |
|
bool removable) |
100 |
|
{ |
101 |
|
Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n"; |
102 |
|
|
103 |
|
if (!d_okay) { |
104 |
|
Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; |
105 |
|
return ClauseIdError; |
106 |
|
} |
107 |
|
|
108 |
|
++(d_statistics.d_xorClausesAdded); |
109 |
|
|
110 |
|
// ensure all sat literals have positive polarity by pushing |
111 |
|
// the negation on the result |
112 |
|
std::vector<CMSatVar> xor_clause; |
113 |
|
for (unsigned i = 0; i < clause.size(); ++i) { |
114 |
|
xor_clause.push_back(toInternalLit(clause[i]).var()); |
115 |
|
rhs ^= clause[i].isNegated(); |
116 |
|
} |
117 |
|
bool res = d_solver->add_xor_clause(xor_clause, rhs); |
118 |
|
d_okay &= res; |
119 |
|
return ClauseIdError; |
120 |
|
} |
121 |
|
|
122 |
3872 |
ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ |
123 |
3872 |
Debug("sat::cryptominisat") << "Add clause " << clause <<"\n"; |
124 |
|
|
125 |
3872 |
if (!d_okay) { |
126 |
|
Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; |
127 |
|
return ClauseIdError; |
128 |
|
} |
129 |
|
|
130 |
3872 |
++(d_statistics.d_clausesAdded); |
131 |
|
|
132 |
7744 |
std::vector<CMSat::Lit> internal_clause; |
133 |
3872 |
toInternalClause(clause, internal_clause); |
134 |
3872 |
bool nowOkay = d_solver->add_clause(internal_clause); |
135 |
|
|
136 |
|
ClauseId freshId; |
137 |
3872 |
freshId = ClauseIdError; |
138 |
|
|
139 |
3872 |
d_okay &= nowOkay; |
140 |
3872 |
return freshId; |
141 |
|
} |
142 |
|
|
143 |
|
bool CryptoMinisatSolver::ok() const { return d_okay; } |
144 |
|
|
145 |
1535 |
SatVariable CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ |
146 |
1535 |
d_solver->new_var(); |
147 |
1535 |
++d_numVariables; |
148 |
1535 |
Assert(d_numVariables == d_solver->nVars()); |
149 |
1535 |
return d_numVariables - 1; |
150 |
|
} |
151 |
|
|
152 |
|
SatVariable CryptoMinisatSolver::trueVar() { |
153 |
|
return d_true; |
154 |
|
} |
155 |
|
|
156 |
|
SatVariable CryptoMinisatSolver::falseVar() { |
157 |
|
return d_false; |
158 |
|
} |
159 |
|
|
160 |
|
void CryptoMinisatSolver::markUnremovable(SatLiteral lit) { |
161 |
|
// cryptominisat supports dynamically adding back variables (?) |
162 |
|
// so this is a no-op |
163 |
|
return; |
164 |
|
} |
165 |
|
|
166 |
|
void CryptoMinisatSolver::interrupt(){ |
167 |
|
d_solver->interrupt_asap(); |
168 |
|
} |
169 |
|
|
170 |
|
SatValue CryptoMinisatSolver::solve(){ |
171 |
|
TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); |
172 |
|
++d_statistics.d_statCallsToSolve; |
173 |
|
return toSatLiteralValue(d_solver->solve()); |
174 |
|
} |
175 |
|
|
176 |
|
SatValue CryptoMinisatSolver::solve(long unsigned int& resource) { |
177 |
|
// CMSat::SalverConf conf = d_solver->getConf(); |
178 |
|
Unreachable() << "Not sure how to set different limits for calls to solve in " |
179 |
|
"Cryptominisat"; |
180 |
|
return solve(); |
181 |
|
} |
182 |
|
|
183 |
21 |
SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions) |
184 |
|
{ |
185 |
42 |
TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); |
186 |
42 |
std::vector<CMSat::Lit> assumpts; |
187 |
71 |
for (const SatLiteral& lit : assumptions) |
188 |
|
{ |
189 |
50 |
assumpts.push_back(toInternalLit(lit)); |
190 |
|
} |
191 |
21 |
++d_statistics.d_statCallsToSolve; |
192 |
42 |
return toSatLiteralValue(d_solver->solve(&assumpts)); |
193 |
|
} |
194 |
|
|
195 |
9 |
void CryptoMinisatSolver::getUnsatAssumptions( |
196 |
|
std::vector<SatLiteral>& assumptions) |
197 |
|
{ |
198 |
39 |
for (const CMSat::Lit& lit : d_solver->get_conflict()) |
199 |
|
{ |
200 |
30 |
assumptions.push_back(toSatLiteral(~lit)); |
201 |
|
} |
202 |
9 |
} |
203 |
|
|
204 |
144 |
SatValue CryptoMinisatSolver::value(SatLiteral l){ |
205 |
288 |
const std::vector<CMSat::lbool> model = d_solver->get_model(); |
206 |
144 |
CMSatVar var = l.getSatVariable(); |
207 |
144 |
Assert(var < model.size()); |
208 |
144 |
CMSat::lbool value = model[var]; |
209 |
288 |
return toSatLiteralValue(value); |
210 |
|
} |
211 |
|
|
212 |
144 |
SatValue CryptoMinisatSolver::modelValue(SatLiteral l) { return value(l); } |
213 |
|
|
214 |
|
unsigned CryptoMinisatSolver::getAssertionLevel() const { |
215 |
|
Unreachable() << "No interface to get assertion level in Cryptominisat"; |
216 |
|
return -1; |
217 |
|
} |
218 |
|
|
219 |
|
// Satistics for CryptoMinisatSolver |
220 |
|
|
221 |
13 |
CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry& registry, |
222 |
13 |
const std::string& prefix) |
223 |
26 |
: d_statCallsToSolve(registry.registerInt(prefix + "cryptominisat::calls_to_solve")), |
224 |
26 |
d_xorClausesAdded(registry.registerInt(prefix + "cryptominisat::xor_clauses")), |
225 |
26 |
d_clausesAdded(registry.registerInt(prefix + "cryptominisat::clauses")), |
226 |
52 |
d_solveTime(registry.registerTimer(prefix + "cryptominisat::solve_time")) |
227 |
|
{ |
228 |
13 |
} |
229 |
|
|
230 |
|
} // namespace prop |
231 |
29574 |
} // namespace cvc5 |
232 |
|
#endif |