Skip to content

Commit

Permalink
Fixes an issue where unnecessary dependencies were added.
Browse files Browse the repository at this point in the history
Some dependencies were incorrectly added to all functions
appearing inside an instantiated axiom.
Also updated a dictionary name as requested in #767.
  • Loading branch information
zafer-esen committed Aug 8, 2023
1 parent e4d5c99 commit b7c14eb
Showing 1 changed file with 7 additions and 5 deletions.
12 changes: 7 additions & 5 deletions Source/Core/Monomorphization.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand All @@ -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(
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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);
Expand Down

0 comments on commit b7c14eb

Please sign in to comment.