Skip to content

Commit

Permalink
fix compile errors due to last #239 commit
Browse files Browse the repository at this point in the history
  • Loading branch information
@alexandernutz
alexandernutz committed Dec 5, 2017
1 parent 66cc184 commit e7c4d7c
Show file tree
Hide file tree
Showing 5 changed files with 166 additions and 28 deletions.
39 changes: 39 additions & 0 deletions ...burg/informatik/ultimate/modelcheckerutils/absint/vpdomain/CongruenceClosureSmtUtils.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
package de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.stream.Collectors;

import de.uni_freiburg.informatik.ultimate.logic.Script;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosure;

public class CongruenceClosureSmtUtils {
public static <NODE extends IEqNodeIdentifier<NODE>> Term congruenceClosureToTerm(final Script script,
final CongruenceClosure<NODE> pa) {
return SmtUtils.and(script, congruenceClosureToCube(script, pa));
}

public static <NODE extends IEqNodeIdentifier<NODE>> List<Term> congruenceClosureToCube(final Script script,
// public static <NODE extends ICongruenceClosureElement<NODE>> List<Term> congruenceClosureToCube(final Script script,
final CongruenceClosure<NODE> pa) {
if (pa.isInconsistent()) {
return Collections.emptyList();
}

final List<Term> elementEqualities = pa.getSupportingElementEqualities().entrySet().stream()
.map(en -> script.term("=", en.getKey().getTerm(), en.getValue().getTerm()))
.collect(Collectors.toList());
final List<Term> elementDisequalities = pa.getElementDisequalities().entrySet().stream()
.map(pair -> script.term("distinct", pair.getKey().getTerm(), pair.getValue().getTerm()))
.collect(Collectors.toList());

final List<Term> result = new ArrayList<>(elementEqualities.size() + elementDisequalities.size());
result.addAll(elementEqualities);
result.addAll(elementDisequalities);
return result;
}

}
13 changes: 6 additions & 7 deletions ...iburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceEdgeLabel.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@
import de.uni_freiburg.informatik.ultimate.logic.Script;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
import de.uni_freiburg.informatik.ultimate.util.datastructures.CcManager;
import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosure;
import de.uni_freiburg.informatik.ultimate.util.datastructures.ICongruenceClosure;
import de.uni_freiburg.informatik.ultimate.util.datastructures.RemoveCcElement;
Expand Down Expand Up @@ -88,7 +87,7 @@ public WeakEquivalenceEdgeLabel(final WeakEquivalenceGraph<NODE> weakEquivalence
mWeakEquivalenceGraph = weakEquivalenceGraph;
mWeqCcManager = weakEquivalenceGraph.getWeqCcManager();
mLabel = new HashSet<>();
mLabel.add(new CongruenceClosure<>(mWeakEquivalenceGraph.getLogger()));
mLabel.add(mWeqCcManager.getEmptyCc());
assert sanityCheck();
}

