CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
cnf.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file cnf.h
4
*\brief Basic classes for reasoning about formulas in CNF
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Mon Dec 12 20:32:33 2005
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*/
19
/*****************************************************************************/
20
21
#ifndef _cvc3__include__cnf_h_
22
#define _cvc3__include__cnf_h_
23
24
#include <deque>
25
#include "
compat_hash_map.h
"
26
#include "
cvc_util.h
"
27
#include "
cdo.h
"
28
#include "
cdlist.h
"
29
#include "
theorem.h
"
30
31
32
namespace
SAT {
33
34
class
Var
{
35
int
d_index
;
36
public
:
37
enum
Val
{
UNKNOWN
= -1,
FALSE_VAL
,
TRUE_VAL
};
38
static
Val
invertValue
(
Val
);
39
Var
() :
d_index
(-1) {}
40
Var
(
int
index) :
d_index
(index) {}
41
operator
int() {
return
d_index
; }
42
bool
isNull
()
const
{
return
d_index
== -1; }
43
void
reset
() {
d_index
= -1; }
44
int
getIndex
()
const
{
return
d_index
; }
45
bool
isVar
()
const
{
return
d_index
> 0; }
46
bool
operator==
(
const
Var
& var)
const
{
return
(
d_index
== var.
d_index
); }
47
};
48
inline
Var::Val
Var::invertValue
(
Var::Val
v)
49
{
return
v ==
Var::UNKNOWN
?
Var::UNKNOWN
:
Var::Val
(1-v); }
50
51
class
Lit
{
52
int
d_index
;
53
static
Lit
mkLit
(
int
index) {
Lit
l; l.
d_index
= index;
return
l; }
54
public
:
55
Lit
() :
d_index
(0) {}
56
explicit
Lit
(
Var
v,
bool
positive=
true
) {
57
if
(v.
isNull
())
d_index
= 0;
58
else
d_index
= positive ? v+1 : -v-1;
59
}
60
static
Lit
getTrue
() {
return
mkLit
(1); }
61
static
Lit
getFalse
() {
return
mkLit
(-1); }
62
63
bool
isNull
()
const
{
return
d_index
== 0; }
64
bool
isPositive
()
const
{
return
d_index
> 1; }
65
bool
isInverted
()
const
{
return
d_index
< -1; }
66
bool
isFalse
()
const
{
return
d_index
== -1; }
67
bool
isTrue
()
const
{
return
d_index
== 1; }
68
bool
isVar
()
const
{
return
abs
(
d_index
) > 1; }
69
int
getID
()
const
{
return
d_index
; }
70
Var
getVar
()
const
{
71
DebugAssert
(
isVar
(),
"Bad call to Lit::getVar"
);
72
return
abs
(
d_index
)-1;
73
}
74
void
reset
() {
d_index
= 0; }
75
friend
Lit
operator!
(
const
Lit
& lit) {
return
mkLit
(-lit.
d_index
); }
76
};
77
78
class
Clause
{
79
int
d_satisfied
:1;
80
int
d_unit
:1;
81
std::vector<Lit>
d_lits
;
82
CVC3::Theorem
d_reason
;
//the theorem for the clause, used in proofs. by yeting
83
84
public
:
85
86
Clause
():
d_satisfied
(0),
d_unit
(0) { };
87
88
Clause
(
const
Clause
& clause)
89
:
d_satisfied
(clause.
d_satisfied
),
d_unit
(clause.
d_unit
),
90
d_lits
(clause.
d_lits
),
d_reason
(clause.
d_reason
) { };
91
92
typedef
std::vector<Lit>::const_iterator
const_iterator
;
93
const_iterator
begin
()
const
{
return
d_lits
.begin(); }
94
const_iterator
end
()
const
{
return
d_lits
.end(); }
95
96
void
clear
() {
d_satisfied
=
d_unit
= 0;
d_lits
.clear(); }
97
unsigned
size
()
const
{
return
d_lits
.size(); }
98
void
addLiteral
(
Lit
l) {
if
(!
d_satisfied
)
d_lits
.push_back(l); }
99
unsigned
getMaxVar
()
const
;
100
bool
isSatisfied
()
const
{
return
d_satisfied
!= 0; }
101
bool
isUnit
()
const
{
return
d_unit
!= 0; }
102
bool
isNull
()
const
{
return
d_lits
.size() == 0; }
103
void
setSatisfied
() {
d_satisfied
= 1; }
104
void
setUnit
() {
d_unit
= 1; }
105
void
print
()
const
;
106
void
setClauseTheorem
(
CVC3::Theorem
thm){
d_reason
= thm;}
107
108
CVC3::Theorem
getClauseTheorem
()
const
{
return
d_reason
;}
109
};
110
111
112
class
CNF_Formula
{
113
protected
:
114
Clause
*
d_current
;
115
116
virtual
void
setNumVars
(
unsigned
numVars
) = 0;
117
void
copy
(
const
CNF_Formula
& cnf);
118
119
public
:
120
CNF_Formula
() :
d_current
(NULL) {}
121
virtual
~CNF_Formula
() {}
122
123
typedef
std::deque<Clause>::const_iterator
const_iterator
;
124
125
virtual
bool
empty
()
const
= 0;
126
virtual
const
Clause
&
operator[]
(
int
i)
const
= 0;
127
virtual
const_iterator
begin
()
const
= 0;
128
virtual
const_iterator
end
()
const
= 0;
129
virtual
unsigned
numVars
()
const
= 0;
130
virtual
unsigned
numClauses
()
const
= 0;
131
virtual
void
newClause
() = 0;
132
virtual
void
registerUnit
() = 0;
133
134
void
addLiteral
(
Lit
l,
bool
invert=
false
)
135
{
if
(l.
isVar
() && unsigned(l.
getVar
()) >
numVars
())
136
setNumVars
(l.
getVar
());
137
d_current
->
addLiteral
(invert ? !l : l); }
138
Clause
&
getCurrentClause
() {
return
*
d_current
; }
139
void
print
()
const
;
140
const
CNF_Formula
&
operator+=
(
const
CNF_Formula
& cnf);
141
const
CNF_Formula
&
operator+=
(
const
Clause
& c);
142
};
143
144
145
class
CNF_Formula_Impl
:
public
CNF_Formula
{
146
std::hash_map<int, bool>
d_lits
;
147
std::deque<Clause>
d_formula
;
148
unsigned
d_numVars
;
149
private
:
150
void
setNumVars
(
unsigned
numVars
) {
d_numVars
=
numVars
; }
151
public
:
152
CNF_Formula_Impl
() :
CNF_Formula
(),
d_numVars
(0) {}
153
CNF_Formula_Impl
(
const
CNF_Formula
& cnf) :
CNF_Formula
() {
copy
(cnf); }
154
~CNF_Formula_Impl
() {};
155
156
bool
empty
()
const
{
return
d_formula
.empty(); }
157
const
Clause
&
operator[]
(
int
i)
const
{
return
d_formula
[i]; }
158
const_iterator
begin
()
const
{
return
d_formula
.begin(); }
159
const_iterator
end
()
const
{
return
d_formula
.end(); }
160
unsigned
numVars
()
const
{
return
d_numVars
; }
161
unsigned
numClauses
()
const
{
return
d_formula
.size(); }
162
void
deleteLast
() {
DebugAssert
(
d_formula
.size() > 0,
"size == 0"
);
d_formula
.pop_back(); }
163
void
newClause
();
164
void
registerUnit
();
165
166
void
simplify
();
167
void
reset
();
168
};
169
170
171
class
CD_CNF_Formula
:
public
CNF_Formula
{
172
CVC3::CDList<Clause>
d_formula
;
173
CVC3::CDO<unsigned>
d_numVars
;
174
private
:
175
void
setNumVars
(
unsigned
numVars
) {
d_numVars
=
numVars
; }
176
public
:
177
CD_CNF_Formula
(
CVC3::Context
* context)
178
:
CNF_Formula
(),
d_formula
(context),
d_numVars
(context, 0, 0) {}
179
~CD_CNF_Formula
() {}
180
181
bool
empty
()
const
{
return
d_formula
.empty(); }
182
const
Clause
&
operator[]
(
int
i)
const
{
return
d_formula
[i]; }
183
const_iterator
begin
()
const
{
return
d_formula
.begin(); }
184
const_iterator
end
()
const
{
return
d_formula
.end(); }
185
unsigned
numVars
()
const
{
return
d_numVars
.
get
(); }
186
unsigned
numClauses
()
const
{
return
d_formula
.size(); }
187
void
deleteLast
() {
d_formula
.pop_back(); }
188
189
void
newClause
();
190
void
registerUnit
();
191
};
192
193
}
194
195
#endif
Generated on Tue May 14 2013 14:44:51 for CVC3 by
1.8.3.1