reworked ssa building and hoare triple checking in treeAutomizer, #143

ultimate-pa · Aug 5, 2017 · e6d8f38 · e6d8f38
1 parent be2d5f0
commit e6d8f38
Show file tree

Hide file tree

Showing 5 changed files with 199 additions and 317 deletions.
diff --git a/...reeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java b/...reeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java
@@ -2,6 +2,7 @@
 
 import java.math.BigInteger;
 import java.util.Arrays;
+import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 
@@ -32,7 +33,7 @@ public class HCSymbolTable extends DefaultIcfgSymbolTable {
 	private HornClausePredicateSymbol mDontCareHornClausePredSym;
 	private HornClausePredicateSymbol mTrueHornClausePredSym;
 
-	private Map<TermVariable, ApplicationTerm> mTermVarToConst;
+	private final Map<TermVariable, ApplicationTerm> mTermVarToConst = new HashMap<>();
 
 
 	public HCSymbolTable(ManagedScript mgdScript) {
@@ -182,13 +183,21 @@ private Sort[] transferSorts(Sort[] sorts) {
 	 */
 	public void registerTermVariable(TermVariable tv) {
 		assert tv == new TermTransferrer(mManagedScript.getScript()).transform(tv);
-		mManagedScript.lock(this);
-		final ApplicationTerm constant = ProgramVarUtils.constructDefaultConstant(mManagedScript, this, tv.getSort(), 
-				tv.getName());
-		mManagedScript.unlock(this);
-		mTermVarToConst.put(tv, constant);
+		if (!mTermVarToConst.containsKey(tv)) {
+			mManagedScript.lock(this);
+			final ApplicationTerm constant = ProgramVarUtils.constructDefaultConstant(mManagedScript, this, tv.getSort(), 
+					tv.getName());
+			mManagedScript.unlock(this);
+			mTermVarToConst.put(tv, constant);
+		}
 	}
 
+	/**
+	 * Every TermVariable that appears in a HornClause has a default constant associated with it, which is declared
+	 * up front. (used for hoare triple checks)
+	 * @param fv
+	 * @return
+	 */
 	public Term getConstForTermVar(TermVariable fv) {
 		final ApplicationTerm res = mTermVarToConst.get(fv);
 		assert res != null;