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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
|
/********************* */
/** cnf_stream.h
** Original author: taking
** Major contributors: dejan
** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 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.
**
** This class takes a sequence of formulas.
** It outputs a stream of clauses that is propositional
** equisatisfiable with the conjunction of the formulas.
** This stream is maintained in an online fashion.
**
** Unlike other parts of the system it is aware of the PropEngine's
** internals such as the representation and translation of
**/
#include "cvc4_private.h"
#ifndef __CVC4__CNF_STREAM_H
#define __CVC4__CNF_STREAM_H
#include "expr/node.h"
#include "prop/sat.h"
#include <ext/hash_map>
namespace CVC4 {
namespace prop {
class PropEngine;
/**
* Comments for the behavior of the whole class...
* @author Tim King <taking@cs.nyu.edu>
*/
class CnfStream {
private:
/** The SAT solver we will be using */
SatSolver *d_satSolver;
/** Cache of what literal have been registered to a node. */
typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
TranslationCache d_translationCache;
/** Cache of what nodes have been registered to a literal. */
typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
NodeCache d_nodeCache;
protected:
/**
* Asserts the given clause to the sat solver.
* @param clause the clasue to assert
*/
void assertClause(SatClause& clause);
/**
* Asserts the unit clause to the sat solver.
* @param a the unit literal of the clause
*/
void assertClause(SatLiteral a);
/**
* Asserts the binary clause to the sat solver.
* @param a the first literal in the clause
* @param b the second literal in the clause
*/
void assertClause(SatLiteral a, SatLiteral b);
/**
* Asserts the ternary clause to the sat solver.
* @param a the first literal in the clause
* @param b the second literal in the clause
* @param c the thirs literal in the clause
*/
void assertClause(SatLiteral a, SatLiteral b, SatLiteral c);
/**
* Returns true if the node has been cashed in the translation cache.
* @param node the node
* @return true if the node has been cached
*/
bool isCached(TNode node) const;
/**
* Returns the cashed literal corresponding to the given node.
* @param node the node to lookup
* @return returns the corresponding literal
*/
SatLiteral lookupInCache(TNode n) const;
/**
* Caches the pair of the node and the literal corresponding to the
* translation.
* @param node node
* @param lit
*/
void cacheTranslation(TNode node, SatLiteral lit);
/**
* Acquires a new variable from the SAT solver to represent the node and
* inserts the necessary data it into the mapping tables.
* @param node a formula
* @param theoryLiteral is this literal a theory literal (i.e. theory to be
* informed when set to true/false
* @return the literal corresponding to the formula
*/
SatLiteral newLiteral(TNode node, bool theoryLiteral = false);
public:
/**
* Constructs a CnfStream that sends constructs an equi-satisfiable set of clauses
* and sends them to the given sat solver.
* @param satSolver the sat solver to use
*/
CnfStream(SatSolver* satSolver);
/**
* Destructs a CnfStream. This implementation does nothing, but we
* need a virtual destructor for safety in case subclasses have a
* destructor.
*/
virtual ~CnfStream() {
}
/**
* Converts and asserts a formula.
* @param node node to convert and assert
* @param whether the sat solver can choose to remove this clause
*/
virtual void convertAndAssert(TNode node) = 0;
/**
* Returns a node the is represented by a give SatLiteral literal.
* @param literal the literal from the sat solver
* @return the actual node
*/
Node getNode(const SatLiteral& literal);
/**
* Returns the literal the represents the given node in the SAT CNF
* representation.
*/
SatLiteral getLiteral(TNode node);
}; /* class CnfStream */
/**
* TseitinCnfStream is based on the following recursive algorithm
* http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
* The general gist of the algorithm is to introduce a new literal that
* will be equivalent to each subexpression in the constructed equisatisfiable
* formula then substitute the new literal for the formula, and to do this
* recursively.
*
* This implementation does this in a single recursive pass.
*/
class TseitinCnfStream : public CnfStream {
public:
/**
* Convert a given formula to CNF and assert it to the SAT solver.
* @param node the formula to assert
*/
void convertAndAssert(TNode node);
/**
* Constructs the stream to use the given sat solver.
* @param satSolver the sat solver to use
*/
TseitinCnfStream(SatSolver* satSolver);
private:
// Each of these formulas handles takes care of a Node of each Kind.
//
// Each handleX(Node &n) is responsible for:
// - constructing a new literal, l (if necessary)
// - calling registerNode(n,l)
// - adding clauses assure that l is equivalent to the Node
// - calling toCNF on its children (if necessary)
// - returning l
//
// handleX( n ) can assume that n is not in d_translationCache
SatLiteral handleAtom(TNode node);
SatLiteral handleNot(TNode node);
SatLiteral handleXor(TNode node);
SatLiteral handleImplies(TNode node);
SatLiteral handleIff(TNode node);
SatLiteral handleIte(TNode node);
SatLiteral handleAnd(TNode node);
SatLiteral handleOr(TNode node);
/**
* Transforms the node into CNF recursively.
* @param node the formula to transform
* @return the literal representing the root of the formula
*/
SatLiteral toCNF(TNode node);
}; /* class TseitinCnfStream */
}/* prop namespace */
}/* CVC4 namespace */
#endif /* __CVC4__CNF_STREAM_H */
|
