reimplemented HCHoareTripleChecker's check method for new HCIn/OutVar…

…-scheme, see #143
ultimate-pa · Mar 29, 2017 · 55dbd26 · 55dbd26
1 parent f7bf98a
commit 55dbd26
Show file tree

Hide file tree

Showing 5 changed files with 144 additions and 17 deletions.
diff --git a/...kerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCOutVar.java b/...kerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCOutVar.java
@@ -43,7 +43,7 @@
  * @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
  *
  */
-public class HCOutVar implements IProgramVar {
+public class HCOutVar implements IProgramVar, Comparable<HCOutVar> {
 
 	private static final long serialVersionUID = 4653727851496150630L;
 
@@ -155,6 +155,11 @@ public Sort getSort() {
 		return mSort;
 	}
 
+	@Override
+	public int compareTo(HCOutVar arg0) {
+		return this.mArgumentPos - arg0.mArgumentPos;
+	}
+
 
 //	@Override
 //	public String getIdentifier() {

diff --git a/...rUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HornClause.java b/...rUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HornClause.java
@@ -1,5 +1,6 @@
 package de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil;
 
+import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
@@ -40,17 +41,22 @@ public class HornClause implements IInternalAction {
 	private final List<HornClausePredicateSymbol> mBodyPreds;
 
 	private final List<List<TermVariable>> mBodyPredToTermVariables;
+	private final List<List<HCInVar>> mBodyPredToHCInVars;
+	private List<List<IProgramVar>> mBodyPredToIProgramVar;
 
 	/**
 	 * Stores for the predicate symbol in the head at every argument position of the represented atom, which
 	 * TermVariable in the transition formula represents that argument in the represented atom.
 	 */
 	private final List<TermVariable> mHeadPredTermVariables;
+	private final List<IProgramVar> mHeadPredProgramVariables;
 	private final HornClausePredicateSymbol mHeadPredicate;
 
 	private final UnmodifiableTransFormula mTransitionFormula;
 
 	private final HCSymbolTable mHornClauseSymbolTable;
+
+
 
 /**
 	 * Standard constructor for a Horn clause as used by TreeAutomizer.
@@ -90,7 +96,11 @@ public HornClause(final ManagedScript script,
 		mHeadPredicate = head;
 		mBodyPreds = bodyPreds;
 
+		mBodyPredToHCInVars = new ArrayList<>();
+		mBodyPredToIProgramVar = new ArrayList<>();
 
+		mHeadPredProgramVariables = new ArrayList<>();
+
 		/*
 		 * build the TransFormula
 		 */
@@ -99,15 +109,19 @@ public HornClause(final ManagedScript script,
 			final TermVariable tv = mHeadPredTermVariables.get(i);
 			final Sort sort = tv.getSort();
 			final HCOutVar hcOutVar = symbolTable.getOrConstructHCOutVar(i, sort);
+			mHeadPredProgramVariables.add(hcOutVar);
 			outVars.put(hcOutVar, tv);
 		}
 
 		final Map<IProgramVar, TermVariable> inVars = new HashMap<>();
 		for (int i = 0; i < mBodyPredToTermVariables.size(); i++) {
+			mBodyPredToHCInVars.add(new ArrayList<>());
 			for (int j = 0; j < mBodyPredToTermVariables.get(i).size(); j++) {
 				final TermVariable tv = mBodyPredToTermVariables.get(i).get(j);
 				final Sort sort = tv.getSort();
 				final HCInVar hcInVar = symbolTable.getOrConstructHCInVar(i, j, sort);
+				mBodyPredToHCInVars.get(i).add(hcInVar);
+				mBodyPredToIProgramVar.get(i).add(hcInVar);
 				inVars.put(hcInVar, tv);
 			}
 		}
@@ -137,6 +151,34 @@ public List<HornClausePredicateSymbol> getBodyPredicates() {
 		return mBodyPreds;
 	}
 
+	public int getNoBodyPredicates() {
+		return mBodyPreds.size();
+	}
+
+	public TermVariable getPredArgTermVariable(int predPos, int argPos) {
+		return mBodyPredToTermVariables.get(predPos).get(argPos);
+	}
+
+	public List<TermVariable> getTermVariablesForPredPos(int predPos) {
+		return mBodyPredToTermVariables.get(predPos);
+	}
+
+	public List<HCInVar> getHCInVarsForPredPos(int predPos) {
+		return mBodyPredToHCInVars.get(predPos);
+	}
+
+	public List<IProgramVar> getProgramVarsForPredPos(int predPos) {
+		return mBodyPredToIProgramVar.get(predPos);
+	}
+
+	public List<TermVariable> getTermVariablesForHeadPred() {
+		return mHeadPredTermVariables;
+	}
+
+	public List<IProgramVar> getProgramVarsForHeadPred() {
+		return mHeadPredProgramVariables;
+	}
+
 	@Override
 	public String toString() {
 //		String cobody = "";

diff --git a/...iburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCHoareTripleChecker.java b/...iburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCHoareTripleChecker.java
@@ -27,17 +27,26 @@
  */
 package de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer.graph;
 
-import java.util.Collection;
-import java.util.HashSet;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
 import java.util.Set;
+import java.util.TreeSet;
 import java.util.stream.Collectors;
 
+import de.uni_freiburg.informatik.ultimate.logic.Script.LBool;
 import de.uni_freiburg.informatik.ultimate.logic.Term;
+import de.uni_freiburg.informatik.ultimate.logic.Util;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.CfgSmtToolkit;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hoaretriple.IHoareTripleChecker;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hoaretriple.IHoareTripleChecker.Validity;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil.HCOutVar;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil.HCSymbolTable;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil.HornClause;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.Substitution;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.IPredicate;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.MonolithicHoareTripleChecker;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.singletracecheck.PredicateUnifier;
@@ -53,20 +62,26 @@
  */
 public class HCHoareTripleChecker {
 
-	private IHoareTripleChecker mHoareTripleChecker;
-	private PredicateUnifier mPredicateUnifier;
-	private HCPredicateFactory mPredicateFactory;
+	private final IHoareTripleChecker mHoareTripleChecker;
+	private final PredicateUnifier mPredicateUnifier;
+	private final HCPredicateFactory mPredicateFactory;
+	private final CfgSmtToolkit mCfgSmtToolkit;
+	private final ManagedScript mManagedScript;
+	private final HCSymbolTable mSymbolTable;
 
 	/**
 	 * Constructor of HCHoareTripleChecker
 	 * @param predicateUnifier Unifer for the predicates.
 	 * @param cfgSmtToolkit 
 	 * */
 	public HCHoareTripleChecker(final PredicateUnifier predicateUnifier, final CfgSmtToolkit cfgSmtToolkit,
-			final HCPredicateFactory predicateFactory) {
+			final HCPredicateFactory predicateFactory, final HCSymbolTable symbolTable) {
 		mPredicateUnifier = predicateUnifier;
 		mHoareTripleChecker = new MonolithicHoareTripleChecker(cfgSmtToolkit);
 		mPredicateFactory = predicateFactory;
+		mCfgSmtToolkit = cfgSmtToolkit;
+		mManagedScript = cfgSmtToolkit.getManagedScript();
+		mSymbolTable = symbolTable;
 	}
 
 
@@ -79,15 +94,76 @@ public HCHoareTripleChecker(final PredicateUnifier predicateUnifier, final CfgSm
 	 * @param succ
 	 * @return a Validity value for the Hoare triple
 	 */
-	public Validity check(Collection<IPredicate> pre, HornClause hornClause, IPredicate succ) {
+	public Validity check(List<IPredicate> pre, HornClause hornClause, IPredicate succ) {
+		assert pre.size() == hornClause.getNoBodyPredicates();
+
+		mManagedScript.lock(this);
+		mManagedScript.push(this, 1);
+
 		/*
-		Set<IPredicate> preAsIPredicates = pre.stream()
-				.map(pred -> mPredicateFactory.convertToIPredicate(pred)) //(IPredicate) pred)
-				.collect(Collectors.toSet());
-		IPredicate preConditionConjunction = mPredicateUnifier.getOrConstructPredicateForConjunction(preAsIPredicates);
+		 * Compute the precondition
+		 *  - substitute the predicate formulas of the "pre" predicates
+		 *  - conjoin the substituted predicates
 		 */
-		IPredicate preConditionConjunction = mPredicateUnifier.getOrConstructPredicateForConjunction(pre);
+		final Term[] substitutedPredicateFormulas = new Term[pre.size()];
+		for (int predPos = 0; predPos < hornClause.getNoBodyPredicates(); predPos++) {
+			assert pre.get(predPos).getVars().size() == hornClause.getBodyPredicates().get(predPos).getArity();
+			final IPredicate currentPrePred = pre.get(predPos);
 
-		return mHoareTripleChecker.checkInternal(preConditionConjunction, hornClause, succ);
+			final Term substitutedFormula = substitutePredicateFormula(currentPrePred, 
+					hornClause.getProgramVarsForPredPos(predPos));
+			substitutedPredicateFormulas[predPos] = substitutedFormula;
+		}
+
+		final Term preConditionFormula = Util.and(mManagedScript.getScript(), substitutedPredicateFormulas);
+
+		/*
+		 * Compute the postcondition
+		 */
+		final Term postConditionFormula = substitutePredicateFormula(succ, hornClause.getProgramVarsForHeadPred());
+
+
+		mManagedScript.assertTerm(this, preConditionFormula);
+		mManagedScript.assertTerm(this, hornClause.getTransformula().getClosedFormula());
+		mManagedScript.assertTerm(this, postConditionFormula);
+
+		final LBool satResult = mManagedScript.checkSat(this);
+
+		mManagedScript.pop(this, 1);
+		mManagedScript.unlock(this);
+		return IHoareTripleChecker.convertLBool2Validity(satResult);
+	}
+
+
+	/**
+	 * Substitute the formula of an IPredicate over HCOutVars through a given list of ProgramVariabls (appearing in a
+	 *  TransFormula)
+	 * 
+	 * @param predicate
+	 * @param programVars
+	 * @param predicateArity
+	 * @return
+	 */
+	private Term substitutePredicateFormula(final IPredicate predicate, final List<IProgramVar> programVars) {
+		int predicateArity = programVars.size();
+		final List<HCOutVar> sortedHCOutVars = sortHCOutVars(predicate.getVars());
+		assert sortedHCOutVars.size() == predicateArity;
+
+		final Map<Term, Term> substitution = new HashMap<>();
+		for (int argPos = 0; argPos < predicateArity; argPos++) {
+			substitution.put(
+					sortedHCOutVars.get(argPos).getTermVariable(), 
+					programVars.get(argPos).getDefaultConstant());
+		}
+		final Term substitutedFormula = 
+				new Substitution(mManagedScript, substitution).transform(predicate.getFormula());
+		return substitutedFormula;
+	}
+
+
+	private List<HCOutVar> sortHCOutVars(Set<IProgramVar> vars) {
+		TreeSet<HCOutVar> treeSet = new TreeSet<>();
+		treeSet.addAll(vars.stream().map(v -> ((HCOutVar) v)).collect(Collectors.toSet()));
+		return new ArrayList<HCOutVar>(treeSet);
 	}
 }
diff --git a/...e/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCPredicate.java b/...e/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCPredicate.java
@@ -94,11 +94,15 @@ public String toString() {
 		return result;
 	}
 
-	public Set<HornClausePredicateSymbol> getHcPredicatedSymbols() {
+	public Set<HornClausePredicateSymbol> getHcPredicateSymbols() {
 		return mHcPredicateSymbols;
 	}
 
 	public List<TermVariable> getSignature() {
 		return mVariables;
 	}
+
+//	public TermVariable getArgumentTermVariable(int argPos) {
+//		return mVariables.get(argPos);
+//	}
 }
diff --git a/...ni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCStateFactory.java b/...ni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCStateFactory.java
@@ -226,7 +226,7 @@ public IPredicate intersection(IPredicate state1, IPredicate state2) {
 		assert state1.getVars().equals(state2.getVars());
 		assert !(state2 instanceof HCPredicate) : "convention: first argument is an HCPredicate, second is not..";
 
-		final Set<HornClausePredicateSymbol> state1PredSymbols = ((HCPredicate) state1).getHcPredicatedSymbols();
+		final Set<HornClausePredicateSymbol> state1PredSymbols = ((HCPredicate) state1).getHcPredicateSymbols();
 
 		final Term conjoinedFormula = mSimplifier.getSimplifiedTerm(Util.and(mBackendSmtSolverScript.getScript(), 
 				state1.getFormula(), state2.getFormula()));
@@ -253,7 +253,7 @@ public IPredicate merge(Collection<IPredicate> states) {
 
 		for (IPredicate pred : states) {
 			if (pred instanceof HCPredicate) {
-				mergedLocations.addAll(((HCPredicate) pred).getHcPredicatedSymbols());
+				mergedLocations.addAll(((HCPredicate) pred).getHcPredicateSymbols());
 				assert varsForHcPred == null || varsForHcPred.equals(((HCPredicate) pred).getSignature()) : "merging "
 						+ "predicates with a different signature. Does that make sense??";
 				varsForHcPred = ((HCPredicate) pred).getSignature();