#239, continued reworking remove, rework sanityChecks, rework Congrue…

…nceClosure.projectToElements
ultimate-pa · Oct 11, 2017 · 7a59268 · 7a59268
1 parent 5cf3081
commit 7a59268
Show file tree

Hide file tree

Showing 8 changed files with 636 additions and 478 deletions.
diff --git a/...c/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java b/...c/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java
@@ -378,6 +378,7 @@ public void addNode(final NODE nodeToAdd) {
 	public void removeElement(final NODE elemToHavoc) {
 		mPartialArrangement.removeSimpleElement(elemToHavoc);
 		assert mPartialArrangement.elementIsFullyRemoved(elemToHavoc);
+		assert mPartialArrangement.sanityCheck();
 	}
 
 	/**

diff --git a/...i_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraintFactory.java b/...i_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraintFactory.java
@@ -38,6 +38,7 @@
 import de.uni_freiburg.informatik.ultimate.logic.Sort;
 import de.uni_freiburg.informatik.ultimate.logic.Term;
 import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.MultiDimensionalSort;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosureComparator;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap2;
@@ -404,6 +405,19 @@ public CCManager<NODE> getCcManager() {
 		return mCcManager;
 	}
 
+	public List<NODE> getAllWeqVarsNodeForFunction(final NODE func) {
+		if (!func.getSort().isArraySort()) {
+			return Collections.emptyList();
+		}
+		final MultiDimensionalSort mdSort = new MultiDimensionalSort(func.getSort());
+		final List<Sort> indexSorts = mdSort.getIndexSorts();
+		final List<NODE> result = new ArrayList<>(mdSort.getDimension());
+		for (int i = 0; i < mdSort.getDimension(); i++) {
+			result.add(this.getWeqVariableNodeForDimension(i, indexSorts.get(i)));
+		}
+		return result;
+	}
+
 //	public  IIcfgSymbolTable getSymbolTable() {
 //		return mCsToolkit.getSymbolTable();
 //	}

diff --git a/...iburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqNodeAndFunctionFactory.java b/...iburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqNodeAndFunctionFactory.java
@@ -26,10 +26,10 @@
  */
 package de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain;
 
-import java.util.ArrayList;
-import java.util.Collection;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.Map;
+import java.util.Set;
 
 import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
 import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
@@ -201,7 +201,7 @@ protected EqNode newBaseElement(final Term term) {
 			return new EqAtomicBaseNode(term, isTermALiteral(term), this);
 		} else {
 			assert term.getFreeVars().length > 0;
-			final Collection<EqNode> supportingNodes = new ArrayList<>();
+			final Set<EqNode> supportingNodes = new HashSet<>();
 			for (final TermVariable fv : term.getFreeVars()) {
 				supportingNodes.add(getOrConstructNode(fv));
 			}