intermediate backup commit, towards #143

ultimate-pa · Apr 4, 2017 · 933d020 · 933d020
1 parent 9700056
commit 933d020
Show file tree

Hide file tree

Showing 7 changed files with 212 additions and 106 deletions.
diff --git a/...e/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/PostfixTree.java b/...e/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/PostfixTree.java
@@ -40,11 +40,12 @@
  */
 public class PostfixTree<LETTER, STATE> {
 
-	private final ArrayList<LETTER> mPostFix;
-	private final ArrayList<STATE> mPostFixStates;
-	private final ArrayList<Integer> mDepths;
+	private final List<LETTER> mPostFix;
+	private final List<STATE> mPostFixStates;
+	private final List<Integer> mDepths;
+	private final List<TreeRun<LETTER, STATE>> mPostFixSubtrees;
 
-	private final ArrayList<Integer> mStartIdx;
+	private final List<Integer> mStartIdx;
 
 	private final HashMap<Integer, Integer> mBeg;
 
@@ -55,6 +56,7 @@ public class PostfixTree<LETTER, STATE> {
 	public PostfixTree(final TreeRun<LETTER, STATE> run) {
 		mPostFix = new ArrayList<>();
 		mPostFixStates = new ArrayList<>();
+		mPostFixSubtrees = new ArrayList<>();
 		mStartIdx = new ArrayList<>();
 		mDepths = new ArrayList<>();
 		mBeg = new HashMap<>();
@@ -72,22 +74,33 @@ public List<Integer> getStartIdx() {
 	public List<STATE> 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<LETTER, STATE> getPostFixSubtree(int postFixPos) {
+		return mPostFixSubtrees.get(postFixPos);
+	}
 
-	private void addSymbol(final LETTER lt, final STATE st, final int depth) {
+	private void addSymbol(final TreeRun<LETTER, STATE> subTree, final LETTER lt, final STATE st, final int depth) {
 		if (!mBeg.containsKey(depth)) {
 			mBeg.put(depth, mDepths.size());
 		}
 		mStartIdx.add(mBeg.get(depth));
 		mPostFix.add(lt);
 		mPostFixStates.add(st);
 		mDepths.add(depth);
+		mPostFixSubtrees.add(subTree);
 	}
 
 	private void constructTree(final TreeRun<LETTER, STATE> 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<TreeRun<LETTER, STATE>> it, final
 		constructSubtrees(it, depth + 1);
 	}
 
+	// TODO: convert to a JUnit test
 	public static void main(String[] args) {
 
 		TreeRun<Character, Integer> r9 = new TreeRun<Character, Integer>(9);

diff --git a/...i_freiburg/informatik/ultimate/plugins/generator/treeautomizer/TreeAutomizerObserver.java b/...i_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/...burg/informatik/ultimate/plugins/generator/treeautomizer/graph/CandidateRuleProvider.java b/...burg/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<TreeAutomatonRule<HornClause, IPredicate>> mCandidateRules;
+
+	/**
+	 * Triggers computation of candidate rules.
+	 * Result can be obtained via getter method.
+	 * 
+	 * @param originalTreeRun
+	 * @param hcSymbolsToInterpolants 
+	 * @param alphabet 
+	 */
+	public CandidateRuleProvider(ITreeRun<HornClause, IPredicate> originalTreeRun, 
+			Map<IPredicate, IPredicate> hcSymbolsToInterpolants, List<HornClause> alphabet) {
+		mCandidateRules = new ArrayList<>();
+
+		for (HornClause letter : alphabet) {
+
+
+		}
+
+	}
+
+	public Iterable<TreeAutomatonRule<HornClause, IPredicate>> getCandidateRules() {
+		return mCandidateRules;
+	}
+}
diff --git a/.../uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java b/.../uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java
@@ -149,31 +149,47 @@ private int getOrConstructIndex(final TreeRun<HornClause, IPredicate> tree) {
 	 * @param interpolantsMap map of predicates to the corresponding interpolant.
 	 * @return A map of the new predicates.
 	 * */
-	public Map<IPredicate, IPredicate> rebuildSSApredicates(final Map<IPredicate, Term> interpolantsMap) {
-		final Map<IPredicate, IPredicate> res = new HashMap<>();
+	public Map<TreeRun<HornClause, IPredicate>, IPredicate> rebuildSSApredicates(
+			final Map<TreeRun<HornClause, IPredicate>, Term> interpolantsMap) {
+		final Map<TreeRun<HornClause, IPredicate>, IPredicate> res = new HashMap<>();
 		mCurrentTree = 0;
 		rebuild((TreeRun<HornClause, IPredicate>) mTreeRun, res, interpolantsMap);
 		return res;
 	}
 
-	private void rebuild(final TreeRun<HornClause, IPredicate> tree, final Map<IPredicate, IPredicate> res,
-			final Map<IPredicate, Term> interpolantsMap) {
+	/**
+	 * 
+	 * @param tree
+	 * @param res The relation that is to be filled.
+	 * @param interpolantsMap
+	 */
+	private void rebuild(final TreeRun<HornClause, IPredicate> tree, 
+			final Map<TreeRun<HornClause, IPredicate>, IPredicate> res,
+			final Map<TreeRun<HornClause, IPredicate>, Term> interpolantsMap) {
 		for (final TreeRun<HornClause, IPredicate> 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<Term, IPredicate> buildNestedFormulaTree(final TreeRun<HornClause, IPredicate> 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<Term, HCOutVar> 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<IProgramVar> vars = new HashSet<>();
 			final Map<Term, Term> backSubstitutionMap = new HashMap<>();
 			final Map<Term, HCOutVar> termToHcVar = new HashMap<>();

diff --git a/.../src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java b/.../src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSsa.java
@@ -52,6 +52,8 @@ public class HCSsa {
 	private final Map<Term, Integer> mCounters;
 	private final Map<Term, Term> 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<Term, IPredicate> nestedFormulas, final Term pre, final Term post,
-			final Map<Term, Integer> counters) {
+	public HCSsa(final TreeRun<Term, IPredicate> 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<Term, IPredicate> 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<Term, IPredicate> 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<Term> flatten() {
-		return flatten(mNestedFormulas);
+		final List<Term> result = flatten(mNestedFormulas, this);
+		mCountersAreFinalized = true;
+		return result;
 	}
 
-	private static List<Term> flatten(final TreeRun<Term, IPredicate> tree) {
+	private static List<Term> flatten(final TreeRun<Term, IPredicate> tree, HCSsa callingSsa) {
 		ArrayList<Term> res = new ArrayList<>();
 		for (final TreeRun<Term, IPredicate> 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;
 	}