PredicateUnifier was called in a solver state that was still unsat fr…

…om the tree-check, in HCSSABuilder.backVersion, towards #143 adapted locking of ManagedScript to better avoid this in the future, reordered interpolant computation and evaluation for that
ultimate-pa · Mar 27, 2017 · 1f5aacf · 1f5aacf
1 parent 5156de1
commit 1f5aacf
Show file tree

Hide file tree

Showing 6 changed files with 66 additions and 46 deletions.
diff --git a/...ckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCInVar.java b/...ckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCInVar.java
@@ -121,12 +121,23 @@ public Term getTerm() {
 		return mTermVariable;
 	}
 
+	public int getInPredPos() {
+		return mInPredPos;
+	}
+
+	public int getArgumentPos() {
+		return mArgumentPos;
+	}
+
+	public Sort getSort() {
+		return mSort;
+	}
+
 	@Override
 	public int hashCode() {
 		return mGloballyUniqueId.hashCode();
 	}
 
-
 	@Override
 	public boolean equals(Object arg0) {
 		if (this == arg0) {

diff --git a/.../source/SmtParser/src/de/uni_freiburg/informatik/ultimate/source/smtparser/SmtParser.java b/.../source/SmtParser/src/de/uni_freiburg/informatik/ultimate/source/smtparser/SmtParser.java
@@ -201,7 +201,8 @@ private void processFile(final File file) throws IOException {
 		if (inHornSolverMode) {
 			mLogger.info("Parsing .smt2 file as a set of Horn Clauses");
 			final ConstructAndInitializeBackendSmtSolver caibss =
-					new HCGBuilderHelper.ConstructAndInitializeBackendSmtSolver(mServices, mStorage, null);
+					new HCGBuilderHelper.ConstructAndInitializeBackendSmtSolver(mServices, mStorage, 
+							"treeAutomizerSolver");
 			script = new HornClauseParserScript(caibss.getScript(), caibss.getLogicForExternalSolver(),
 					caibss.getSolverSettings());
 		} else {

diff --git a/.../uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java b/.../uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java
@@ -304,17 +304,18 @@ private Term getOrConstructCurrentVarVersion(final HCInVar bv) {
 		/**
 		 * We are going through the TreeRun from root to leaf. Thus the first versioning we do is to version the outVars
 		 * of a HornClause according to the versions we got from the parent node.
-		 * @param currentTree 
+		 * @param currentPos 
 		 */
-		public void versionOutVars(int currentTree) {
+		public void versionOutVars(int currentPos) {
 			for (final Entry<IProgramVar, TermVariable> en : mTF.getTransformula().getOutVars().entrySet()) {
 				final HCOutVar hv = (HCOutVar) en.getKey();
 				final TermVariable tv = transferToCurrentScriptIfNecessary(en.getValue());
-				final HCInVar inVar = mTF.getHornClauseSymbolTable().getOrConstructHCInVar(currentTree, 
+				final HCInVar inVar = mTF.getHornClauseSymbolTable().getOrConstructHCInVar(currentPos, 
 						hv.getArgumentPos(), hv.getSort());
 				final Term versioneered = getOrConstructCurrentVarVersion(inVar);
 				mConstants2HCOutVar.put(versioneered, hv);
 				mSubstitutionMapping.put(tv, versioneered);
+				mBackSubstitutionMapping.put(versioneered, hv);
 			}
 		}
 
@@ -337,8 +338,12 @@ public void versionOldVars(final int currentPos) {
 				final TermVariable tv = transferToCurrentScriptIfNecessary(en.getValue());
 				final Term versioneered = setCurrentVarVersion(hv, mCurrentTree);
 //				mConstants2HCOutVar.put(versioneered, hv);
+
 				mSubstitutionMapping.put(tv, versioneered);
-//				mBackSubstitutionMapping.put(versioneered, hv);
+
+				final HCOutVar outVar = mTF.getHornClauseSymbolTable().getOrConstructHCOutVar(hv.getArgumentPos(), 
+						hv.getSort());
+				mBackSubstitutionMapping.put(versioneered, outVar);
 			}
 
 			for (TermVariable aux : mTF.getTransformula().getAuxVars()) {

diff --git a/.../src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java b/.../src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java
@@ -132,15 +132,15 @@ public TreeRun<Term, IPredicate> getFormulasTree() {
 		return mNestedFormulas;
 	}
 
-	protected Term getPredicateVariable(final Term term, final ManagedScript script) {
-		script.lock(this);
+	protected Term getPredicateVariable(final Term term, final ManagedScript script, final Object lockOwner) {
+//		script.lock(this);
 		if (!mTermToAssertion.containsKey(term)) {
 			final String name = getName(term);
-			mTermToAssertion.put(term, script.term(this, name));
+			mTermToAssertion.put(term, script.term(lockOwner, name));
 		}
 
 		final Term result = mTermToAssertion.get(term);
-		script.unlock(this);
+//		script.unlock(this);
 		return result;
 	}
 }
diff --git a/...reiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java b/...reiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java
@@ -198,34 +198,14 @@ protected boolean isAbstractionCorrect() throws AutomataOperationCanceledExcepti
 		return false;
 	}
 
-	public LBool getCounterexampleFeasibility() {
+	public LBool getCounterexampleFeasibility(Object lockOwner) {
 		mChecker = new TreeChecker(mCounterexample, mBackendSmtSolverScript, mInitialPredicate, mFinalPredicate,
 				mLogger, mPredicateUnifier);
 		mSSA = mChecker.getSSA();
-		return mChecker.checkTrace();
+		return mChecker.checkTrace(lockOwner);
 	}
 
-	protected void constructInterpolantAutomaton() throws AutomataOperationCanceledException {
-		// Using simple interpolant automaton : the counterexample's automaton.
-		PostfixTree<Term, IPredicate> postfixT = new PostfixTree<>(mSSA.getFormulasTree());
-
-		Term[] ts = new Term[postfixT.getPostFix().size()];
-		for (int i = 0; i < ts.length; ++i) {
-			ts[i] = mSSA.getPredicateVariable(postfixT.getPostFix().get(i), mBackendSmtSolverScript);
-		}
-		int[] idx = new int[postfixT.getStartIdx().size()];
-		for (int i = 0; i < idx.length; ++i) {
-			idx[i] = postfixT.getStartIdx().get(i);
-		}
-		mBackendSmtSolverScript.lock(this);
-		Term[] interpolants = mBackendSmtSolverScript.getInterpolants(this, ts, idx);
-		mBackendSmtSolverScript.unlock(this);
-
-		Map<IPredicate, Term> interpolantsMap = new HashMap<>();
-		for (int i = 0; i < interpolants.length; ++i) {
-			IPredicate p = postfixT.getPostFixStates().get(i);
-			interpolantsMap.put(p, interpolants[i]);
-		}
+	protected void constructInterpolantAutomaton(Map<IPredicate, Term> interpolantsMap) throws AutomataOperationCanceledException {
 
 		mInterpolAutomaton = ((TreeRun<HornClause, IPredicate>) mCounterexample)
 				.reconstruct(mChecker.rebuild(interpolantsMap)).getAutomaton();
@@ -332,9 +312,9 @@ public Result iterate() throws AutomataLibraryException {
 
 			mBackendSmtSolverScript.lock(this);
 			mBackendSmtSolverScript.push(this, 1);
-			mBackendSmtSolverScript.unlock(this);
-			if (getCounterexampleFeasibility() == LBool.SAT) {
-				mBackendSmtSolverScript.lock(this);
+
+			if (getCounterexampleFeasibility(this) == LBool.SAT) {
+
 				mLogger.info("The program is unsafe, feasible counterexample.");
 				mLogger.info(mCounterexample.getTree());
 				mBackendSmtSolverScript.pop(this, 1);
@@ -343,15 +323,14 @@ public Result iterate() throws AutomataLibraryException {
 
 			}
 			mLogger.debug("Getting Interpolants...");
-			constructInterpolantAutomaton();
+			final Map<IPredicate, Term> interpolantsMap = retrieveInterpolantsMap();
+			mBackendSmtSolverScript.pop(this, 1);
+			mBackendSmtSolverScript.unlock(this);
 
+			constructInterpolantAutomaton(interpolantsMap);
 			mLogger.debug("Interpolant automaton:");
 			mLogger.debug(mInterpolAutomaton);
 
-			mBackendSmtSolverScript.lock(this);
-			mBackendSmtSolverScript.pop(this, 1);
-			mBackendSmtSolverScript.unlock(this);
-
 			mLogger.debug("Refining abstract model...");
 			refineAbstraction();
 			mLogger.debug("Abstraction tree automaton before iteration #" + (mIteration + 1));
@@ -361,6 +340,30 @@ public Result iterate() throws AutomataLibraryException {
 		return Result.UNKNOWN;
 	}
 
+	private Map<IPredicate, Term> retrieveInterpolantsMap() {
+		// Using simple interpolant automaton : the counterexample's automaton.
+		PostfixTree<Term, IPredicate> postfixT = new PostfixTree<>(mSSA.getFormulasTree());
+
+		Term[] ts = new Term[postfixT.getPostFix().size()];
+		for (int i = 0; i < ts.length; ++i) {
+			ts[i] = mSSA.getPredicateVariable(postfixT.getPostFix().get(i), mBackendSmtSolverScript, this);
+		}
+		int[] idx = new int[postfixT.getStartIdx().size()];
+		for (int i = 0; i < idx.length; ++i) {
+			idx[i] = postfixT.getStartIdx().get(i);
+		}
+//		mBackendSmtSolverScript.lock(this);
+		Term[] interpolants = mBackendSmtSolverScript.getInterpolants(this, ts, idx);
+//		mBackendSmtSolverScript.unlock(this);
+
+		final Map<IPredicate, Term> interpolantsMap = new HashMap<>();
+		for (int i = 0; i < interpolants.length; ++i) {
+			IPredicate p = postfixT.getPostFixStates().get(i);
+			interpolantsMap.put(p, interpolants[i]);
+		}
+		return interpolantsMap;
+	}
+
 	protected void computeCFGHoareAnnotation() {
 		return;
 	}

diff --git a/...e/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeChecker.java b/...e/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeChecker.java
@@ -99,8 +99,8 @@ protected HCSsa getSSA() {
 		return mSSABuilder.getSSA();
 	}
 
-	protected LBool checkTrace() {
-		mBackendSmtSolverScript.lock(this);
+	protected LBool checkTrace(Object lockOwner) {
+//		mBackendSmtSolverScript.lock(this);
 		final HCSsa ssa = getSSA();
 		final List<Term> nestedExp = ssa.flatten();
 		HashSet<Integer> visited = new HashSet<>();
@@ -109,12 +109,12 @@ protected LBool checkTrace() {
 			if (!visited.contains(ssa.getCounter(t))) {
 				mLogger.debug("assert: " + ssa.getName(t) + " :: " + t.toString());
 				visited.add(ssa.getCounter(t));
-				final Term annT = mBackendSmtSolverScript.annotate(this, t, ann);
+				final Term annT = mBackendSmtSolverScript.annotate(lockOwner, t, ann);
 				mBackendSmtSolverScript.assertTerm(this, annT);
 			}
 		}
-		final LBool result = mBackendSmtSolverScript.checkSat(this);
-		mBackendSmtSolverScript.unlock(this);
+		final LBool result = mBackendSmtSolverScript.checkSat(lockOwner);
+//		mBackendSmtSolverScript.unlock(this);
 		return result;
 	}
 }