CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
cnf_manager.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file cnf_manager.h
4
*\brief Manager for conversion to and traversal of CNF formulas
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Thu Dec 15 13:53:16 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_manager_h_
22
#define _cvc3__include__cnf_manager_h_
23
24
#include "
cnf.h
"
25
#include "
expr.h
"
26
#include "
expr_map.h
"
27
#include "
cdmap.h
"
28
#include "
statistics.h
"
29
30
namespace
CVC3 {
31
32
class
CommonProofRules;
33
class
CNF_Rules;
34
class
ValidityChecker;
35
class
Statistics;
36
37
}
38
39
namespace
SAT {
40
41
class
CNF_Manager
{
42
43
//! For clause minimization
44
CVC3::ValidityChecker
*
d_vc
;
45
46
//! Whether to use brute-force clause minimization
47
bool
d_minimizeClauses
;
48
49
//! Common proof rules
50
CVC3::CommonProofRules
*
d_commonRules
;
51
52
//! Rules for manipulating CNF
53
CVC3::CNF_Rules
*
d_rules
;
54
55
//! Information kept for each CNF variable
56
struct
Varinfo
{
57
CVC3::Expr
expr
;
58
std::vector<Lit>
fanins
;
59
std::vector<Var>
fanouts
;
60
};
61
62
//! vector that maps a variable index to information for that variable
63
std::vector<Varinfo>
d_varInfo
;
64
65
//! Map from Exprs to Vars representing those Exprs
66
CVC3::ExprHashMap<Var>
d_cnfVars
;
67
68
//! Cached translation of term-ite-containing expressions
69
CVC3::ExprHashMap<CVC3::Theorem>
d_iteMap
;
70
71
//! Map of possibly useful lemmas
72
// CVC3::ExprMap<int> d_usefulLemmas;
73
74
//! Maps a clause id to the theorem justifying that clause
75
/*! Note that clauses created by simple CNF translation are not given id's.
76
* This is because theorems for these clauses can be created lazily later. */
77
// CVC3::CDMap<int, CVC3::Theorem> d_theorems;
78
// CVC3::CDMap<int, CVC3::Theorem> d_theorems;
79
80
//! Next clause id
81
int
d_clauseIdNext
;
82
83
//! Whether expr has already been translated
84
// CVC3::CDMap<CVC3::Expr, bool> d_translated;
85
86
//! Bottom scope in which translation is valid
87
int
d_bottomScope
;
88
89
//! Queue of theorems to translate
90
std::deque<CVC3::Theorem>
d_translateQueueThms
;
91
92
//! Queue of fanouts corresponding to thms to translate
93
std::deque<Var>
d_translateQueueVars
;
94
95
//! Whether thm to translate is "translate only"
96
std::deque<bool>
d_translateQueueFlags
;
97
98
//! Reference to statistics object
99
CVC3::Statistics
&
d_statistics
;
100
101
//! Reference to command-line flags
102
const
CVC3::CLFlags
&
d_flags
;
103
104
//! Reference to null Expr
105
const
CVC3::Expr
&
d_nullExpr
;
106
107
public
:
108
//! Abstract class for callbacks
109
class
CNFCallback
{
110
public
:
111
CNFCallback
() {}
112
virtual
~CNFCallback
() {}
113
//! Register an atom
114
virtual
void
registerAtom
(
const
CVC3::Expr
& e,
115
const
CVC3::Theorem
& thm) = 0;
116
};
117
118
private
:
119
//! Instance of CNF_CallBack: must be registered
120
CNFCallback
*
d_cnfCallback
;
121
122
CVC3::CNF_Rules
*
createProofRules
(
CVC3::TheoremManager
* tm,
const
CVC3::CLFlags
&);
123
124
//! Register a new atomic formula
125
void
registerAtom
(
const
CVC3::Expr
& e,
const
CVC3::Theorem
& thm);
126
127
//! Return the expr corresponding to the literal unless the expr is TRUE of FALSE
128
CVC3::Expr
concreteExpr
(
const
CVC3::Expr
& e,
const
Lit
& literal);
129
130
//! Return the theorem if e is not as concreteExpr(e).
131
CVC3::Theorem
concreteThm
(
const
CVC3::Expr
& e);
132
133
//! Recursively translate e into cnf
134
/*! A non-context dependent cache, d_cnfVars is used to remember translations
135
* of expressions. A context-dependent attribute, isTranslated, is used to
136
* remember whether an expression has been translated in the current context */
137
Lit
translateExprRec
(
const
CVC3::Expr
& e,
CNF_Formula
& cnf,
138
const
CVC3::Theorem
& thmIn);
139
140
//! Recursively traverse an expression with an embedded term ITE
141
/*! Term ITE's are handled by introducing a skolem variable for the ITE term
142
* and then adding new constraints describing the ITE in terms of the new variable.
143
*/
144
CVC3::Theorem
replaceITErec
(
const
CVC3::Expr
& e,
Var
v,
bool
translateOnly);
145
146
//! Recursively translate e into cnf
147
/*! Call translateExprRec. If additional expressions are queued up,
148
* translate them too, until none are left. */
149
Lit
translateExpr
(
const
CVC3::Theorem
& thmIn,
CNF_Formula
& cnf);
150
151
// bool isTranslated(const CVC3::Expr& e)
152
// { CVC3::CDMap<CVC3::Expr, bool>::iterator i = d_translated.find(e);
153
// return i != d_translated.end() && (*i).second; }
154
// void setTranslated(const CVC3::Expr& e)
155
// { DebugAssert(!isTranslated(e),"already set");
156
// d_translated.insert(e, true, d_bottomScope); }
157
// void clearTranslated(const CVC3::Expr& e)
158
// { d_translated.insert(e, false, d_bottomScope); }
159
160
public
:
161
CNF_Manager
(
CVC3::TheoremManager
* tm,
CVC3::Statistics
& statistics,
162
const
CVC3::CLFlags
& flags);
163
~CNF_Manager
();
164
165
//! Register CNF callback
166
void
registerCNFCallback
(
CNFCallback
* cnfCallback)
167
{
d_cnfCallback
= cnfCallback; }
168
169
//! Set scope for translation
170
void
setBottomScope
(
int
scope) {
d_bottomScope
= scope; }
171
172
//! Return the number of variables being managed
173
unsigned
numVars
() {
return
d_varInfo
.size(); }
174
175
//! Return number of fanins for CNF node c
176
/*! A CNF node x is a fanin of CNF node y if the expr for x is a child of the
177
* expr for y or if y is an ITE leaf and x is a new CNF node obtained by
178
* translating the ITE leaf y.
179
* \sa isITELeaf()
180
*/
181
unsigned
numFanins
(
Var
c) {
182
if
(!c.
isVar
())
return
0;
183
if
(
unsigned
(c) >=
d_varInfo
.size())
return
0;
184
return
d_varInfo
[c].fanins.size();
185
}
186
187
//! Returns the ith fanin of c.
188
Lit
getFanin
(
Var
c,
unsigned
i) {
189
DebugAssert
(i <
numFanins
(c),
"attempt to access unknown fanin"
);
190
return
d_varInfo
[c].fanins[i];
191
}
192
193
//! Return number of fanins for c
194
/*! x is a fanout of y if y is a fanin of x
195
* \sa numFanins
196
*/
197
unsigned
numFanouts
(
Var
c) {
198
if
(!c.
isVar
())
return
0;
199
if
(
unsigned
(c) >=
d_varInfo
.size())
return
0;
200
return
d_varInfo
[c].fanouts.size();
201
}
202
203
//! Returns the ith fanout of c.
204
Lit
getFanout
(
Var
c,
unsigned
i) {
205
DebugAssert
(i <
numFanouts
(c),
"attempt to access unknown fanin"
);
206
return
Lit
(
d_varInfo
[c].fanouts[i]);
207
}
208
209
//! Convert a CNF literal to an Expr literal
210
/*! Returns a NULL Expr if there is no corresponding Expr for l
211
*/
212
const
CVC3::Expr
&
concreteVar
(
Var
v) {
213
if
(v.
isNull
())
return
d_nullExpr
;
214
if
(
unsigned
(v) >=
d_varInfo
.size() ||
215
(!
d_varInfo
[v].expr.isTranslated()))
216
return
d_nullExpr
;
217
return
d_varInfo
[v].expr;
218
}
219
220
//! Convert a CNF literal to an Expr literal
221
/*! Returns a NULL Expr if there is no corresponding Expr for l
222
*/
223
CVC3::Expr
concreteLit
(
Lit
l,
bool
checkTranslated =
true
) {
224
if
(l.
isNull
())
return
d_nullExpr
;
225
bool
inverted = !l.
isPositive
();
226
int
index = l.
getVar
();
227
if
((
unsigned
)index >=
d_varInfo
.size() ||
228
(checkTranslated && !
d_varInfo
[index].expr.isTranslated()))
229
return
d_nullExpr
;
230
return
inverted ? !
d_varInfo
[index].expr :
d_varInfo
[index].expr;
231
}
232
233
//! Look up the CNF literal for an Expr
234
/*! Returns a NULL Lit if there is no corresponding CNF literal for e
235
*/
236
Lit
getCNFLit
(
const
CVC3::Expr
& e) {
237
if
(e.
isFalse
())
return
Lit::getFalse
();
238
if
(e.
isTrue
())
return
Lit::getTrue
();
239
if
(e.
isNot
())
return
!
getCNFLit
(e[0]);
240
CVC3::ExprHashMap<Var>::iterator
i =
d_cnfVars
.find(e);
241
if
(!e.
isTranslated
() || i ==
d_cnfVars
.end())
return
Lit
();
242
return
Lit
((*i).second);
243
}
244
245
void
cons
(
unsigned
lb,
unsigned
ub,
const
CVC3::Expr
& e2, std::vector<unsigned>& newLits);
246
247
//! Convert thm A |- B (A is a set of literals) into one or more clauses
248
/*! cnf should be empty -- it will be filled with the result */
249
void
convertLemma
(
const
CVC3::Theorem
& thm,
CNF_Formula
& cnf);
250
251
//! Given thm of form A |- B, convert B to CNF and add it to cnf
252
/*! Returns Lit corresponding to the root of the expression that was
253
* translated. */
254
Lit
addAssumption
(
const
CVC3::Theorem
& thm,
CNF_Formula
& cnf);
255
256
//! Convert thm to CNF and add it to the current formula
257
/*! \param thm should be of form A |- B where A is a set of literals.
258
* \param cnf the new clauses are added to cnf.
259
* Returns Lit corresponding to the root of the expression that was
260
* translated. */
261
Lit
addLemma
(
CVC3::Theorem
thm,
CNF_Formula
& cnf);
262
263
};
264
265
}
266
267
#endif
Generated on Tue May 14 2013 15:43:24 for CVC3 by
1.8.3.1