368a79b80d99f499085c88c96591545112d59657
1 /********************* */
2 /*! \file bvminisat.cpp
4 ** Original author: dejan
6 ** Minor contributors (to current version):
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
16 ** Implementation of the minisat for cvc4 (bitvectors).
19 #include "prop/bvminisat/bvminisat.h"
21 #include "prop/bvminisat/simp/SimpSolver.h"
22 #include "proof/clause_id.h"
23 #include "proof/sat_proof.h"
24 #include "util/statistics_registry.h"
29 BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry
* registry
, context::Context
* mainSatContext
, const std::string
& name
)
30 : context::ContextNotifyObj(mainSatContext
, false),
31 d_minisat(new BVMinisat::SimpSolver(mainSatContext
)),
34 d_assertionsRealCount(mainSatContext
, 0),
35 d_lastPropagation(mainSatContext
, 0),
36 d_statistics(registry
, name
)
38 d_statistics
.init(d_minisat
);
42 BVMinisatSatSolver::~BVMinisatSatSolver() {
44 delete d_minisatNotify
;
47 void BVMinisatSatSolver::setNotify(Notify
* notify
) {
48 d_minisatNotify
= new MinisatNotify(notify
);
49 d_minisat
->setNotify(d_minisatNotify
);
52 ClauseId
BVMinisatSatSolver::addClause(SatClause
& clause
,
54 Debug("sat::minisat") << "Add clause " << clause
<<"\n";
55 BVMinisat::vec
<BVMinisat::Lit
> minisat_clause
;
56 toMinisatClause(clause
, minisat_clause
);
57 // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
58 // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
60 ClauseId clause_id
= ClauseIdError
;
61 d_minisat
->addClause(minisat_clause
, clause_id
);
62 THEORY_PROOF(Assert (clause_id
!= ClauseIdError
););
66 SatValue
BVMinisatSatSolver::propagate() {
67 return toSatLiteralValue(d_minisat
->propagateAssumptions());
70 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit
) {
71 d_minisat
->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit
)));
75 void BVMinisatSatSolver::explain(SatLiteral lit
, std::vector
<SatLiteral
>& explanation
) {
76 std::vector
<BVMinisat::Lit
> minisat_explanation
;
77 d_minisat
->explain(toMinisatLit(lit
), minisat_explanation
);
78 for (unsigned i
= 0; i
< minisat_explanation
.size(); ++i
) {
79 explanation
.push_back(toSatLiteral(minisat_explanation
[i
]));
83 SatValue
BVMinisatSatSolver::assertAssumption(SatLiteral lit
, bool propagate
) {
85 d_assertionsRealCount
= d_assertionsRealCount
+ 1;
86 return toSatLiteralValue(d_minisat
->assertAssumption(toMinisatLit(lit
), propagate
));
89 void BVMinisatSatSolver::contextNotifyPop() {
90 while (d_assertionsCount
> d_assertionsRealCount
) {
96 void BVMinisatSatSolver::popAssumption() {
97 d_minisat
->popAssumption();
100 void BVMinisatSatSolver::setProofLog( BitVectorProof
* bvp
) {
101 d_minisat
->setProofLog( bvp
);
104 SatVariable
BVMinisatSatSolver::newVar(bool isTheoryAtom
, bool preRegister
, bool canErase
){
105 return d_minisat
->newVar(true, true, !canErase
);
108 void BVMinisatSatSolver::markUnremovable(SatLiteral lit
){
109 d_minisat
->setFrozen(BVMinisat::var(toMinisatLit(lit
)), true);
113 void BVMinisatSatSolver::interrupt(){
114 d_minisat
->interrupt();
117 SatValue
BVMinisatSatSolver::solve(){
118 ++d_statistics
.d_statCallsToSolve
;
119 return toSatLiteralValue(d_minisat
->solve());
122 SatValue
BVMinisatSatSolver::solve(long unsigned int& resource
){
123 Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource
<< " conflicts" << std::endl
;
124 ++d_statistics
.d_statCallsToSolve
;
126 d_minisat
->budgetOff();
128 d_minisat
->setConfBudget(resource
);
130 // BVMinisat::vec<BVMinisat::Lit> empty;
131 unsigned long conflictsBefore
= d_minisat
->conflicts
;
132 SatValue result
= toSatLiteralValue(d_minisat
->solveLimited());
133 d_minisat
->clearInterrupt();
134 resource
= d_minisat
->conflicts
- conflictsBefore
;
135 Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource
<< " conflicts" << std::endl
;
139 bool BVMinisatSatSolver::ok() const {
140 return d_minisat
->okay();
143 void BVMinisatSatSolver::getUnsatCore(SatClause
& unsatCore
) {
144 // TODO add assertion to check the call was after an unsat call
145 for (int i
= 0; i
< d_minisat
->conflict
.size(); ++i
) {
146 unsatCore
.push_back(toSatLiteral(d_minisat
->conflict
[i
]));
150 SatValue
BVMinisatSatSolver::value(SatLiteral l
){
151 return toSatLiteralValue(d_minisat
->value(toMinisatLit(l
)));
154 SatValue
BVMinisatSatSolver::modelValue(SatLiteral l
){
155 return toSatLiteralValue(d_minisat
->modelValue(toMinisatLit(l
)));
158 void BVMinisatSatSolver::unregisterVar(SatLiteral lit
) {
159 // this should only be called when user context is implemented
160 // in the BVSatSolver
164 void BVMinisatSatSolver::renewVar(SatLiteral lit
, int level
) {
165 // this should only be called when user context is implemented
166 // in the BVSatSolver
171 unsigned BVMinisatSatSolver::getAssertionLevel() const {
172 // we have no user context implemented so far
176 // converting from internal Minisat representation
178 SatVariable
BVMinisatSatSolver::toSatVariable(BVMinisat::Var var
) {
179 if (var
== var_Undef
) {
180 return undefSatVariable
;
182 return SatVariable(var
);
185 BVMinisat::Lit
BVMinisatSatSolver::toMinisatLit(SatLiteral lit
) {
186 if (lit
== undefSatLiteral
) {
187 return BVMinisat::lit_Undef
;
189 return BVMinisat::mkLit(lit
.getSatVariable(), lit
.isNegated());
192 SatLiteral
BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit
) {
193 if (lit
== BVMinisat::lit_Undef
) {
194 return undefSatLiteral
;
197 return SatLiteral(SatVariable(BVMinisat::var(lit
)),
198 BVMinisat::sign(lit
));
201 SatValue
BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res
) {
202 if(res
== (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE
;
203 if(res
== (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN
;
204 Assert(res
== (BVMinisat::lbool((uint8_t)1)));
205 return SAT_VALUE_FALSE
;
208 void BVMinisatSatSolver::toMinisatClause(SatClause
& clause
,
209 BVMinisat::vec
<BVMinisat::Lit
>& minisat_clause
) {
210 for (unsigned i
= 0; i
< clause
.size(); ++i
) {
211 minisat_clause
.push(toMinisatLit(clause
[i
]));
213 Assert(clause
.size() == (unsigned)minisat_clause
.size());
216 void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause
& clause
,
217 SatClause
& sat_clause
) {
218 for (int i
= 0; i
< clause
.size(); ++i
) {
219 sat_clause
.push_back(toSatLiteral(clause
[i
]));
221 Assert((unsigned)clause
.size() == sat_clause
.size());
225 // Satistics for BVMinisatSatSolver
227 BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry
* registry
, const std::string
& prefix
)
228 : d_registry(registry
),
229 d_statStarts("theory::bv::"+prefix
+"bvminisat::starts"),
230 d_statDecisions("theory::bv::"+prefix
+"bvminisat::decisions"),
231 d_statRndDecisions("theory::bv::"+prefix
+"bvminisat::rnd_decisions"),
232 d_statPropagations("theory::bv::"+prefix
+"bvminisat::propagations"),
233 d_statConflicts("theory::bv::"+prefix
+"bvminisat::conflicts"),
234 d_statClausesLiterals("theory::bv::"+prefix
+"bvminisat::clauses_literals"),
235 d_statLearntsLiterals("theory::bv::"+prefix
+"bvminisat::learnts_literals"),
236 d_statMaxLiterals("theory::bv::"+prefix
+"bvminisat::max_literals"),
237 d_statTotLiterals("theory::bv::"+prefix
+"bvminisat::tot_literals"),
238 d_statEliminatedVars("theory::bv::"+prefix
+"bvminisat::eliminated_vars"),
239 d_statCallsToSolve("theory::bv::"+prefix
+"bvminisat::calls_to_solve", 0),
240 d_statSolveTime("theory::bv::"+prefix
+"bvminisat::solve_time", 0),
241 d_registerStats(!prefix
.empty())
243 if (!d_registerStats
){
247 d_registry
->registerStat(&d_statStarts
);
248 d_registry
->registerStat(&d_statDecisions
);
249 d_registry
->registerStat(&d_statRndDecisions
);
250 d_registry
->registerStat(&d_statPropagations
);
251 d_registry
->registerStat(&d_statConflicts
);
252 d_registry
->registerStat(&d_statClausesLiterals
);
253 d_registry
->registerStat(&d_statLearntsLiterals
);
254 d_registry
->registerStat(&d_statMaxLiterals
);
255 d_registry
->registerStat(&d_statTotLiterals
);
256 d_registry
->registerStat(&d_statEliminatedVars
);
257 d_registry
->registerStat(&d_statCallsToSolve
);
258 d_registry
->registerStat(&d_statSolveTime
);
261 BVMinisatSatSolver::Statistics::~Statistics() {
262 if (!d_registerStats
){
265 d_registry
->unregisterStat(&d_statStarts
);
266 d_registry
->unregisterStat(&d_statDecisions
);
267 d_registry
->unregisterStat(&d_statRndDecisions
);
268 d_registry
->unregisterStat(&d_statPropagations
);
269 d_registry
->unregisterStat(&d_statConflicts
);
270 d_registry
->unregisterStat(&d_statClausesLiterals
);
271 d_registry
->unregisterStat(&d_statLearntsLiterals
);
272 d_registry
->unregisterStat(&d_statMaxLiterals
);
273 d_registry
->unregisterStat(&d_statTotLiterals
);
274 d_registry
->unregisterStat(&d_statEliminatedVars
);
275 d_registry
->unregisterStat(&d_statCallsToSolve
);
276 d_registry
->unregisterStat(&d_statSolveTime
);
279 void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver
* minisat
){
280 if (!d_registerStats
){
284 d_statStarts
.setData(minisat
->starts
);
285 d_statDecisions
.setData(minisat
->decisions
);
286 d_statRndDecisions
.setData(minisat
->rnd_decisions
);
287 d_statPropagations
.setData(minisat
->propagations
);
288 d_statConflicts
.setData(minisat
->conflicts
);
289 d_statClausesLiterals
.setData(minisat
->clauses_literals
);
290 d_statLearntsLiterals
.setData(minisat
->learnts_literals
);
291 d_statMaxLiterals
.setData(minisat
->max_literals
);
292 d_statTotLiterals
.setData(minisat
->tot_literals
);
293 d_statEliminatedVars
.setData(minisat
->eliminated_vars
);
296 } /* namespace CVC4::prop */
297 } /* namespace CVC4 */
301 prop::SatLiteral toSatLiteral
< BVMinisat::Solver
>(BVMinisat::Solver::TLit lit
) {
302 return prop::BVMinisatSatSolver::toSatLiteral(lit
);
306 void toSatClause
< BVMinisat::Solver
> (const BVMinisat::Solver::TClause
& minisat_cl
,
307 prop::SatClause
& sat_cl
) {
308 prop::BVMinisatSatSolver::toSatClause(minisat_cl
, sat_cl
);