Skip to content

Commit

Permalink
some fixes concerning recent changes
Browse files Browse the repository at this point in the history 
cleanup
#143
  • Loading branch information
@alexandernutz
alexandernutz committed Aug 7, 2017
1 parent cd0ae26 commit f19a7d2
Show file tree
Hide file tree
Showing 4 changed files with 44 additions and 161 deletions.
4 changes: 4 additions & 0 deletions ...reeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,4 +204,8 @@ public Term getConstForTermVar(TermVariable fv) {
return res;
}

public boolean hasConstForTermVar(TermVariable fv) {
return mTermVarToConst.containsKey(fv);
}

}
115 changes: 6 additions & 109 deletions ...y-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HornClause.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,32 +27,18 @@
*/
public class HornClause implements IRankedLetter {

// /**
// * Stores for each predicate symbol in the body and, every argument
// position of the represented atom, which
// * TermVariable in the transition formula represents that argument in the
// represented atom.
// */
// private final Map<HornClausePredicateSymbol, List<TermVariable>>
// mBodyPredToTermVariables;

private final List<HornClausePredicateSymbol> mBodyPreds;

private final List<List<TermVariable>> mBodyPredToTermVariables;
// private final List<List<HCInVar>> mBodyPredToHCInVars;
// private List<List<IProgramVar>> mBodyPredToIProgramVar;

/**
* Stores for the predicate symbol in the head at every argument position of
* the represented atom, which TermVariable in the transition formula
* represents that argument in the represented atom.
*/
private final List<TermVariable> mHeadPredTermVariables;
// private final List<IProgramVar> mHeadPredProgramVariables;
private final HornClausePredicateSymbol mHeadPredicate;

// private final UnmodifiableTransFormula mTransitionFormula;

private final HCSymbolTable mHornClauseSymbolTable;

private final Term mFormula;
Expand All @@ -64,16 +50,16 @@ public class HornClause implements IRankedLetter {
* The script that will be used in TreeAutomizer (not the
* HornClauseParserScript)
* @param symbolTable
* @param transitionFormula
* @param constraint
* @param headPred
* @param headVars
* @param bodyPreds
* @param bodyPredToTermVariables
*/
public HornClause(final ManagedScript script, final HCSymbolTable symbolTable,
final Term transitionFormula,
public HornClause(final ManagedScript script, final HCSymbolTable symbolTable, final Term constraint,
final HornClausePredicateSymbol headPred, final List<TermVariable> headVars,
final List<HornClausePredicateSymbol> bodyPreds, final List<List<TermVariable>> bodyPredToTermVariables, int version) {
final List<HornClausePredicateSymbol> bodyPreds, final List<List<TermVariable>> bodyPredToTermVariables,
int version) {

mHornClauseSymbolTable = symbolTable;

Expand All @@ -89,88 +75,28 @@ public HornClause(final ManagedScript script, final HCSymbolTable symbolTable,
.collect(Collectors.toList());

// transfer the transition formula to the solver script
// Term convertedFormula = ttf.transform(transitionFormula);
mFormula = ttf.transform(transitionFormula);
mFormula = ttf.transform(constraint);

for (TermVariable fv : mFormula.getFreeVars()) {
mHornClauseSymbolTable.registerTermVariable(fv);
}

mHeadPredicate = headPred;
mBodyPreds = bodyPreds;

// mBodyPredToHCInVars = new ArrayList<>();
// mBodyPredToIProgramVar = new ArrayList<>();

// mHeadPredProgramVariables = new ArrayList<>();

// /*
// * build the TransFormula
// */
// final Map<IProgramVar, TermVariable> outVars = new HashMap<>();
// for (int i = 0; i < mHeadPredTermVariables.size(); ++i) {
// final TermVariable tv = mHeadPredTermVariables.get(i);
// final Sort sort = tv.getSort();
// final HCOutVar hcOutVar = symbolTable.getOrConstructHCOutVar(i, sort);
// mHeadPredProgramVariables.add(hcOutVar);
//// if (Arrays.asList(convertedFormula.getFreeVars()).contains(tv)) {
// outVars.put(hcOutVar, tv);
//// }
// }
//
// final Map<IProgramVar, TermVariable> inVars = new HashMap<>();
// for (int i = 0; i < mBodyPredToTermVariables.size(); i++) {
// mBodyPredToHCInVars.add(new ArrayList<>());
// mBodyPredToIProgramVar.add(new ArrayList<>());
// for (int j = 0; j < mBodyPredToTermVariables.get(i).size(); j++) {
// final TermVariable tv = mBodyPredToTermVariables.get(i).get(j);
// final Sort sort = tv.getSort();
// final HCInVar hcInVar = symbolTable.getOrConstructHCInVar(i, j, sort);
// mBodyPredToHCInVars.get(i).add(hcInVar);
// mBodyPredToIProgramVar.get(i).add(hcInVar);
//// if (Arrays.asList(convertedFormula.getFreeVars()).contains(tv)) {
// inVars.put(hcInVar, tv);
//// }
// }
// }

// introduce "x = x" for any unchanged var x, i.e., a var that occurs in head and body..
// final Set<TermVariable> intersection = new HashSet<>();
// mBodyPredToTermVariables.stream().forEach(bptvList -> intersection.addAll(bptvList));
// intersection.retainAll(mHeadPredTermVariables);
// script.lock(this);
// for (TermVariable unchangedVar : intersection) {
// convertedFormula = Util.and(script.getScript(), convertedFormula,
// script.term(this, "=", unchangedVar, unchangedVar));
// }
// script.unlock(this);


// final TransFormulaBuilder tb = new TransFormulaBuilder(inVars, outVars, true, null, true, null, true);
// tb.setFormula(convertedFormula);
// tb.setInfeasibility(Infeasibility.NOT_DETERMINED);
// mTransitionFormula = tb.finishConstruction(script);
}

public HornClause(final ManagedScript script, final HCSymbolTable symbolTable,
final Term transitionFormula,
final HornClausePredicateSymbol head, final List<TermVariable> headVars,
final List<HornClausePredicateSymbol> bodyPreds, final List<List<TermVariable>> bodyPredToTermVariables) {
this(script, symbolTable, transitionFormula, head, headVars, bodyPreds, bodyPredToTermVariables, 0);
}

// @Override
// public UnmodifiableTransFormula getTransformula() {
// return mTransitionFormula;
// // assert false : "TODO : what?";
// // return null;
// }

public HornClausePredicateSymbol getHeadPredicate() {
return mHeadPredicate;
}

public List<HornClausePredicateSymbol> getBodyPredicates() {
// return mBodyPredToTermVariables.keySet();
return mBodyPreds;
}

Expand All @@ -190,22 +116,10 @@ public List<List<TermVariable>> getBodyPredToTermVariables() {
return Collections.unmodifiableList(mBodyPredToTermVariables);
}

// public List<HCInVar> getHCInVarsForPredPos(int predPos) {
// return mBodyPredToHCInVars.get(predPos);
// }

// public List<IProgramVar> getProgramVarsForPredPos(int predPos) {
// return mBodyPredToIProgramVar.get(predPos);
// }

public List<TermVariable> getTermVariablesForHeadPred() {
return mHeadPredTermVariables;
}

// public List<IProgramVar> getProgramVarsForHeadPred() {
// return mHeadPredProgramVariables;
// }

@Override
public String toString() {
// String cobody = "";
Expand Down Expand Up @@ -237,22 +151,6 @@ public String toString() {
// return "HornClause TODO: better description"; //TODO
}

// /**
// * This method is added only for fulfilling the IInternalAction interface.
// */
// @Override
// public String getPrecedingProcedure() {
// return HornUtilConstants.HORNCLAUSEMETHODNAME;
// }

// /**
// * This method is added only for fulfilling the IInternalAction interface.
// */
// @Override
// public String getSucceedingProcedure() {
// return HornUtilConstants.HORNCLAUSEMETHODNAME;
// }

public HCSymbolTable getHornClauseSymbolTable() {
return mHornClauseSymbolTable;
}
Expand All @@ -264,7 +162,6 @@ public int getRank() {
return 1;
}
return mBodyPreds.size();// mTransitionFormula.getInVars().size();
//return mBodyPreds.size();
}
public Term getFormula() {
return mFormula;
Expand Down
81 changes: 29 additions & 52 deletions ...iburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCHoareTripleChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@
import de.uni_freiburg.informatik.ultimate.lib.treeautomizer.HCSymbolTable;
import de.uni_freiburg.informatik.ultimate.lib.treeautomizer.HornClause;
import de.uni_freiburg.informatik.ultimate.logic.Script.LBool;
import de.uni_freiburg.informatik.ultimate.logic.Sort;
import de.uni_freiburg.informatik.ultimate.logic.Term;
import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
import de.uni_freiburg.informatik.ultimate.logic.Util;
Expand Down Expand Up @@ -68,10 +69,11 @@ public class HCHoareTripleChecker {
private final CfgSmtToolkit mCfgSmtToolkit;
private final ManagedScript mManagedScript;
private final HCSymbolTable mSymbolTable;
private int mFreshConstantCounter;

/**
* Constructor of HCHoareTripleChecker
* @param predicateUnifier Unifer for the predicates.
* @param predicateUnifier Unifier for the predicates.
* @param cfgSmtToolkit
* */
public HCHoareTripleChecker(final PredicateUnifier predicateUnifier, final CfgSmtToolkit cfgSmtToolkit,
Expand Down Expand Up @@ -107,41 +109,10 @@ public Validity check(List<IPredicate> preOld, HornClause hornClause, IPredicate
} else {
pre = preOld;
}
//
//
// assert pre.size() == hornClause.getNoBodyPredicates() : "The number of preconditions must match the number of "
// + "uninterpreted predicates in the Horn clause's body!";

mManagedScript.lock(this);
mManagedScript.push(this, 1);

// /*
// * Compute the precondition
// * - substitute the predicate formulas of the "pre" predicates
// * - conjoin the substituted predicates
// */
// final Term[] substitutedPredicateFormulas = new Term[pre.size()];
// for (int predPos = 0; predPos < hornClause.getNoBodyPredicates(); predPos++) {
// assert pre.get(predPos).getVars().size() == hornClause.getBodyPredicates().get(predPos).getArity();
// final IPredicate currentPrePred = pre.get(predPos);
//
// final Term substitutedFormula = substitutePredicateFormula(currentPrePred,
// hornClause.getProgramVarsForPredPos(predPos));
// assert substitutedFormula != null;
// assert substitutedFormula.getFreeVars().length == 0 : "formula should have been closed by substitution";
// substitutedPredicateFormulas[predPos] = substitutedFormula;
// }
//
// final Term preConditionFormula = Util.and(mManagedScript.getScript(), substitutedPredicateFormulas);
// assert preConditionFormula.getFreeVars().length == 0 : "formula should have been closed by substitution";
//
// /*
// * Compute the postcondition
// */
// final Term postConditionFormula = substitutePredicateFormula(succ, hornClause.getProgramVarsForHeadPred());
// assert postConditionFormula.getFreeVars().length == 0 : "formula should have been closed by substitution";
// final Term negatedPostConditionFormula = Util.not(mManagedScript.getScript(), postConditionFormula);

Term preConditionFormula = mManagedScript.term(this, "true");

for (int i = 0; i < pre.size(); i++) {
Expand All @@ -151,7 +122,8 @@ public Validity check(List<IPredicate> preOld, HornClause hornClause, IPredicate
}
mManagedScript.assertTerm(this, preConditionFormula);

mManagedScript.assertTerm(this, close(hornClause.getFormula(), mSymbolTable));
final Term closedConstraint = close(hornClause.getFormula(), mSymbolTable);
mManagedScript.assertTerm(this, closedConstraint);

final Term negatedPostConditionFormula = SmtUtils.not(mManagedScript.getScript(),
unify(succ, hornClause.getTermVariablesForHeadPred()));
Expand All @@ -170,7 +142,19 @@ private Term close(Term term, HCSymbolTable symbolTable) {
final Map<Term, Term> substitution = new HashMap<>();

for (TermVariable fv : term.getFreeVars()) {
substitution.put(fv, symbolTable.getConstForTermVar(fv));
if (symbolTable.hasConstForTermVar(fv)) {
// the variable occurs in one of the input hornClauses --> we already have a constant declared for it
substitution.put(fv, symbolTable.getConstForTermVar(fv));
} else {
/*
* the variable was introduced at unification because we could not match all positions (because the
* predicate symbol in the Horn clause has lower arity than the current pre/postcondition predicate)
*/
final String freshConstantName = "c_" + fv.toString().substring(2, fv.toString().length()) + "_" +
+ mFreshConstantCounter++;
mManagedScript.declareFun(this, freshConstantName, new Sort[0], fv.getSort());
substitution.put(fv, mManagedScript.term(this, freshConstantName));
}
}

return new Substitution(mManagedScript, substitution).transform(term);
Expand All @@ -181,25 +165,21 @@ private Term unify(IPredicate iPredicate, List<TermVariable> termVariablesForPre
final Map<Term, Term> substitution = new HashMap<>();
for (IProgramVar pvar : iPredicate.getVars()) {
final HCOutVar hcvar = (HCOutVar) pvar;
substitution.put(hcvar.getTermVariable(), termVariablesForPredPos.get(hcvar.getArgumentPos()));

if (termVariablesForPredPos.size() > hcvar.getArgumentPos()) {
substitution.put(hcvar.getTermVariable(), termVariablesForPredPos.get(hcvar.getArgumentPos()));
} else {
/*
* the predicate we want to unify with has less arguments than the hornClause's head predicate
* --> introduce a fresh variable
*/
substitution.put(hcvar.getTermVariable(),
mManagedScript.constructFreshTermVariable("any", hcvar.getSort()));
}
}
return new Substitution(mManagedScript, substitution).transform(iPredicate.getFormula());
}


// private Term closeHcTransFormula(Term term) {
// Map<Term, Term> substitution = new HashMap<>();
// assert false;
//// for (Entry<IProgramVar, TermVariable> en : term.getInVars().entrySet()) {
//// substitution.put(en.getValue(), en.getKey().getDefaultConstant());
//// }
//// for (Entry<IProgramVar, TermVariable> en : term.getOutVars().entrySet()) {
//// substitution.put(en.getValue(), en.getKey().getDefaultConstant());
//// }
// return new Substitution(mManagedScript, substitution).transform(term);
// }


/**
* Substitute the formula of an IPredicate over HCOutVars through a given list of ProgramVariabls (appearing in a
* TransFormula)
Expand Down Expand Up @@ -232,7 +212,6 @@ private Term substitutePredicateFormula(final IPredicate predicate, final List<I
return substitutedFormula;
}


private Term replaceFreeVarsWithFreshConstants(Term formula) {
final Map<Term, Term> substitution = new HashMap<>();
for (TermVariable fv : formula.getFreeVars()) {
Expand All @@ -242,7 +221,6 @@ private Term replaceFreeVarsWithFreshConstants(Term formula) {
return new Substitution(mManagedScript, substitution).transform(formula);
}


private Map<Integer, HCOutVar> sortHCOutVars(IPredicate pred) {
Map<Integer, HCOutVar> result = new HashMap<>();
for (IProgramVar var : pred.getVars()) {
Expand All @@ -252,7 +230,6 @@ private Map<Integer, HCOutVar> sortHCOutVars(IPredicate pred) {
return result;
}


public Validity check(TreeAutomatonRule<HornClause, IPredicate> rule) {
return check(rule.getSource(), rule.getLetter(), rule.getDest());
}
Expand Down
5 changes: 5 additions & 0 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 @@ -270,6 +270,11 @@ private int getFreshIndex(TermVariable tv) {

}

/**
* Keeps the information about the SSA-substitution of one node in a TreeRun.
*
* @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
*/
class SsaInfo {

final HornClause mHornClause;
Expand Down

0 comments on commit f19a7d2

Please sign in to comment.