#295, fixes for obtaining the literal set constraint from an intermed…

…iate eq state
ultimate-pa · Aug 25, 2018 · 59d76be · 59d76be
1 parent 5edce35
commit 59d76be
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 10 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
@@ -447,10 +447,12 @@ public boolean isClosed() {
 	}
 
 	public Set<NODE> getSetConstraintForExpression(final NODE exp) {
-		if (!this.getAllNodes().contains(exp)) {
-			// add it before querying!
-			throw new IllegalArgumentException();
-		}
+//		if (!this.getAllNodes().contains(exp)) {
+//			// add it before querying!
+//			throw new IllegalArgumentException();
+//		}
+
+		mWeqCc.addElement(exp, false);
 
 		final CCLiteralSetConstraints<NODE> lsc = mWeqCc.getCongruenceClosure().getLiteralSetConstraints();
 		final SetConstraintConjunction<NODE> c = lsc.getContainsConstraint(exp);

diff --git a/...i_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraintFactory.java b/...i_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraintFactory.java
@@ -608,4 +608,12 @@ static String[] getNames() {
 	public WeqSettings getWeqSettings() {
 		return mWeqCcManager.getSettings();
 	}
+
+	public EqDisjunctiveConstraint<NODE> closeIfNecessary(final EqDisjunctiveConstraint<NODE> resNotClosed) {
+		final Collection<EqConstraint<NODE>> constraintList = new ArrayList<>();
+		for (final EqConstraint<NODE> c : resNotClosed.getConstraints()) {
+			constraintList.add(closeIfNecessary(c));
+		}
+		return getDisjunctiveConstraint(constraintList);
+	}
 }
diff --git a/...eiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqDisjunctiveConstraint.java b/...eiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqDisjunctiveConstraint.java
@@ -306,14 +306,14 @@ public Set<Term> getSetConstraintForExpression(final Term exp) {
 //			sc = c.getSetConstraintForExpression(locArraySelect);
 //
 //		}
-		final NODE node = mNodeAndFunctionFactory.getExistingNode(exp);
+		final NODE node = mNodeAndFunctionFactory.getOrConstructNode(exp);
 
 		final EqConstraint<NODE> flat = this.flatten();
-		if (!flat.getAllNodes().contains(exp)) {
-			// add it before querying!
-			throw new IllegalArgumentException();
-		}
-
+//		if (!flat.getAllNodes().contains(node)) {
+//			// add it before querying!
+//			mFactory.addEquality(node1, node2, inputConstraint, inplace)
+//		}
+//
 		final Set<NODE> nodes = flat.getSetConstraintForExpression(node);
 		return nodes.stream().map(n -> n.getTerm()).collect(Collectors.toSet());
 	}