Skip to content

Commit

Permalink
Fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Jun 12, 2024
1 parent fdc8903 commit e7b8287
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 13 deletions.
8 changes: 4 additions & 4 deletions Source/Graph/Graph.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1182,17 +1182,17 @@ public static IEnumerable<object> FindReachableNodesInGraphWithMergeNodes(
continue;
}

if (visit != null && visit(node) == false)
{
continue;
}

if (node is IEnumerable<object> objects) {
if (!visitedEdges.IsSupersetOf(objects)) {
continue;
}
}
visitedEdges.Add(node);
if (visit != null && visit(node) == false)
{
continue;
}

var outgoing = edges.GetValueOrDefault(node) ?? new List<object>();
foreach (var x in outgoing)
Expand Down
15 changes: 6 additions & 9 deletions Source/VCGeneration/Prune/Prune.cs
Original file line number Diff line number Diff line change
Expand Up @@ -67,21 +67,18 @@ public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options,
blocksVisitor.Visit(block);
}

var revealedOutgoing = options.Prune == PruneMode.AllRevealed
? blocksVisitor.Outgoing
: blocksVisitor.Outgoing.Where(d =>
DeclarationFilter(d));

var keepRoots = program.TopLevelDeclarations.Where(d => QKeyValue.FindBoolAttribute(d.Attributes, "keep"));
var reachableDeclarations = GraphAlgorithms.FindReachableNodesInGraphWithMergeNodes(program.DeclarationDependencies,
revealedOutgoing.Concat(keepRoots).ToHashSet(),
node => node is not Function function || blocksVisitor.RevealedFunctions.Contains(function))
.OfType<Declaration>().Where(d => DeclarationFilter(d)).ToHashSet();
blocksVisitor.Outgoing.Concat(keepRoots).ToHashSet(), DeclarationFilter).ToHashSet();
return program.TopLevelDeclarations.Where(d =>
d is not Constant && d is not Axiom && d is not Function || reachableDeclarations.Contains(d));

bool DeclarationFilter(Declaration d)
bool DeclarationFilter(object d)
{
if (options.Prune != PruneMode.ExplicitReveal)
{
return true;
}
return d is not Function function || blocksVisitor.RevealedFunctions.Contains(function);
}
}
Expand Down

0 comments on commit e7b8287

Please sign in to comment.