d_giveup("decision::jh::giveup", 0),
d_timestat("decision::jh::time"),
d_assertions(uc),
- d_iteAssertions(uc),
- d_iteCache(uc),
+ d_skolemAssertions(uc),
+ d_skolemCache(uc),
d_visited(),
- d_visitedComputeITE(),
+ d_visitedComputeSkolems(),
d_curDecision(),
d_curThreshold(0),
d_childCache(uc),
<< " assertionsEnd = " << assertionsEnd
<< std::endl;
- // Save the 'real' assertions locally
- for (size_t i = 0; i < assertionsEnd; i++)
+ // Save all assertions locally, including the assertions generated by term
+ // removal. We have to make sure that we assign a value to all the Boolean
+ // term variables. To illustrate why this is, consider the case where we have
+ // a single assertion
+ //
+ // (or (f a) (f b))
+ //
+ // where `f` is a function `Bool -> Bool`. Given an assignment:
+ //
+ // (f a) -> true
+ // (f b) -> false
+ // a -> false
+ //
+ // UF will not complain and the justification heuristic considers the
+ // assertion to be satisifed. However, we also have to make sure that we pick
+ // a value for `b` that is not in conflict with the other assignments (we can
+ // only choose `b` to be `true` otherwise the model is incorrect).
+ for (const Node& assertion : assertions)
{
- d_assertions.push_back(assertions[i]);
+ d_assertions.push_back(assertion);
}
// Save mapping between ite skolems and ite assertions
<< assertions[(i.second)] << std::endl;
Assert(i.second >= assertionsEnd && i.second < assertions.size());
- d_iteAssertions[i.first] = assertions[i.second];
+ d_skolemAssertions[i.first] = assertions[i.second];
}
// Automatic weight computation
}//end of else
}
-JustificationHeuristic::IteList
-JustificationHeuristic::getITEs(TNode n)
+JustificationHeuristic::SkolemList JustificationHeuristic::getSkolems(TNode n)
{
- IteCache::iterator it = d_iteCache.find(n);
- if(it != d_iteCache.end()) {
+ SkolemCache::iterator it = d_skolemCache.find(n);
+ if (it != d_skolemCache.end())
+ {
return (*it).second;
- } else {
- // Compute the list of ITEs
- // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
- d_visitedComputeITE.clear();
- IteList ilist;
- computeITEs(n, ilist);
- d_iteCache.insert(n, ilist);
+ }
+ else
+ {
+ // Compute the list of Skolems
+ // TODO: optimize by avoiding multiple lookup for d_skolemCache[n]
+ d_visitedComputeSkolems.clear();
+ SkolemList ilist;
+ computeSkolems(n, ilist);
+ d_skolemCache.insert(n, ilist);
return ilist;
}
}
-void JustificationHeuristic::computeITEs(TNode n, IteList &l)
+void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l)
{
- Trace("decision::jh::ite") << " computeITEs( " << n << ", &l)\n";
- d_visitedComputeITE.insert(n);
+ Trace("decision::jh::skolems") << " computeSkolems( " << n << ", &l)\n";
+ d_visitedComputeSkolems.insert(n);
for(unsigned i=0; i<n.getNumChildren(); ++i) {
- SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
- if(it2 != d_iteAssertions.end()) {
+ SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]);
+ if (it2 != d_skolemAssertions.end())
+ {
l.push_back(make_pair(n[i], (*it2).second));
Assert(n[i].getNumChildren() == 0);
}
- if(d_visitedComputeITE.find(n[i]) ==
- d_visitedComputeITE.end()) {
- computeITEs(n[i], l);
+ if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end())
+ {
+ computeSkolems(n[i], l);
}
}
}
* If not in theory of booleans, check if this is something to split-on.
*/
if(isAtom) {
- // if node has embedded ites, resolve that first
- if(handleEmbeddedITEs(node) == FOUND_SPLITTER)
- return FOUND_SPLITTER;
+ // if node has embedded skolems due to term removal, resolve that first
+ if (handleEmbeddedSkolems(node) == FOUND_SPLITTER) return FOUND_SPLITTER;
if(litVal != SAT_VALUE_UNKNOWN) {
Assert(litVal == desiredVal);
}// else (...ifVal...)
}
-JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs(TNode node)
+JustificationHeuristic::SearchResult
+JustificationHeuristic::handleEmbeddedSkolems(TNode node)
{
- const IteList l = getITEs(node);
- Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
+ const SkolemList l = getSkolems(node);
+ Trace("decision::jh::skolems") << " skolems size = " << l.size() << std::endl;
bool noSplitter = true;
- for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
+ for (SkolemList::const_iterator i = l.begin(); i != l.end(); ++i)
+ {
if(d_visited.find((*i).first) == d_visited.end()) {
d_visited.insert((*i).first);
SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE);
// TRUE FALSE MEH
enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
- typedef std::vector<pair<TNode,TNode> > IteList;
- typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache;
+ typedef std::vector<pair<TNode, TNode> > SkolemList;
+ typedef context::CDHashMap<TNode, SkolemList, TNodeHashFunction> SkolemCache;
typedef std::vector<TNode> ChildList;
typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache;
typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
/**
* A copy of the assertions that need to be justified
- * directly. Doesn't have ones introduced during during ITE-removal.
+ * directly. Doesn't have ones introduced during during term removal.
*/
context::CDList<TNode> d_assertions;
//TNode is fine since decisionEngine has them too
- /** map from ite-rewrite skolem to a boolean-ite assertion */
- SkolemMap d_iteAssertions;
+ /** map from skolems introduced in term removal to the corresponding assertion
+ */
+ SkolemMap d_skolemAssertions;
// 'key' being TNode is fine since if a skolem didn't exist anywhere,
// we won't look it up. as for 'value', same reason as d_assertions
- /** Cache for ITE skolems present in a atomic formula */
- IteCache d_iteCache;
+ /** Cache for skolems present in a atomic formula */
+ SkolemCache d_skolemCache;
/**
* This is used to prevent infinite loop when trying to find a
std::unordered_set<TNode,TNodeHashFunction> d_visited;
/**
- * Set to track visited nodes in a dfs search done in computeITE
+ * Set to track visited nodes in a dfs search done in computeSkolems
* function
*/
- std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+ std::unordered_set<TNode, TNodeHashFunction> d_visitedComputeSkolems;
/** current decision for the recursive call */
SatLiteral d_curDecision;
SatValue tryGetSatValue(Node n);
/* Get list of all term-ITEs for the atomic formula v */
- JustificationHeuristic::IteList getITEs(TNode n);
-
+ JustificationHeuristic::SkolemList getSkolems(TNode n);
/**
* For big and/or nodes, a cache to save starting index into children
int getStartIndex(TNode node);
void saveStartIndex(TNode node, int val);
- /* Compute all term-ITEs in a node recursively */
- void computeITEs(TNode n, IteList &l);
+ /* Compute all term-removal skolems in a node recursively */
+ void computeSkolems(TNode n, SkolemList& l);
SearchResult handleAndOrEasy(TNode node, SatValue desiredVal);
SearchResult handleAndOrHard(TNode node, SatValue desiredVal);
SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1,
TNode node2, SatValue desiredVal2);
SearchResult handleITE(TNode node, SatValue desiredVal);
- SearchResult handleEmbeddedITEs(TNode node);
+ SearchResult handleEmbeddedSkolems(TNode node);
};/* class JustificationHeuristic */
}/* namespace decision */
projects / cvc5.git / commitdiff