1 /********************* */
2 /*! \file relevance_manager.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Implementation of relevance manager.
15 #include "theory/relevance_manager.h"
17 using namespace CVC4::kind
;
22 RelevanceManager::RelevanceManager(context::UserContext
* userContext
,
24 : d_val(val
), d_input(userContext
), d_computed(false), d_success(false)
28 void RelevanceManager::notifyPreprocessedAssertions(
29 const std::vector
<Node
>& assertions
)
31 // add to input list, which is user-context dependent
32 std::vector
<Node
> toProcess
;
33 for (const Node
& a
: assertions
)
35 if (a
.getKind() == AND
)
37 // split top-level AND
38 for (const Node
& ac
: a
)
40 toProcess
.push_back(ac
);
48 addAssertionsInternal(toProcess
);
51 void RelevanceManager::notifyPreprocessedAssertion(Node n
)
53 std::vector
<Node
> toProcess
;
54 toProcess
.push_back(n
);
55 addAssertionsInternal(toProcess
);
58 void RelevanceManager::addAssertionsInternal(std::vector
<Node
>& toProcess
)
61 while (i
< toProcess
.size())
63 Node a
= toProcess
[i
];
64 if (a
.getKind() == AND
)
67 for (const Node
& ac
: a
)
69 toProcess
.push_back(ac
);
74 // note that a could be a literal, in which case we could add it to
75 // an "always relevant" set here.
82 void RelevanceManager::resetRound()
88 void RelevanceManager::computeRelevance()
91 Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl
;
92 std::unordered_map
<TNode
, int, TNodeHashFunction
> cache
;
93 for (const Node
& node
: d_input
)
96 int val
= justify(n
, cache
);
99 std::stringstream serr
;
100 serr
<< "RelevanceManager::computeRelevance: WARNING: failed to justify "
102 Trace("rel-manager") << serr
.str() << std::endl
;
103 Assert(false) << serr
.str();
108 Trace("rel-manager") << "...success, size = " << d_rset
.size() << std::endl
;
112 bool RelevanceManager::isBooleanConnective(TNode cur
)
114 Kind k
= cur
.getKind();
115 return k
== NOT
|| k
== IMPLIES
|| k
== AND
|| k
== OR
|| k
== ITE
|| k
== XOR
116 || (k
== EQUAL
&& cur
[0].getType().isBoolean());
119 bool RelevanceManager::updateJustifyLastChild(
121 std::vector
<int>& childrenJustify
,
122 std::unordered_map
<TNode
, int, TNodeHashFunction
>& cache
)
124 // This method is run when we are informed that child index of cur
125 // has justify status lastChildJustify. We return true if we would like to
126 // compute the next child, in this case we push the status of the current
127 // child to childrenJustify.
128 size_t nchildren
= cur
.getNumChildren();
129 Assert(isBooleanConnective(cur
));
130 size_t index
= childrenJustify
.size();
131 Assert(index
< nchildren
);
132 Assert(cache
.find(cur
[index
]) != cache
.end());
133 Kind k
= cur
.getKind();
134 // Lookup the last child's value in the overall cache, we may choose to
135 // add this to childrenJustify if we return true.
136 int lastChildJustify
= cache
[cur
[index
]];
139 cache
[cur
] = -lastChildJustify
;
141 else if (k
== IMPLIES
|| k
== AND
|| k
== OR
)
143 if (lastChildJustify
!= 0)
145 // See if we short circuited? The value for short circuiting is false if
146 // we are AND or the first child of IMPLIES.
148 == ((k
== AND
|| (k
== IMPLIES
&& index
== 0)) ? -1 : 1))
150 cache
[cur
] = k
== AND
? -1 : 1;
154 if (index
+ 1 == nchildren
)
156 // finished all children, compute the overall value
157 int ret
= k
== AND
? 1 : -1;
158 for (int cv
: childrenJustify
)
171 childrenJustify
.push_back(lastChildJustify
);
175 else if (lastChildJustify
== 0)
177 // all other cases, an unknown child implies we are unknown
184 Assert(lastChildJustify
!= 0);
185 // continue with branch
186 childrenJustify
.push_back(lastChildJustify
);
187 if (lastChildJustify
== -1)
189 // also mark first branch as don't care
190 childrenJustify
.push_back(0);
196 // should be in proper branch
197 Assert(childrenJustify
[0] == (index
== 1 ? 1 : -1));
198 // we are the value of the branch
199 cache
[cur
] = lastChildJustify
;
204 Assert(k
== XOR
|| k
== EQUAL
);
205 Assert(nchildren
== 2);
206 Assert(lastChildJustify
!= 0);
209 // must compute the other child
210 childrenJustify
.push_back(lastChildJustify
);
215 // both children known, compute value
216 Assert(childrenJustify
.size() == 1 && childrenJustify
[0] != 0);
218 ((k
== XOR
? -1 : 1) * lastChildJustify
== childrenJustify
[0]) ? 1
225 int RelevanceManager::justify(
226 TNode n
, std::unordered_map
<TNode
, int, TNodeHashFunction
>& cache
)
228 // the vector of values of children
229 std::unordered_map
<TNode
, std::vector
<int>, TNodeHashFunction
> childJustify
;
230 std::unordered_map
<TNode
, int, TNodeHashFunction
>::iterator it
;
231 std::unordered_map
<TNode
, std::vector
<int>, TNodeHashFunction
>::iterator itc
;
232 std::vector
<TNode
> visit
;
238 // should always have Boolean type
239 Assert(cur
.getType().isBoolean());
240 it
= cache
.find(cur
);
241 if (it
!= cache
.end())
244 // already computed value
247 itc
= childJustify
.find(cur
);
248 // have we traversed to children yet?
249 if (itc
== childJustify
.end())
251 // are we not a Boolean connective (including NOT)?
252 if (isBooleanConnective(cur
))
254 // initialize its children justify vector as empty
255 childJustify
[cur
].clear();
256 // start with the first child
257 visit
.push_back(cur
[0]);
262 // The atom case, lookup the value in the valuation class to
263 // see its current value in the SAT solver, if it has one.
265 // otherwise we look up the value
267 if (d_val
.hasSatValue(cur
, value
))
269 ret
= value
? 1 : -1;
277 // this processes the impact of the current child on the value of cur,
278 // and possibly requests that a new child is computed.
279 if (updateJustifyLastChild(cur
, itc
->second
, cache
))
281 Assert(itc
->second
.size() < cur
.getNumChildren());
282 TNode nextChild
= cur
[itc
->second
.size()];
283 visit
.push_back(nextChild
);
290 } while (!visit
.empty());
291 Assert(cache
.find(n
) != cache
.end());
295 bool RelevanceManager::isRelevant(Node lit
)
303 // always relevant if we failed to compute
306 // agnostic to negation
307 while (lit
.getKind() == NOT
)
311 return d_rset
.find(lit
) != d_rset
.end();
314 } // namespace theory