1 /********************* */
2 /*! \file justification_heuristic.h
4 ** Original author: kshitij
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Justification heuristic for decision making
16 ** A ATGP-inspired justification-based decision heuristic. See
17 ** [insert reference] for more details. This code is, or not, based
18 ** on the CVC3 implementation of the same heuristic.
20 ** It needs access to the simplified but non-clausal formula.
23 #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
24 #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
26 #include "decision_engine.h"
27 #include "decision_strategy.h"
29 #include "context/cdhashset.h"
30 #include "expr/node.h"
31 #include "prop/sat_solver_types.h"
37 class GiveUpException
: public Exception
{
40 Exception("justification heuristic: giving up") {
42 };/* class GiveUpException */
44 class JustificationHeuristic
: public ITEDecisionStrategy
{
45 typedef std::vector
<pair
<TNode
,TNode
> > IteList
;
46 typedef hash_map
<TNode
,IteList
,TNodeHashFunction
> IteCache
;
47 typedef hash_map
<TNode
,TNode
,TNodeHashFunction
> SkolemMap
;
49 // being 'justified' is monotonic with respect to decisions
50 typedef context::CDHashSet
<TNode
,TNodeHashFunction
> JustifiedSet
;
51 JustifiedSet d_justified
;
52 context::CDO
<unsigned> d_prvsIndex
;
59 * A copy of the assertions that need to be justified
60 * directly. Doesn't have ones introduced during during ITE-removal.
62 std::vector
<TNode
> d_assertions
;
63 //TNode is fine since decisionEngine has them too
65 /** map from ite-rewrite skolem to a boolean-ite assertion */
66 SkolemMap d_iteAssertions
;
67 // 'key' being TNode is fine since if a skolem didn't exist anywhere,
68 // we won't look it up. as for 'value', same reason as d_assertions
70 /** Cache for ITE skolems present in a atomic formula */
74 * This is used to prevent infinite loop when trying to find a
75 * splitter. Can happen when exploring assertion corresponding to a
78 hash_set
<TNode
,TNodeHashFunction
> d_visited
;
80 JustificationHeuristic(CVC4::DecisionEngine
* de
, context::Context
*c
):
81 ITEDecisionStrategy(de
, c
),
84 d_helfulness("decision::jh::helpfulness", 0),
85 d_giveup("decision::jh::giveup", 0),
86 d_timestat("decision::jh::time") {
87 StatisticsRegistry::registerStat(&d_helfulness
);
88 StatisticsRegistry::registerStat(&d_giveup
);
89 StatisticsRegistry::registerStat(&d_timestat
);
90 Trace("decision") << "Justification heuristic enabled" << std::endl
;
92 ~JustificationHeuristic() {
93 StatisticsRegistry::unregisterStat(&d_helfulness
);
94 StatisticsRegistry::unregisterStat(&d_timestat
);
96 prop::SatLiteral
getNext(bool &stopSearch
) {
97 Trace("decision") << "JustificationHeuristic::getNext()" << std::endl
;
98 TimerStat::CodeTimer
codeTimer(d_timestat
);
102 if(Trace
.isOn("justified")) {
103 for(JustifiedSet::iterator i
= d_justified
.begin();
104 i
!= d_justified
.end(); ++i
) {
106 SatLiteral l
= d_decisionEngine
->hasSatLiteral(n
) ?
107 d_decisionEngine
->getSatLiteral(n
) : -1;
108 SatValue v
= tryGetSatValue(n
);
109 Trace("justified") <<"{ "<<l
<<"}" << n
<<": "<<v
<< std::endl
;
113 for(unsigned i
= d_prvsIndex
; i
< d_assertions
.size(); ++i
) {
114 Debug("decision") << "---" << std::endl
<< d_assertions
[i
] << std::endl
;
116 // Sanity check: if it was false, aren't we inconsistent?
117 Assert( tryGetSatValue(d_assertions
[i
]) != SAT_VALUE_FALSE
);
119 SatValue desiredVal
= SAT_VALUE_TRUE
;
120 SatLiteral litDecision
;
122 litDecision
= findSplitter(d_assertions
[i
], desiredVal
);
123 }catch(GiveUpException
&e
) {
124 return prop::undefSatLiteral
;
127 if(litDecision
!= undefSatLiteral
)
131 Trace("decision") << "jh: Nothing to split on " << std::endl
;
133 #if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
134 bool alljustified
= true;
135 for(unsigned i
= 0 ; i
< d_assertions
.size() && alljustified
; ++i
) {
136 TNode curass
= d_assertions
[i
];
137 while(curass
.getKind() == kind::NOT
)
139 alljustified
&= checkJustified(curass
);
141 if(Debug
.isOn("decision")) {
142 if(!checkJustified(curass
))
143 Debug("decision") << "****** Not justified [i="<<i
<<"]: "
144 << d_assertions
[i
] << std::endl
;
147 Assert(alljustified
);
150 // SAT solver can stop...
152 d_decisionEngine
->setResult(SAT_VALUE_TRUE
);
153 return prop::undefSatLiteral
;
156 void addAssertions(const std::vector
<Node
> &assertions
,
157 unsigned assertionsEnd
,
158 IteSkolemMap iteSkolemMap
) {
160 << "JustificationHeuristic::addAssertions()"
161 << " size = " << assertions
.size()
162 << " assertionsEnd = " << assertionsEnd
165 // Save the 'real' assertions locally
166 for(unsigned i
= 0; i
< assertionsEnd
; ++i
)
167 d_assertions
.push_back(assertions
[i
]);
169 // Save mapping between ite skolems and ite assertions
170 for(IteSkolemMap::iterator i
= iteSkolemMap
.begin();
171 i
!= iteSkolemMap
.end(); ++i
) {
172 Trace("jh-ite") << " jh-ite: " << (i
->first
) << " maps to "
173 << assertions
[(i
->second
)] << std::endl
;
174 Assert(i
->second
>= assertionsEnd
&& i
->second
< assertions
.size());
175 d_iteAssertions
[i
->first
] = assertions
[i
->second
];
179 /* Compute justified */
180 /*bool computeJustified() {
184 SatLiteral
findSplitter(TNode node
, SatValue desiredVal
)
187 SatLiteral litDecision
;
188 ret
= findSplitterRec(node
, desiredVal
, &litDecision
);
190 Debug("decision") << "Yippee!!" << std::endl
;
195 return undefSatLiteral
;
200 * Do all the hard work.
201 * @param findFirst returns
203 bool findSplitterRec(TNode node
, SatValue value
, SatLiteral
* litDecision
);
205 /* Helper functions */
206 void setJustified(TNode
);
207 bool checkJustified(TNode
);
209 /* If literal exists corresponding to the node return
210 that. Otherwise an UNKNOWN */
211 SatValue
tryGetSatValue(Node n
);
213 /* Get list of all term-ITEs for the atomic formula v */
214 const JustificationHeuristic::IteList
& getITEs(TNode n
);
216 /* Compute all term-ITEs in a node recursively */
217 void computeITEs(TNode n
, IteList
&l
);
218 };/* class JustificationHeuristic */
220 }/* namespace decision */
222 }/* namespace CVC4 */
224 #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */