1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Kshitij Bansal, Andres Noetzli, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Justification heuristic for decision making |
14 |
|
* |
15 |
|
* A ATGP-inspired justification-based decision heuristic. This code is based |
16 |
|
* on the CVC3 implementation of the same heuristic -- note below. |
17 |
|
* |
18 |
|
* It needs access to the simplified but non-clausal formula. |
19 |
|
*/ |
20 |
|
#include "justification_heuristic.h" |
21 |
|
|
22 |
|
#include "decision/decision_attributes.h" |
23 |
|
#include "decision/decision_engine_old.h" |
24 |
|
#include "expr/kind.h" |
25 |
|
#include "expr/node_manager.h" |
26 |
|
#include "options/decision_options.h" |
27 |
|
#include "smt/smt_statistics_registry.h" |
28 |
|
#include "smt/term_formula_removal.h" |
29 |
|
#include "theory/rewriter.h" |
30 |
|
#include "util/random.h" |
31 |
|
|
32 |
|
using namespace cvc5::prop; |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
namespace decision { |
36 |
|
|
37 |
|
JustificationHeuristic::JustificationHeuristic(DecisionEngineOld* de, |
38 |
|
context::UserContext* uc, |
39 |
|
context::Context* c) |
40 |
|
: ITEDecisionStrategy(de, c), |
41 |
|
d_justified(c), |
42 |
|
d_exploredThreshold(c), |
43 |
|
d_prvsIndex(c, 0), |
44 |
|
d_threshPrvsIndex(c, 0), |
45 |
|
d_helpfulness( |
46 |
|
smtStatisticsRegistry().registerInt("decision::jh::helpfulness")), |
47 |
|
d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")), |
48 |
|
d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")), |
49 |
|
d_assertions(uc), |
50 |
|
d_skolemAssertions(uc), |
51 |
|
d_skolemCache(uc), |
52 |
|
d_visited(), |
53 |
|
d_visitedComputeSkolems(), |
54 |
|
d_curDecision(), |
55 |
|
d_curThreshold(0), |
56 |
|
d_childCache(uc), |
57 |
|
d_weightCache(uc), |
58 |
|
d_startIndexCache(c) |
59 |
|
{ |
60 |
|
Trace("decision") << "Justification heuristic enabled" << std::endl; |
61 |
|
} |
62 |
|
|
63 |
|
JustificationHeuristic::~JustificationHeuristic() {} |
64 |
|
|
65 |
|
cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch) |
66 |
|
{ |
67 |
|
if(options::decisionThreshold() > 0) { |
68 |
|
bool stopSearchTmp = false; |
69 |
|
prop::SatLiteral lit = |
70 |
|
getNextThresh(stopSearchTmp, options::decisionThreshold()); |
71 |
|
if (lit != prop::undefSatLiteral) |
72 |
|
{ |
73 |
|
Assert(stopSearchTmp == false); |
74 |
|
return lit; |
75 |
|
} |
76 |
|
Assert(stopSearchTmp == true); |
77 |
|
} |
78 |
|
return getNextThresh(stopSearch, 0); |
79 |
|
} |
80 |
|
|
81 |
|
cvc5::prop::SatLiteral JustificationHeuristic::getNextThresh( |
82 |
|
bool& stopSearch, DecisionWeight threshold) |
83 |
|
{ |
84 |
|
Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<<threshold<<")" << std::endl; |
85 |
|
TimerStat::CodeTimer codeTimer(d_timestat); |
86 |
|
|
87 |
|
d_visited.clear(); |
88 |
|
d_curThreshold = threshold; |
89 |
|
|
90 |
|
if(Trace.isOn("justified")) { |
91 |
|
for(JustifiedSet::key_iterator i = d_justified.key_begin(); |
92 |
|
i != d_justified.key_end(); ++i) { |
93 |
|
TNode n = *i; |
94 |
|
prop::SatLiteral l = d_decisionEngine->hasSatLiteral(n) |
95 |
|
? d_decisionEngine->getSatLiteral(n) |
96 |
|
: -1; |
97 |
|
prop::SatValue v = tryGetSatValue(n); |
98 |
|
Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl; |
99 |
|
} |
100 |
|
} |
101 |
|
|
102 |
|
for(unsigned i = getPrvsIndex(); i < d_assertions.size(); ++i) { |
103 |
|
Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl; |
104 |
|
|
105 |
|
// Sanity check: if it was false, aren't we inconsistent? |
106 |
|
// Commenting out. See bug 374. In short, to do with how CNF stream works. |
107 |
|
// Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); |
108 |
|
|
109 |
|
prop::SatValue desiredVal = prop::SAT_VALUE_TRUE; |
110 |
|
prop::SatLiteral litDecision; |
111 |
|
|
112 |
|
litDecision = findSplitter(d_assertions[i], desiredVal); |
113 |
|
|
114 |
|
if (litDecision != prop::undefSatLiteral) |
115 |
|
{ |
116 |
|
setPrvsIndex(i); |
117 |
|
Trace("decision") << "jh: splitting on " << litDecision << std::endl; |
118 |
|
++d_helpfulness; |
119 |
|
return litDecision; |
120 |
|
} |
121 |
|
} |
122 |
|
|
123 |
|
Trace("decision") << "jh: Nothing to split on " << std::endl; |
124 |
|
|
125 |
|
#if defined CVC5_DEBUG |
126 |
|
bool alljustified = true; |
127 |
|
for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) { |
128 |
|
TNode curass = d_assertions[i]; |
129 |
|
while(curass.getKind() == kind::NOT) |
130 |
|
curass = curass[0]; |
131 |
|
alljustified &= checkJustified(curass); |
132 |
|
|
133 |
|
if(Debug.isOn("decision")) { |
134 |
|
if(!checkJustified(curass)) |
135 |
|
Debug("decision") << "****** Not justified [i="<<i<<"]: " |
136 |
|
<< d_assertions[i] << std::endl; |
137 |
|
} |
138 |
|
} |
139 |
|
Assert(alljustified || d_curThreshold != 0); |
140 |
|
#endif |
141 |
|
|
142 |
|
// SAT solver can stop... |
143 |
|
stopSearch = true; |
144 |
|
if (d_curThreshold == 0) d_decisionEngine->setResult(prop::SAT_VALUE_TRUE); |
145 |
|
return prop::undefSatLiteral; |
146 |
|
} |
147 |
|
|
148 |
|
inline void computeXorIffDesiredValues(Kind k, |
149 |
|
prop::SatValue desiredVal, |
150 |
|
prop::SatValue& desiredVal1, |
151 |
|
prop::SatValue& desiredVal2) |
152 |
|
{ |
153 |
|
Assert(k == kind::EQUAL || k == kind::XOR); |
154 |
|
|
155 |
|
bool shouldInvert = |
156 |
|
(desiredVal == prop::SAT_VALUE_TRUE && k == kind::EQUAL) |
157 |
|
|| (desiredVal == prop::SAT_VALUE_FALSE && k == kind::XOR); |
158 |
|
|
159 |
|
if (desiredVal1 == prop::SAT_VALUE_UNKNOWN |
160 |
|
&& desiredVal2 == prop::SAT_VALUE_UNKNOWN) |
161 |
|
{ |
162 |
|
// CHOICE: pick one of them arbitarily |
163 |
|
desiredVal1 = prop::SAT_VALUE_FALSE; |
164 |
|
} |
165 |
|
|
166 |
|
if(desiredVal2 == SAT_VALUE_UNKNOWN) { |
167 |
|
desiredVal2 = shouldInvert ? invertValue(desiredVal1) : desiredVal1; |
168 |
|
} else if(desiredVal1 == SAT_VALUE_UNKNOWN) { |
169 |
|
desiredVal1 = shouldInvert ? invertValue(desiredVal2) : desiredVal2; |
170 |
|
} |
171 |
|
} |
172 |
|
|
173 |
|
void JustificationHeuristic::addAssertion(TNode assertion) |
174 |
|
{ |
175 |
|
// Save all assertions locally, including the assertions generated by term |
176 |
|
// removal. We have to make sure that we assign a value to all the Boolean |
177 |
|
// term variables. To illustrate why this is, consider the case where we have |
178 |
|
// a single assertion |
179 |
|
// |
180 |
|
// (or (f a) (f b)) |
181 |
|
// |
182 |
|
// where `f` is a function `Bool -> Bool`. Given an assignment: |
183 |
|
// |
184 |
|
// (f a) -> true |
185 |
|
// (f b) -> false |
186 |
|
// a -> false |
187 |
|
// |
188 |
|
// UF will not complain and the justification heuristic considers the |
189 |
|
// assertion to be satisifed. However, we also have to make sure that we pick |
190 |
|
// a value for `b` that is not in conflict with the other assignments (we can |
191 |
|
// only choose `b` to be `true` otherwise the model is incorrect). |
192 |
|
d_assertions.push_back(assertion); |
193 |
|
} |
194 |
|
|
195 |
|
void JustificationHeuristic::addSkolemDefinition(TNode lem, TNode skolem) |
196 |
|
{ |
197 |
|
Trace("decision::jh::ite") |
198 |
|
<< " jh-ite: " << skolem << " maps to " << lem << std::endl; |
199 |
|
d_skolemAssertions[skolem] = lem; |
200 |
|
} |
201 |
|
|
202 |
|
SatLiteral JustificationHeuristic::findSplitter(TNode node, |
203 |
|
SatValue desiredVal) |
204 |
|
{ |
205 |
|
d_curDecision = undefSatLiteral; |
206 |
|
findSplitterRec(node, desiredVal); |
207 |
|
return d_curDecision; |
208 |
|
} |
209 |
|
|
210 |
|
|
211 |
|
void JustificationHeuristic::setJustified(TNode n) |
212 |
|
{ |
213 |
|
d_justified.insert(n); |
214 |
|
} |
215 |
|
|
216 |
|
bool JustificationHeuristic::checkJustified(TNode n) |
217 |
|
{ |
218 |
|
return d_justified.find(n) != d_justified.end(); |
219 |
|
} |
220 |
|
|
221 |
|
DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n) |
222 |
|
{ |
223 |
|
return d_exploredThreshold.find(n) == d_exploredThreshold.end() |
224 |
|
? std::numeric_limits<DecisionWeight>::max() |
225 |
|
: d_exploredThreshold[n]; |
226 |
|
} |
227 |
|
|
228 |
|
void JustificationHeuristic::setExploredThreshold(TNode n) |
229 |
|
{ |
230 |
|
d_exploredThreshold[n] = d_curThreshold; |
231 |
|
} |
232 |
|
|
233 |
|
int JustificationHeuristic::getPrvsIndex() |
234 |
|
{ |
235 |
|
if(d_curThreshold == 0) |
236 |
|
return d_prvsIndex; |
237 |
|
else |
238 |
|
return d_threshPrvsIndex; |
239 |
|
} |
240 |
|
|
241 |
|
void JustificationHeuristic::setPrvsIndex(int prvsIndex) |
242 |
|
{ |
243 |
|
if(d_curThreshold == 0) |
244 |
|
d_prvsIndex = prvsIndex; |
245 |
|
else |
246 |
|
d_threshPrvsIndex = prvsIndex; |
247 |
|
} |
248 |
|
|
249 |
|
DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satValue) |
250 |
|
{ |
251 |
|
Assert(satValue == SAT_VALUE_TRUE || satValue == SAT_VALUE_FALSE); |
252 |
|
return getWeightPolarized(n, satValue == SAT_VALUE_TRUE); |
253 |
|
} |
254 |
|
|
255 |
|
DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity) |
256 |
|
{ |
257 |
|
if (options::decisionWeightInternal() |
258 |
|
!= options::DecisionWeightInternal::USR1) |
259 |
|
{ |
260 |
|
return getWeight(n); |
261 |
|
} |
262 |
|
|
263 |
|
if(d_weightCache.find(n) == d_weightCache.end()) { |
264 |
|
Kind k = n.getKind(); |
265 |
|
theory::TheoryId tId = theory::kindToTheoryId(k); |
266 |
|
DecisionWeight dW1, dW2; |
267 |
|
if(tId != theory::THEORY_BOOL) { |
268 |
|
dW1 = dW2 = getWeight(n); |
269 |
|
} else { |
270 |
|
|
271 |
|
if(k == kind::OR) { |
272 |
|
dW1 = std::numeric_limits<DecisionWeight>::max(), dW2 = 0; |
273 |
|
for(TNode::iterator i=n.begin(); i != n.end(); ++i) { |
274 |
|
dW1 = std::min(dW1, getWeightPolarized(*i, true)); |
275 |
|
dW2 = std::max(dW2, getWeightPolarized(*i, false)); |
276 |
|
} |
277 |
|
} else if(k == kind::AND) { |
278 |
|
dW1 = 0, dW2 = std::numeric_limits<DecisionWeight>::max(); |
279 |
|
for(TNode::iterator i=n.begin(); i != n.end(); ++i) { |
280 |
|
dW1 = std::max(dW1, getWeightPolarized(*i, true)); |
281 |
|
dW2 = std::min(dW2, getWeightPolarized(*i, false)); |
282 |
|
} |
283 |
|
} else if(k == kind::IMPLIES) { |
284 |
|
dW1 = std::min(getWeightPolarized(n[0], false), |
285 |
|
getWeightPolarized(n[1], true)); |
286 |
|
dW2 = std::max(getWeightPolarized(n[0], true), |
287 |
|
getWeightPolarized(n[1], false)); |
288 |
|
} else if(k == kind::NOT) { |
289 |
|
dW1 = getWeightPolarized(n[0], false); |
290 |
|
dW2 = getWeightPolarized(n[0], true); |
291 |
|
} else { |
292 |
|
dW1 = 0; |
293 |
|
for(TNode::iterator i=n.begin(); i != n.end(); ++i) { |
294 |
|
dW1 = std::max(dW1, getWeightPolarized(*i, true)); |
295 |
|
dW1 = std::max(dW1, getWeightPolarized(*i, false)); |
296 |
|
} |
297 |
|
dW2 = dW1; |
298 |
|
} |
299 |
|
|
300 |
|
} |
301 |
26820 |
d_weightCache[n] = std::make_pair(dW1, dW2); |
302 |
|
} |
303 |
|
return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second; |
304 |
|
} |
305 |
|
|
306 |
|
DecisionWeight JustificationHeuristic::getWeight(TNode n) { |
307 |
|
if(!n.hasAttribute(DecisionWeightAttr()) ) { |
308 |
|
options::DecisionWeightInternal combiningFn = |
309 |
|
options::decisionWeightInternal(); |
310 |
|
|
311 |
|
if (combiningFn == options::DecisionWeightInternal::OFF |
312 |
|
|| n.getNumChildren() == 0) |
313 |
|
{ |
314 |
|
if (options::decisionRandomWeight() != 0) |
315 |
|
{ |
316 |
|
n.setAttribute(DecisionWeightAttr(), |
317 |
|
Random::getRandom().pick(0, options::decisionRandomWeight()-1)); |
318 |
|
} |
319 |
|
} |
320 |
|
else if (combiningFn == options::DecisionWeightInternal::MAX) |
321 |
|
{ |
322 |
|
DecisionWeight dW = 0; |
323 |
|
for (TNode::iterator i = n.begin(); i != n.end(); ++i) |
324 |
|
dW = std::max(dW, getWeight(*i)); |
325 |
|
n.setAttribute(DecisionWeightAttr(), dW); |
326 |
|
} |
327 |
|
else if (combiningFn == options::DecisionWeightInternal::SUM |
328 |
|
|| combiningFn == options::DecisionWeightInternal::USR1) |
329 |
|
{ |
330 |
|
DecisionWeight dW = 0; |
331 |
|
for (TNode::iterator i = n.begin(); i != n.end(); ++i) |
332 |
|
dW = std::max(dW, getWeight(*i)); |
333 |
|
n.setAttribute(DecisionWeightAttr(), dW); |
334 |
|
} |
335 |
|
else |
336 |
|
{ |
337 |
|
Unreachable(); |
338 |
|
} |
339 |
|
} |
340 |
|
return n.getAttribute(DecisionWeightAttr()); |
341 |
|
} |
342 |
|
|
343 |
|
typedef std::vector<TNode> ChildList; |
344 |
|
TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) { |
345 |
|
if(options::decisionUseWeight()) { |
346 |
|
// TODO: Optimize storing & access |
347 |
|
if(d_childCache.find(n) == d_childCache.end()) { |
348 |
|
ChildList list0(n.begin(), n.end()), list1(n.begin(), n.end()); |
349 |
|
std::sort(list0.begin(), list0.end(), JustificationHeuristic::myCompareClass(this,false)); |
350 |
|
std::sort(list1.begin(), list1.end(), JustificationHeuristic::myCompareClass(this,true)); |
351 |
|
d_childCache[n] = make_pair(list0, list1); |
352 |
|
} |
353 |
|
return polarity ? d_childCache[n].get().second[i] : d_childCache[n].get().first[i]; |
354 |
|
} else { |
355 |
|
return n[i]; |
356 |
|
} |
357 |
|
} |
358 |
|
|
359 |
|
SatValue JustificationHeuristic::tryGetSatValue(Node n) |
360 |
|
{ |
361 |
|
Debug("decision") << " " << n << " has sat value " << " "; |
362 |
|
if(d_decisionEngine->hasSatLiteral(n) ) { |
363 |
|
Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl; |
364 |
|
return d_decisionEngine->getSatValue(n); |
365 |
|
} else { |
366 |
|
Debug("decision") << "NO SAT LITERAL" << std::endl; |
367 |
|
return SAT_VALUE_UNKNOWN; |
368 |
|
}//end of else |
369 |
|
} |
370 |
|
|
371 |
|
JustificationHeuristic::SkolemList JustificationHeuristic::getSkolems(TNode n) |
372 |
|
{ |
373 |
|
SkolemCache::iterator it = d_skolemCache.find(n); |
374 |
|
if (it != d_skolemCache.end()) |
375 |
|
{ |
376 |
|
return (*it).second; |
377 |
|
} |
378 |
|
else |
379 |
|
{ |
380 |
|
// Compute the list of Skolems |
381 |
|
// TODO: optimize by avoiding multiple lookup for d_skolemCache[n] |
382 |
|
d_visitedComputeSkolems.clear(); |
383 |
|
SkolemList ilist; |
384 |
|
computeSkolems(n, ilist); |
385 |
|
d_skolemCache.insert(n, ilist); |
386 |
|
return ilist; |
387 |
|
} |
388 |
|
} |
389 |
|
|
390 |
|
void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l) |
391 |
|
{ |
392 |
|
Trace("decision::jh::skolems") << " computeSkolems( " << n << ", &l)\n"; |
393 |
|
d_visitedComputeSkolems.insert(n); |
394 |
|
for(unsigned i=0; i<n.getNumChildren(); ++i) { |
395 |
|
SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]); |
396 |
|
if (it2 != d_skolemAssertions.end()) |
397 |
|
{ |
398 |
|
l.push_back(std::make_pair(n[i], (*it2).second)); |
399 |
|
Assert(n[i].getNumChildren() == 0); |
400 |
|
} |
401 |
|
if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end()) |
402 |
|
{ |
403 |
|
computeSkolems(n[i], l); |
404 |
|
} |
405 |
|
} |
406 |
|
} |
407 |
|
|
408 |
|
JustificationHeuristic::SearchResult |
409 |
|
JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) |
410 |
|
{ |
411 |
|
/** |
412 |
|
* Main idea |
413 |
|
* |
414 |
|
* Given a boolean formula "node", the goal is to try to make it |
415 |
|
* evaluate to "desiredVal" (true/false). for instance if "node" is a OR |
416 |
|
* formula we want to make it evaluate to true, we'd like one of the |
417 |
|
* children to be true. this is done recursively. |
418 |
|
*/ |
419 |
|
|
420 |
|
Trace("decision::jh") |
421 |
|
<< "findSplitterRec(" << node << ", " |
422 |
|
<< desiredVal << ", .. )" << std::endl; |
423 |
|
|
424 |
|
/* Handle NOT as a special case */ |
425 |
|
while (node.getKind() == kind::NOT) { |
426 |
|
desiredVal = invertValue(desiredVal); |
427 |
|
node = node[0]; |
428 |
|
} |
429 |
|
|
430 |
|
/* Base case */ |
431 |
|
if (checkJustified(node)) { |
432 |
|
Debug("decision::jh") << " justified, returning" << std::endl; |
433 |
|
return NO_SPLITTER; |
434 |
|
} |
435 |
|
if (getExploredThreshold(node) < d_curThreshold) { |
436 |
|
Debug("decision::jh") << " explored, returning" << std::endl; |
437 |
|
Assert(d_curThreshold != 0); |
438 |
|
return DONT_KNOW; |
439 |
|
} |
440 |
|
|
441 |
|
#if defined CVC5_ASSERTIONS || defined CVC5_DEBUG |
442 |
|
// We don't always have a sat literal, so remember that. Will need |
443 |
|
// it for some assertions we make. |
444 |
|
bool litPresent = d_decisionEngine->hasSatLiteral(node); |
445 |
|
if(Debug.isOn("decision")) { |
446 |
|
if(!litPresent) { |
447 |
|
Debug("decision") << "no sat literal for this node" << std::endl; |
448 |
|
} |
449 |
|
} |
450 |
|
#endif |
451 |
|
|
452 |
|
// Get value of sat literal for the node, if there is one |
453 |
|
SatValue litVal = tryGetSatValue(node); |
454 |
|
|
455 |
|
/* You'd better know what you want */ |
456 |
|
Assert(desiredVal != SAT_VALUE_UNKNOWN) << "expected known value"; |
457 |
|
|
458 |
|
/* Good luck, hope you can get what you want */ |
459 |
|
// See bug 374 |
460 |
|
// Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN) << |
461 |
|
// "invariant violated"; |
462 |
|
|
463 |
|
/* What type of node is this */ |
464 |
|
Kind k = node.getKind(); |
465 |
|
theory::TheoryId tId = theory::kindToTheoryId(k); |
466 |
|
bool isAtom = |
467 |
|
(k == kind::BOOLEAN_TERM_VARIABLE ) || |
468 |
|
( (tId != theory::THEORY_BOOL) && |
469 |
|
(k != kind::EQUAL || (!node[0].getType().isBoolean())) ); |
470 |
|
|
471 |
|
/* Some debugging stuff */ |
472 |
|
Debug("decision::jh") << "kind = " << k << std::endl |
473 |
|
<< "theoryId = " << tId << std::endl |
474 |
|
<< "node = " << node << std::endl |
475 |
|
<< "litVal = " << litVal << std::endl; |
476 |
|
|
477 |
|
/** |
478 |
|
* If not in theory of booleans, check if this is something to split-on. |
479 |
|
*/ |
480 |
|
if(isAtom) { |
481 |
|
// if node has embedded skolems due to term removal, resolve that first |
482 |
|
if (handleEmbeddedSkolems(node) == FOUND_SPLITTER) return FOUND_SPLITTER; |
483 |
|
|
484 |
|
if(litVal != SAT_VALUE_UNKNOWN) { |
485 |
|
Assert(litVal == desiredVal); |
486 |
|
setJustified(node); |
487 |
|
return NO_SPLITTER; |
488 |
|
} |
489 |
|
else { |
490 |
|
Assert(d_decisionEngine->hasSatLiteral(node)); |
491 |
|
if(d_curThreshold != 0 && getWeightPolarized(node, desiredVal) >= d_curThreshold) |
492 |
|
return DONT_KNOW; |
493 |
|
SatVariable v = |
494 |
|
d_decisionEngine->getSatLiteral(node).getSatVariable(); |
495 |
|
d_curDecision = SatLiteral(v, /* negated = */ desiredVal != SAT_VALUE_TRUE ); |
496 |
|
Trace("decision-node") << "[decision-node] requesting split on " << d_curDecision |
497 |
|
<< ", node: " << node |
498 |
|
<< ", polarity: " << (desiredVal == SAT_VALUE_TRUE ? "true" : "false") << std::endl; |
499 |
|
return FOUND_SPLITTER; |
500 |
|
} |
501 |
|
} |
502 |
|
|
503 |
|
SearchResult ret = NO_SPLITTER; |
504 |
|
switch (k) { |
505 |
|
|
506 |
|
case kind::CONST_BOOLEAN: |
507 |
|
Assert(node.getConst<bool>() == false || desiredVal == SAT_VALUE_TRUE); |
508 |
|
Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE); |
509 |
|
break; |
510 |
|
|
511 |
|
case kind::AND: |
512 |
|
if (desiredVal == SAT_VALUE_FALSE) |
513 |
|
ret = handleAndOrEasy(node, desiredVal); |
514 |
|
else |
515 |
|
ret = handleAndOrHard(node, desiredVal); |
516 |
|
break; |
517 |
|
|
518 |
|
case kind::OR: |
519 |
|
if (desiredVal == SAT_VALUE_FALSE) |
520 |
|
ret = handleAndOrHard(node, desiredVal); |
521 |
|
else |
522 |
|
ret = handleAndOrEasy(node, desiredVal); |
523 |
|
break; |
524 |
|
|
525 |
|
case kind::IMPLIES: |
526 |
|
if (desiredVal == SAT_VALUE_FALSE) |
527 |
|
ret = handleBinaryHard(node[0], SAT_VALUE_TRUE, |
528 |
|
node[1], SAT_VALUE_FALSE); |
529 |
|
|
530 |
|
else |
531 |
|
ret = handleBinaryEasy(node[0], SAT_VALUE_FALSE, |
532 |
|
node[1], SAT_VALUE_TRUE); |
533 |
|
break; |
534 |
|
|
535 |
|
case kind::XOR: |
536 |
|
case kind::EQUAL: { |
537 |
|
SatValue desiredVal1 = tryGetSatValue(node[0]); |
538 |
|
SatValue desiredVal2 = tryGetSatValue(node[1]); |
539 |
|
computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2); |
540 |
|
ret = handleBinaryHard(node[0], desiredVal1, |
541 |
|
node[1], desiredVal2); |
542 |
|
break; |
543 |
|
} |
544 |
|
|
545 |
|
case kind::ITE: |
546 |
|
ret = handleITE(node, desiredVal); |
547 |
|
break; |
548 |
|
|
549 |
|
default: Assert(false) << "Unexpected Boolean operator"; break; |
550 |
|
}//end of switch(k) |
551 |
|
|
552 |
|
if(ret == DONT_KNOW) { |
553 |
|
setExploredThreshold(node); |
554 |
|
} |
555 |
|
|
556 |
|
if(ret == NO_SPLITTER) { |
557 |
|
Assert(litPresent == false || litVal == desiredVal) |
558 |
|
<< "Output should be justified"; |
559 |
|
setJustified(node); |
560 |
|
} |
561 |
|
return ret; |
562 |
|
}/* findRecSplit method */ |
563 |
|
|
564 |
|
JustificationHeuristic::SearchResult |
565 |
|
JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) |
566 |
|
{ |
567 |
|
Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) |
568 |
|
or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE)); |
569 |
|
|
570 |
|
int numChildren = node.getNumChildren(); |
571 |
|
SatValue desiredValInverted = invertValue(desiredVal); |
572 |
|
for(int i = 0; i < numChildren; ++i) { |
573 |
|
TNode curNode = getChildByWeight(node, i, desiredVal); |
574 |
|
if ( tryGetSatValue(curNode) != desiredValInverted ) { |
575 |
|
SearchResult ret = findSplitterRec(curNode, desiredVal); |
576 |
|
if(ret != DONT_KNOW) { |
577 |
|
return ret; |
578 |
|
} |
579 |
|
} |
580 |
|
} |
581 |
|
Assert(d_curThreshold != 0) << "handleAndOrEasy: No controlling input found"; |
582 |
|
return DONT_KNOW; |
583 |
|
} |
584 |
|
|
585 |
|
int JustificationHeuristic::getStartIndex(TNode node) { |
586 |
|
return d_startIndexCache[node]; |
587 |
|
} |
588 |
|
void JustificationHeuristic::saveStartIndex(TNode node, int val) { |
589 |
|
d_startIndexCache[node] = val; |
590 |
|
} |
591 |
|
|
592 |
|
JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node, |
593 |
|
SatValue desiredVal) { |
594 |
|
Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) |
595 |
|
or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE)); |
596 |
|
|
597 |
|
int numChildren = node.getNumChildren(); |
598 |
|
bool noSplitter = true; |
599 |
|
int i_st = getStartIndex(node); |
600 |
|
for(int i = i_st; i < numChildren; ++i) { |
601 |
|
TNode curNode = getChildByWeight(node, i, desiredVal); |
602 |
|
SearchResult ret = findSplitterRec(curNode, desiredVal); |
603 |
|
if (ret == FOUND_SPLITTER) { |
604 |
|
if(i != i_st) saveStartIndex(node, i); |
605 |
|
return FOUND_SPLITTER; |
606 |
|
} |
607 |
|
noSplitter = noSplitter && (ret == NO_SPLITTER); |
608 |
|
} |
609 |
|
return noSplitter ? NO_SPLITTER : DONT_KNOW; |
610 |
|
} |
611 |
|
|
612 |
|
JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TNode node1, |
613 |
|
SatValue desiredVal1, |
614 |
|
TNode node2, |
615 |
|
SatValue desiredVal2) |
616 |
|
{ |
617 |
|
if(options::decisionUseWeight() && |
618 |
|
getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { |
619 |
|
std::swap(node1, node2); |
620 |
|
std::swap(desiredVal1, desiredVal2); |
621 |
|
} |
622 |
|
|
623 |
|
if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) { |
624 |
|
SearchResult ret = findSplitterRec(node1, desiredVal1); |
625 |
|
if(ret != DONT_KNOW) |
626 |
|
return ret; |
627 |
|
} |
628 |
|
if ( tryGetSatValue(node2) != invertValue(desiredVal2) ) { |
629 |
|
SearchResult ret = findSplitterRec(node2, desiredVal2); |
630 |
|
if(ret != DONT_KNOW) |
631 |
|
return ret; |
632 |
|
} |
633 |
|
Assert(d_curThreshold != 0) << "handleBinaryEasy: No controlling input found"; |
634 |
|
return DONT_KNOW; |
635 |
|
} |
636 |
|
|
637 |
|
JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TNode node1, |
638 |
|
SatValue desiredVal1, |
639 |
|
TNode node2, |
640 |
|
SatValue desiredVal2) |
641 |
|
{ |
642 |
|
if(options::decisionUseWeight() && |
643 |
|
getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { |
644 |
|
std::swap(node1, node2); |
645 |
|
std::swap(desiredVal1, desiredVal2); |
646 |
|
} |
647 |
|
|
648 |
|
bool noSplitter = true; |
649 |
|
SearchResult ret; |
650 |
|
|
651 |
|
ret = findSplitterRec(node1, desiredVal1); |
652 |
|
if (ret == FOUND_SPLITTER) |
653 |
|
return FOUND_SPLITTER; |
654 |
|
noSplitter &= (ret == NO_SPLITTER); |
655 |
|
|
656 |
|
ret = findSplitterRec(node2, desiredVal2); |
657 |
|
if (ret == FOUND_SPLITTER) |
658 |
|
return FOUND_SPLITTER; |
659 |
|
noSplitter &= (ret == NO_SPLITTER); |
660 |
|
|
661 |
|
return noSplitter ? NO_SPLITTER : DONT_KNOW; |
662 |
|
} |
663 |
|
|
664 |
|
JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) |
665 |
|
{ |
666 |
|
Debug("decision::jh") << " handleITE (" << node << ", " |
667 |
|
<< desiredVal << std::endl; |
668 |
|
|
669 |
|
//[0]: if, [1]: then, [2]: else |
670 |
|
SatValue ifVal = tryGetSatValue(node[0]); |
671 |
|
if (ifVal == SAT_VALUE_UNKNOWN) { |
672 |
|
SatValue trueChildVal = tryGetSatValue(node[1]); |
673 |
|
SatValue falseChildVal = tryGetSatValue(node[2]); |
674 |
|
SatValue ifDesiredVal; |
675 |
|
|
676 |
|
if(trueChildVal == desiredVal || falseChildVal == invertValue(desiredVal)) { |
677 |
|
ifDesiredVal = SAT_VALUE_TRUE; |
678 |
|
} else if(trueChildVal == invertValue(desiredVal) || |
679 |
|
falseChildVal == desiredVal || |
680 |
|
(options::decisionUseWeight() && |
681 |
|
getWeightPolarized(node[1], true) > getWeightPolarized(node[2], false)) |
682 |
|
) { |
683 |
|
ifDesiredVal = SAT_VALUE_FALSE; |
684 |
|
} else { |
685 |
|
ifDesiredVal = SAT_VALUE_TRUE; |
686 |
|
} |
687 |
|
|
688 |
|
if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER) |
689 |
|
return FOUND_SPLITTER; |
690 |
|
|
691 |
|
Assert(d_curThreshold != 0) << "No controlling input found (6)"; |
692 |
|
return DONT_KNOW; |
693 |
|
} else { |
694 |
|
// Try to justify 'if' |
695 |
|
if(findSplitterRec(node[0], ifVal) == FOUND_SPLITTER) |
696 |
|
return FOUND_SPLITTER; |
697 |
|
|
698 |
|
// If that was successful, we need to go into only one of 'then' |
699 |
|
// or 'else' |
700 |
|
int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; |
701 |
|
|
702 |
|
if( findSplitterRec(node[ch], desiredVal) == FOUND_SPLITTER ) { |
703 |
|
return FOUND_SPLITTER; |
704 |
|
} |
705 |
|
|
706 |
|
return NO_SPLITTER; |
707 |
|
}// else (...ifVal...) |
708 |
|
} |
709 |
|
|
710 |
|
JustificationHeuristic::SearchResult |
711 |
|
JustificationHeuristic::handleEmbeddedSkolems(TNode node) |
712 |
|
{ |
713 |
|
const SkolemList l = getSkolems(node); |
714 |
|
Trace("decision::jh::skolems") << " skolems size = " << l.size() << std::endl; |
715 |
|
|
716 |
|
bool noSplitter = true; |
717 |
|
for (SkolemList::const_iterator i = l.begin(); i != l.end(); ++i) |
718 |
|
{ |
719 |
|
if(d_visited.find((*i).first) == d_visited.end()) { |
720 |
|
d_visited.insert((*i).first); |
721 |
|
SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE); |
722 |
|
if (ret == FOUND_SPLITTER) |
723 |
|
return FOUND_SPLITTER; |
724 |
|
noSplitter = noSplitter && (ret == NO_SPLITTER); |
725 |
|
d_visited.erase((*i).first); |
726 |
|
} |
727 |
|
} |
728 |
|
return noSplitter ? NO_SPLITTER : DONT_KNOW; |
729 |
|
} |
730 |
|
|
731 |
|
} /* namespace decision */ |
732 |
29358 |
} // namespace cvc5 |