CVC3
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
decision_engine.cpp
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file decision_engine.cpp
4
* \brief Decision Engine
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Sun Jul 13 22:44:55 2003
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
22
23
#include "
decision_engine.h
"
24
#include "
theory_core.h
"
25
#include "
search.h
"
26
27
28
using namespace
std;
29
using namespace
CVC3;
30
31
32
DecisionEngine::DecisionEngine(
TheoryCore
* core,
SearchImplBase
* se)
33
: d_core(core), d_se(se),
34
d_splitters(core->getCM()->getCurrentContext()),
35
d_splitterCount(core->getStatistics().counter(
"splitters"
))
36
{
37
IF_DEBUG
(
d_splitters
.setName(
"CDList[SearchEngineDefault.d_splitters]"
);)
38
}
39
40
/*****************************************************************************/
41
/*!
42
* Function: DecisionEngine::findSplitterRec
43
*
44
* Author: Clark Barrett
45
*
46
* Created: Sun Jul 13 22:47:06 2003
47
*
48
* Search the expression e (depth-first) for an atomic formula. Note that in
49
* order to support the "simplify in-place" option, each sub-expression is
50
* checked to see if it has a find pointer, and if it does, the find is
51
* followed instead of continuing to recurse on the given expression.
52
* \return a NULL expr if no atomic formula is found.
53
*/
54
/*****************************************************************************/
55
Expr
DecisionEngine::findSplitterRec
(
const
Expr
& e)
56
{
57
Expr
best;
58
59
if
(
d_visited
.
count
(e) > 0)
60
return
d_visited
[e];
61
62
if
(e.
isTrue
() || e.
isFalse
() || e.
isAtomic
()
63
|| !
d_se
->
isGoodSplitter
(e)) {
64
d_visited
[e] = best;
65
return
best;
66
}
67
68
if
(e.
isAbsAtomicFormula
()) {
69
d_visited
[e] = e;
70
return
e;
71
}
72
73
ExprMap<Expr>::iterator
it =
d_bestByExpr
.
find
(e);
74
if
(it !=
d_bestByExpr
.
end
()) {
75
d_visited
[e] = it->second;
76
return
it->second;
77
}
78
79
vector<int> order(e.
arity
());
80
int
i = 0;
81
82
if
(e.
isITE
())
83
{
84
order[i++] = 0;
85
order[i++] = 1;
//e.getHighestKid(); // always 1 or 2
86
order[i++] = 2;
//3 - e.getHighestKid();
87
}
88
89
else
90
{
91
if
(e.
arity
() > 0)
92
{
93
order[i++] = 0;
//e.getHighestKid();
94
for
(
int
k = 0; k < e.
arity
(); ++k)
95
if
(k != 0)
//e.getHighestKid())
96
order[i++] = k;
97
}
98
}
99
100
for
(
int
k = 0; k < e.
arity
(); k++)
101
{
102
Expr
splitter =
103
findSplitterRec
(
d_core
->
findExpr
(e[order[k]]));
104
if
(!splitter.
isNull
() && (best.
isNull
() ||
isBetter
(splitter, best)))
105
best = splitter;
106
}
107
108
d_bestByExpr
[e] = best;
109
d_visited
[e] = best;
110
return
best;
111
}
112
113
114
/*****************************************************************************/
115
/*!
116
* Function: DecisionEngine::pushDecision
117
*
118
* Author: Clark Barrett
119
*
120
* Created: Sun Jul 13 22:55:16 2003
121
*
122
* \param splitter
123
* \param whichCase If true, increment the splitter count and assert the
124
* splitter. If false, do NOT increment the splitter count and assert the
125
* negation of the splitter. Defaults to true.
126
*/
127
/*****************************************************************************/
128
void
DecisionEngine::pushDecision
(
Expr
splitter,
bool
whichCase)
129
{
130
string
stCase = whichCase ?
"TRUE"
:
"FALSE"
;
131
if
(whichCase)
d_splitterCount
++;
132
d_core
->
getCM
()->
push
();
133
TRACE
(
"search trace"
,
"Asserting splitter("
+stCase+
"): "
, splitter,
""
);
134
TRACE
(
"search"
,
"Asserting splitter("
+stCase+
"): "
, splitter,
""
);
135
d_splitters
.
push_back
(splitter);
136
if
(!whichCase)
137
splitter = splitter.
negate
();
138
Theorem
thm =
d_se
->
newIntAssumption
(splitter);
139
d_core
->
addFact
(thm);
140
// Search engine needs to know what original facts it derived or
141
// split on, so that we don't split on them twice. addFact() may
142
// simplify these facts before calling addLiteralFact() and lose
143
// this information. There is no reason to add non-literals though,
144
// as we never split on them directly.
145
if
(thm.
getExpr
().
isAbsLiteral
())
146
d_se
->
addLiteralFact
(thm);
147
}
148
149
150
void
DecisionEngine::popDecision
()
151
{
152
d_core
->
getCM
()->
pop
();
153
TRACE
(
"search trace"
,
"Pop: scope level ="
,
d_core
->
getCM
()->
scopeLevel
(),
""
);
154
}
155
156
157
void
DecisionEngine::popTo
(
int
dl)
158
{
159
d_core
->
getCM
()->
popto
(dl);
160
TRACE
(
"search trace"
,
"Popto: scope level ="
,
d_core
->
getCM
()->
scopeLevel
(),
""
);
161
}
162
163
164
Expr
DecisionEngine::lastSplitter
()
165
{
166
return
d_splitters
.
back
();
167
}
Generated on Thu May 16 2013 13:25:13 for CVC3 by
1.8.2