CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
clause.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file clause.h
4
*
5
* Author: Sergey Berezin
6
*
7
* Created: Fri Mar 7 16:03:38 2003
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
* Class to represent a clause, which is a disjunction of formulas
19
* which are literals for conflict clauses, and possibly more complex
20
* formulas for the clauses derived from the user-asserted formulas.
21
*
22
* class Clause is implemented as a smart pointer to ClauseValue, so
23
* it can be freely copied and assigned with low overhead (like
24
* Theorem or Expr).
25
*/
26
/*****************************************************************************/
27
28
// Include it before ifndef, since it includes this file recursively
29
#ifndef DOXYGEN
30
#include "
variable.h
"
31
#endif
32
33
#ifndef _cvc3__include__clause_h_
34
#define _cvc3__include__clause_h_
35
36
namespace
CVC3 {
37
38
class
Clause;
39
class
ClauseOwner;
40
class
TheoryCore;
41
42
class
ClauseValue
{
43
friend
class
Clause
;
44
private
:
45
//! Ref. counter
46
int
d_refcount
;
47
//! Ref. counter of ClauseOwner classes holding it
48
int
d_refcountOwner
;
49
// The original clause (disjunction of literals)
50
Theorem
d_thm
;
51
// Scope where the clause is valid
52
int
d_scope
;
53
// Theorems l_i <=> l'_i for each literal l_i
54
// FIXME: more efficient implementation for fixed arrays of CDOs
55
std::vector<Literal>
d_literals
;
56
// Disallow copy constructor and assignment (make private)
57
ClauseValue
(
const
ClauseValue
& c);
// Undefined (since it cannot be used)
58
ClauseValue
&
operator=
(
const
ClauseValue
& c) {
return
*
this
; }
59
// Pointers to watched literals (Watch Pointers). They are not
60
// backtrackable.
61
size_t
d_wp
[2];
62
// Direction flags for the watch pointers (1 or -1)
63
// FIXME: should we use one bit of d_wp{1,2} instead? (efficiency
64
// vs. space)
65
int
d_dir
[2];
66
// A flag indicating that the clause is shown satisfiable
67
CDO<bool>
d_sat
;
68
// Marks the clause as deleted
69
bool
d_deleted
;
70
// Creation file and line number (for debugging)
71
IF_DEBUG
(std::string d_file;
int
d_line;)
72
// Constructor: takes the main clause theorem which must be a
73
// disjunction of literals and have no assumptions.
74
ClauseValue
(
TheoryCore
* core,
VariableManager
* vm,
75
const
Theorem
& clause,
int
scope);
76
public
:
77
// Destructor
78
~ClauseValue
();
79
80
};
// end of class ClauseValue
81
82
//! A class representing a CNF clause (a smart pointer)
83
class
Clause
{
84
private
:
85
friend
class
ClauseOwner
;
86
//! The only value member
87
ClauseValue
*
d_clause
;
88
//! Export owner refcounting to ClauseOwner
89
int
&
countOwner
() {
90
DebugAssert
(
d_clause
!= NULL,
""
);
91
return
d_clause
->
d_refcountOwner
;
92
}
93
public
:
94
Clause
():
d_clause
(NULL) { }
95
// Constructors
96
Clause
(
TheoryCore
* core,
VariableManager
* vm,
const
Theorem
& clause,
97
int
scope,
const
std::string& file =
""
,
int
line = 0)
98
:
d_clause
(new
ClauseValue
(core, vm, clause, scope)) {
99
d_clause
->
d_refcount
++;
100
IF_DEBUG
(
d_clause
->d_file = file;
d_clause
->d_line=line;)
101
}
102
// Copy constructor
103
Clause
(
const
Clause
& c):
d_clause
(c.
d_clause
) {
104
if
(
d_clause
!= NULL)
d_clause
->
d_refcount
++;
105
}
106
// Destructor
107
~Clause
();
108
// Assignment operator
109
Clause
&
operator=
(
const
Clause
& c);
110
111
bool
isNull
()
const
{
return
d_clause
== NULL; }
112
// Other public methods
113
size_t
size
()
const
{
114
return
(
d_clause
== NULL)? 0 :
d_clause
->
d_literals
.size();
115
}
116
// Get the theorem representing the entire clause
117
const
Theorem
&
getTheorem
()
const
{
118
DebugAssert
(!
isNull
(),
"Clause::getTheorem(): Null Clause"
);
119
return
d_clause
->
d_thm
;
120
}
121
// Get the scope where the clause is valid
122
int
getScope
()
const
{
123
if
(
isNull
())
return
0;
124
else
return
d_clause
->
d_scope
;
125
}
126
// Get the current value of the i-th literal
127
const
Literal
&
getLiteral
(
size_t
i)
const
{
128
DebugAssert
(!
isNull
(),
"Clause::getLiteral(): Null Clause"
);
129
DebugAssert
(i <
size
(),
130
"Clause::getLiteral("
+
int2string
(i)
131
+
"): i >= size = "
+
int2string
(
size
()));
132
return
d_clause
->
d_literals
[i];
133
}
134
// Get the current value of the i-th literal
135
const
Literal
&
operator[]
(
size_t
i)
const
{
return
getLiteral
(i); }
136
137
// Get the reference to the vector of literals, for fast access
138
const
std::vector<Literal>&
getLiterals
()
const
{
139
DebugAssert
(!
isNull
(),
"Clause::getLiterals(): Null Clause"
);
140
return
d_clause
->
d_literals
;
141
}
142
// Get the values of watch pointers
143
size_t
wp
(
int
i)
const
{
144
DebugAssert
(!
isNull
(),
"Clause::wp(i): Null Clause"
);
145
DebugAssert
(i==0 || i==1,
146
"wp(i): Watch pointer index is out of bounds: i = "
147
+
int2string
(i));
148
return
d_clause
->
d_wp
[i];
149
}
150
// Get the watched literals
151
const
Literal
&
watched
(
int
i)
const
{
return
getLiteral
(
wp
(i)); }
152
// Set the watch pointers and return the new value
153
size_t
wp
(
int
i,
size_t
l)
const
{
154
DebugAssert
(!
isNull
(),
"Clause::wp(i,l): Null Clause"
);
155
DebugAssert
(i==0 || i==1,
156
"wp(i,l): Watch pointer index is out of bounds: i = "
157
+
int2string
(i));
158
DebugAssert
(l <
size
(),
"Clause::wp(i = "
+
int2string
(i)
159
+
", l = "
+
int2string
(l)
160
+
"): l >= size() = "
+
int2string
(
size
()));
161
TRACE
(
"clauses"
,
" **clauses** UPDATE wp(idx="
162
+
int2string
(i)+
", l="
+
int2string
(l),
163
")\n clause #: "
,
id
());
164
d_clause
->
d_wp
[i] = l;
165
return
l;
166
}
167
// Get the direction of the i-th watch pointer
168
int
dir
(
int
i)
const
{
169
DebugAssert
(!
isNull
(),
"Clause::dir(i): Null Clause"
);
170
DebugAssert
(i==0 || i==1,
171
"dir(i): Watch pointer index is out of bounds: i = "
172
+
int2string
(i));
173
return
d_clause
->
d_dir
[i];
174
}
175
// Set the direction of the i-th watch pointer
176
int
dir
(
int
i,
int
d)
const
{
177
DebugAssert
(!
isNull
(),
"Clause::dir(i,d): Null Clause"
);
178
DebugAssert
(i==0 || i==1,
179
"dir(i="
+
int2string
(i)+
",d="
+
int2string
(d)
180
+
"): Watch pointer index is out of bounds"
);
181
DebugAssert
(d==1 || d==-1,
"dir(i="
+
int2string
(i)+
",d="
+
int2string
(d)
182
+
"): Direction is out of bounds"
);
183
d_clause
->
d_dir
[i] = d;
184
return
d;
185
}
186
//! Check if the clause marked as SAT
187
bool
sat
()
const
{
188
DebugAssert
(!
isNull
(),
"Clause::sat()"
);
189
return
d_clause
->
d_sat
;
190
}
191
//! Precise version of sat(): check all the literals and cache the result
192
bool
sat
(
bool
ignored)
const
{
193
DebugAssert
(!
isNull
(),
"Clause::sat()"
);
194
bool
flag =
false
;
195
if
(!
d_clause
->
d_sat
) {
196
for
(
size_t
i = 0; !flag && i <
d_clause
->
d_literals
.size(); ++i)
197
if
(
d_clause
->
d_literals
[i].getValue() == 1)
198
flag =
true
;
199
}
200
if
(flag) {
201
//std::cout << "*** Manually marking SAT" << std::endl;
202
markSat
();
203
}
204
return
d_clause
->
d_sat
;
205
}
206
// Mark the clause as SAT
207
void
markSat
()
const
{
208
DebugAssert
(!
isNull
(),
"Clause::markSat()"
);
209
d_clause
->
d_sat
=
true
;
210
}
211
// Check / mark the clause as deleted
212
bool
deleted
()
const
{
213
DebugAssert
(!
isNull
(),
"Clause::deleted()"
);
214
return
d_clause
->
d_deleted
;
215
}
216
void
markDeleted
()
const
;
217
218
// For debugging: return some kind of unique ID
219
size_t
id
()
const
{
return
(
size_t
)
d_clause
; }
220
221
// Equality: compare the pointers
222
bool
operator==
(
const
Clause
& c)
const
{
return
d_clause
== c.
d_clause
; }
223
224
//! Tell how many owners this clause has (for debugging)
225
int
owners
()
const
{
return
d_clause
->
d_refcountOwner
; }
226
227
// Printing
228
std::string
toString
()
const
;
229
230
friend
std::ostream&
operator<<
(std::ostream& os,
const
Clause
& c);
231
232
IF_DEBUG
(
bool
wpCheck()
const
;)
233
IF_DEBUG
(
const
std::string& getFile()
const
{
return
d_clause
->d_file; })
234
IF_DEBUG
(
int
getLine()
const
{
return
d_clause
->d_line; })
235
236
};
// end of class Clause
237
238
//! Same as class Clause, but when destroyed, marks the clause as deleted
239
/*! Needed for backtraking data structures. When the SAT solver
240
backtracks, some clauses will be thrown away automatically, and we
241
need to mark those as deleted. */
242
class
ClauseOwner
{
243
Clause
d_clause
;
244
//! Disable default constructor
245
ClauseOwner
() { }
246
public
:
247
//! Constructor from class Clause
248
ClauseOwner
(
const
Clause
& c):
d_clause
(c) {
d_clause
.countOwner()++; }
249
//! Construct a new Clause
250
ClauseOwner
(
TheoryCore
* core,
VariableManager
* vm,
const
Theorem
& clause,
251
int
scope):
d_clause
(core, vm, clause, scope) {
252
d_clause
.countOwner()++;
253
}
254
//! Copy constructor (keep track of refcounts)
255
ClauseOwner
(
const
ClauseOwner
& c):
d_clause
(c.
d_clause
) {
256
d_clause
.countOwner()++;
257
}
258
//! Assignment (keep track of refcounts)
259
ClauseOwner
&
operator=
(
const
ClauseOwner
& c) {
260
if
(&c ==
this
)
return
*
this
;
// Seft-assignment
261
DebugAssert
(
d_clause
.countOwner() > 0,
"in operator="
);
262
if
(--(
d_clause
.countOwner()) == 0)
263
d_clause
.markDeleted();
264
d_clause
= c.
d_clause
;
265
d_clause
.countOwner()++;
266
return
*
this
;
267
}
268
//! Destructor: mark the clause as deleted
269
~ClauseOwner
() {
270
FatalAssert
(
d_clause
.countOwner() > 0,
"in ~ClauseOwner"
);
271
if
(--(
d_clause
.countOwner()) == 0) {
272
d_clause
.markDeleted();
273
}
274
}
275
//! Automatic type conversion to Clause ref
276
operator
Clause
& () {
return
d_clause
; }
277
//! Automatic type conversion to Clause const ref
278
operator
const
Clause
& ()
const
{
return
d_clause
; }
279
};
// end of class ClauseOwner
280
281
282
// I/O Manipulators
283
284
// Print clause in a compact form: Clause[x=-1@scope, ...], mark
285
// watched literals by '*'
286
class
CompactClause
{
287
private
:
288
Clause
d_clause
;
289
public
:
290
CompactClause
(
const
Clause
& c):
d_clause
(c) { }
291
friend
std::ostream&
operator<<
(std::ostream& os,
const
CompactClause
& c);
292
std::string
toString
()
const
;
293
};
294
295
}
// end of namespace CVC3
296
297
#endif
Generated on Sun Aug 5 2012 13:18:32 for CVC3 by
1.8.1.2