Skip to content

Commit

Permalink
reworking of interpolants computation (ssa, postorder stuff, HcVars e…
Browse files Browse the repository at this point in the history 
…tc) roughly there now, see #143
  • Loading branch information
@alexandernutz
alexandernutz committed Apr 4, 2017
1 parent bf05bb4 commit 5bf3274
Show file tree
Hide file tree
Showing 5 changed files with 92 additions and 64 deletions.
20 changes: 17 additions & 3 deletions ...ource/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeRun.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,10 @@
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Set;


/**
* A run of a tree automaton.
*
Expand Down Expand Up @@ -91,11 +93,15 @@ public TreeRun(final STATE state, final LETTER letter, final List<TreeRun<LETTER
childStates.add(child.getRoot());
allRules.addAll(child.getRules());
}
allRules.add(new TreeAutomatonRule<LETTER, STATE>(mLetter, childStates, state));
if (mLetter != null) {
allRules.add(new TreeAutomatonRule<LETTER, STATE>(mLetter, childStates, state));
}
allStates.add(mState);

mAllStates = Collections.unmodifiableSet(allStates);
mAllRules = Collections.unmodifiableSet(allRules);

assert !mAllStates.stream().anyMatch(Objects::isNull);
}

/***
Expand Down Expand Up @@ -126,8 +132,11 @@ public <ST> TreeRun<LETTER, ST> reconstructViaSubtrees(final Map<TreeRun<LETTER,
for (final TreeRun<LETTER, STATE> c : mChildren) {
children.add(c.reconstructViaSubtrees(stMap));
}

return new TreeRun<>(stMap.get(this), mLetter, children);
if (stMap.get(this) == null) {
return (TreeRun<LETTER, ST>) this;
} else {
return new TreeRun<>(stMap.get(this), mLetter, children);
}
}


Expand Down Expand Up @@ -212,6 +221,11 @@ public LETTER getRootSymbol() {
return mLetter;
}

public List<TreeRun<LETTER, STATE>> getSubtreesInPostOrder() {
// TODO Auto-generated method stub
return null;
}

@Override
public String toString() {
if (mChildren.isEmpty()) {
Expand Down
7 changes: 4 additions & 3 deletions .../uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ public class HCSSABuilder {

private final Map<TreeRun<HornClause, IPredicate>, Integer> mIdxMap = new HashMap<>();
private int mCurrentIdx;
private final Map<TreeRun<HornClause, IPredicate>, Term> mSubtreeToVersioneeredTerm;
// private final Map<TreeRun<HornClause, IPredicate>, Term> mSubtreeToVersioneeredTerm;


/**
Expand All @@ -125,11 +125,11 @@ public HCSSABuilder(final TreeRun<HornClause, IPredicate> trace, final IPredicat
mSubsMap = new HashMap<>();
mPredicateUnifier = predicateUnifier;

// mSubtreeToVersioneeredTerm = new HashMap<>();
// mPredPosToArgPosToCurrentVarVersion = new NestedMap2<>();
mCurrentHcInVarVersion = new HashMap<>();
mResult = buildSSA();

mSubtreeToVersioneeredTerm = new HashMap<>();
}

public HCSsa getSSA() {
Expand Down Expand Up @@ -162,6 +162,7 @@ public TreeRun<HornClause, IPredicate> buildTreeRunWithBackVersionedInterpolants
VariableVersioneer versioneer = mSubsMap.get(en.getKey());
assert versioneer != null;
backVersionedInterpolantsMap.put(en.getKey(), versioneer.backVersion(en.getValue()));
assert backVersionedInterpolantsMap.get(en.getKey()) != null;
}

return mTreeRun.reconstructViaSubtrees(backVersionedInterpolantsMap);
Expand Down Expand Up @@ -213,7 +214,7 @@ private TreeRun<Term, IPredicate> buildNestedFormulaTree(final TreeRun<HornClaus
mCurrentTree = treeIdx;
vvRoot.versionOldVars(childPos);
mSubsMap.put(tree, vvRoot);
mSubtreeToVersioneeredTerm.put(tree, vvRoot.getVersioneeredTerm());
// mSubtreeToVersioneeredTerm.put(tree, vvRoot.getVersioneeredTerm());

/*
* recursively descend into the tree run
Expand Down
59 changes: 27 additions & 32 deletions .../src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@
import de.uni_freiburg.informatik.ultimate.logic.Term;
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.util.datastructures.relation.Pair;

/**
* HCSsa HornClause-SSA
Expand All @@ -54,6 +55,7 @@ public class HCSsa {

private boolean mCountersAreFinalized;
private Term[] mFlattenedTerms;
private int[] mStartsOfSubtrees;

/**
* Constructor for HC-SSA
Expand All @@ -71,32 +73,25 @@ public HCSsa(final TreeRun<Term, IPredicate> nestedFormulas, final Term pre, fin
mNestedFormulas = nestedFormulas;
mPostCondition = post;
mPreCondition = pre;
// mCounters = counters;

mCounters = new HashMap<>();
mCountersAreFinalized = false;
mTermToAssertion = new HashMap<>();

final List<Term> flattenedTermslist = flatten(mNestedFormulas, this);

final Pair<List<Term>, List<Integer>> flattenRes = flatten(mNestedFormulas, 0);
final List<Term> flattenedTermslist = flattenRes.getFirst();
final List<Integer> startsOfSubtrees = flattenRes.getSecond();
mFlattenedTerms = flattenedTermslist.toArray(new Term[flattenedTermslist.size()]);
mStartsOfSubtrees = new int[startsOfSubtrees.size()];
for (int i = 0; i < startsOfSubtrees.size(); i++) {
mStartsOfSubtrees[i] = startsOfSubtrees.get(i);
}
mCountersAreFinalized = true;
}

// /**
// * Constructor for HC-SSA that overrides the treeRun
// * @param ssa Old SSA
// * @param nestedFormulas The new tree run.
// */
// public HCSsa(final HCSsa ssa, final TreeRun<Term, IPredicate> nestedFormulas) {
// mNestedFormulas = nestedFormulas;
// mPostCondition = ssa.mPostCondition;
// mPreCondition = ssa.mPreCondition;
// mCounters = ssa.mCounters;
// mTermToAssertion = ssa.mTermToAssertion;
// }

