Skip to content

Commit b78bad2

Browse files
alexandernutzalexandernutz
committed
license headers, cleanup
1 parent d57f190 commit b78bad2

File tree

8 files changed

+183
-113
lines changed

8 files changed

+183
-113
lines changed

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPDomainBenchmark.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,29 @@
1+
/*
2+
* Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de)
3+
* Copyright (C) 2017 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE AbstractInterpretationV2 plug-in.
6+
*
7+
* The ULTIMATE AbstractInterpretationV2 plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE AbstractInterpretationV2 plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE AbstractInterpretationV2 plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE AbstractInterpretationV2 plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE AbstractInterpretationV2 plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
127
package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp;
228

329
import java.util.ArrayList;

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPStatistics.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,29 @@
1+
/*
2+
* Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de)
3+
* Copyright (C) 2017 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE AbstractInterpretationV2 plug-in.
6+
*
7+
* The ULTIMATE AbstractInterpretationV2 plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE AbstractInterpretationV2 plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE AbstractInterpretationV2 plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE AbstractInterpretationV2 plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE AbstractInterpretationV2 plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
127
package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp;
228

329
import java.util.function.BinaryOperator;

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/elements/AbstractNodeAndFunctionFactory.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,29 @@
1+
/*
2+
* Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de)
3+
* Copyright (C) 2017 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE AbstractInterpretationV2 plug-in.
6+
*
7+
* The ULTIMATE AbstractInterpretationV2 plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE AbstractInterpretationV2 plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE AbstractInterpretationV2 plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE AbstractInterpretationV2 plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE AbstractInterpretationV2 plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
127
package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp.elements;
228

329
import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp.IEqNodeIdentifier;

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/elements/EqFunction.java‎

Lines changed: 0 additions & 88 deletions
This file was deleted.

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/FloydWarshall.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,29 @@
1+
/*
2+
* Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de)
3+
* Copyright (C) 2017 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE AbstractInterpretationV2 plug-in.
6+
*
7+
* The ULTIMATE AbstractInterpretationV2 plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE AbstractInterpretationV2 plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE AbstractInterpretationV2 plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE AbstractInterpretationV2 plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE AbstractInterpretationV2 plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
127
package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp.states;
228

329
import java.util.ArrayList;

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/LiteralManager.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,29 @@
1+
/*
2+
* Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de)
3+
* Copyright (C) 2017 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE AbstractInterpretationV2 plug-in.
6+
*
7+
* The ULTIMATE AbstractInterpretationV2 plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE AbstractInterpretationV2 plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE AbstractInterpretationV2 plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE AbstractInterpretationV2 plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE AbstractInterpretationV2 plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
127
package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp.states;
228

329
import java.util.Collection;

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/WeakEquivalenceGraph.java‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,29 @@
1+
/*
2+
* Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de)
3+
* Copyright (C) 2017 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE AbstractInterpretationV2 plug-in.
6+
*
7+
* The ULTIMATE AbstractInterpretationV2 plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE AbstractInterpretationV2 plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE AbstractInterpretationV2 plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE AbstractInterpretationV2 plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE AbstractInterpretationV2 plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
127
package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp.states;
228

329
import java.util.ArrayList;

‎trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/WeqCongruenceClosure.java‎

Lines changed: 27 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,29 @@
1+
/*
2+
* Copyright (C) 2017 Alexander Nutz (nutz@informatik.uni-freiburg.de)
3+
* Copyright (C) 2017 University of Freiburg
4+
*
5+
* This file is part of the ULTIMATE AbstractInterpretationV2 plug-in.
6+
*
7+
* The ULTIMATE AbstractInterpretationV2 plug-in is free software: you can redistribute it and/or modify
8+
* it under the terms of the GNU Lesser General Public License as published
9+
* by the Free Software Foundation, either version 3 of the License, or
10+
* (at your option) any later version.
11+
*
12+
* The ULTIMATE AbstractInterpretationV2 plug-in is distributed in the hope that it will be useful,
13+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
14+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15+
* GNU Lesser General Public License for more details.
16+
*
17+
* You should have received a copy of the GNU Lesser General Public License
18+
* along with the ULTIMATE AbstractInterpretationV2 plug-in. If not, see <http://www.gnu.org/licenses/>.
19+
*
20+
* Additional permission under GNU GPL version 3 section 7:
21+
* If you modify the ULTIMATE AbstractInterpretationV2 plug-in, or any covered work, by linking
22+
* or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
23+
* containing parts covered by the terms of the Eclipse Public License, the
24+
* licensors of the ULTIMATE AbstractInterpretationV2 plug-in grant you additional permission
25+
* to convey the resulting work.
26+
*/
127
package de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp.states;
228

