EGraph: Remove redundant mapping

usi-verification-and-security · Jul 1, 2023 · 596501b · 596501b
1 parent fe7214b
commit 596501b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/src/tsolvers/egraph/EnodeStore.cc b/src/tsolvers/egraph/EnodeStore.cc
@@ -71,9 +71,8 @@ ERef EnodeStore::addTerm(PTRef term, bool ignoreChildren) {
     }();
     ERef newEnode = ea.alloc(symref, argSpan, term);
 
+    assert(not termToERef.has(term));
     termToERef.insert(term, newEnode);
-    assert(not ERefToTerm.has(newEnode));
-    ERefToTerm.insert(newEnode, term);
     termEnodes.push(newEnode);
     return newEnode;
 }

diff --git a/src/tsolvers/egraph/EnodeStore.h b/src/tsolvers/egraph/EnodeStore.h
@@ -78,7 +78,6 @@ class EnodeStore {
     uint32_t       dist_idx;
 
     Map<PTRef,ERef,PTRefHash,Equal<PTRef> >    termToERef;
-    Map<ERef,PTRef,ERefHash,Equal<ERef> >      ERefToTerm;
 
     vec<PTRef>     index_to_dist;                    // Table distinction index --> proper term
     vec<ERef>      termEnodes;
@@ -108,7 +107,7 @@ class EnodeStore {
      * @return true if tr is in the store, false if not.
      */
     bool         peekERef(PTRef tr, ERef& er)  const { return termToERef.peek(tr, er); }
-    PTRef        getPTRef(ERef er)     const { return ERefToTerm[er]; }
+    PTRef        getPTRef(ERef er)     const { return ea[er].getTerm(); }
 
     vec<PTRefERefPair> constructTerm(PTRef tr);