Replace old sygus term reconstruction algorithm with a new one. (#5779)

This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index bb8c5618c..9e485ae78 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -514,6 +514,12 @@ public:
                   Iterator substitutionsEnd) const;
 
   /**
+   * Simultaneous substitution of Nodes in cache.
+   */
+  Node substitute(
+      std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
+
+  /**
    * Returns the kind of this node.
    * @return the kind
    */
@@ -1381,6 +1387,16 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
 }
 
 template <bool ref_count>
+inline Node NodeTemplate<ref_count>::substitute(
+    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const
+{
+  // Since no substitution is given (other than what may already be in the
+  // cache), we pass dummy iterators to conform to the main substitute method,
+  // giving the same value to substitutionsBegin and substitutionsEnd.
+  return substitute(cache.cend(), cache.cend(), cache);
+}
+
+template <bool ref_count>
 template <class Iterator>
 Node
 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,