329
import java.util.ArrayList;
@@ -33,9 +59,6 @@ public class WeqCongruenceClosure<ACTION extends IIcfgTransition<IcfgLocation>,
3359
private final WeakEquivalenceGraph<ACTION, NODE> mWeakEquivalenceGraph;
3460
private final EqConstraintFactory<ACTION, NODE> mFactory;
3561

36-
// private final LiteralManager<NODE> mLiteralManager;
37-
// private final Collection<NODE> mAllLiterals;
38-
3962
private final HashRelation<Object, NODE> mNodeToDependents;
4063

4164
/**
@@ -48,8 +71,6 @@ public WeqCongruenceClosure(final EqConstraintFactory<ACTION, NODE> factory) {
4871
assert factory != null;
4972
mWeakEquivalenceGraph = new WeakEquivalenceGraph<>(this, factory);
5073
mFactory = factory;
51-
// mLiteralManager = mFactory.getLiteralManager();
52-
// mAllLiterals = new HashSet<>();
5374
mNodeToDependents = new HashRelation<>();
5475
assert sanityCheck();
5576
}
@@ -66,8 +87,6 @@ public WeqCongruenceClosure(final boolean isInconsistent) {
6687
}
6788
mWeakEquivalenceGraph = null;
6889
mFactory = null;
69-
// mLiteralManager = null;
70-
// mAllLiterals = null;
7190
mNodeToDependents = null;
7291
}
7392

@@ -84,10 +103,6 @@ public WeqCongruenceClosure(final CongruenceClosure<NODE> original,
84103
assert factory != null;
85104
mWeakEquivalenceGraph = new WeakEquivalenceGraph<>(this, factory);
86105
mFactory = factory;
87-
// mLiteralManager = mFactory.getLiteralManager();
88-
// mAllLiterals = original.getAllElementRepresentatives().stream().filter(elem -> mLiteralManager.isLiteral(elem))
89-
// .collect(Collectors.toCollection(HashSet::new));
90-
91106
mNodeToDependents = new HashRelation<>();
92107
initializeNodeToDependents(original);
93108
assert sanityCheck();
@@ -126,9 +141,7 @@ public WeqCongruenceClosure(final WeqCongruenceClosure<ACTION, NODE> original) {
126141
super(original);
127142
assert original.mFactory != null;
128143
mFactory = original.mFactory;
129-
// mLiteralManager = mFactory.getLiteralManager();
130144
mWeakEquivalenceGraph = new WeakEquivalenceGraph<>(this, original.mWeakEquivalenceGraph);
131-
// mAllLiterals = new HashSet<>(original.mAllLiterals);
132145
mNodeToDependents = new HashRelation<>(original.mNodeToDependents);
133146
assert sanityCheck();
134147
}
@@ -176,24 +189,13 @@ protected boolean addElementRec(final NODE elem) {
176189
return false;
177190
}
178191

179-
// if (mLiteralManager.isLiteral(elem)) {
180-
// for (final NODE other : mLiteralManager.getDisequalities(elem, getAllLiteralElements())) {
181-
// reportDisequalityRec(elem, other);
182-
// }
183-
// mAllLiterals.add(elem);
184-
// }
185-
186192
// executeFloydWarshallAndReportResult();
187193
// reportAllArrayEqualitiesFromWeqGraph();
188194

189195
// assert weqGraphFreeOfArrayEqualities();
190196
return true;
191197
}
192198

193-
// private Collection<NODE> getAllLiteralElements() {
194-
// return mAllLiterals;
195-
// }
196-
197199
@Override
198200
protected CongruenceClosure<NODE> alignElementsAndFunctions(final CongruenceClosure<NODE> otherCC) {
199201
assert !this.isInconsistent() && !otherCC.isInconsistent();
@@ -1235,4 +1237,4 @@ public Integer getStatistics(final VPStatistics stat) {
12351237
}
12361238
}
12371239

1238-
}
1240+
}

0 commit comments

Comments
 (0)