From 883298e4d5bf54b83125fc256601cdbb6c21ad03 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Oct 2020 18:17:53 -0500
Subject: [PATCH] Minor simplifications to substitution map class (#5180)

This class is an important utility in preprocessing, which we are adding proof support for. This simplifies the interface of this class with regards to unused interfaces for clarity.
---
 src/theory/substitutions.cpp | 52 ------------------------------------
 src/theory/substitutions.h   | 34 ++++++-----------------
 2 files changed, 8 insertions(+), 78 deletions(-)

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 365fd4a05..664fcd1b3 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -147,36 +147,6 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
 }/* SubstitutionMap::internalSubstitute() */
 
 
-void SubstitutionMap::simplifyRHS(const SubstitutionMap& subMap)
-{
-  // Put the new substitutions into the old ones
-  NodeMap::iterator it = d_substitutions.begin();
-  NodeMap::iterator it_end = d_substitutions.end();
-  for(; it != it_end; ++ it) {
-    d_substitutions[(*it).first] = subMap.apply((*it).second);
-  }  
-}
-
-
-void SubstitutionMap::simplifyRHS(TNode x, TNode t) {
-  // Temporary substitution cache
-  NodeCache tempCache;
-  tempCache[x] = t;
-
-  // Put the new substitution into the old ones
-  NodeMap::iterator it = d_substitutions.begin();
-  NodeMap::iterator it_end = d_substitutions.end();
-  for(; it != it_end; ++ it) {
-    d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
-  }  
-  // it = d_substitutionsLazy.begin();
-  // it_end = d_substitutionsLazy.end();
-  // for(; it != it_end; ++ it) {
-  //   d_substitutionsLazy[(*it).first] = internalSubstitute((*it).second, tempCache);
-  // }  
-}
-
-
 void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
 {
   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
@@ -214,26 +184,6 @@ void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateC
   }
 }
 
-static bool check(TNode node,
-                  const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
-static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions)
-{
-  SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
-  SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
-  Debug("substitution") << "checking " << node << endl;
-  for (; it != it_end; ++it)
-  {
-    Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << endl;
-    if (expr::hasSubterm(node, (*it).first))
-    {
-      Debug("substitution") << "-- FAIL" << endl;
-      return false;
-    }
-  }
-  Debug("substitution") << "-- SUCCEED" << endl;
-  return true;
-}
-
 Node SubstitutionMap::apply(TNode t) {
 
   Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
@@ -249,8 +199,6 @@ Node SubstitutionMap::apply(TNode t) {
   Node result = internalSubstitute(t, d_substitutionCache);
   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
 
-  //  Assert(check(result, d_substitutions));
-
   return result;
 }
 
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 5db10e5bd..66dcd81a0 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -66,9 +66,6 @@ private:
   /** Has the cache been invalidated? */
   bool d_cacheInvalidated;
 
-  /** Whether to keep substitutions in solved form */
-  bool d_solvedForm;
-
   /** Internal method that performs substitution */
   Node internalSubstitute(TNode t, NodeCache& cache);
 
@@ -93,15 +90,14 @@ private:
   CacheInvalidator d_cacheInvalidator;
 
 public:
-
-  SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) :
-    d_substitutions(context),
-    d_substitutionCache(),
-    d_substituteUnderQuantifiers(substituteUnderQuantifiers),
-    d_cacheInvalidated(false),
-    d_solvedForm(solvedForm),
-    d_cacheInvalidator(context, d_cacheInvalidated)
-    {
+ SubstitutionMap(context::Context* context,
+                 bool substituteUnderQuantifiers = true)
+     : d_substitutions(context),
+       d_substitutionCache(),
+       d_substituteUnderQuantifiers(substituteUnderQuantifiers),
+       d_cacheInvalidated(false),
+       d_cacheInvalidator(context, d_cacheInvalidated)
+ {
   }
 
   /**
@@ -166,20 +162,6 @@ public:
     return d_substitutions.empty();
   }
 
-  // NOTE [MGD]: removed clear() and swap() from the interface
-  // when this data structure became context-dependent
-  // because they weren't used---and it's not clear how they
-  // should best interact with cache invalidation on context
-  // pops.
-
-  // Simplify right-hand sides of current map using the given substitutions
-  void simplifyRHS(const SubstitutionMap& subMap);
-
-  // Simplify right-hand sides of current map with lhs -> rhs
-  void simplifyRHS(TNode lhs, TNode rhs);
-
-  bool isSolvedForm() const { return d_solvedForm; }
-
   /**
    * Print to the output stream
    */
-- 
2.30.2