int getCounter(final Term t) {
if (!mCounters.containsKey(t)) {
assert mCountersAreFinalized == false;
assert !mCountersAreFinalized;
int r = mCounters.size() + 1;
mCounters.put(t, r);
}
Expand Down Expand Up @@ -128,37 +123,37 @@ public Term[] getFlattenedTermList() {
return mFlattenedTerms;
}

private static List<Term> flatten(final TreeRun<Term, IPredicate> tree, HCSsa callingSsa) {
private Pair<List<Term>, List<Integer>> flatten(final TreeRun<Term, IPredicate> tree, int depth) {
ArrayList<Term> res = new ArrayList<>();
for (final TreeRun<Term, IPredicate> child : tree.getChildren()) {
res.addAll(flatten(child, callingSsa));
ArrayList<Integer> resStartsOfSubtrees = new ArrayList<>();
// for (final TreeRun<Term, IPredicate> child : tree.getChildren()) {
for (int i = 0; i < tree.getChildren().size(); i++) {
TreeRun<Term, IPredicate> child = tree.getChildren().get(i);
Pair<List<Term>, List<Integer>> childRes = flatten(child, depth + i);
res.addAll(childRes.getFirst());
resStartsOfSubtrees.addAll(childRes.getSecond());
}
if (tree.getRootSymbol() != null) {
res.add(tree.getRootSymbol());
callingSsa.getCounter(tree.getRootSymbol());
resStartsOfSubtrees.add(depth);
this.getCounter(tree.getRootSymbol());
}
return res;
return new Pair<>(res, resStartsOfSubtrees);
}

public TreeRun<Term, IPredicate> getFormulasTree() {
return mNestedFormulas;
}

// protected Term getPredicateVariable(final Term term, final ManagedScript script, final Object lockOwner) {
// if (!mTermToAssertion.containsKey(term)) {
// final String name = getName(term);
// mTermToAssertion.put(term, script.term(lockOwner, name));
// }
//
// final Term result = mTermToAssertion.get(term);
// return result;
// }

public Term[] getNamedTermList(final ManagedScript script, final Object lockOwner) {
final Term[] result = new Term[mFlattenedTerms.length];
for (int i = 0; i < mFlattenedTerms.length; i++) {
result[i] = script.term(lockOwner, getName(mFlattenedTerms[i]));
}
return result;
}

public int[] getStartsOfSubTrees() {
return mStartsOfSubtrees;
}
}
18 changes: 16 additions & 2 deletions ...ni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCStateFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -223,8 +223,8 @@ public IPredicate intersection(IPredicate state1, IPredicate state2) {
// new HashSet<>(Arrays.asList(state2.getFormula().getFreeVars())))) : "the free variables of the two "
// + "predicates must be equal modulo ordering"; // we cannot demand this, the formula does not need to talk about all variables of that HCPredicatesymbol..

assert state1.getVars().equals(state2.getVars());
assert !(state2 instanceof HCPredicate) : "convention: first argument is an HCPredicate, second is not..";
// assert state1.getVars().equals(state2.getVars());
// assert !(state2 instanceof HCPredicate) || isTrueHcPredicate(state2) : "convention: first argument is an HCPredicate, second is not..";

final Set<HornClausePredicateSymbol> state1PredSymbols = ((HCPredicate) state1).getHcPredicateSymbols();

Expand All @@ -237,6 +237,20 @@ public IPredicate intersection(IPredicate state1, IPredicate state2) {
return result;
}

private boolean isTrueHcPredicate(IPredicate state2) {
if (!(state2 instanceof HCPredicate)) {
return false;
}
final HCPredicate hcPred = (HCPredicate) state2;
if (hcPred.getHcPredicateSymbols().size() != 1) {
return false;
}
if (!"True".equals(hcPred.getHcPredicateSymbols().iterator().next().toString())) {
return false;
}
return true;
}

@Override
public IPredicate merge(Collection<IPredicate> states) {
/*
Expand Down
52 changes: 28 additions & 24 deletions ...reiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,6 @@
import de.uni_freiburg.informatik.ultimate.automata.AutomataLibraryServices;
import de.uni_freiburg.informatik.ultimate.automata.AutomataOperationCanceledException;
import de.uni_freiburg.informatik.ultimate.automata.tree.ITreeAutomatonBU;
import de.uni_freiburg.informatik.ultimate.automata.tree.PostfixTree;
import de.uni_freiburg.informatik.ultimate.automata.tree.TreeAutomatonBU;
import de.uni_freiburg.informatik.ultimate.automata.tree.TreeAutomatonRule;
import de.uni_freiburg.informatik.ultimate.automata.tree.TreeRun;
Expand Down Expand Up @@ -375,37 +374,42 @@ protected boolean refineAbstraction() throws AutomataLibraryException {

private Map<TreeRun<HornClause, IPredicate>, Term> retrieveInterpolantsMap(HCSsa ssa,
TreeRun<HornClause, IPredicate> counterExample) {
// Using simple interpolant automaton : the counterexample's automaton.
// final PostfixTree<Term, IPredicate> postfixT = new PostfixTree<>(ssa.getFormulasTree());
final PostfixTree<HornClause, IPredicate> postfixT =
new PostfixTree<>(counterExample);

// ssa.getFlattenedTermList();
//
// Term[] ts = new Term[postfixT.getPostFix().size()];
// for (int i = 0; i < ts.length; ++i) {
//// ts[i] = ssa.getPredicateVariable(postfixT.getPostFix().get(i), mBackendSmtSolverScript, this);
// ts[i] = ssa.getPredicateVariable(postfixT.getPostFixSubtree(i), mBackendSmtSolverScript, this);
//// 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);
}
// final Term[] interpolants = mBackendSmtSolverScript.getInterpolants(this, ts, idx);

final Term[] interpolants = mBackendSmtSolverScript.getInterpolants(this,
ssa.getNamedTermList(mBackendSmtSolverScript, this), idx);
ssa.getNamedTermList(mBackendSmtSolverScript, this),
ssa.getStartsOfSubTrees());

final List<TreeRun<HornClause, IPredicate>> subtreesInPostOrder = computeSubtreesInPostOrder(counterExample);

final Map<TreeRun<HornClause, IPredicate>, Term> interpolantsMap = new HashMap<>();

for (int i = 0; i < interpolants.length; ++i) {
// HCPredicate p = (HCPredicate) postfixT.getPostFixStates().get(i);
TreeRun<HornClause, IPredicate> p = postfixT.getPostFixSubtree(i);
interpolantsMap.put(p, interpolants[i]);
// interpolantsMap.addPair(p, interpolants[i]);
final TreeRun<HornClause, IPredicate> st = subtreesInPostOrder.get(i);

interpolantsMap.put(st, interpolants[i]);
}

// the root of a tree interpolant is implicitly "false"
interpolantsMap.put(counterExample, mBackendSmtSolverScript.term(this, "false"));

return interpolantsMap;
}

private static List<TreeRun<HornClause, IPredicate>> computeSubtreesInPostOrder(
final TreeRun<HornClause, IPredicate> root) {
final List<TreeRun<HornClause, IPredicate>> result = new ArrayList<>();

for (TreeRun<HornClause, IPredicate> ch : root.getChildren()) {
result.addAll(computeSubtreesInPostOrder(ch));
}

//need to make an exception for the leafs (related to the fact that our tree automata have initial states)
if (root.getRootSymbol() != null) {
result.add(root);
}
return result;
}

protected void computeCFGHoareAnnotation() {
return;
}
Expand Down

0 comments on commit 5bf3274

Please sign in to comment.