From b7c14ebe432eba8c8d7052a879309dded8a2bab2 Mon Sep 17 00:00:00 2001
From: Zafer Esen <zesen@amazon.com>
Date: Tue, 8 Aug 2023 17:56:37 -0400
Subject: [PATCH] Fixes an issue where unnecessary dependencies were added.
 Some dependencies were incorrectly added to all functions appearing inside an
 instantiated axiom. Also updated a dictionary name as requested in #767.

---
 Source/Core/Monomorphization.cs | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs
index 4e4ae2a6f..b0dfb3f13 100644
--- a/Source/Core/Monomorphization.cs
+++ b/Source/Core/Monomorphization.cs
@@ -1301,7 +1301,7 @@ class MonomorphizationVisitor : VarDeclOnceStandardVisitor
     private readonly HashSet<Constant> originalConstants;
     // Note that original axioms refer to axioms of the original program which might have been updated in-place during monomorphization.
     public readonly Dictionary<Axiom, HashSet<Axiom>> originalAxiomToSplitAxioms;
-    private readonly Dictionary<Axiom, Axiom> originalAxiomToUninstantiatedCopies;
+    private readonly Dictionary<Axiom, Axiom> originalAxiomToUninstantiatedCopy;
 
     private MonomorphizationVisitor(CoreOptions options, Program program, HashSet<Axiom> polymorphicFunctionAxioms)
     {
@@ -1310,7 +1310,7 @@ private MonomorphizationVisitor(CoreOptions options, Program program, HashSet<Ax
       originalFunctions = program.Functions.ToHashSet();
       originalConstants = program.Constants.ToHashSet();
       originalAxiomToSplitAxioms = program.Axioms.ToDictionary(ax => ax, _ => new HashSet<Axiom>());
-      originalAxiomToUninstantiatedCopies = program.Axioms.ToDictionary(ax => ax, ax => (Axiom) ax.Clone() );
+      originalAxiomToUninstantiatedCopy = program.Axioms.ToDictionary(ax => ax, ax => (Axiom) ax.Clone() );
       implInstantiations = new Dictionary<Implementation, Dictionary<List<Type>, Implementation>>();
       nameToImplementation = new Dictionary<string, Implementation>();
       program.TopLevelDeclarations.OfType<Implementation>().Where(impl => impl.TypeParameters.Count > 0).ForEach(
@@ -1410,7 +1410,7 @@ private static void UpdateDependencies(MonomorphizationVisitor monomorphizationV
       foreach (var (originalAxiom, newAxioms) in monomorphizationVisitor.originalAxiomToSplitAxioms)
       {
         var originalAxiomFc = new FunctionAndConstantCollector();
-        var uninstantiatedOriginalAxiom = monomorphizationVisitor.originalAxiomToUninstantiatedCopies[originalAxiom];
+        var uninstantiatedOriginalAxiom = monomorphizationVisitor.originalAxiomToUninstantiatedCopy[originalAxiom];
         originalAxiomFc.Visit(uninstantiatedOriginalAxiom);
         var originalAxiomFunctions = originalAxiomFc.Functions;
 
@@ -1440,9 +1440,11 @@ private static void UpdateDependencies(MonomorphizationVisitor monomorphizationV
           {
             if (function.TypeParameters.Any()) // Polymorphic function
             {
+              var functionInstantiations =
+                monomorphizationVisitor.functionInstantiations[function].Values.ToHashSet();
               var instancesToAddDependency = originalAxiomFunctions.Contains(function)
-                ? newAxiomFunctions[newAxiom]
-                : monomorphizationVisitor.functionInstantiations[function].Values.ToHashSet();
+                ? newAxiomFunctions[newAxiom].Intersect(functionInstantiations)
+                : functionInstantiations;
               foreach (var inst in instancesToAddDependency)
               {
                 inst.OtherDefinitionAxioms.Add(newAxiom);