From: Gereon Kremer <gkremer@stanford.edu>
Date: Mon, 8 Mar 2021 14:46:30 +0000 (+0100)
Subject: Fix justification heuristic again (#6074)
X-Git-Tag: cvc5-1.0.0~2141
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7dc81173107bf65b9a90e163a1e85ce7b3c20ff;p=cvc5.git

Fix justification heuristic again (#6074)



This PR replaces all TNode types in datatypes by Node within justification heuristic.
Fixes #6073.
Unfortunately, the example from #6073 times out now, thus there is no new regression.
---

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 1cf2810fd..20dec12d8 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -43,16 +43,16 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   //                   TRUE           FALSE         MEH
   enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
 
-  typedef std::vector<std::pair<TNode, TNode> > SkolemList;
-  typedef context::CDHashMap<TNode, SkolemList, TNodeHashFunction> SkolemCache;
-  typedef std::vector<TNode> ChildList;
+  typedef std::vector<std::pair<Node, Node> > SkolemList;
+  typedef context::CDHashMap<Node, SkolemList, NodeHashFunction> SkolemCache;
+  typedef std::vector<Node> ChildList;
   typedef context::
-      CDHashMap<TNode, std::pair<ChildList, ChildList>, TNodeHashFunction>
+      CDHashMap<Node, std::pair<ChildList, ChildList>, NodeHashFunction>
           ChildCache;
-  typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
-  typedef context::CDHashMap<TNode,
+  typedef context::CDHashMap<Node,Node,NodeHashFunction> SkolemMap;
+  typedef context::CDHashMap<Node,
                              std::pair<DecisionWeight, DecisionWeight>,
-                             TNodeHashFunction>
+                             NodeHashFunction>
       WeightCache;
 
   // being 'justified' is monotonic with respect to decisions
@@ -72,14 +72,11 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * directly. Doesn't have ones introduced during during term removal.
    */
   context::CDList<Node> d_assertions;
-  //TNode is fine since decisionEngine has them too
 
   /** 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 skolems present in a atomic formula */
   SkolemCache d_skolemCache;
 
@@ -88,13 +85,13 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * splitter. Can happen when exploring assertion corresponding to a
    * term-ITE.
    */
-  std::unordered_set<TNode,TNodeHashFunction> d_visited;
+  std::unordered_set<Node,NodeHashFunction> d_visited;
 
   /**
    * Set to track visited nodes in a dfs search done in computeSkolems
    * function
    */
-  std::unordered_set<TNode, TNodeHashFunction> d_visitedComputeSkolems;
+  std::unordered_set<Node, NodeHashFunction> d_visitedComputeSkolems;
 
   /** current decision for the recursive call */
   prop::SatLiteral d_curDecision;
@@ -174,7 +171,7 @@ public:
    * For big and/or nodes, a cache to save starting index into children
    * for efficiently.
    */
-  typedef context::CDHashMap<TNode, int, TNodeHashFunction> StartIndexCache;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> StartIndexCache;
   StartIndexCache d_startIndexCache;
   int getStartIndex(TNode node);
   void saveStartIndex(TNode node, int val);