From b1b3978a4af23882a221aaf010407e1feafb0d9a Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Mon, 27 Mar 2017 17:24:33 +0200 Subject: [PATCH] intermediate commit, working towards #143 --- .../automata/tree/TreeAutomatonBU.java | 4 + .../ultimate/automata/tree/TreeRun.java | 2 +- .../modelcheckerutils/hornutil/HCInVar.java | 2 +- .../modelcheckerutils/hornutil/HCOutVar.java | 8 + .../hornutil/HornClause.java | 17 ++- .../graph/HCPredicateFactory.java | 121 ++++++++++----- .../treeautomizer/graph/HCSSABuilder.java | 138 ++++++++++++------ 7 files changed, 200 insertions(+), 92 deletions(-) diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeAutomatonBU.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeAutomatonBU.java index f93f5db9693..8abc0df44c1 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeAutomatonBU.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeAutomatonBU.java @@ -228,6 +228,10 @@ public Set getInitialStates() { return mInitalStates; } + public Set getFinalStates() { + return mFinalStates; + } + @Override public Set getStates() { return mStates; diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeRun.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeRun.java index 665cd2152a6..97d07ff2ec3 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeRun.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeRun.java @@ -87,7 +87,7 @@ public TreeRun reconstruct(final Map stMap) { return new TreeRun<>(stMap.containsKey(state) ? stMap.get(state) : null, letter, child); } - public Collection> getChildren() { + public List> getChildren() { return children; } diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCInVar.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCInVar.java index a5dcb07627b..afda16e4e14 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCInVar.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCInVar.java @@ -47,7 +47,6 @@ public class HCInVar implements IProgramVar { private static final long serialVersionUID = 4653727851496150630L; - private final TermVariable mTermVariable; private final int mInPredPos; private final int mArgumentPos; @@ -58,6 +57,7 @@ public class HCInVar implements IProgramVar { private final Sort mSort; + private final TermVariable mTermVariable; private final ApplicationTerm mDefaultConstant; private final ApplicationTerm mPrimedConstant; diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCOutVar.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCOutVar.java index dcf5099812c..1c0073c032b 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCOutVar.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCOutVar.java @@ -147,6 +147,14 @@ public boolean equals(Object arg0) { return true; } + public int getArgumentPos() { + return mArgumentPos; + } + + public Sort getSort() { + return mSort; + } + // @Override // public String getIdentifier() { diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HornClause.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HornClause.java index dff590b7a57..d27a1e286e9 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HornClause.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HornClause.java @@ -49,10 +49,10 @@ public class HornClause implements IInternalAction { private final HornClausePredicateSymbol mHeadPredicate; private final UnmodifiableTransFormula mTransitionFormula; + + private final HCSymbolTable mHornClauseSymbolTable; -// private final HCTransFormula mHcTransFormula; - - /** +/** * Standard constructor for a Horn clause as used by TreeAutomizer. * * @param script The script that will be used in TreeAutomizer (not the HornClauseParserScript) @@ -85,6 +85,7 @@ public HornClause(final ManagedScript script, .collect(Collectors.toList())) .collect(Collectors.toList()); + mHornClauseSymbolTable = symbolTable; mHeadPredicate = head; mBodyPreds = bodyPreds; @@ -151,10 +152,10 @@ public String toString() { // // final String body = mHeadPredicate.getName() + mHeadPredTermVariables; -// return mTransitionFormula.getFormula().toString(); + return mTransitionFormula.getFormula().toString(); //return String.format("(%s) ^^ (%s) ~~> (%s) || in : %s || out : %s ", cobody, mTransitionFormula, body, //return String.format("(%s) ^^ (%s) ~~> (%s)", cobody, mTransitionFormula.getFormula(), body); - return "HornClause TODO: better description"; //TODO +// return "HornClause TODO: better description"; //TODO } /** @@ -173,6 +174,12 @@ public String getSucceedingProcedure() { return HornUtilConstants.HORNCLAUSEMETHODNAME; } + // private final HCTransFormula mHcTransFormula; + + public HCSymbolTable getHornClauseSymbolTable() { + return mHornClauseSymbolTable; + } + // public HCTransFormula getHcTransformula() { // return mHcTransFormula; // } diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCPredicateFactory.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCPredicateFactory.java index 5988edfa416..5ae22205804 100644 --- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCPredicateFactory.java +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCPredicateFactory.java @@ -29,6 +29,7 @@ import java.util.Collections; import java.util.HashMap; +import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Set; @@ -38,6 +39,7 @@ import de.uni_freiburg.informatik.ultimate.logic.Term; import de.uni_freiburg.informatik.ultimate.logic.TermVariable; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar; +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.HornClausePredicateSymbol; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils.SimplificationTechnique; @@ -63,6 +65,7 @@ public class HCPredicateFactory extends PredicateFactory { /** * The constructor of HornClause Factory + * * @param services * @param mgdScript * @param symbolTable @@ -87,9 +90,11 @@ public HCPredicateFactory(IUltimateServiceProvider services, ManagedScript mgdSc /** * Create a True predicate with symbol. - * @param headPredicate The given symbol + * + * @param headPredicate + * The given symbol * @return The new true HCPredicate - * */ + */ public HCPredicate createTruePredicateWithLocation(HornClausePredicateSymbol headPredicate) { mBackendSmtSolverScript.lock(this); final HCPredicate result = newPredicate(headPredicate, mBackendSmtSolverScript.term(this, "true"), @@ -109,50 +114,61 @@ public HCPredicate getFalsePredicate() { public HCPredicate getDontCarePredicate() { return mDontCarePredicate; } - -// public HCPredicate convertItoHCPredicate(final IPredicate p) { -// return newPredicate(mSymbolTable.getDontCareHornClausePredicateSymbol(), p.getFormula(), new HashMap<>()); -// } + + // public HCPredicate convertItoHCPredicate(final IPredicate p) { + // return newPredicate(mSymbolTable.getDontCareHornClausePredicateSymbol(), + // p.getFormula(), new HashMap<>()); + // } private HCPredicate newPredicate(HornClausePredicateSymbol loc, Term term, List vars) { - return new HCPredicate(loc, term, computeHcOutVarsFromTermVariables(vars), computeClosedFormula(term), vars); + final ComputeHcOutVarsAndNormalizeTerm chovant = new ComputeHcOutVarsAndNormalizeTerm(term, vars); + + return new HCPredicate(loc, chovant.getNormalizedTerm(), chovant.getProgramVars(), + computeClosedFormula(chovant.getNormalizedTerm()), vars); } - + public HCPredicate newHCPredicate(HornClausePredicateSymbol loc, Term term, List vars) { return newPredicate(loc, term, vars); } - - -// /** -// * Create a new predicate from symbol and formula. -// * -// * @param mProgramPoint -// * symbol -// * @param hashCode -// * hash code of the formula -// * @param formula -// * The formula of the predicate -// * @param vars -// * the set of variables of the formula -// * @param termToHcVar -// * a map of the variables to HCVars. -// * @return HCPredicate the new predicate -// */ -// public HCPredicate newPredicate(final HornClausePredicateSymbol mProgramPoint, final int hashCode, -// final Term formula, final Set vars, final Map termToHcVar) { -// return new HCPredicate(mProgramPoint, hashCode, formula, vars, termToHcVar, computeClosedFormula(formula)); -// } - - /** - * - * @param vars - * @return - */ - private Set computeHcOutVarsFromTermVariables(List vars) { - // TODO - return null; - } + // /** + // * Create a new predicate from symbol and formula. + // * + // * @param mProgramPoint + // * symbol + // * @param hashCode + // * hash code of the formula + // * @param formula + // * The formula of the predicate + // * @param vars + // * the set of variables of the formula + // * @param termToHcVar + // * a map of the variables to HCVars. + // * @return HCPredicate the new predicate + // */ + // public HCPredicate newPredicate(final HornClausePredicateSymbol + // mProgramPoint, final int hashCode, + // final Term formula, final Set vars, final Map + // termToHcVar) { + // return new HCPredicate(mProgramPoint, hashCode, formula, vars, + // termToHcVar, computeClosedFormula(formula)); + // } + + // /** + // * + // * @param vars + // * @return + // */ + // private Set + // computeHcOutVarsFromTermVariables(List vars) { + // final Set result = new HashSet<>(); + // for (int i = 0; i < vars.size(); i++) { + // final HCOutVar hcOutVar = mSymbolTable.getOrConstructHCOutVar(i, + // vars.get(i).getSort()); + // result.add(hcOutVar); + // } + // return result; + // } private Term computeClosedFormula(final Term formula) { final Map substitutionMapping = new HashMap<>(); @@ -162,4 +178,31 @@ private Term computeClosedFormula(final Term formula) { } return new Substitution(mBackendSmtSolverScript, substitutionMapping).transform(formula); } + + class ComputeHcOutVarsAndNormalizeTerm { + private final Term mNormalizedTerm; + private final Set mProgramVars; + + public ComputeHcOutVarsAndNormalizeTerm(Term formula, List variables) { + final Map normalizingSubstitution = new HashMap<>(); + final Set hcOutVars = new HashSet<>(); + + for (int i = 0; i < variables.size(); i++) { + final HCOutVar hcOutVar = mSymbolTable.getOrConstructHCOutVar(i, variables.get(i).getSort()); + hcOutVars.add(hcOutVar); + normalizingSubstitution.put(variables.get(i), hcOutVar.getTermVariable()); + } + + mNormalizedTerm = new Substitution(mScript, normalizingSubstitution).transform(formula); + mProgramVars = hcOutVars; + } + + public Term getNormalizedTerm() { + return mNormalizedTerm; + } + + public Set getProgramVars() { + return mProgramVars; + } + } } diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java index 364bb754740..e5488334b27 100644 --- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java @@ -41,6 +41,7 @@ import de.uni_freiburg.informatik.ultimate.logic.TermVariable; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.MultiElementCounter; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar; +import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil.HCInVar; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil.HCOutVar; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil.HornClause; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils; @@ -81,8 +82,18 @@ public class HCSSABuilder { protected final Map mConstants2HCOutVar = new HashMap<>(); private final TermTransferrer mTermTransferrer; private final MultiElementCounter mConstForTvCounter = new MultiElementCounter<>(); - private final Map mCurrentLocalAndOldVarVersion; - private final NestedMap2 mIndexedVarRepresentative = new NestedMap2<>(); + + /** + * When we match the outVars of a HornClause H1 to the inVars of a HornClause H2, (H1 is the child of H2 in the + * TreeRun), the matching depends on + * - the child index of H1, i.e., the i, in "H1 is the i-th child of H2), called PredPos + * - the index of the variable in the predicate, called argPos + */ +// private final NestedMap2 mPredPosToArgPosToCurrentVarVersion; + private final Map mCurrentHcInVarVersion; + + + private final NestedMap2 mIndexedVarRepresentative = new NestedMap2<>(); private final Map, VariableVersioneer> mSubsMap; private final Map mCounters; @@ -115,7 +126,8 @@ public HCSSABuilder(final ITreeRun trace, final IPredica mSubsMap = new HashMap<>(); mPredicateUnifier = predicateUnifier; - mCurrentLocalAndOldVarVersion = new HashMap<>(); +// mPredPosToArgPosToCurrentVarVersion = new NestedMap2<>(); + mCurrentHcInVarVersion = new HashMap<>(); mResult = buildSSA(); } @@ -124,7 +136,7 @@ public HCSsa getSSA() { } - private int getIndex(final TreeRun tree) { + private int getOrConstructIndex(final TreeRun tree) { if (!mIdxMap.containsKey(tree)) { ++mCurrentIdx; mIdxMap.put(tree, mCurrentIdx); @@ -147,7 +159,7 @@ public Map rebuildSSApredicates(final Map tree, final Map res, final Map interpolantsMap) { for (final TreeRun child : tree.getChildren()) { - mCurrentTree = getIndex(tree); + mCurrentTree = getOrConstructIndex(tree); rebuild(child, res, interpolantsMap); } @@ -155,7 +167,7 @@ private void rebuild(final TreeRun tree, final Map tree, final Map buildNestedFormulaTree(final TreeRun tree, - int treeIdx) { + int treeIdx, int childPos) { // /* // * exit condition @@ -179,19 +191,23 @@ private TreeRun buildNestedFormulaTree(final TreeRun> childTrees = new ArrayList<>(); - for (final TreeRun child : tree.getChildren()) { - mCurrentTree = getIndex(tree); - childTrees.add(buildNestedFormulaTree(child, mCurrentTree)); +// for (final TreeRun child : tree.getChildren()) { + for (int i = 0; i < tree.getChildren().size(); i++) { + TreeRun child = tree.getChildren().get(i); + mCurrentTree = getOrConstructIndex(tree); + if (child.getRootSymbol() != null) { + childTrees.add(buildNestedFormulaTree(child, mCurrentTree, i)); + } } @@ -202,12 +218,12 @@ private TreeRun buildNestedFormulaTree(final TreeRun tree = buildNestedFormulaTree((TreeRun) mTreeRun, 0); + final TreeRun tree = buildNestedFormulaTree((TreeRun) mTreeRun, 0, 0); mCurrentTree = 0; final VariableVersioneer vvPost = new VariableVersioneer(mPostCondition); - vvPost.versionPredicate(); + vvPost.versionPredicate(mCurrentTree); return new HCSsa(tree, vvPre.getVersioneeredTerm(), vvPost.getVersioneeredTerm(), mCounters); } @@ -240,8 +256,9 @@ public VariableVersioneer(final IPredicate p) { /** * Build constant bv_index that represents BoogieVar bv that obtains a new * value at position index. + * @param predPos */ - private Term buildVersion(final HCOutVar bv, final int index) { + private Term buildVersion(final HCInVar bv, final int index) { assert mIndexedVarRepresentative.get(bv) == null || !mIndexedVarRepresentative.get(bv).containsKey(index) : "version was already constructed"; final Sort sort = transferToCurrentScriptIfNecessary(bv.getTermVariable()).getSort(); @@ -255,18 +272,28 @@ private Term buildVersion(final HCOutVar bv, final int index) { * Set the current version of BoogieVariable bv to the constant b_index and * return b_index. */ - private Term setCurrentVarVersion(final HCOutVar bv, final int index) { - final Term var = buildVersion(bv, index); - if (mCurrentLocalAndOldVarVersion.containsKey(bv)) { - mCurrentLocalAndOldVarVersion.remove(bv); - } - mCurrentLocalAndOldVarVersion.put(bv, var); + private Term setCurrentVarVersion(final HCInVar inVar, final int index) { + final Term var = buildVersion(inVar, index); + mCurrentHcInVarVersion.put(inVar, var); +// mPredPosToArgPosToCurrentVarVersion.put(predPos, argPos, var); +// if (mCurrentLocalAndOldVarVersion.containsKey(argPos)) { +// mCurrentLocalAndOldVarVersion.remove(argPos); +// } +// mCurrentLocalAndOldVarVersion.put(argPos, var); return var; } - private Term getCurrentVarVersion(final HCOutVar bv) { - Term result = mCurrentLocalAndOldVarVersion.get(bv); + /** + * If we currently keep a versioned Term for bv, returns that; + * otherwise returns a freshly versioned Term for bv. + * @param bv + * @return + */ +// private Term getOrConstructCurrentVarVersion(final HCOutVar bv) { + private Term getOrConstructCurrentVarVersion(final HCInVar bv) { +// Term result = mCurrentLocalAndOldVarVersion.get(bv); + Term result = mCurrentHcInVarVersion.get(bv); if (result == null) { // variable was not yet assigned in the calling context result = setCurrentVarVersion(bv, mCurrentTree); @@ -274,31 +301,48 @@ private Term getCurrentVarVersion(final HCOutVar bv) { return result; } - public void versionInVars() { - for (final IProgramVar bv : mTF.getTransformula().getInVars().keySet()) { - HCOutVar hv = (HCOutVar) bv; - final TermVariable tv = transferToCurrentScriptIfNecessary(mTF.getTransformula().getInVars().get(hv)); - final Term versioneered = getCurrentVarVersion(hv); + /** + * 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 + */ + public void versionOutVars(int currentTree) { + for (final Entry en : mTF.getTransformula().getOutVars().entrySet()) { + final HCOutVar hv = (HCOutVar) en.getKey(); + final TermVariable tv = transferToCurrentScriptIfNecessary(en.getValue()); + final HCInVar inVar = mTF.getHornClauseSymbolTable().getOrConstructHCInVar(currentTree, + hv.getArgumentPos(), hv.getSort()); + final Term versioneered = getOrConstructCurrentVarVersion(inVar); mConstants2HCOutVar.put(versioneered, hv); mSubstitutionMapping.put(tv, versioneered); } } - public void versionAssignedVars(final int currentPos) { - - for (final IProgramVar bv : mTF.getTransformula().getInVars().keySet()) { - HCOutVar hv = (HCOutVar) bv; - final Term versioneered = getCurrentVarVersion(hv); - mBackSubstitutionMapping.put(versioneered, hv); - } - - for (final IProgramVar bv : mTF.getTransformula().getOutVars().keySet()) { - HCOutVar hv = (HCOutVar) bv; - final TermVariable tv = transferToCurrentScriptIfNecessary(mTF.getTransformula().getOutVars().get(hv)); - final Term versioneered = setCurrentVarVersion(hv, currentPos); - mConstants2HCOutVar.put(versioneered, hv); + /** + * As we are going through the TreeRun from root to leaf, the second versioning step is to version all the vars + * that are used by the child, but are not seen by the parent. This is the analogue to the assigned vars when + * we are going from start to end of a trace.. + * @param currentPos + */ + public void versionOldVars(final int currentPos) { + +// for (final IProgramVar bv : mTF.getTransformula().getInVars().keySet()) { +// HCOutVar hv = (HCOutVar) bv; +// final Term versioneered = getOrConstructCurrentVarVersion(hv); +// mBackSubstitutionMapping.put(versioneered, hv); +// } +// + for (final Entry en : mTF.getTransformula().getInVars().entrySet()) { + HCInVar hv = (HCInVar) en.getKey(); + final TermVariable tv = transferToCurrentScriptIfNecessary(en.getValue()); + final Term versioneered = setCurrentVarVersion(hv, mCurrentTree); +// mConstants2HCOutVar.put(versioneered, hv); mSubstitutionMapping.put(tv, versioneered); - mBackSubstitutionMapping.put(versioneered, hv); +// mBackSubstitutionMapping.put(versioneered, hv); + } + + for (TermVariable aux : mTF.getTransformula().getAuxVars()) { + assert false : "rename this, too, right?.."; } } @@ -313,11 +357,13 @@ private Term constructFreshConstant(final TermVariable tv) { return result; } - public void versionPredicate() { + public void versionPredicate(int currentTree) { for (final IProgramVar bv : mPred.getVars()) { final HCOutVar hv = (HCOutVar) bv; final TermVariable tv = transferToCurrentScriptIfNecessary(hv.getTermVariable()); - final Term versioneered = getCurrentVarVersion(hv); + final HCInVar inVar = mTF.getHornClauseSymbolTable().getOrConstructHCInVar(currentTree, + hv.getArgumentPos(), hv.getSort()); + final Term versioneered = getOrConstructCurrentVarVersion(inVar); mConstants2HCOutVar.put(versioneered, hv); mSubstitutionMapping.put(tv, versioneered); mBackSubstitutionMapping.put(versioneered, hv);