63c17f5130507ee3840d3b1cfdbb2ab8a044361c
1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: taking, dejan, cconway
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 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
19 #include "cvc4_private.h"
21 #ifndef __CVC4__PROP__SAT_H
22 #define __CVC4__PROP__SAT_H
24 // Just defining this for now, since there's no other SAT solver bindings.
25 // Optional blocks below will be unconditionally included
26 #define __CVC4_USE_MINISAT
28 #include "util/options.h"
29 #include "util/stats.h"
30 #include "theory/theory.h"
32 #ifdef __CVC4_USE_MINISAT
34 #include "prop/minisat/core/Solver.h"
35 #include "prop/minisat/core/SolverTypes.h"
36 #include "prop/minisat/simp/SimpSolver.h"
38 #endif /* __CVC4_USE_MINISAT */
49 /* Definitions of abstract types and conversion functions for SAT interface */
51 #ifdef __CVC4_USE_MINISAT
53 /** Type of the SAT variables */
54 typedef Minisat::Var SatVariable
;
56 /** Type of the Sat literals */
57 typedef Minisat::Lit SatLiteral
;
59 /** Type of the SAT clauses */
60 typedef Minisat::vec
<SatLiteral
> SatClause
;
62 typedef Minisat::lbool SatLiteralValue
;
65 * Returns the variable of the literal.
66 * @param lit the literal
68 inline SatVariable
literalToVariable(SatLiteral lit
) {
69 return Minisat::var(lit
);
72 inline bool literalSign(SatLiteral lit
) {
73 return Minisat::sign(lit
);
77 hashSatLiteral(const SatLiteral
& literal
) {
78 return (size_t) Minisat::toInt(literal
);
81 inline std::string
stringOfLiteralValue(SatLiteralValue val
) {
82 if( val
== l_False
) {
84 } else if (val
== l_True
) {
90 #endif /* __CVC4_USE_MINISAT */
92 /** Interface encapsulating the "input" to the solver, e.g., from the
95 * TODO: Is it possible to push the typedefs of SatClause and SatVariable
98 class SatInputInterface
{
100 /** Virtual destructor to make g++ happy */
101 virtual ~SatInputInterface() { }
102 /** Assert a clause in the solver. */
103 virtual void addClause(SatClause
& clause
, bool lemma
) = 0;
104 /** Create a new boolean variable in the solver. */
105 virtual SatVariable
newVar(bool theoryAtom
= false) = 0;
109 * The proxy class that allows us to modify the internals of the SAT solver.
110 * It's only accessible from the PropEngine, and should be treated with major
113 class SatSolver
: public SatInputInterface
{
115 /** The prop engine we are using */
116 PropEngine
* d_propEngine
;
118 /** The CNF engine we are using */
119 CnfStream
* d_cnfStream
;
121 /** The theory engine we are using */
122 TheoryEngine
* d_theoryEngine
;
124 /** Context we will be using to synchronzie the sat solver */
125 context::Context
* d_context
;
127 /** Remember the options */
130 /* Pointer to the concrete SAT solver. Including this via the
131 preprocessor saves us a level of indirection vs, e.g., defining a
132 sub-class for each solver. */
134 #ifdef __CVC4_USE_MINISAT
136 /** Minisat solver */
137 Minisat::SimpSolver
* d_minisat
;
141 ReferenceStat
<uint64_t> d_statStarts
, d_statDecisions
;
142 ReferenceStat
<uint64_t> d_statRndDecisions
, d_statPropagations
;
143 ReferenceStat
<uint64_t> d_statConflicts
, d_statClausesLiterals
;
144 ReferenceStat
<uint64_t> d_statLearntsLiterals
, d_statMaxLiterals
;
145 ReferenceStat
<uint64_t> d_statTotLiterals
;
148 d_statStarts("sat::starts"),
149 d_statDecisions("sat::decisions"),
150 d_statRndDecisions("sat::rnd_decisions"),
151 d_statPropagations("sat::propagations"),
152 d_statConflicts("sat::conflicts"),
153 d_statClausesLiterals("sat::clauses_literals"),
154 d_statLearntsLiterals("sat::learnts_literals"),
155 d_statMaxLiterals("sat::max_literals"),
156 d_statTotLiterals("sat::tot_literals")
158 StatisticsRegistry::registerStat(&d_statStarts
);
159 StatisticsRegistry::registerStat(&d_statDecisions
);
160 StatisticsRegistry::registerStat(&d_statRndDecisions
);
161 StatisticsRegistry::registerStat(&d_statPropagations
);
162 StatisticsRegistry::registerStat(&d_statConflicts
);
163 StatisticsRegistry::registerStat(&d_statClausesLiterals
);
164 StatisticsRegistry::registerStat(&d_statLearntsLiterals
);
165 StatisticsRegistry::registerStat(&d_statMaxLiterals
);
166 StatisticsRegistry::registerStat(&d_statTotLiterals
);
169 StatisticsRegistry::unregisterStat(&d_statStarts
);
170 StatisticsRegistry::unregisterStat(&d_statDecisions
);
171 StatisticsRegistry::unregisterStat(&d_statRndDecisions
);
172 StatisticsRegistry::unregisterStat(&d_statPropagations
);
173 StatisticsRegistry::unregisterStat(&d_statConflicts
);
174 StatisticsRegistry::unregisterStat(&d_statClausesLiterals
);
175 StatisticsRegistry::unregisterStat(&d_statLearntsLiterals
);
176 StatisticsRegistry::unregisterStat(&d_statMaxLiterals
);
177 StatisticsRegistry::unregisterStat(&d_statTotLiterals
);
179 void init(Minisat::SimpSolver
* d_minisat
){
180 d_statStarts
.setData(d_minisat
->starts
);
181 d_statDecisions
.setData(d_minisat
->decisions
);
182 d_statRndDecisions
.setData(d_minisat
->rnd_decisions
);
183 d_statPropagations
.setData(d_minisat
->propagations
);
184 d_statConflicts
.setData(d_minisat
->conflicts
);
185 d_statClausesLiterals
.setData(d_minisat
->clauses_literals
);
186 d_statLearntsLiterals
.setData(d_minisat
->learnts_literals
);
187 d_statMaxLiterals
.setData(d_minisat
->max_literals
);
188 d_statTotLiterals
.setData(d_minisat
->tot_literals
);
191 Statistics d_statistics
;
193 #endif /* __CVC4_USE_MINISAT */
198 /** Hash function for literals */
199 struct SatLiteralHashFunction
{
200 inline size_t operator()(const SatLiteral
& literal
) const;
203 SatSolver(PropEngine
* propEngine
,
204 TheoryEngine
* theoryEngine
,
205 context::Context
* context
,
206 const Options
* options
);
212 void addClause(SatClause
& clause
, bool lemma
);
214 SatVariable
newVar(bool theoryAtom
= false);
216 void theoryCheck(theory::Theory::Effort effort
, SatClause
& conflict
);
218 void explainPropagation(SatLiteral l
, SatClause
& explanation
);
220 void theoryPropagate(std::vector
<SatLiteral
>& output
);
222 void clearPropagatedLiterals();
224 void enqueueTheoryLiteral(const SatLiteral
& l
);
226 void setCnfStream(CnfStream
* cnfStream
);
228 SatLiteralValue
value(SatLiteral l
);
231 /* Functions that delegate to the concrete SAT solver. */
233 #ifdef __CVC4_USE_MINISAT
235 inline SatSolver::SatSolver(PropEngine
* propEngine
, TheoryEngine
* theoryEngine
,
236 context::Context
* context
, const Options
* options
) :
237 d_propEngine(propEngine
),
239 d_theoryEngine(theoryEngine
),
244 d_minisat
= new Minisat::SimpSolver(this, d_context
);
245 // Setup the verbosity
246 d_minisat
->verbosity
= (options
->verbosity
> 0) ? 1 : -1;
249 if(Debug
.isOn("no_rnd_decisions")){
250 d_minisat
->random_var_freq
= 0;
253 d_statistics
.init(d_minisat
);
256 inline SatSolver::~SatSolver() {
260 inline bool SatSolver::solve() {
261 return d_minisat
->solve();
264 inline void SatSolver::addClause(SatClause
& clause
, bool lemma
) {
265 d_minisat
->addClause(clause
, lemma
? Minisat::Solver::CLAUSE_LEMMA
: Minisat::Solver::CLAUSE_PROBLEM
);
268 inline SatVariable
SatSolver::newVar(bool theoryAtom
) {
269 return d_minisat
->newVar(true, true, theoryAtom
);
272 inline SatLiteralValue
SatSolver::value(SatLiteral l
) {
273 return d_minisat
->modelValue(l
);
276 #endif /* __CVC4_USE_MINISAT */
279 SatSolver::SatLiteralHashFunction::operator()(const SatLiteral
& literal
) const {
280 return hashSatLiteral(literal
);
283 }/* CVC4::prop namespace */
285 inline std::ostream
& operator <<(std::ostream
& out
, prop::SatLiteral lit
) {
286 const char * s
= (prop::literalSign(lit
)) ? "~" : " ";
287 out
<< s
<< prop::literalToVariable(lit
);
291 inline std::ostream
& operator <<(std::ostream
& out
, const prop::SatClause
& clause
) {
293 for(int i
= 0; i
< clause
.size(); ++i
) {
294 out
<< " " << clause
[i
];
300 inline std::ostream
& operator <<(std::ostream
& out
, prop::SatLiteralValue val
) {
301 out
<< prop::stringOfLiteralValue(val
);
305 }/* CVC4 namespace */
307 #endif /* __CVC4__PROP__SAT_H */