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