From 933d020d267672a674ce2ce1af5cbeaacf534260 Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Mon, 3 Apr 2017 16:33:19 +0200 Subject: [PATCH] intermediate backup commit, towards #143 --- .../ultimate/automata/tree/PostfixTree.java | 26 +++- .../treeautomizer/TreeAutomizerObserver.java | 5 +- .../graph/CandidateRuleProvider.java | 47 +++++++ .../treeautomizer/graph/HCSSABuilder.java | 46 ++++-- .../generator/treeautomizer/graph/HCSsa.java | 47 ++++--- .../graph/TreeAutomizerCEGAR.java | 133 ++++++++++-------- .../treeautomizer/graph/TreeChecker.java | 14 +- 7 files changed, 212 insertions(+), 106 deletions(-) create mode 100644 trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/CandidateRuleProvider.java diff --git a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/PostfixTree.java b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/PostfixTree.java index 618872e98b8..0ba33e45931 100644 --- a/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/PostfixTree.java +++ b/trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/PostfixTree.java @@ -40,11 +40,12 @@ */ public class PostfixTree { - private final ArrayList mPostFix; - private final ArrayList mPostFixStates; - private final ArrayList mDepths; + private final List mPostFix; + private final List mPostFixStates; + private final List mDepths; + private final List> mPostFixSubtrees; - private final ArrayList mStartIdx; + private final List mStartIdx; private final HashMap mBeg; @@ -55,6 +56,7 @@ public class PostfixTree { public PostfixTree(final TreeRun run) { mPostFix = new ArrayList<>(); mPostFixStates = new ArrayList<>(); + mPostFixSubtrees = new ArrayList<>(); mStartIdx = new ArrayList<>(); mDepths = new ArrayList<>(); mBeg = new HashMap<>(); @@ -72,8 +74,18 @@ public List getStartIdx() { public List getPostFixStates() { return mPostFixStates; } + + /** + * Retrieve the subtree in the input tree run that corresponds to the given position in the post-order + * + * @param postFixPos + * @return + */ + public TreeRun getPostFixSubtree(int postFixPos) { + return mPostFixSubtrees.get(postFixPos); + } - private void addSymbol(final LETTER lt, final STATE st, final int depth) { + private void addSymbol(final TreeRun subTree, final LETTER lt, final STATE st, final int depth) { if (!mBeg.containsKey(depth)) { mBeg.put(depth, mDepths.size()); } @@ -81,13 +93,14 @@ private void addSymbol(final LETTER lt, final STATE st, final int depth) { mPostFix.add(lt); mPostFixStates.add(st); mDepths.add(depth); + mPostFixSubtrees.add(subTree); } private void constructTree(final TreeRun run, final int depth) { constructSubtrees(run.getChildren().iterator(), depth); if (run.getRootSymbol() != null) { - addSymbol(run.getRootSymbol(), run.getRoot(), depth); + addSymbol(run, run.getRootSymbol(), run.getRoot(), depth); } } @@ -99,6 +112,7 @@ private void constructSubtrees(final Iterator> it, final constructSubtrees(it, depth + 1); } + // TODO: convert to a JUnit test public static void main(String[] args) { TreeRun r9 = new TreeRun(9); diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/TreeAutomizerObserver.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/TreeAutomizerObserver.java index 7c1de3a138f..129ea8f0bb8 100644 --- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/TreeAutomizerObserver.java +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/TreeAutomizerObserver.java @@ -91,8 +91,9 @@ public boolean process(final IElement root) throws Throwable { final HornAnnot annot = (HornAnnot) st.get(HornUtilConstants.HORN_ANNOT_NAME); mLogger.debug(annot.getAnnotationsAsMap().get(HornUtilConstants.HORN_ANNOT_NAME)); - TreeAutomizerCEGAR cegar = new TreeAutomizerCEGAR(mServices, mToolchainStorage, - rootNode, taPrefs, mLogger, annot.getScript(), annot.getSymbolTable()); + TreeAutomizerCEGAR cegar = new TreeAutomizerCEGAR(mServices, mToolchainStorage, annot, + taPrefs, mLogger); +// rootNode, taPrefs, mLogger, annot.getScript(), annot.getSymbolTable()); cegar.iterate(); diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/CandidateRuleProvider.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/CandidateRuleProvider.java new file mode 100644 index 00000000000..6e4e1efa982 --- /dev/null +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/CandidateRuleProvider.java @@ -0,0 +1,47 @@ +package de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer.graph; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map; + +import de.uni_freiburg.informatik.ultimate.automata.tree.ITreeRun; +import de.uni_freiburg.informatik.ultimate.automata.tree.TreeAutomatonRule; +import de.uni_freiburg.informatik.ultimate.modelcheckerutils.hornutil.HornClause; +import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.IPredicate; + +/** + * Provides rules that might be added to an interpolant automaton during the generalization phase. + * + * + * @author Alexander Nutz (nutz@informatik.uni-freiburg.de) + * + */ +public class CandidateRuleProvider { + + + + private Iterable> mCandidateRules; + + /** + * Triggers computation of candidate rules. + * Result can be obtained via getter method. + * + * @param originalTreeRun + * @param hcSymbolsToInterpolants + * @param alphabet + */ + public CandidateRuleProvider(ITreeRun originalTreeRun, + Map hcSymbolsToInterpolants, List alphabet) { + mCandidateRules = new ArrayList<>(); + + for (HornClause letter : alphabet) { + + + } + + } + + public Iterable> getCandidateRules() { + return mCandidateRules; + } +} 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 835bc00d387..83df99c3364 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 @@ -149,31 +149,47 @@ private int getOrConstructIndex(final TreeRun tree) { * @param interpolantsMap map of predicates to the corresponding interpolant. * @return A map of the new predicates. * */ - public Map rebuildSSApredicates(final Map interpolantsMap) { - final Map res = new HashMap<>(); + public Map, IPredicate> rebuildSSApredicates( + final Map, Term> interpolantsMap) { + final Map, IPredicate> res = new HashMap<>(); mCurrentTree = 0; rebuild((TreeRun) mTreeRun, res, interpolantsMap); return res; } - private void rebuild(final TreeRun tree, final Map res, - final Map interpolantsMap) { + /** + * + * @param tree + * @param res The relation that is to be filled. + * @param interpolantsMap + */ + private void rebuild(final TreeRun tree, + final Map, IPredicate> res, + final Map, Term> interpolantsMap) { for (final TreeRun child : tree.getChildren()) { mCurrentTree = getOrConstructIndex(tree); rebuild(child, res, interpolantsMap); } - if (tree.getRootSymbol() == null) { - res.put(tree.getRoot(), tree.getRoot()); - return; - } +// if (tree.getRootSymbol() == null) { +//// res.put(tree.getRoot(), tree.getRoot()); +// res.addPair((HCPredicate) tree.getRoot(), tree.getRoot()); +// return; +// } mCurrentTree = getOrConstructIndex(tree); final VariableVersioneer vvRoot = mSubsMap.get(tree); - if (interpolantsMap.containsKey(tree.getRoot())) { - res.put(tree.getRoot(), vvRoot.backVersion(tree.getRoot(), interpolantsMap.get(tree.getRoot()))); - } else { - res.put(tree.getRoot(), tree.getRoot()); - } + + res.put(tree, vvRoot.backVersion(interpolantsMap.get(tree))); + +// if (interpolantsMap.containsKey(tree.getRoot())) { +// if (interpolantsMap.getDomain().contains(tree.getRoot())) { +//// res.put(tree.getRoot(), vvRoot.backVersion(tree.getRoot(), interpolantsMap.get(tree.getRoot()))); +// res.addPair(tree.getRoot(), vvRoot.backVersion(tree.getRoot(), interpolantsMap.get(tree.getRoot()))); +// } else { +// res.put(tree.getRoot(), tree.getRoot()); +// } + +// return res; } private TreeRun buildNestedFormulaTree(final TreeRun tree, @@ -225,7 +241,7 @@ private HCSsa buildSSA() { final VariableVersioneer vvPost = new VariableVersioneer(mPostCondition); vvPost.versionPredicate(mCurrentTree); - return new HCSsa(tree, vvPre.getVersioneeredTerm(), vvPost.getVersioneeredTerm(), mCounters); + return new HCSsa(tree, vvPre.getVersioneeredTerm(), vvPost.getVersioneeredTerm()); } public Map getConstants2BoogieVar() { @@ -397,7 +413,7 @@ public Term getVersioneeredTerm() { * @param term * @return */ - public IPredicate backVersion(final IPredicate pl, final Term term) { + public IPredicate backVersion(final Term term) { final Set vars = new HashSet<>(); final Map backSubstitutionMap = new HashMap<>(); final Map termToHcVar = new HashMap<>(); diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java index 53911a668df..7857a5afc02 100644 --- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java @@ -52,6 +52,8 @@ public class HCSsa { private final Map mCounters; private final Map mTermToAssertion; + private boolean mCountersAreFinalized; + /** * Constructor for HC-SSA * @@ -64,30 +66,32 @@ public class HCSsa { * @param counters * A map of the counts of each Term. */ - public HCSsa(final TreeRun nestedFormulas, final Term pre, final Term post, - final Map counters) { + public HCSsa(final TreeRun nestedFormulas, final Term pre, final Term post) { mNestedFormulas = nestedFormulas; mPostCondition = post; mPreCondition = pre; - mCounters = counters; +// mCounters = counters; + mCounters = new HashMap<>(); + mCountersAreFinalized = false; mTermToAssertion = new HashMap<>(); } - /** - * 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 nestedFormulas) { - mNestedFormulas = nestedFormulas; - mPostCondition = ssa.mPostCondition; - mPreCondition = ssa.mPreCondition; - mCounters = ssa.mCounters; - mTermToAssertion = ssa.mTermToAssertion; - } +// /** +// * 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 nestedFormulas) { +// mNestedFormulas = nestedFormulas; +// mPostCondition = ssa.mPostCondition; +// mPreCondition = ssa.mPreCondition; +// mCounters = ssa.mCounters; +// mTermToAssertion = ssa.mTermToAssertion; +// } - protected int getCounter(final Term t) { + int getCounter(final Term t) { if (!mCounters.containsKey(t)) { + assert mCountersAreFinalized == false; int r = mCounters.size() + 1; mCounters.put(t, r); } @@ -110,20 +114,25 @@ public String getName(final Term t) { * Computes a flat version of the SSA. * This flat version is used by the TreeChecker to construct named formulas from it and assert each one in the * solver. + * + * The order of the flattened list corresponds to a post-order over the tree, this * * @return */ public List flatten() { - return flatten(mNestedFormulas); + final List result = flatten(mNestedFormulas, this); + mCountersAreFinalized = true; + return result; } - private static List flatten(final TreeRun tree) { + private static List flatten(final TreeRun tree, HCSsa callingSsa) { ArrayList res = new ArrayList<>(); for (final TreeRun child : tree.getChildren()) { - res.addAll(flatten(child)); + res.addAll(flatten(child, callingSsa)); } if (tree.getRootSymbol() != null) { res.add(tree.getRootSymbol()); + callingSsa.getCounter(tree.getRootSymbol()); } return res; } diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java index b3607f7fa1b..825ed7e3603 100644 --- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java @@ -29,7 +29,6 @@ import java.util.ArrayList; import java.util.Collections; -import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; @@ -40,7 +39,6 @@ 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.ITreeRun; -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; @@ -49,9 +47,7 @@ import de.uni_freiburg.informatik.ultimate.automata.tree.operations.Minimize; import de.uni_freiburg.informatik.ultimate.automata.tree.operations.Totalize; import de.uni_freiburg.informatik.ultimate.automata.tree.operations.TreeEmptinessCheck; -import de.uni_freiburg.informatik.ultimate.core.lib.models.BasePayloadContainer; import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; -import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.core.model.services.IToolchainStorage; import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; @@ -89,7 +85,8 @@ public class TreeAutomizerCEGAR { private int mIteration; private ILogger mLogger; - private final BasePayloadContainer mRootNode; +// private final BasePayloadContainer mRootNode; + private final HornAnnot mHornAnnot; private final HCPredicate mInitialPredicate; private final HCPredicate mFinalPredicate; @@ -108,6 +105,8 @@ public class TreeAutomizerCEGAR { private final HCPredicateFactory mPredicateFactory; private final AutomataLibraryServices mAutomataLibraryServices; + private List mAlphabet; + /** * Constructor for TreeAutomizer CEGAR * @@ -120,20 +119,29 @@ public class TreeAutomizerCEGAR { * @param hcSymbolTable */ public TreeAutomizerCEGAR(IUltimateServiceProvider services, IToolchainStorage storage, - BasePayloadContainer rootNode, TAPreferences taPrefs, ILogger logger, ManagedScript script, - HCSymbolTable hcSymbolTable) { - mBackendSmtSolverScript = script; - mSymbolTable = hcSymbolTable; +// BasePayloadContainer rootNode, + HornAnnot annot, + TAPreferences taPrefs, ILogger logger) { +// ManagedScript script, +// HCSymbolTable hcSymbolTable) { + mBackendSmtSolverScript = annot.getScript(); + mSymbolTable = annot.getSymbolTable(); mLogger = logger; - mRootNode = rootNode; +// mRootNode = rootNode; + mHornAnnot = annot; + + + mAlphabet = (List) mHornAnnot.getAnnotationsAsMap() + .get(HornUtilConstants.HORN_ANNOT_NAME); + mIteration = 0; mAutomataLibraryServices = new AutomataLibraryServices(services); - mPredicateFactory = new HCPredicateFactory(services, mBackendSmtSolverScript, hcSymbolTable, + mPredicateFactory = new HCPredicateFactory(services, mBackendSmtSolverScript, mSymbolTable, SimplificationTechnique.SIMPLIFY_DDA, XnfConversionTechnique.BDD_BASED); - mStateFactory = new HCStateFactory(script, mPredicateFactory, hcSymbolTable); + mStateFactory = new HCStateFactory(mBackendSmtSolverScript, mPredicateFactory, mSymbolTable); mInitialPredicate = mPredicateFactory.getTruePredicate(); mFinalPredicate = mPredicateFactory.getFalsePredicate(); @@ -153,13 +161,17 @@ public TreeAutomizerCEGAR(IUltimateServiceProvider services, IToolchainStorage s protected void getInitialAbstraction() throws AutomataLibraryException { - final Map st = mRootNode.getPayload().getAnnotations(); - final HornAnnot annot = (HornAnnot) st.get(HornUtilConstants.HORN_ANNOT_NAME); - final List hornClauses = (List) annot.getAnnotationsAsMap() - .get(HornUtilConstants.HORN_ANNOT_NAME); +// final Map st = mRootNode.getPayload().getAnnotations(); +// final HornAnnot annot = (HornAnnot) st.get(HornUtilConstants.HORN_ANNOT_NAME); +// final List hornClauses = (List) annot.getAnnotationsAsMap() +// .get(HornUtilConstants.HORN_ANNOT_NAME); +// final List hornClauses = (List) mHornAnnot.getAnnotationsAsMap() +// .get(HornUtilConstants.HORN_ANNOT_NAME); +// +// mAlphabet = hornClauses; mAbstraction = new TreeAutomatonBU<>(); - for (final HornClause clause : hornClauses) { + for (final HornClause clause : mAlphabet) { final List tail = new ArrayList<>(); for (HornClausePredicateSymbol sym : clause.getBodyPredicates()) { tail.add(mPredicateFactory.createTruePredicateWithLocation(sym)); @@ -206,7 +218,7 @@ public LBool getCounterexampleFeasibility(Object lockOwner) { return mChecker.checkTrace(lockOwner); } - protected void constructInterpolantAutomaton(Map interpolantsMap) + protected void constructInterpolantAutomaton(Map, Term> interpolantsMap) throws AutomataOperationCanceledException { mInterpolAutomaton = ((TreeRun) mCounterexample) @@ -217,7 +229,7 @@ protected void constructInterpolantAutomaton(Map interpolantsM ((TreeAutomatonBU) mInterpolAutomaton).extendAlphabet(mAbstraction.getAlphabet()); - generalizeCounterExample(); + generalizeCounterExample(mChecker.rebuild(interpolantsMap)); assert allRulesAreInductive(mInterpolAutomaton); } @@ -239,14 +251,24 @@ private boolean allRulesAreInductive(final ITreeAutomatonBU hcSymbolsToInterpolants) { final Set> rules = new HashSet<>(); - for (final TreeAutomatonRule r : mInterpolAutomaton.getRules()) { - for (final IPredicate pf : mInterpolAutomaton.getStates()) { - if (mHoareTripleChecker.check(r.getSource(), r.getLetter(), pf) == Validity.VALID) { - mLogger.debug("Adding Rule: " + r.getLetter() + "(" + r.getSource() + ")" + " --> " + pf); - rules.add(new TreeAutomatonRule(r.getLetter(), r.getSource(), pf)); - } + // for (final TreeAutomatonRule r : + // mInterpolAutomaton.getRules()) { + // for (final IPredicate pf : mInterpolAutomaton.getStates()) { + for (TreeAutomatonRule rule : + new CandidateRuleProvider(mCounterexample, hcSymbolsToInterpolants, mAlphabet).getCandidateRules()) { + // if (mHoareTripleChecker.check(rule.getSource(), rule.getLetter(), + // pf) == Validity.VALID) { + // mLogger.debug("Adding Rule: " + rule.getLetter() + "(" + + // rule.getSource() + ")" + " --> " + pf); + // rules.add(new TreeAutomatonRule(rule.getLetter(), rule.getSource(), pf)); + // } + if (mHoareTripleChecker.check(rule) == Validity.VALID) { + mLogger.debug( + "Adding Rule: " + rule.getLetter() + "(" + rule.getSource() + ")" + " --> " + rule.getDest()); + rules.add(rule); } } mLogger.debug("Generalizing counterExample:"); @@ -255,15 +277,7 @@ private void generalizeCounterExample() { } } - // private TreeAutomatonBU getCounterExample() { private ITreeAutomatonBU getCounterExample() { - // //generalizeCounterExample(); - // final Map mp = new HashMap<>(); - // for (final IPredicate p : mInterpolAutomaton.getStates()) { - // mp.put(p, mPredicateFactory.convertItoHCPredicate(p)); - // } - // return ((TreeAutomatonBU) - // mInterpolAutomaton).reconstruct(mp); return mInterpolAutomaton; } @@ -325,7 +339,7 @@ public Result iterate() throws AutomataLibraryException { } mLogger.debug("Getting Interpolants..."); - final Map interpolantsMap = retrieveInterpolantsMap(); + final Map, Term> interpolantsMap = retrieveInterpolantsMap(); mBackendSmtSolverScript.pop(this, 1); mBackendSmtSolverScript.unlock(this); @@ -342,29 +356,32 @@ public Result iterate() throws AutomataLibraryException { return Result.UNKNOWN; } - private Map retrieveInterpolantsMap() { - // Using simple interpolant automaton : the counterexample's automaton. - PostfixTree 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 interpolantsMap = new HashMap<>(); - for (int i = 0; i < interpolants.length; ++i) { - IPredicate p = postfixT.getPostFixStates().get(i); - interpolantsMap.put(p, interpolants[i]); - } - return interpolantsMap; - } +// private HashRelation retrieveInterpolantsMap() { +// // Using simple interpolant automaton : the counterexample's automaton. +//// final PostfixTree postfixT = new PostfixTree<>(mSSA.getFormulasTree()); +// final PostfixTree postfixT = +// new PostfixTree<>((TreeRun) mCounterexample); +// +// 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); +// 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 HashRelation interpolantsMap = new HashRelation<>(); +// for (int i = 0; i < interpolants.length; ++i) { +//// HCPredicate p = (HCPredicate) postfixT.getPostFixStates().get(i); +// TreeRun p = postfixT.getPostFixSubtree(i); +//// interpolantsMap.put(p, interpolants[i]); +// interpolantsMap.addPair(p, interpolants[i]); +// } +// return interpolantsMap; +// } protected void computeCFGHoareAnnotation() { return; diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeChecker.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeChecker.java index f5577f83a57..06bbcb23b61 100644 --- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeChecker.java +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeChecker.java @@ -32,6 +32,7 @@ import java.util.Map; import de.uni_freiburg.informatik.ultimate.automata.tree.ITreeRun; +import de.uni_freiburg.informatik.ultimate.automata.tree.TreeRun; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.logic.Annotation; import de.uni_freiburg.informatik.ultimate.logic.Script.LBool; @@ -91,7 +92,8 @@ public TreeChecker(final ITreeRun tree, final ManagedScr * the map of predicates to the corresponding interpolants. * @return */ - public Map rebuild(final Map interpolantsMap) { + public Map, IPredicate> rebuild( + final Map, Term> interpolantsMap) { return mSSABuilder.rebuildSSApredicates(interpolantsMap); } @@ -100,21 +102,21 @@ protected HCSsa getSSA() { } protected LBool checkTrace(Object lockOwner) { -// mBackendSmtSolverScript.lock(this); + final HCSsa ssa = getSSA(); final List nestedExp = ssa.flatten(); - HashSet visited = new HashSet<>(); + HashSet visited = new HashSet<>(); for (final Term t : nestedExp) { final Annotation ann = new Annotation(":named", ssa.getName(t)); - if (!visited.contains(ssa.getCounter(t))) { + if (!visited.contains(ssa.getName(t))) { mLogger.debug("assert: " + ssa.getName(t) + " :: " + t.toString()); - visited.add(ssa.getCounter(t)); + visited.add(ssa.getName(t)); final Term annT = mBackendSmtSolverScript.annotate(lockOwner, t, ann); mBackendSmtSolverScript.assertTerm(lockOwner, annT); } } final LBool result = mBackendSmtSolverScript.checkSat(lockOwner); -// mBackendSmtSolverScript.unlock(this); + return result; } } \ No newline at end of file