From eb54cd7738d0675b52c9bf496130fa650f0da621 Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Thu, 21 Sep 2017 23:11:35 +0200 Subject: [PATCH] (Weq)CongruenceClosure: added sanityCheck, fixes to auxdata handling, #224 --- .../vp/states/WeqCongruenceClosure.java | 5 +- .../datastructures/CongruenceClosure.java | 68 ++++++++++++++++--- 2 files changed, 64 insertions(+), 9 deletions(-) diff --git a/trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/WeqCongruenceClosure.java b/trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/WeqCongruenceClosure.java index b3957f9419d..7033d07e2a5 100644 --- a/trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/WeqCongruenceClosure.java +++ b/trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/states/WeqCongruenceClosure.java @@ -720,6 +720,10 @@ private boolean removeElement(final NODE elem, final CongruenceClosure cop for (final NODE parent : mFaAuxData.getArgParents(elem)) { removeElement(parent, copy); } + if (elem.isFunctionApplication()) { + mFaAuxData.removeAfParent(elem.getAppliedFunction(), elem); + mFaAuxData.removeArgParent(elem.getArgument(), elem); + } for (final NODE dependent : new HashSet<>(mNodeToDependents.getImage(elem))) { removeElement(dependent, copy); @@ -809,7 +813,6 @@ public boolean isConstrained(final NODE elem) { @Override protected void registerNewElement(final NODE elem) { - assert sanityCheck(); super.registerNewElement(elem); if (elem.isDependent()) { diff --git a/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java b/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java index e090f3e1ffe..74656f69a64 100644 --- a/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java +++ b/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java @@ -222,17 +222,15 @@ protected boolean addElement(final ELEM elem) { * @param elem */ protected void registerNewElement(final ELEM elem) { - assert sanityCheck(); if (!elem.isFunctionApplication()) { // nothing to do assert mElementTVER.getRepresentative(elem) != null : "this method assumes that elem has been added " + "already"; + assert sanityCheck(); return; } - addElement(elem.getAppliedFunction()); - addElement(elem.getArgument()); mFaAuxData.addAfParent(elem.getAppliedFunction(), elem); mFaAuxData.addArgParent(elem.getArgument(), elem); @@ -242,6 +240,10 @@ protected void registerNewElement(final ELEM elem) { * (could be circumvented, I suppose..) */ final HashRelation equalitiesToPropagate = mAuxData.registerNewElement(elem); + + addElement(elem.getAppliedFunction()); + addElement(elem.getArgument()); + for (final Entry eq : equalitiesToPropagate.entrySet()) { reportEquality(eq.getKey(), eq.getValue()); } @@ -497,6 +499,45 @@ protected boolean sanityCheck() { return false; } + /* + * check that for each function application a[i], its representative's ccchild contains the corresponding + * af/arg-pair (a,i) + */ + for (final ELEM elem : getAllElements()) { + if (!elem.isFunctionApplication()) { + continue; + } + final ELEM rep = getRepresentativeElement(elem); + if (!mAuxData.getCcChildren(rep).containsPair(elem.getAppliedFunction(), elem.getArgument())) { + assert false; + return false; + } + } + + /* + * check that for each element, its parents in funcAppTreeAuxData and ccAuxData agree + */ + for (final ELEM elem : getAllElements()) { + + + final Set afCcparFromDirectParents = new HashSet<>(); + final Set argCcparFromDirectParents = new HashSet<>(); + for (final ELEM eqcMember : mElementTVER.getEquivalenceClass(elem)) { + afCcparFromDirectParents.addAll(mFaAuxData.getAfParents(eqcMember)); + argCcparFromDirectParents.addAll(mFaAuxData.getArgParents(eqcMember)); + } + + final ELEM rep = getRepresentativeElement(elem); + if (!afCcparFromDirectParents.equals(mAuxData.getAfCcPars(rep))) { + assert false; + return false; + } + if (!argCcparFromDirectParents.equals(mAuxData.getArgCcPars(rep))) { + assert false; + return false; + } + } + /* * check that all elements that are related are of the same type * while same type means here: @@ -718,7 +759,7 @@ protected class CcAuxData { private final HashRelation mAfCcPars; private final HashRelation mArgCcPars; - Map> mCcChildren = new HashMap<>(); + private final Map> mCcChildren; /** * normally we only allow get..(elem) calls when elem is a representative of the encolosing CongruenceClosure @@ -729,12 +770,17 @@ protected class CcAuxData { CcAuxData() { mAfCcPars = new HashRelation<>(); mArgCcPars = new HashRelation<>(); + mCcChildren = new HashMap<>(); mOmitRepresentativeChecks = false; } public CcAuxData(final CcAuxData auxData, final boolean omitRepresentativeChecks) { mAfCcPars = new HashRelation<>(auxData.mAfCcPars); mArgCcPars = new HashRelation<>(auxData.mArgCcPars); + mCcChildren = new HashMap<>(); + for (final Entry> en : auxData.mCcChildren.entrySet()) { + mCcChildren.put(en.getKey(), new HashRelation<>(en.getValue())); + } mOmitRepresentativeChecks = omitRepresentativeChecks; } @@ -935,14 +981,19 @@ public void removeElement(final ELEM elem, final boolean elemWasRepresentative, HashRelation registerNewElement(final ELEM elem) { assert elem.isFunctionApplication() : "right?.."; - final ELEM afRep = mElementTVER.getRepresentative(elem.getAppliedFunction()); - final ELEM argRep = mElementTVER.getRepresentative(elem.getArgument()); + final ELEM afRep = hasElement(elem.getAppliedFunction()) ? + mElementTVER.getRepresentative(elem.getAppliedFunction()) : + elem.getAppliedFunction(); + final ELEM argRep = hasElement(elem.getArgument()) ? + mElementTVER.getRepresentative(elem.getArgument()) : + elem.getArgument(); final HashRelation equalitiesToPropagate = new HashRelation<>(); final Set afCcPars = mAfCcPars.getImage(afRep); final Set candidates = afCcPars.stream() - .filter(afccpar -> (hasElement(afccpar.getArgument()) && + .filter(afccpar -> (hasElement(argRep) && + hasElement(afccpar.getArgument()) && getEqualityStatus(argRep, afccpar.getArgument()) == EqualityStatus.EQUAL)) .collect(Collectors.toSet()); candidates.forEach(c -> equalitiesToPropagate.addPair(elem, c)); @@ -1030,7 +1081,8 @@ public void transformElements(final Function elemTransformer) { for (final Entry> en : new HashMap<>(mCcChildren).entrySet()) { mCcChildren.remove(en.getKey()); - assert !mCcChildren.values().contains(en.getValue()) : "just to make sure there's no overlap in the " + assert en.getValue().isEmpty() || + !mCcChildren.values().contains(en.getValue()) : "just to make sure there's no overlap in the " + "map's image values"; en.getValue().transformElements(elemTransformer, elemTransformer); mCcChildren.put(elemTransformer.apply(en.getKey()), en.getValue());