Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Gereon Kremer, Liana Hadarean, Dejan Jovanovic
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 minisat interface for cvc5.
16 : : */
17 : :
18 : : #include "prop/minisat/minisat.h"
19 : :
20 : : #include "options/base_options.h"
21 : : #include "options/decision_options.h"
22 : : #include "options/proof_options.h"
23 : : #include "options/prop_options.h"
24 : : #include "options/smt_options.h"
25 : : #include "proof/clause_id.h"
26 : : #include "prop/minisat/simp/SimpSolver.h"
27 : : #include "util/statistics_stats.h"
28 : :
29 : : namespace cvc5::internal {
30 : : namespace prop {
31 : :
32 : : //// DPllMinisatSatSolver
33 : :
34 : 50572 : MinisatSatSolver::MinisatSatSolver(Env& env, StatisticsRegistry& registry)
35 : : : EnvObj(env),
36 : : d_minisat(NULL),
37 : : d_context(NULL),
38 : : d_assumptions(),
39 : 50572 : d_statistics(registry)
40 : 50572 : {}
41 : :
42 : 100632 : MinisatSatSolver::~MinisatSatSolver()
43 : : {
44 : 50316 : d_statistics.deinit();
45 [ + - ]: 50316 : delete d_minisat;
46 : 100632 : }
47 : :
48 : 0 : SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
49 [ - - ]: 0 : if (var == var_Undef) {
50 : 0 : return undefSatVariable;
51 : : }
52 : 0 : return SatVariable(var);
53 : : }
54 : :
55 : 114794000 : Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
56 [ + + ]: 114794000 : if (lit == undefSatLiteral) {
57 : 3546980 : return Minisat::lit_Undef;
58 : : }
59 : 111247000 : return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
60 : : }
61 : :
62 : 174932000 : SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
63 [ - + ]: 174932000 : if (lit == Minisat::lit_Undef) {
64 : 0 : return undefSatLiteral;
65 : : }
66 : :
67 : 174932000 : return SatLiteral(SatVariable(Minisat::var(lit)),
68 : 349863000 : Minisat::sign(lit));
69 : : }
70 : :
71 : 67066900 : SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
72 [ + + ]: 67066900 : if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
73 [ + + ]: 36700100 : if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
74 [ - + ][ - + ]: 6836380 : Assert(res == (Minisat::lbool((uint8_t)1)));
[ - - ]
75 : 6836380 : return SAT_VALUE_FALSE;
76 : : }
77 : :
78 : 0 : Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
79 : : {
80 [ - - ]: 0 : if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
81 [ - - ]: 0 : if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
82 : 0 : Assert(val == SAT_VALUE_FALSE);
83 : 0 : return Minisat::lbool((uint8_t)1);
84 : : }
85 : :
86 : : /*bool MinisatSatSolver::tobool(SatValue val)
87 : : {
88 : : if(val == SAT_VALUE_TRUE) return true;
89 : : Assert(val == SAT_VALUE_FALSE);
90 : : return false;
91 : : }*/
92 : :
93 : 22420900 : void MinisatSatSolver::toMinisatClause(SatClause& clause,
94 : : Minisat::vec<Minisat::Lit>& minisat_clause) {
95 [ + + ]: 55717900 : for (unsigned i = 0; i < clause.size(); ++i) {
96 : 33297000 : minisat_clause.push(toMinisatLit(clause[i]));
97 : : }
98 [ - + ][ - + ]: 22420900 : Assert(clause.size() == (unsigned)minisat_clause.size());
[ - - ]
99 : 22420900 : }
100 : :
101 : 984543 : void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
102 : : SatClause& sat_clause) {
103 [ + + ]: 39970500 : for (int i = 0; i < clause.size(); ++i) {
104 : 38986000 : sat_clause.push_back(toSatLiteral(clause[i]));
105 : : }
106 [ - + ][ - + ]: 984543 : Assert((unsigned)clause.size() == sat_clause.size());
[ - - ]
107 : 984543 : }
108 : :
109 : 50572 : void MinisatSatSolver::initialize(context::Context* context,
110 : : TheoryProxy* theoryProxy,
111 : : context::UserContext* userContext,
112 : : PropPfManager* ppm)
113 : : {
114 : 50572 : d_context = context;
115 : :
116 [ + + ]: 50572 : if (options().decision.decisionMode != options::DecisionMode::INTERNAL)
117 : : {
118 : 40211 : verbose(1) << "minisat: Incremental solving is forced on (to avoid "
119 : : "variable elimination)"
120 : 40211 : << " unless using internal decision strategy." << std::endl;
121 : : }
122 : :
123 : : // Create the solver
124 : 50572 : d_minisat =
125 : : new Minisat::SimpSolver(d_env,
126 : : theoryProxy,
127 : : d_context,
128 : : userContext,
129 : : ppm,
130 : 50572 : options().base.incrementalSolving
131 [ + + ][ + + ]: 50572 : || options().decision.decisionMode
132 : 50572 : != options::DecisionMode::INTERNAL);
133 : :
134 : 50572 : d_statistics.init(d_minisat);
135 : :
136 : : // Since the prop engine asserts "true" to the CNF stream regardless of what
137 : : // is in the input (see PropEngine::finishInit), if a real "true" assertion is
138 : : // made to the SAT solver via the Proof CNF stream, that would be ignored,
139 : : // since there is already "true" in the CNF stream. Thus the SAT proof would
140 : : // not have True as an assumption, which can lead to issues when building its
141 : : // proof. To prevent this problem, we track it directly here.
142 : 50572 : SatProofManager* spfm = d_minisat->getProofManager();
143 [ + + ]: 50572 : if (spfm)
144 : : {
145 : 10881 : NodeManager* nm = nodeManager();
146 : 21762 : spfm->registerSatAssumptions({nm->mkConst(true)});
147 : : }
148 : 50572 : }
149 : :
150 : : // Like initialize() above, but called just before each search when in
151 : : // incremental mode
152 : 49986 : void MinisatSatSolver::setupOptions() {
153 : : // Copy options from cvc5 options structure into minisat, as appropriate
154 : :
155 : : // Set up the verbosity
156 [ + + ]: 49986 : d_minisat->verbosity = (options().base.verbosity > 0) ? 1 : -1;
157 : :
158 : : // Set up the random decision parameters
159 : 49986 : d_minisat->random_var_freq = options().prop.satRandomFreq;
160 : : // If 0, we use whatever we like (here, the Minisat default seed)
161 [ + + ]: 49986 : if (options().prop.satRandomSeed != 0)
162 : : {
163 : 2 : d_minisat->random_seed = double(options().prop.satRandomSeed);
164 : : }
165 : :
166 : : // Give access to all possible options in the sat solver
167 : 49986 : d_minisat->var_decay = options().prop.satVarDecay;
168 : 49986 : d_minisat->clause_decay = options().prop.satClauseDecay;
169 : 49986 : d_minisat->restart_first = options().prop.satRestartFirst;
170 : 49986 : d_minisat->restart_inc = options().prop.satRestartInc;
171 : 49986 : }
172 : :
173 : 6258670 : ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable)
174 : : {
175 : 12517300 : Minisat::vec<Minisat::Lit> minisat_clause;
176 : 6258670 : toMinisatClause(clause, minisat_clause);
177 : 6258670 : ClauseId clause_id = ClauseIdError;
178 : : // FIXME: This relies on the invariant that when ok() is false
179 : : // the SAT solver does not add the clause (which is what Minisat currently does)
180 [ + + ]: 6258670 : if (!ok()) {
181 : 8574 : return ClauseIdUndef;
182 : : }
183 : 6250100 : d_minisat->addClause(minisat_clause, removable, clause_id);
184 : : // FIXME: to be deleted when we kill old proof code for unsat cores
185 [ + + ][ - + ]: 6250100 : Assert(!options().smt.produceUnsatCores || options().smt.produceProofs
[ - - ][ - + ]
[ - - ]
186 : : || clause_id != ClauseIdError);
187 : 6250100 : return clause_id;
188 : : }
189 : :
190 : 2230920 : SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool canErase)
191 : : {
192 : 2230920 : return d_minisat->newVar(true, true, isTheoryAtom, canErase);
193 : : }
194 : :
195 : 0 : SatValue MinisatSatSolver::solve(unsigned long& resource) {
196 [ - - ]: 0 : Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
197 : 0 : setupOptions();
198 [ - - ]: 0 : if(resource == 0) {
199 : 0 : d_minisat->budgetOff();
200 : : } else {
201 : 0 : d_minisat->setConfBudget(resource);
202 : : }
203 : 0 : Minisat::vec<Minisat::Lit> empty;
204 : 0 : unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed;
205 : 0 : SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
206 : 0 : d_minisat->clearInterrupt();
207 : 0 : resource = d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
208 [ - - ]: 0 : Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
209 : 0 : return result;
210 : : }
211 : :
212 : 40996 : SatValue MinisatSatSolver::solve() {
213 : 40996 : setupOptions();
214 : 40996 : d_minisat->budgetOff();
215 : 40996 : SatValue result = toSatLiteralValue(d_minisat->solve());
216 : 40983 : d_minisat->clearInterrupt();
217 : 40983 : return result;
218 : : }
219 : :
220 : 8990 : SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
221 : : {
222 : 8990 : setupOptions();
223 : 8990 : d_minisat->budgetOff();
224 : :
225 : 8990 : d_assumptions.clear();
226 : 8990 : Minisat::vec<Minisat::Lit> assumps;
227 : :
228 [ + + ]: 157968 : for (const SatLiteral& lit : assumptions)
229 : : {
230 : 148978 : Minisat::Lit mlit = toMinisatLit(lit);
231 : 148978 : assumps.push(mlit);
232 : 148978 : d_assumptions.emplace(lit);
233 : : }
234 : :
235 : 8990 : SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
236 : 8990 : d_minisat->clearInterrupt();
237 : 17980 : return result;
238 : : }
239 : :
240 : 4242 : void MinisatSatSolver::getUnsatAssumptions(
241 : : std::vector<SatLiteral>& unsat_assumptions)
242 : : {
243 [ + + ]: 24295 : for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
244 : : {
245 : 20053 : Minisat::Lit mlit = d_minisat->d_conflict[i];
246 : 20053 : SatLiteral lit = ~toSatLiteral(mlit);
247 [ + - ]: 20053 : if (d_assumptions.find(lit) != d_assumptions.end())
248 : : {
249 : 20053 : unsat_assumptions.push_back(lit);
250 : : }
251 : : }
252 : 4242 : }
253 : :
254 : 6258670 : bool MinisatSatSolver::ok() const {
255 : 6258670 : return d_minisat->okay();
256 : : }
257 : :
258 : 20152 : void MinisatSatSolver::interrupt() {
259 : 20152 : d_minisat->interrupt();
260 : 20152 : }
261 : :
262 : 67016900 : SatValue MinisatSatSolver::value(SatLiteral l) {
263 : 67016900 : return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
264 : : }
265 : :
266 : 0 : SatValue MinisatSatSolver::modelValue(SatLiteral l){
267 : 0 : return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
268 : : }
269 : :
270 : 167894 : void MinisatSatSolver::preferPhase(SatLiteral lit)
271 : : {
272 [ - + ][ - + ]: 167894 : Assert(!d_minisat->rnd_pol);
[ - - ]
273 [ + - ]: 335788 : Trace("minisat") << "preferPhase(" << lit << ")"
274 : 167894 : << " " << lit.getSatVariable() << " " << lit.isNegated()
275 : 167894 : << std::endl;
276 : 167894 : SatVariable v = lit.getSatVariable();
277 : 167894 : d_minisat->freezePolarity(v, lit.isNegated());
278 : 167894 : }
279 : :
280 : 193757 : bool MinisatSatSolver::isDecision(SatVariable decn) const {
281 : 193757 : return d_minisat->isDecision( decn );
282 : : }
283 : :
284 : 16 : bool MinisatSatSolver::isFixed(SatVariable var) const
285 : : {
286 [ + + ]: 32 : return d_minisat->intro_level(var) == 0 && d_minisat->user_level(var) == 0
287 [ + - ][ + + ]: 32 : && d_minisat->level(var) == 0;
288 : : }
289 : :
290 : 0 : std::vector<SatLiteral> MinisatSatSolver::getDecisions() const
291 : : {
292 : 0 : std::vector<SatLiteral> decisions;
293 : : const Minisat::vec<Minisat::Lit>& miniDecisions =
294 : 0 : d_minisat->getMiniSatAssignmentTrail();
295 [ - - ]: 0 : for (size_t i = 0, ndec = miniDecisions.size(); i < ndec; ++i)
296 : : {
297 : 0 : auto satLit = toSatLiteral(miniDecisions[i]);
298 [ - - ]: 0 : if (isDecision(satLit.getSatVariable()))
299 : : {
300 : 0 : decisions.push_back(satLit);
301 : : }
302 : : }
303 : 0 : return decisions;
304 : : }
305 : :
306 : 0 : std::vector<Node> MinisatSatSolver::getOrderHeap() const
307 : : {
308 : 0 : return d_minisat->getMiniSatOrderHeap();
309 : : }
310 : :
311 : 9830 : std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
312 : : {
313 [ - + ][ - + ]: 9830 : Assert(d_env.isSatProofProducing());
[ - - ]
314 : 9830 : return d_minisat->getProof();
315 : : }
316 : :
317 : : /** Incremental interface */
318 : :
319 : 49968 : uint32_t MinisatSatSolver::getAssertionLevel() const
320 : : {
321 : 49968 : return d_minisat->getAssertionLevel();
322 : : }
323 : :
324 : 9025 : void MinisatSatSolver::push() {
325 : 9025 : d_minisat->push();
326 : 9025 : }
327 : :
328 : 9020 : void MinisatSatSolver::pop() {
329 : 9020 : d_minisat->pop();
330 : 9020 : }
331 : :
332 : 49204 : void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
333 : :
334 : : /// Statistics for MinisatSatSolver
335 : :
336 : 50572 : MinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry)
337 : : : d_statStarts(registry.registerReference<int64_t>("sat::starts")),
338 : : d_statDecisions(registry.registerReference<int64_t>("sat::decisions")),
339 : : d_statRndDecisions(
340 : : registry.registerReference<int64_t>("sat::rnd_decisions")),
341 : : d_statPropagations(
342 : : registry.registerReference<int64_t>("sat::propagations")),
343 : : d_statConflicts(registry.registerReference<int64_t>("sat::conflicts")),
344 : : d_statClausesLiterals(
345 : : registry.registerReference<int64_t>("sat::clauses_literals")),
346 : : d_statLearntsLiterals(
347 : : registry.registerReference<int64_t>("sat::learnts_literals")),
348 : : d_statMaxLiterals(
349 : : registry.registerReference<int64_t>("sat::max_literals")),
350 : : d_statTotLiterals(
351 : 50572 : registry.registerReference<int64_t>("sat::tot_literals"))
352 : : {
353 : 50572 : }
354 : :
355 : 50572 : void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
356 : 50572 : d_statStarts.set(minisat->starts);
357 : 50572 : d_statDecisions.set(minisat->decisions);
358 : 50572 : d_statRndDecisions.set(minisat->rnd_decisions);
359 : 50572 : d_statPropagations.set(minisat->propagations);
360 : 50572 : d_statConflicts.set(minisat->conflicts);
361 : 50572 : d_statClausesLiterals.set(minisat->clauses_literals);
362 : 50572 : d_statLearntsLiterals.set(minisat->learnts_literals);
363 : 50572 : d_statMaxLiterals.set(minisat->max_literals);
364 : 50572 : d_statTotLiterals.set(minisat->tot_literals);
365 : 50572 : }
366 : 50316 : void MinisatSatSolver::Statistics::deinit()
367 : : {
368 : 50316 : d_statStarts.reset();
369 : 50316 : d_statDecisions.reset();
370 : 50316 : d_statRndDecisions.reset();
371 : 50316 : d_statPropagations.reset();
372 : 50316 : d_statConflicts.reset();
373 : 50316 : d_statClausesLiterals.reset();
374 : 50316 : d_statLearntsLiterals.reset();
375 : 50316 : d_statMaxLiterals.reset();
376 : 50316 : d_statTotLiterals.reset();
377 : 50316 : }
378 : :
379 : : } // namespace prop
380 : : } // namespace cvc5::internal
381 : :
382 : : namespace cvc5::internal {
383 : : template <>
384 : 0 : prop::SatLiteral toSatLiteral<cvc5::internal::Minisat::Solver>(Minisat::Solver::TLit lit)
385 : : {
386 : 0 : return prop::MinisatSatSolver::toSatLiteral(lit);
387 : : }
388 : :
389 : : template <>
390 : 0 : void toSatClause<cvc5::internal::Minisat::Solver>(
391 : : const cvc5::internal::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
392 : : {
393 : 0 : prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
394 : 0 : }
395 : :
396 : : } // namespace cvc5::internal
|
