Skip to content

Commit

Permalink
Fix forget identifier + tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@michelemartelli2002
michelemartelli2002 committed Jun 14, 2024
1 parent d85b624 commit 1e2a9a0
Show file tree
Hide file tree
Showing 7 changed files with 97 additions and 14 deletions.
13 changes: 13 additions & 0 deletions lisa/lisa-analyses/imp-testcases/string/strings-subs.imp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,5 +142,18 @@ class strings {
x = "a";
}

scopetest(x){
def s = "a";
def y = "z";
if (x > 0){
def k = "x";
y = k;
} else {
def k = "x";
y = k;
}
s = s + "c";
}


}
18 changes: 9 additions & 9 deletions lisa/lisa-analyses/imp-testcases/string/subs-domain/report.json
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
{
"warnings" : [ ],
"files" : [ "report.json", "untyped_strings.assume(strings__this).json", "untyped_strings.branching(strings__this,_untyped_x).json", "untyped_strings.closure(strings__this).json", "untyped_strings.closure2(strings__this).json", "untyped_strings.closure3(strings__this).json", "untyped_strings.constants(strings__this).json", "untyped_strings.iftest1(strings__this).json", "untyped_strings.iftest2(strings__this).json", "untyped_strings.iftestand(strings__this).json", "untyped_strings.iftestor(strings__this).json", "untyped_strings.integers(strings__this).json", "untyped_strings.interassign(strings__this).json", "untyped_strings.loops(strings__this,_untyped_x).json", "untyped_strings.paper1(strings__this).json", "untyped_strings.paper2(strings__this).json", "untyped_strings.paper3(strings__this,_untyped_x).json", "untyped_strings.stringconcat(strings__this).json", "untyped_strings.type(strings__this,_untyped_x).json" ],
"files" : [ "report.json", "untyped_strings.assume(strings__this).json", "untyped_strings.branching(strings__this,_untyped_x).json", "untyped_strings.closure(strings__this).json", "untyped_strings.closure2(strings__this).json", "untyped_strings.closure3(strings__this).json", "untyped_strings.constants(strings__this).json", "untyped_strings.iftest1(strings__this).json", "untyped_strings.iftest2(strings__this).json", "untyped_strings.iftestand(strings__this).json", "untyped_strings.iftestor(strings__this).json", "untyped_strings.integers(strings__this).json", "untyped_strings.interassign(strings__this).json", "untyped_strings.loops(strings__this,_untyped_x).json", "untyped_strings.paper1(strings__this).json", "untyped_strings.paper2(strings__this).json", "untyped_strings.paper3(strings__this,_untyped_x).json", "untyped_strings.scopetest(strings__this,_untyped_x).json", "untyped_strings.stringconcat(strings__this).json", "untyped_strings.type(strings__this,_untyped_x).json" ],
"info" : {
"cfgs" : "18",
"duration" : "77ms",
"end" : "2024-04-18T17:41:10.990+02:00",
"expressions" : "188",
"files" : "18",
"cfgs" : "19",
"duration" : "92ms",
"end" : "2024-06-14T23:04:08.375+02:00",
"expressions" : "206",
"files" : "19",
"globals" : "0",
"members" : "18",
"members" : "19",
"programs" : "1",
"start" : "2024-04-18T17:41:10.913+02:00",
"statements" : "91",
"start" : "2024-06-14T23:04:08.283+02:00",
"statements" : "100",
"units" : "1",
"version" : "0.1b9",
"warnings" : "0"
Expand Down
2 changes: 1 addition & 1 deletion ...lisa-analyses/imp-testcases/string/subs-domain/untyped_strings.paper2(strings__this).json
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"name":"untyped strings::paper2(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = \"\""},{"id":1,"text":"x"},{"id":2,"text":"\"\""},{"id":3,"subNodes":[4,5],"text":"y = \"\""},{"id":4,"text":"y"},{"id":5,"text":"\"\""},{"id":6,"subNodes":[7,8],"text":"equals(x, y)"},{"id":7,"text":"x"},{"id":8,"text":"y"},{"id":9,"subNodes":[10,11],"text":"x = +(x, \"c\")"},{"id":10,"text":"x"},{"id":11,"subNodes":[12,13],"text":"+(x, \"c\")"},{"id":12,"text":"x"},{"id":13,"text":"\"c\""},{"id":14,"subNodes":[15,16],"text":"x = +(y, \"c\")"},{"id":15,"text":"x"},{"id":16,"subNodes":[17,18],"text":"+(y, \"c\")"},{"id":17,"text":"y"},{"id":18,"text":"\"c\""},{"id":19,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":9,"destId":19,"kind":"SequentialEdge"},{"sourceId":14,"destId":19,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["x strcmp y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":8,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":9,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y"]}}}},{"nodeId":10,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":11,"description":{"expressions":["x strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":13,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y","y strcat \"c\""]}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":16,"description":{"expressions":["y strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":17,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":18,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":19,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y"]}}}}]}
{"name":"untyped strings::paper2(strings* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = \"\""},{"id":1,"text":"x"},{"id":2,"text":"\"\""},{"id":3,"subNodes":[4,5],"text":"y = \"\""},{"id":4,"text":"y"},{"id":5,"text":"\"\""},{"id":6,"subNodes":[7,8],"text":"equals(x, y)"},{"id":7,"text":"x"},{"id":8,"text":"y"},{"id":9,"subNodes":[10,11],"text":"x = +(x, \"c\")"},{"id":10,"text":"x"},{"id":11,"subNodes":[12,13],"text":"+(x, \"c\")"},{"id":12,"text":"x"},{"id":13,"text":"\"c\""},{"id":14,"subNodes":[15,16],"text":"x = +(y, \"c\")"},{"id":15,"text":"x"},{"id":16,"subNodes":[17,18],"text":"+(y, \"c\")"},{"id":17,"text":"y"},{"id":18,"text":"\"c\""},{"id":19,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":9,"destId":19,"kind":"SequentialEdge"},{"sourceId":14,"destId":19,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["\"\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"]},"value":"#TOP#"}}},{"nodeId":6,"description":{"expressions":["x strcmp y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":8,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":9,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\""]}}}},{"nodeId":10,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":11,"description":{"expressions":["x strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":13,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["y"],"y":["x"]}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\"","y","y strcat \"c\""]}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":16,"description":{"expressions":["y strcat \"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":17,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":18,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":"#TOP#"}}},{"nodeId":19,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":["string"],"y":["string"]},"value":{"x":["\"c\""]}}}}]}
1 change: 1 addition & 0 deletions ...imp-testcases/string/subs-domain/untyped_strings.scopetest(strings__this,_untyped_x).json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"name":"untyped strings::scopetest(strings* this, untyped x)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"s = \"a\""},{"id":1,"text":"s"},{"id":2,"text":"\"a\""},{"id":3,"subNodes":[4,5],"text":"y = \"z\""},{"id":4,"text":"y"},{"id":5,"text":"\"z\""},{"id":6,"subNodes":[7,8],"text":">(x, 0)"},{"id":7,"text":"x"},{"id":8,"text":"0"},{"id":9,"subNodes":[10,11],"text":"k = \"x\""},{"id":10,"text":"k"},{"id":11,"text":"\"x\""},{"id":12,"subNodes":[13,14],"text":"y = k"},{"id":13,"text":"y"},{"id":14,"text":"k"},{"id":15,"subNodes":[16,17],"text":"k = \"x\""},{"id":16,"text":"k"},{"id":17,"text":"\"x\""},{"id":18,"subNodes":[19,20],"text":"y = k"},{"id":19,"text":"y"},{"id":20,"text":"k"},{"id":21,"subNodes":[22,23],"text":"s = +(s, \"c\")"},{"id":22,"text":"s"},{"id":23,"subNodes":[24,25],"text":"+(s, \"c\")"},{"id":24,"text":"s"},{"id":25,"text":"\"c\""},{"id":26,"text":"ret"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":9,"kind":"TrueEdge"},{"sourceId":6,"destId":15,"kind":"FalseEdge"},{"sourceId":9,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":21,"kind":"SequentialEdge"},{"sourceId":15,"destId":18,"kind":"SequentialEdge"},{"sourceId":18,"destId":21,"kind":"SequentialEdge"},{"sourceId":21,"destId":26,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["s"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#"},"value":{"s":["\"a\""]}}}},{"nodeId":1,"description":{"expressions":["s"],"state":{"heap":"monolith","type":{"this":["strings*"],"x":"#TOP#"},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["\"a\""],"state":{"heap":"monolith","type":{"this":["strings*"],"x":"#TOP#"},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#"},"value":{"s":["\"a\""]}}}},{"nodeId":5,"description":{"expressions":["\"z\""],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#"},"value":{"s":["\"a\""]}}}},{"nodeId":6,"description":{"expressions":["x > 0"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":7,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":8,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":9,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":10,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":11,"description":{"expressions":["\"x\""],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":12,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"x\"","k"]}}}},{"nodeId":13,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":14,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":15,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":16,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":17,"description":{"expressions":["\"x\""],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":18,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"x\"","k"]}}}},{"nodeId":19,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":20,"description":{"expressions":["k"],"state":{"heap":"monolith","type":{"k":["string"],"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"k":["\"x\""],"s":["\"a\""],"y":["\"z\""]}}}},{"nodeId":21,"description":{"expressions":["s"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\"","\"c\""],"y":["\"x\""]}}}},{"nodeId":22,"description":{"expressions":["s"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"x\""]}}}},{"nodeId":23,"description":{"expressions":["s strcat \"c\""],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"x\""]}}}},{"nodeId":24,"description":{"expressions":["s"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"x\""]}}}},{"nodeId":25,"description":{"expressions":["\"c\""],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\""],"y":["\"x\""]}}}},{"nodeId":26,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"s":["string"],"this":["strings*"],"x":"#TOP#","y":["string"]},"value":{"s":["\"a\"","\"c\""],"y":["\"x\""]}}}}]}
41 changes: 37 additions & 4 deletions lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/SubstringDomain.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -266,6 +266,13 @@ public boolean knowsIdentifier(

if (function.containsKey(id))
return true;

for (Map.Entry<Identifier, ExpressionInverseSet> entry : function.entrySet()) {
for (SymbolicExpression expr : entry.getValue().elements) {
if (appears(id, expr))
return true;
}
}

return false;
}
Expand All @@ -282,6 +289,12 @@ public SubstringDomain forgetIdentifier(
// null

newFunction.remove(id);

newFunction.replaceAll((key, value) ->
new ExpressionInverseSet(value.elements.stream()
.filter(v -> !appears(id, v))
.collect(Collectors.toSet())
));

return mk(lattice, newFunction);
}
Expand All @@ -296,10 +309,30 @@ public SubstringDomain forgetIdentifiersIf(
Map<Identifier, ExpressionInverseSet> newFunction = mkNewFunction(function, false); // function
// !=
// null

Set<Identifier> keys = newFunction.keySet().stream().filter(test::test).collect(Collectors.toSet());

keys.forEach(newFunction::remove);

Set<Identifier> ids = new HashSet<>();
for (Map.Entry<Identifier, ExpressionInverseSet> entry : newFunction.entrySet()) {
ids.add(entry.getKey());
for(SymbolicExpression s : entry.getValue().elements()) {
if (s instanceof Identifier) {
Identifier id = (Identifier) s;
ids.add(id);
}
}
}


for (Identifier id : ids) {
if (test.test(id)) {
newFunction.remove(id);

newFunction.replaceAll((key, value) ->
new ExpressionInverseSet(value.elements.stream()
.filter(v -> !appears(id, v))
.collect(Collectors.toSet())
));
}
}

return mk(lattice, newFunction);
}
Expand Down
Loading

0 comments on commit 1e2a9a0

Please sign in to comment.