diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-05 19:06:21 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-05 19:06:21 +0000 |
commit | 7f52115ab0dcba4c8ba9403a5f25b8e8c588911a (patch) | |
tree | 14b74c89069cd6e9b443853ac1f15cca2ce586a1 /src/decision/justification_heuristic.h | |
parent | 7efd777609f7fbc20701402ad949971cbc251f8f (diff) |
This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
Diffstat (limited to 'src/decision/justification_heuristic.h')
-rw-r--r-- | src/decision/justification_heuristic.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index adccc0d55..a1b29ed47 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -49,7 +49,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; // being 'justified' is monotonic with respect to decisions - typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet; + typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet; JustifiedSet d_justified; context::CDO<unsigned> d_prvsIndex; @@ -107,8 +107,8 @@ public: d_visited.clear(); if(Trace.isOn("justified")) { - for(JustifiedSet::iterator i = d_justified.begin(); - i != d_justified.end(); ++i) { + for(JustifiedSet::key_iterator i = d_justified.key_begin(); + i != d_justified.key_end(); ++i) { TNode n = *i; SatLiteral l = d_decisionEngine->hasSatLiteral(n) ? d_decisionEngine->getSatLiteral(n) : -1; |