intermediate commit, working towards #143

ultimate-pa · Mar 27, 2017 · b1b3978 · b1b3978
1 parent 90cdbec
commit b1b3978
Show file tree

Hide file tree

Showing 7 changed files with 200 additions and 92 deletions.
diff --git a/...brary-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeAutomatonBU.java b/...brary-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeAutomatonBU.java
@@ -228,6 +228,10 @@ public Set<STATE> getInitialStates() {
 		return mInitalStates;
 	}
 
+	public Set<STATE> getFinalStates() {
+		return mFinalStates;
+	}
+
 	@Override
 	public Set<STATE> getStates() {
 		return mStates;

diff --git a/...ource/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeRun.java b/...ource/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/tree/TreeRun.java
@@ -87,7 +87,7 @@ public <ST> TreeRun<R, ST> reconstruct(final Map<S, ST> stMap) {
 		return new TreeRun<>(stMap.containsKey(state) ? stMap.get(state) : null, letter, child);
 	}
 
-	public Collection<TreeRun<R, S>> getChildren() {
+	public List<TreeRun<R, S>> getChildren() {
 		return children;
 	}
 

diff --git a/...ckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCInVar.java b/...ckerUtils/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/...kerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HCOutVar.java b/...kerUtils/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/...rUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/hornutil/HornClause.java b/...rUtils/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/...reiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCPredicateFactory.java b/...reiburg/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<TermVariable> 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<TermVariable> 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<IProgramVar> vars, final Map<Term, HCVar> termToHcVar) {
-//		return new HCPredicate(mProgramPoint, hashCode, formula, vars, termToHcVar, computeClosedFormula(formula));
-//	}
-
 
-	/**
-	 * 
-	 * @param vars
-	 * @return
-	 */
-	private Set<IProgramVar> computeHcOutVarsFromTermVariables(List<TermVariable> 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<IProgramVar> vars, final Map<Term, HCVar>
+	// termToHcVar) {
+	// return new HCPredicate(mProgramPoint, hashCode, formula, vars,
+	// termToHcVar, computeClosedFormula(formula));
+	// }
+
+	// /**
+	// *
+	// * @param vars
+	// * @return
+	// */
+	// private Set<IProgramVar>
+	// computeHcOutVarsFromTermVariables(List<TermVariable> vars) {
+	// final Set<IProgramVar> 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<Term, Term> 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<IProgramVar> mProgramVars;
+
+		public ComputeHcOutVarsAndNormalizeTerm(Term formula, List<TermVariable> variables) {
+			final Map<Term, Term> normalizingSubstitution = new HashMap<>();
+			final Set<IProgramVar> 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<IProgramVar> getProgramVars() {
+			return mProgramVars;
+		}
+	}
 }