blob: f34699e2b4485d121031c286164fcd9b797a1fb7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
/********************* */
/*! \file sat.cpp
** \verbatim
** Original author: cconway
** Major contributors: dejan, mdeters, taking
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/sat.h"
#include "context/context.h"
#include "theory/theory_engine.h"
#include "expr/expr_stream.h"
namespace CVC4 {
namespace prop {
void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) {
Assert(conflict.size() == 0);
// Try theory propagation
bool ok = d_theoryEngine->check(effort);
// If in conflict construct the conflict clause
if (!ok) {
// We have a conflict, get it
Node conflictNode = d_theoryEngine->getConflict();
Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
if(conflictNode.getKind() == kind::AND) {
// Go through the literals and construct the conflict clause
Node::const_iterator literal_it = conflictNode.begin();
Node::const_iterator literal_end = conflictNode.end();
while (literal_it != literal_end) {
// Get the literal corresponding to the node
SatLiteral l = d_cnfStream->getLiteral(*literal_it);
// Add the negation to the conflict clause and continue
conflict.push(~l);
literal_it ++;
}
} else { // unit conflict
// Get the literal corresponding to the node
SatLiteral l = d_cnfStream->getLiteral(conflictNode);
// construct the unit conflict clause
conflict.push(~l);
}
}
}
void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {
// Propagate
d_theoryEngine->propagate();
// Get the propagated literals
const std::vector<TNode>& outputNodes = d_theoryEngine->getPropagatedLiterals();
// If any literals, make a clause
const unsigned i_end = outputNodes.size();
for (unsigned i = 0; i < i_end; ++ i) {
Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl;
SatLiteral l = d_cnfStream->getLiteral(outputNodes[i]);
output.push_back(l);
}
}
void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) {
TNode lNode = d_cnfStream->getNode(l);
Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
if (theoryExplanation.getKind() == kind::AND) {
Node::const_iterator it = theoryExplanation.begin();
Node::const_iterator it_end = theoryExplanation.end();
explanation.push(l);
for (; it != it_end; ++ it) {
explanation.push(~d_cnfStream->getLiteral(*it));
}
} else {
explanation.push(l);
explanation.push(~d_cnfStream->getLiteral(theoryExplanation));
}
}
void SatSolver::clearPropagatedLiterals() {
d_theoryEngine->clearPropagatedLiterals();
}
void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
Node literalNode = d_cnfStream->getNode(l);
Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
Assert(!literalNode.isNull());
d_theoryEngine->assertFact(literalNode);
}
void SatSolver::setCnfStream(CnfStream* cnfStream) {
d_cnfStream = cnfStream;
}
void SatSolver::removeClausesAboveLevel(int level) {
d_cnfStream->removeClausesAboveLevel(level);
}
TNode SatSolver::getNode(SatLiteral lit) {
return d_cnfStream->getNode(lit);
}
void SatSolver::notifyRestart() {
d_theoryEngine->notifyRestart();
}
SatLiteral SatSolver::getNextReplayDecision() {
#ifdef CVC4_REPLAY
if(Options::current()->replayStream != NULL) {
Expr e = Options::current()->replayStream->nextExpr();
if(!e.isNull()) { // we get null node when out of decisions to replay
// convert & return
return d_cnfStream->getLiteral(e);
}
}
#endif /* CVC4_REPLAY */
return Minisat::lit_Undef;
}
void SatSolver::logDecision(SatLiteral lit) {
#ifdef CVC4_REPLAY
if(Options::current()->replayLog != NULL) {
Assert(lit != Minisat::lit_Undef, "logging an `undef' decision ?!");
*Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
}
#endif /* CVC4_REPLAY */
}
}/* CVC4::prop namespace */
}/* CVC4 namespace */
|