Expand Down Expand Up @@ -191,7 +190,7 @@ public Set<NODE> projectSimpleElement(final NODE elem, final boolean useWeqGpaMo
if (lab.isTautological()) {
// a disjunct became "true" through projection --> the whole disjunction is tautological
mLabel.clear();
mLabel.add(new CongruenceClosure<>(mWeakEquivalenceGraph.getLogger()));
mLabel.add(mWeqCcManager.getEmptyCc());
return Collections.emptySet();
}
assert lab.sanityCheckOnlyCc(mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved());
Expand Down Expand Up @@ -353,7 +352,7 @@ public WeakEquivalenceEdgeLabel<NODE> reportChangeInGroundPartialArrangement(
public List<Term> toDNF(final Script script) {
final List<Term> result = new ArrayList<>();
for (final CongruenceClosure<NODE> cc : mLabel) {
final List<Term> cube = CcManager.congruenceClosureToCube(script, cc);
final List<Term> cube = CongruenceClosureSmtUtils.congruenceClosureToCube(script, cc);
final Term cubeTerm = SmtUtils.and(script, cube);
result.add(cubeTerm);
}
Expand Down Expand Up @@ -587,7 +586,7 @@ public void meetWithWeqGpa(final WeqCongruenceClosure<NODE> originalPa) {

if (paCopy.isTautological()) {
mLabel.clear();
mLabel.add(new CongruenceClosure<NODE>(mWeakEquivalenceGraph.getLogger()));
mLabel.add(mWeqCcManager.getEmptyCc());
return;
}

Expand All @@ -614,7 +613,7 @@ public void meetWithCcGpa() {
return;
}
mLabel.clear();
mLabel.add(new CongruenceClosure<>(mWeakEquivalenceGraph.getLogger()));
mLabel.add(mWeqCcManager.getEmptyCc());
return;
}
final CongruenceClosure<NODE> meet;
Expand All @@ -637,7 +636,7 @@ public void meetWithCcGpa() {
+ "is, too, right?";
// we have one "true" disjunct --> the whole disjunction is tautological
mLabel.clear();
mLabel.add(new CongruenceClosure<>(mWeakEquivalenceGraph.getLogger()));
mLabel.add(mWeqCcManager.getEmptyCc());
return;
}
newLabelContents.add(meet);
Expand Down
2 changes: 1 addition & 1 deletion ..._freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCongruenceClosure.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1150,7 +1150,7 @@ public String toLogString() {
if (mWeakEquivalenceGraph != null && !mWeakEquivalenceGraph.isEmpty()) {
sb.append("Weak equivalences:\n");
sb.append(mWeakEquivalenceGraph.toLogString());
} else if (mWeakEquivalenceGraph.isEmpty()) {
} else if (mWeakEquivalenceGraph != null && mWeakEquivalenceGraph.isEmpty()) {
sb.append("weak equivalence graph is empty\n");
} else {
sb.append("weak equivalence graph is null\n");
Expand Down
3 changes: 2 additions & 1 deletion trunk/source/Library-UltimateUtilTest/META-INF/MANIFEST.MF
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@ Bundle-SymbolicName: de.uni_freiburg.informatik.ultimate.lib.util.test
Bundle-Version: 0.1.23
Fragment-Host: de.uni_freiburg.informatik.ultimate.lib.util
Bundle-RequiredExecutionEnvironment: JavaSE-1.8
Require-Bundle: org.junit
Require-Bundle: org.junit,
de.uni_freiburg.informatik.ultimate.lib.test
Import-Package: de.uni_freiburg.informatik.ultimate.util.csv,
junit.framework,
org.junit,
Expand Down
137 changes: 118 additions & 19 deletions ...-UltimateUtilTest/src/de/uni_freiburg/informatik/ultimate/util/CongruenceClosureTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,11 @@
import org.junit.Test;

import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
import de.uni_freiburg.informatik.ultimate.test.mocks.ConsoleLogger;
import de.uni_freiburg.informatik.ultimate.util.datastructures.AbstractCCElementFactory;
import de.uni_freiburg.informatik.ultimate.util.datastructures.CcManager;
import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosure;
import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosureComparator;
import de.uni_freiburg.informatik.ultimate.util.datastructures.EqualityStatus;
import de.uni_freiburg.informatik.ultimate.util.datastructures.ICongruenceClosureElement;
import de.uni_freiburg.informatik.ultimate.util.datastructures.RemoveCcElement;
Expand All @@ -23,7 +26,12 @@ public class CongruenceClosureTest {
*/
@Test
public void test01() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -86,7 +94,14 @@ public void test01() {

@Test
public void test02() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

// final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -140,7 +155,14 @@ public void test02() {

@Test
public void test03() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

// final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -176,7 +198,14 @@ public void test03() {

@Test
public void test04() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

// final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -222,7 +251,14 @@ public void test04() {
*/
@Test
public void test05() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

// final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -258,7 +294,14 @@ public void test05() {
*/
@Test
public void test06() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

// final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -293,7 +336,12 @@ public void test06() {
*/
@Test
public void test07() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand All @@ -316,7 +364,12 @@ public void test07() {

@Test
public void test07a() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -344,7 +397,12 @@ public void test07a() {
*/
@Test
public void test07b() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -380,7 +438,12 @@ public void test07b() {
*/
@Test
public void test08() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand All @@ -405,7 +468,12 @@ public void test08() {
*/
@Test
public void test09() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand All @@ -432,8 +500,14 @@ public void test09() {
*/
@Test
public void testOperators1() {
final CongruenceClosure<StringCcElement> cc1 = new CongruenceClosure<>((ILogger) null);
final CongruenceClosure<StringCcElement> cc2 = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc1 = manager.getEmptyCc();
final CongruenceClosure<StringCcElement> cc2 = manager.getEmptyCc();


final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -538,8 +612,13 @@ public void testOperators1() {
*/
@Test
public void testOperators2() {
final CongruenceClosure<StringCcElement> cc1 = new CongruenceClosure<>((ILogger) null);
final CongruenceClosure<StringCcElement> cc2 = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc1 = manager.getEmptyCc();
final CongruenceClosure<StringCcElement> cc2 = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -639,7 +718,12 @@ public void testOperators2() {

@Test
public void testRemove01() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand All @@ -661,7 +745,12 @@ public void testRemove01() {

@Test
public void testRemove02() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand Down Expand Up @@ -691,7 +780,12 @@ public void testRemove02() {

@Test
public void testRemove03() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand All @@ -718,7 +812,12 @@ public void testRemove03() {

@Test
public void testRemove04() {
final CongruenceClosure<StringCcElement> cc = new CongruenceClosure<>((ILogger) null);
final ILogger logger = new ConsoleLogger();
final CongruenceClosureComparator<StringCcElement> ccComparator =
new CongruenceClosureComparator<StringCcElement>();
final CcManager<StringCcElement> manager = new CcManager<>(logger, ccComparator);

final CongruenceClosure<StringCcElement> cc = manager.getEmptyCc();

final StringElementFactory factory = new StringElementFactory();

Expand Down

0 comments on commit e7c4d7c

Please sign in to comment.