1 /********************* */
2 /*! \file bvminisat.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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.\endverbatim
14 ** Implementation of the minisat for cvc4 (bitvectors).
17 #include "prop/bvminisat/bvminisat.h"
19 #include "prop/bvminisat/simp/SimpSolver.h"
20 #include "proof/clause_id.h"
21 #include "proof/sat_proof.h"
22 #include "util/statistics_registry.h"
27 BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry
* registry
, context::Context
* mainSatContext
, const std::string
& name
)
28 : context::ContextNotifyObj(mainSatContext
, false),
29 d_minisat(new BVMinisat::SimpSolver(mainSatContext
)),
32 d_assertionsRealCount(mainSatContext
, 0),
33 d_lastPropagation(mainSatContext
, 0),
34 d_statistics(registry
, name
)
36 d_statistics
.init(d_minisat
);
40 BVMinisatSatSolver::~BVMinisatSatSolver() {
42 delete d_minisatNotify
;
45 void BVMinisatSatSolver::setNotify(Notify
* notify
) {
46 d_minisatNotify
= new MinisatNotify(notify
);
47 d_minisat
->setNotify(d_minisatNotify
);
50 ClauseId
BVMinisatSatSolver::addClause(SatClause
& clause
,
52 Debug("sat::minisat") << "Add clause " << clause
<<"\n";
53 BVMinisat::vec
<BVMinisat::Lit
> minisat_clause
;
54 toMinisatClause(clause
, minisat_clause
);
55 // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
56 // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
58 ClauseId clause_id
= ClauseIdError
;
59 d_minisat
->addClause(minisat_clause
, clause_id
);
60 THEORY_PROOF(Assert (clause_id
!= ClauseIdError
););
64 SatValue
BVMinisatSatSolver::propagate() {
65 return toSatLiteralValue(d_minisat
->propagateAssumptions());
68 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit
) {
69 d_minisat
->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit
)));
73 void BVMinisatSatSolver::explain(SatLiteral lit
, std::vector
<SatLiteral
>& explanation
) {
74 std::vector
<BVMinisat::Lit
> minisat_explanation
;
75 d_minisat
->explain(toMinisatLit(lit
), minisat_explanation
);
76 for (unsigned i
= 0; i
< minisat_explanation
.size(); ++i
) {
77 explanation
.push_back(toSatLiteral(minisat_explanation
[i
]));
81 SatValue
BVMinisatSatSolver::assertAssumption(SatLiteral lit
, bool propagate
) {
83 d_assertionsRealCount
= d_assertionsRealCount
+ 1;
84 return toSatLiteralValue(d_minisat
->assertAssumption(toMinisatLit(lit
), propagate
));
87 void BVMinisatSatSolver::contextNotifyPop() {
88 while (d_assertionsCount
> d_assertionsRealCount
) {
94 void BVMinisatSatSolver::popAssumption() {
95 d_minisat
->popAssumption();
98 void BVMinisatSatSolver::setProofLog( BitVectorProof
* bvp
) {
99 d_minisat
->setProofLog( bvp
);
102 SatVariable
BVMinisatSatSolver::newVar(bool isTheoryAtom
, bool preRegister
, bool canErase
){
103 return d_minisat
->newVar(true, true, !canErase
);
106 void BVMinisatSatSolver::markUnremovable(SatLiteral lit
){
107 d_minisat
->setFrozen(BVMinisat::var(toMinisatLit(lit
)), true);
111 void BVMinisatSatSolver::interrupt(){
112 d_minisat
->interrupt();
115 SatValue
BVMinisatSatSolver::solve(){
116 ++d_statistics
.d_statCallsToSolve
;
117 return toSatLiteralValue(d_minisat
->solve());
120 SatValue
BVMinisatSatSolver::solve(long unsigned int& resource
){
121 Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource
<< " conflicts" << std::endl
;
122 ++d_statistics
.d_statCallsToSolve
;
124 d_minisat
->budgetOff();
126 d_minisat
->setConfBudget(resource
);
128 // BVMinisat::vec<BVMinisat::Lit> empty;
129 unsigned long conflictsBefore
= d_minisat
->conflicts
;
130 SatValue result
= toSatLiteralValue(d_minisat
->solveLimited());
131 d_minisat
->clearInterrupt();
132 resource
= d_minisat
->conflicts
- conflictsBefore
;
133 Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource
<< " conflicts" << std::endl
;
137 bool BVMinisatSatSolver::ok() const {
138 return d_minisat
->okay();
141 void BVMinisatSatSolver::getUnsatCore(SatClause
& unsatCore
) {
142 // TODO add assertion to check the call was after an unsat call
143 for (int i
= 0; i
< d_minisat
->conflict
.size(); ++i
) {
144 unsatCore
.push_back(toSatLiteral(d_minisat
->conflict
[i
]));
148 SatValue
BVMinisatSatSolver::value(SatLiteral l
){
149 return toSatLiteralValue(d_minisat
->value(toMinisatLit(l
)));
152 SatValue
BVMinisatSatSolver::modelValue(SatLiteral l
){
153 return toSatLiteralValue(d_minisat
->modelValue(toMinisatLit(l
)));
156 void BVMinisatSatSolver::unregisterVar(SatLiteral lit
) {
157 // this should only be called when user context is implemented
158 // in the BVSatSolver
162 void BVMinisatSatSolver::renewVar(SatLiteral lit
, int level
) {
163 // this should only be called when user context is implemented
164 // in the BVSatSolver
169 unsigned BVMinisatSatSolver::getAssertionLevel() const {
170 // we have no user context implemented so far
174 // converting from internal Minisat representation
176 SatVariable
BVMinisatSatSolver::toSatVariable(BVMinisat::Var var
) {
177 if (var
== var_Undef
) {
178 return undefSatVariable
;
180 return SatVariable(var
);
183 BVMinisat::Lit
BVMinisatSatSolver::toMinisatLit(SatLiteral lit
) {
184 if (lit
== undefSatLiteral
) {
185 return BVMinisat::lit_Undef
;
187 return BVMinisat::mkLit(lit
.getSatVariable(), lit
.isNegated());
190 SatLiteral
BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit
) {
191 if (lit
== BVMinisat::lit_Undef
) {
192 return undefSatLiteral
;
195 return SatLiteral(SatVariable(BVMinisat::var(lit
)),
196 BVMinisat::sign(lit
));
199 SatValue
BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res
) {
200 if(res
== (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE
;
201 if(res
== (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN
;
202 Assert(res
== (BVMinisat::lbool((uint8_t)1)));
203 return SAT_VALUE_FALSE
;
206 void BVMinisatSatSolver::toMinisatClause(SatClause
& clause
,
207 BVMinisat::vec
<BVMinisat::Lit
>& minisat_clause
) {
208 for (unsigned i
= 0; i
< clause
.size(); ++i
) {
209 minisat_clause
.push(toMinisatLit(clause
[i
]));
211 Assert(clause
.size() == (unsigned)minisat_clause
.size());
214 void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause
& clause
,
215 SatClause
& sat_clause
) {
216 for (int i
= 0; i
< clause
.size(); ++i
) {
217 sat_clause
.push_back(toSatLiteral(clause
[i
]));
219 Assert((unsigned)clause
.size() == sat_clause
.size());
223 // Satistics for BVMinisatSatSolver
225 BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry
* registry
, const std::string
& prefix
)
226 : d_registry(registry
),
227 d_statStarts("theory::bv::"+prefix
+"bvminisat::starts"),
228 d_statDecisions("theory::bv::"+prefix
+"bvminisat::decisions"),
229 d_statRndDecisions("theory::bv::"+prefix
+"bvminisat::rnd_decisions"),
230 d_statPropagations("theory::bv::"+prefix
+"bvminisat::propagations"),
231 d_statConflicts("theory::bv::"+prefix
+"bvminisat::conflicts"),
232 d_statClausesLiterals("theory::bv::"+prefix
+"bvminisat::clauses_literals"),
233 d_statLearntsLiterals("theory::bv::"+prefix
+"bvminisat::learnts_literals"),
234 d_statMaxLiterals("theory::bv::"+prefix
+"bvminisat::max_literals"),
235 d_statTotLiterals("theory::bv::"+prefix
+"bvminisat::tot_literals"),
236 d_statEliminatedVars("theory::bv::"+prefix
+"bvminisat::eliminated_vars"),
237 d_statCallsToSolve("theory::bv::"+prefix
+"bvminisat::calls_to_solve", 0),
238 d_statSolveTime("theory::bv::"+prefix
+"bvminisat::solve_time", 0),
239 d_registerStats(!prefix
.empty())
241 if (!d_registerStats
){
245 d_registry
->registerStat(&d_statStarts
);
246 d_registry
->registerStat(&d_statDecisions
);
247 d_registry
->registerStat(&d_statRndDecisions
);
248 d_registry
->registerStat(&d_statPropagations
);
249 d_registry
->registerStat(&d_statConflicts
);
250 d_registry
->registerStat(&d_statClausesLiterals
);
251 d_registry
->registerStat(&d_statLearntsLiterals
);
252 d_registry
->registerStat(&d_statMaxLiterals
);
253 d_registry
->registerStat(&d_statTotLiterals
);
254 d_registry
->registerStat(&d_statEliminatedVars
);
255 d_registry
->registerStat(&d_statCallsToSolve
);
256 d_registry
->registerStat(&d_statSolveTime
);
259 BVMinisatSatSolver::Statistics::~Statistics() {
260 if (!d_registerStats
){
263 d_registry
->unregisterStat(&d_statStarts
);
264 d_registry
->unregisterStat(&d_statDecisions
);
265 d_registry
->unregisterStat(&d_statRndDecisions
);
266 d_registry
->unregisterStat(&d_statPropagations
);
267 d_registry
->unregisterStat(&d_statConflicts
);
268 d_registry
->unregisterStat(&d_statClausesLiterals
);
269 d_registry
->unregisterStat(&d_statLearntsLiterals
);
270 d_registry
->unregisterStat(&d_statMaxLiterals
);
271 d_registry
->unregisterStat(&d_statTotLiterals
);
272 d_registry
->unregisterStat(&d_statEliminatedVars
);
273 d_registry
->unregisterStat(&d_statCallsToSolve
);
274 d_registry
->unregisterStat(&d_statSolveTime
);
277 void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver
* minisat
){
278 if (!d_registerStats
){
282 d_statStarts
.setData(minisat
->starts
);
283 d_statDecisions
.setData(minisat
->decisions
);
284 d_statRndDecisions
.setData(minisat
->rnd_decisions
);
285 d_statPropagations
.setData(minisat
->propagations
);
286 d_statConflicts
.setData(minisat
->conflicts
);
287 d_statClausesLiterals
.setData(minisat
->clauses_literals
);
288 d_statLearntsLiterals
.setData(minisat
->learnts_literals
);
289 d_statMaxLiterals
.setData(minisat
->max_literals
);
290 d_statTotLiterals
.setData(minisat
->tot_literals
);
291 d_statEliminatedVars
.setData(minisat
->eliminated_vars
);
294 } /* namespace CVC4::prop */
295 } /* namespace CVC4 */
299 prop::SatLiteral toSatLiteral
< BVMinisat::Solver
>(BVMinisat::Solver::TLit lit
) {
300 return prop::BVMinisatSatSolver::toSatLiteral(lit
);
304 void toSatClause
< BVMinisat::Solver
> (const BVMinisat::Solver::TClause
& minisat_cl
,
305 prop::SatClause
& sat_cl
) {
306 prop::BVMinisatSatSolver::toSatClause(minisat_cl
, sat_cl
);