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
DecisionEngine(TheoryCore * core,SearchImplBase * se)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 /*****************************************************************************/
findSplitterRec(const Expr & e)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 /*****************************************************************************/
pushDecision(Expr splitter,bool whichCase)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
popDecision()150 void DecisionEngine::popDecision()
151 {
152 d_core->getCM()->pop();
153 TRACE("search trace", "Pop: scope level =", d_core->getCM()->scopeLevel(), "");
154 }
155
156
popTo(int dl)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
lastSplitter()164 Expr DecisionEngine::lastSplitter()
165 {
166 return d_splitters.back();
167 }
168