Skip to content

Commit

Permalink
#239, CongruenceClosure.projectToElements now also keeps constraints …
Browse files Browse the repository at this point in the history
…that refer to elements that are equivalent to an element in the parameter set (perhaps make removeSimpleElementWithReplacementPreference obsolete)
  • Loading branch information
alexandernutz committed Oct 6, 2017
1 parent 0228e8a commit af5109a
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 5 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -282,7 +282,12 @@ WeakEquivalenceGraph<ACTION, NODE> join(final WeakEquivalenceGraph<ACTION, NODE>
if (other.mPartialArrangement.hasElements(source, target)
&& other.mPartialArrangement.getEqualityStatus(source, target) == EqualityStatus.EQUAL) {
// case "weak equivalence in this, strong equivalence in other"
newWeakEquivalenceEdges.put(thisWeqEdge.getKey(), thisWeqEdge.getValue());

final WeakEquivalenceGraph<ACTION, NODE>.WeakEquivalenceEdgeLabel newEdgeLabel = thisWeqEdge.getValue()
.meet(Collections.singletonList(this.mPartialArrangement))
.projectToElements(mFactory.getAllWeqNodes());

newWeakEquivalenceEdges.put(thisWeqEdge.getKey(), newEdgeLabel);
assert correspondingWeqEdgeInOther == null;
continue;
}
Expand All @@ -305,7 +310,11 @@ WeakEquivalenceGraph<ACTION, NODE> join(final WeakEquivalenceGraph<ACTION, NODE>

if (this.mPartialArrangement.hasElements(source, target)
&& this.mPartialArrangement.getEqualityStatus(source, target) == EqualityStatus.EQUAL) {
newWeakEquivalenceEdges.put(otherWeqEdge.getKey(), otherWeqEdge.getValue());
final WeakEquivalenceGraph<ACTION, NODE>.WeakEquivalenceEdgeLabel newEdgeLabel = otherWeqEdge.getValue()
.meet(Collections.singletonList(other.mPartialArrangement))
.projectToElements(mFactory.getAllWeqNodes());

newWeakEquivalenceEdges.put(otherWeqEdge.getKey(), newEdgeLabel);
continue;
}
}
Expand Down Expand Up @@ -1209,8 +1218,13 @@ public void projectElement(final NODE elem,// final NODE newRep,
* <li> However, if q was the representative and not j, we would get
* meet = {q, j} -- rep: q, {a[q] = i}
* <li> and projectToElements would keep both blocks
*
* EDIT: actually, a fix to projectToElements, removes the necessity for
* removeSimpleElementWithReplacementPreference at this place (--> we keep the constraint
* {a[j] = i} by detecting that j = q)
*/
meet.removeSimpleElementWithReplacementPreference(elem, mFactory.getAllWeqNodes());
// meet.removeSimpleElementWithReplacementPreference(elem, mFactory.getAllWeqNodes());
meet.removeSimpleElement(elem);
// meet.transformElementsAndFunctions(node -> node.replaceSubNode(replacer, replacee));

final CongruenceClosure<NODE> newPa = meet.projectToElements(mFactory.getAllWeqNodes());
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1212,11 +1212,23 @@ public boolean isConstrained(final ELEM elem) {
* @return
*/
public CongruenceClosure<ELEM> projectToElements(final Set<ELEM> set) {
// final CongruenceClosure<ELEM> result = new CongruenceClosure<>(this);
/*
* we need to augment the set such that all equivalent elements are contained, too.
* example:
* we project to {q}
* current partition: {q, i} {a[i], 0}
* then the second block implicitly puts a constraint on q, too, thus we need to keep it.
*/
final HashSet<ELEM> augmentedSet = new HashSet<>();
for (final ELEM e : set) {
if (hasElement(e)) {
augmentedSet.addAll(mElementTVER.getEquivalenceClass(e));
}
}

// collect all elements that contain an element from the given set as a sub-node (i.e. child/descendant)
final Set<ELEM> elemsWithSubFromSet =
getAllElements().stream().filter(e -> hasSubElement(e, set)).collect(Collectors.toSet());
getAllElements().stream().filter(e -> hasSubElement(e, augmentedSet)).collect(Collectors.toSet());

final ThreeValuedEquivalenceRelation<ELEM> newTver =
mElementTVER.filterAndKeepOnlyConstraintsThatIntersectWith(elemsWithSubFromSet);
Expand Down

0 comments on commit af5109a

Please sign in to comment.