Skip to content

Commit

Permalink
#295, when replacing an array equality with an array equality with lo…
Browse files Browse the repository at this point in the history 
…c-array updates, do the position-based substitution and the term-based substitution in one go (otherwise it is impossible to build Terms as they will have the wrong type)
  • Loading branch information
@alexandernutz
alexandernutz committed Aug 24, 2018
1 parent 234d561 commit dfbc2ac
Show file tree
Hide file tree
Showing 3 changed files with 109 additions and 81 deletions.
18 changes: 10 additions & 8 deletions ...tik/ultimate/icfgtransformer/heapseparator/datastructures/ArrayEqualityLocUpdateInfo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SubTermFinder;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.Substitution;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.MultiDimensionalSort;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;

Expand Down Expand Up @@ -102,16 +101,17 @@ private void computeResult() {
final int currentDim = dim;

// substitute arrays with their loc-arrays for the current dimension
final Term equalityWithLocArrays;
// final Term equalityWithLocArrays;
final Map<Term, Term> termSubstitutionMapping = new HashMap<>();
{
final Map<Term, Term> subs = new HashMap<>();
// final Map<Term, Term> subs = new HashMap<>();
for (final Term bat : baseArrayTerms) {
// obtain the loc array for the given base array term (typically a term-variable like a, or mem..)
final LocArrayInfo locArray =
mLocArrayManager.getOrConstructLocArray(mEdge, bat, currentDim);

// update the substitution mapping (e.g. with a pair (a, a-loc-dim))
subs.put(bat, locArray.getTerm());
termSubstitutionMapping.put(bat, locArray.getTerm());

/* update invars, outvars, etc. E.g. if a was an invar and we introduced a-loc-1, then a-loc-1
* must also be an invar. */
Expand All @@ -130,7 +130,7 @@ private void computeResult() {
mExtraConstants.add((IProgramConst) locArray.getPvoc());
}
}
equalityWithLocArrays = new Substitution(mMgdScript, subs).transform(mEquality);
// equalityWithLocArrays = new Substitution(mMgdScript, subs).transform(mEquality);
}

/* substitute store-values with their corresponding loc literals for the current dimension
Expand All @@ -139,14 +139,16 @@ private void computeResult() {
{
final List<StoreInfo> storeInfosForCurrentDimension = mRelPositionToInnerStoreInfo.values().stream()
.filter(si -> (si.getDimension() == currentDim)).collect(Collectors.toList());
final Map<SubtreePosition, Term> substitutionMapping = new HashMap<>();
final Map<SubtreePosition, Term> positionSubstitutionMapping = new HashMap<>();
for (final StoreInfo si : storeInfosForCurrentDimension) {
substitutionMapping.put(si.getPositionOfStoredValueRelativeToEquality(),
positionSubstitutionMapping.put(si.getPositionOfStoredValueRelativeToEquality(),
si.getLocLiteral().getTerm());

}
equalityWithLocArraysAndLocLiterals =
new PositionAwareSubstitution(mMgdScript, substitutionMapping).transform(equalityWithLocArrays);
// new PositionAwareSubstitution(mMgdScript, substitutionMapping).transform(equalityWithLocArrays);
new PositionAwareSubstitution(mMgdScript, positionSubstitutionMapping, termSubstitutionMapping)
.transform(mEquality);
}
conjuncts.add(equalityWithLocArraysAndLocLiterals);
}
Expand Down
157 changes: 85 additions & 72 deletions ...rmatik/ultimate/icfgtransformer/heapseparator/transformers/PositionAwareSubstitution.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,8 @@
import java.util.Arrays;
import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;

import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.SubtreePosition;
Expand All @@ -16,9 +14,9 @@
import de.uni_freiburg.informatik.ultimate.logic.Script;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
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.util.datastructures.DataStructureUtils;
import de.uni_freiburg.informatik.ultimate.util.datastructures.ScopedHashMap;

/**
Expand All @@ -30,38 +28,50 @@
*
*/
public class PositionAwareSubstitution extends PositionAwareTermTransformer {
private final Script mScript;
protected final ManagedScript mMgdScript;
private final ScopedHashMap<SubtreePosition, Term> mScopedSubstitutionMapping;
private final ScopedHashMap<SubtreePosition, Term> mScopedPositionSubstitutionMapping;
private final ScopedHashMap<Term, Term> mScopedTermSubstitutionMapping;

public PositionAwareSubstitution(final Script script,
final Map<? extends SubtreePosition, ? extends Term> substitutionMapping) {
final Map<? extends SubtreePosition, ? extends Term> positionSubstitution,
final Map<Term, Term> termSubstitution) {
super();
mMgdScript = null;
mScript = script;
mScopedSubstitutionMapping = new ScopedHashMap<>();
mScopedSubstitutionMapping.putAll(substitutionMapping);
mScopedPositionSubstitutionMapping = new ScopedHashMap<>();
mScopedPositionSubstitutionMapping.putAll(positionSubstitution);
mScopedTermSubstitutionMapping = new ScopedHashMap<>();
mScopedTermSubstitutionMapping.putAll(termSubstitution);
}

public PositionAwareSubstitution(final ManagedScript mgdScript,
final Map<? extends SubtreePosition, ? extends Term> substitutionMapping) {
super();
mMgdScript = mgdScript;
mScript = mgdScript.getScript();
mScopedSubstitutionMapping = new ScopedHashMap<>();
mScopedSubstitutionMapping.putAll(substitutionMapping);
final Map<? extends SubtreePosition, ? extends Term> positionSubstitution,
final Map<Term, Term> termSubstitution) {
this(mgdScript.getScript(), positionSubstitution, termSubstitution);
}

public PositionAwareSubstitution(final Script script,
final Map<? extends SubtreePosition, ? extends Term> positionBasedSubstitution) {
this(script, positionBasedSubstitution, Collections.emptyMap());
}


public PositionAwareSubstitution(final ManagedScript mgdScript,
final Map<? extends SubtreePosition, ? extends Term> positionBasedSubstitution) {
this(mgdScript, positionBasedSubstitution, Collections.emptyMap());
}

@Override
protected void convert(Term term, final SubtreePosition pos) {
if (mScopedSubstitutionMapping.containsKey(term)) {
setResult(mScopedSubstitutionMapping.get(term));
protected void convert(final Term term, final SubtreePosition pos) {
if (mScopedPositionSubstitutionMapping.containsKey(pos)) {
setResult(mScopedPositionSubstitutionMapping.get(pos));
} else if (mScopedTermSubstitutionMapping.containsKey(term)) {
setResult(mScopedTermSubstitutionMapping.get(term));
} else {
if (term instanceof QuantifiedFormula) {
mScopedSubstitutionMapping.beginScope();
final QuantifiedFormula qFormula = (QuantifiedFormula) term;
removeQuantifiedVarContainingKeys(qFormula);
term = renameQuantifiedVarsThatOccurInValues(qFormula);
mScopedPositionSubstitutionMapping.beginScope();
mScopedTermSubstitutionMapping.beginScope();
throw new UnsupportedOperationException("quantified formulas are not yet supported by this class");
// final QuantifiedFormula qFormula = (QuantifiedFormula) term;
// removeQuantifiedVarContainingKeys(qFormula);
// term = renameQuantifiedVarsThatOccurInValues(qFormula);
} else if (term instanceof LetTerm) {
throw new UnsupportedOperationException("LetTerm not supported");
}
Expand All @@ -77,18 +87,20 @@ protected void convert(Term term, final SubtreePosition pos) {
* @return
*/
private Term renameQuantifiedVarsThatOccurInValues(final QuantifiedFormula qFormula) {
final Set<TermVariable> toRename = varsOccuringInValues(qFormula.getVariables(), mScopedSubstitutionMapping);
if (toRename.isEmpty()) {
return qFormula;
}
if (mMgdScript == null) {
throw new UnsupportedOperationException("Substitution in quantified formula such that substitute "
+ "containes quantified variable. This (rare) case is "
+ "only supported if you call substitution with fresh " + "variable construction.");
}
final Term result = SmtUtils.renameQuantifiedVariables(mMgdScript, qFormula, toRename, "subst");
return result;

final Set<TermVariable> toRename = DataStructureUtils.union(
varsOccuringInValues(qFormula.getVariables(), mScopedPositionSubstitutionMapping),
varsOccuringInValues(qFormula.getVariables(), mScopedTermSubstitutionMapping));
throw new UnsupportedOperationException("quantified formulas are not yet supported by this class");
// if (toRename.isEmpty()) {
// return qFormula;
// }
// if (mMgdScript == null) {
// throw new UnsupportedOperationException("Substitution in quantified formula such that substitute "
// + "containes quantified variable. This (rare) case is "
// + "only supported if you call substitution with fresh " + "variable construction.");
// }
// final Term result = SmtUtils.renameQuantifiedVariables(mMgdScript, qFormula, toRename, "subst");
// return result;
}

/**
Expand All @@ -97,17 +109,17 @@ private Term renameQuantifiedVarsThatOccurInValues(final QuantifiedFormula qForm
*
*/
private void removeQuantifiedVarContainingKeys(final QuantifiedFormula qFormula) {
throw new UnsupportedOperationException("quantified formulas are not yet supported by this class");

final Iterator<Entry<SubtreePosition, Term>> it = mScopedSubstitutionMapping.entrySet().iterator();
while (it.hasNext()) {
final Entry<SubtreePosition, Term> entry = it.next();
final List<TermVariable> quantifiedVars = Arrays.asList(qFormula.getVariables());
throw new UnsupportedOperationException("quantified formulas are not yet supported by this class");
// final Iterator<Entry<SubtreePosition, Term>> it = mScopedPositionSubstitutionMapping.entrySet().iterator();
// while (it.hasNext()) {
// final Entry<SubtreePosition, Term> entry = it.next();
// final List<TermVariable> quantifiedVars = Arrays.asList(qFormula.getVariables());
// final List<TermVariable> occuringVars = Arrays.asList(entry.getKey().getFreeVars());
// if (!Collections.disjoint(quantifiedVars, occuringVars)) {
// it.remove();
// }
}
// }
}

/**
Expand Down Expand Up @@ -141,40 +153,41 @@ private static Set<TermVariable> addToSet(final TermVariable tv, Set<TermVariabl

@Override
public void postConvertQuantifier(final QuantifiedFormula old, final Term newBody) {
Term result;
// to avoid capturing of variables we had to rename quantified vars
// to fresh vars in subterms. Now we have to construct the appropriate
// supterterm.
// How can we detect if a variable was renamed?
// If a variable (of the old superterm) was renamed, it is a key in the
// current substitution mapping.
TermVariable[] newQuantifiedVars = new TermVariable[old.getVariables().length];
boolean quantifiedVariablesChanged = false;
for (int i = 0; i < old.getVariables().length; i++) {
if (mScopedSubstitutionMapping.containsKey(old.getVariables()[i])) {
newQuantifiedVars[i] = old.getVariables()[i];
quantifiedVariablesChanged = true;
} else {
newQuantifiedVars[i] = old.getVariables()[i];
}
}
if (old.getSubformula() == newBody) {
assert !quantifiedVariablesChanged;
result = old;
} else {
if (!quantifiedVariablesChanged) {
// reuse old array
newQuantifiedVars = old.getVariables();
}
result = mScript.quantifier(old.getQuantifier(), newQuantifiedVars, newBody);
}
mScopedSubstitutionMapping.endScope();
setResult(result);
throw new UnsupportedOperationException("quantified formulas are not yet supported by this class");
// Term result;
// // to avoid capturing of variables we had to rename quantified vars
// // to fresh vars in subterms. Now we have to construct the appropriate
// // supterterm.
// // How can we detect if a variable was renamed?
// // If a variable (of the old superterm) was renamed, it is a key in the
// // current substitution mapping.
// TermVariable[] newQuantifiedVars = new TermVariable[old.getVariables().length];
// boolean quantifiedVariablesChanged = false;
// for (int i = 0; i < old.getVariables().length; i++) {
// if (mScopedPositionSubstitutionMapping.containsKey(old.getVariables()[i])) {
// newQuantifiedVars[i] = old.getVariables()[i];
// quantifiedVariablesChanged = true;
// } else {
// newQuantifiedVars[i] = old.getVariables()[i];
// }
// }
// if (old.getSubformula() == newBody) {
// assert !quantifiedVariablesChanged;
// result = old;
// } else {
// if (!quantifiedVariablesChanged) {
// // reuse old array
// newQuantifiedVars = old.getVariables();
// }
// result = mScript.quantifier(old.getQuantifier(), newQuantifiedVars, newBody);
// }
// mScopedPositionSubstitutionMapping.endScope();
// setResult(result);
}

@Override
public String toString() {
return "Substitution " + mScopedSubstitutionMapping.toString();
return "Substitution " + mScopedPositionSubstitutionMapping.toString();
}

/**
Expand Down
15 changes: 14 additions & 1 deletion ...tik/ultimate/icfgtransformer/heapseparator/transformers/PositionAwareTermTransformer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
import de.uni_freiburg.informatik.ultimate.logic.LetTerm;
import de.uni_freiburg.informatik.ultimate.logic.NonRecursive;
import de.uni_freiburg.informatik.ultimate.logic.QuantifiedFormula;
import de.uni_freiburg.informatik.ultimate.logic.Sort;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.logic.TermTransformer;
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
Expand Down Expand Up @@ -146,7 +147,19 @@ public void convertApplicationTerm(
if (newArgs != appTerm.getParameters()) {
final FunctionSymbol fun = appTerm.getFunction();
final Theory theory = fun.getTheory();
newTerm = theory.term(fun, newArgs);

/*
* Difference to {@link Substitution}:
* PositionAwareSubstition may replace Terms with Terms of different type.
* Thus the type of an instance of a polymorphic function symbol has to be recomputed.
*/
final Sort[] paramTypes = new Sort[newArgs.length];
for (int i = 0; i < newArgs.length; i++) {
paramTypes[i] = newArgs[i].getSort();
}
final FunctionSymbol newFun = theory.getFunction(fun.getName(), paramTypes);

newTerm = theory.term(newFun, newArgs);
}
setResult(newTerm);
}
Expand Down

0 comments on commit dfbc2ac

Please sign in to comment.