blob: cb2216d6d35d08bedff5a92e79a5d920596f78d8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
/********************* */
/*! \file justification_heuristic.h
** \verbatim
** Original author: kshitij
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Justification heuristic for decision making
**
** A ATGP-inspired justification-based decision heuristic. See
** [insert reference] for more details. This code is, or not, based
** on the CVC3 implementation of the same heuristic.
**
** It needs access to the simplified but non-clausal formula.
**/
#ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
#define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
#include "decision_engine.h"
#include "decision_strategy.h"
#include "prop/sat_solver_types.h"
#include "expr/node.h"
using namespace CVC4::prop;
namespace CVC4 {
namespace decision {
class JustificationHeuristic : public DecisionStrategy {
set<SatVariable> d_justified;
unsigned d_prvsIndex;
public:
JustificationHeuristic(CVC4::DecisionEngine* de) :
DecisionStrategy(de) {
Trace("decision") << "Justification heuristic enabled" << std::endl;
}
prop::SatLiteral getNext() {
Trace("decision") << "JustificationHeuristic::getNext()" << std::endl;
const vector<Node>& assertions = d_decisionEngine->getAssertions();
for(unsigned i = d_prvsIndex; i < assertions.size(); ++i) {
SatLiteral litDecision;
/* Make sure there is a literal corresponding to the node */
if( not d_decisionEngine->hasSatLiteral(assertions[i]) ) {
// Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
continue;
// Assert(not lit.isNull());
}
SatLiteral lit = d_decisionEngine->getSatLiteral(assertions[i]);
SatValue desiredVal = d_decisionEngine->getSatValue(lit);
if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE;
bool ret = findSplitterRec(lit, desiredVal, &litDecision);
if(ret == true) {
d_prvsIndex = i;
return litDecision;
}
}
return prop::undefSatLiteral;
}
bool needSimplifiedPreITEAssertions() { return true; }
void notifyAssertionsAvailable() {
Trace("decision") << "JustificationHeuristic::notifyAssertionsAvailable()"
<< " size = " << d_decisionEngine->getAssertions().size()
<< std::endl;
/* clear the justifcation labels -- reconsider if/when to do
this */
d_justified.clear();
d_prvsIndex = 0;
}
private:
/* Do all the hardwork. */
bool findSplitterRec(SatLiteral lit, SatValue value, SatLiteral* litDecision);
/* Helper functions */
void setJustified(SatVariable v);
bool checkJustified(SatVariable v);
};/* class JustificationHeuristic */
}/* namespace decision */
}/* namespace CVC4 */
#endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */
|
