1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner, Liana Hadarean, Tim King |
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 minisat for cvc5 (bit-vectors). |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "cvc5_private.h" |
19 |
|
|
20 |
|
#pragma once |
21 |
|
|
22 |
|
#include <memory> |
23 |
|
|
24 |
|
#include "context/cdo.h" |
25 |
|
#include "prop/bv_sat_solver_notify.h" |
26 |
|
#include "prop/bvminisat/simp/SimpSolver.h" |
27 |
|
#include "prop/sat_solver.h" |
28 |
|
#include "util/resource_manager.h" |
29 |
|
#include "util/statistics_stats.h" |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
namespace prop { |
33 |
|
|
34 |
|
class BVMinisatSatSolver : public BVSatSolverInterface, |
35 |
|
public context::ContextNotifyObj |
36 |
|
{ |
37 |
|
private: |
38 |
18844 |
class MinisatNotify : public BVMinisat::Notify |
39 |
|
{ |
40 |
|
BVSatSolverNotify* d_notify; |
41 |
|
|
42 |
|
public: |
43 |
9422 |
MinisatNotify(BVSatSolverNotify* notify) : d_notify(notify) {} |
44 |
2125902 |
bool notify(BVMinisat::Lit lit) override |
45 |
|
{ |
46 |
2125902 |
return d_notify->notify(toSatLiteral(lit)); |
47 |
|
} |
48 |
|
void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override; |
49 |
1623 |
void spendResource(Resource r) override |
50 |
|
{ |
51 |
1623 |
d_notify->spendResource(r); |
52 |
1623 |
} |
53 |
22064355 |
void safePoint(Resource r) override |
54 |
|
{ |
55 |
22064355 |
d_notify->safePoint(r); |
56 |
22064355 |
} |
57 |
|
}; |
58 |
|
|
59 |
|
std::unique_ptr<BVMinisat::SimpSolver> d_minisat; |
60 |
|
std::unique_ptr<MinisatNotify> d_minisatNotify; |
61 |
|
|
62 |
|
unsigned d_assertionsCount; |
63 |
|
context::CDO<unsigned> d_assertionsRealCount; |
64 |
|
context::CDO<unsigned> d_lastPropagation; |
65 |
|
|
66 |
|
protected: |
67 |
|
void contextNotifyPop() override; |
68 |
|
|
69 |
|
public: |
70 |
|
BVMinisatSatSolver(StatisticsRegistry& registry, |
71 |
|
context::Context* mainSatContext, |
72 |
|
const std::string& name = ""); |
73 |
|
virtual ~BVMinisatSatSolver(); |
74 |
|
|
75 |
|
void setNotify(BVSatSolverNotify* notify) override; |
76 |
|
|
77 |
|
ClauseId addClause(SatClause& clause, bool removable) override; |
78 |
|
|
79 |
|
ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override |
80 |
|
{ |
81 |
|
Unreachable() << "Minisat does not support native XOR reasoning"; |
82 |
|
return ClauseIdError; |
83 |
|
} |
84 |
|
|
85 |
|
SatValue propagate() override; |
86 |
|
|
87 |
|
SatVariable newVar(bool isTheoryAtom = false, |
88 |
|
bool preRegister = false, |
89 |
|
bool canErase = true) override; |
90 |
|
|
91 |
123 |
SatVariable trueVar() override { return d_minisat->trueVar(); } |
92 |
223 |
SatVariable falseVar() override { return d_minisat->falseVar(); } |
93 |
|
|
94 |
|
void markUnremovable(SatLiteral lit) override; |
95 |
|
|
96 |
|
void interrupt() override; |
97 |
|
|
98 |
|
SatValue solve() override; |
99 |
|
SatValue solve(long unsigned int&) override; |
100 |
|
bool ok() const override; |
101 |
|
void getUnsatCore(SatClause& unsatCore) override; |
102 |
|
|
103 |
|
SatValue value(SatLiteral l) override; |
104 |
|
SatValue modelValue(SatLiteral l) override; |
105 |
|
|
106 |
|
void unregisterVar(SatLiteral lit); |
107 |
|
void renewVar(SatLiteral lit, int level = -1); |
108 |
|
unsigned getAssertionLevel() const override; |
109 |
|
|
110 |
|
// helper methods for converting from the internal Minisat representation |
111 |
|
|
112 |
|
static SatVariable toSatVariable(BVMinisat::Var var); |
113 |
|
static BVMinisat::Lit toMinisatLit(SatLiteral lit); |
114 |
|
static SatLiteral toSatLiteral(BVMinisat::Lit lit); |
115 |
|
static SatValue toSatLiteralValue(BVMinisat::lbool res); |
116 |
|
|
117 |
|
static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); |
118 |
|
static void toSatClause (const BVMinisat::Clause& clause, SatClause& sat_clause); |
119 |
|
void addMarkerLiteral(SatLiteral lit) override; |
120 |
|
|
121 |
|
void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) override; |
122 |
|
|
123 |
|
SatValue assertAssumption(SatLiteral lit, bool propagate) override; |
124 |
|
|
125 |
|
void popAssumption() override; |
126 |
|
|
127 |
|
private: |
128 |
|
/* Disable the default constructor. */ |
129 |
|
BVMinisatSatSolver() = delete; |
130 |
|
|
131 |
9422 |
class Statistics { |
132 |
|
public: |
133 |
|
ReferenceStat<int64_t> d_statStarts, d_statDecisions; |
134 |
|
ReferenceStat<int64_t> d_statRndDecisions, d_statPropagations; |
135 |
|
ReferenceStat<int64_t> d_statConflicts, d_statClausesLiterals; |
136 |
|
ReferenceStat<int64_t> d_statLearntsLiterals, d_statMaxLiterals; |
137 |
|
ReferenceStat<int64_t> d_statTotLiterals; |
138 |
|
ReferenceStat<int64_t> d_statEliminatedVars; |
139 |
|
IntStat d_statCallsToSolve; |
140 |
|
TimerStat d_statSolveTime; |
141 |
|
bool d_registerStats = true; |
142 |
|
Statistics(StatisticsRegistry& registry, const std::string& prefix); |
143 |
|
void init(BVMinisat::SimpSolver* minisat); |
144 |
|
void deinit(); |
145 |
|
}; |
146 |
|
|
147 |
|
Statistics d_statistics; |
148 |
|
}; |
149 |
|
|
150 |
|
} // namespace prop |
151 |
|
} // namespace cvc5 |