diff --git a/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java b/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java index 0c4b7c0f3cf..9ad141c9735 100644 --- a/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java +++ b/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HCSymbolTable.java @@ -204,4 +204,8 @@ public Term getConstForTermVar(TermVariable fv) { return res; } + public boolean hasConstForTermVar(TermVariable fv) { + return mTermVarToConst.containsKey(fv); + } + } diff --git a/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HornClause.java b/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HornClause.java index cb9d68af717..da8b1126bfc 100644 --- a/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HornClause.java +++ b/trunk/source/Library-TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/lib/treeautomizer/HornClause.java @@ -27,20 +27,9 @@ */ 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> - // mBodyPredToTermVariables; - private final List mBodyPreds; private final List> mBodyPredToTermVariables; -// private final List> mBodyPredToHCInVars; -// private List> mBodyPredToIProgramVar; /** * Stores for the predicate symbol in the head at every argument position of @@ -48,11 +37,8 @@ public class HornClause implements IRankedLetter { * represents that argument in the represented atom. */ private final List mHeadPredTermVariables; -// private final List mHeadPredProgramVariables; private final HornClausePredicateSymbol mHeadPredicate; -// private final UnmodifiableTransFormula mTransitionFormula; - private final HCSymbolTable mHornClauseSymbolTable; private final Term mFormula; @@ -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 headVars, - final List bodyPreds, final List> bodyPredToTermVariables, int version) { + final List bodyPreds, final List> bodyPredToTermVariables, + int version) { mHornClauseSymbolTable = symbolTable; @@ -89,8 +75,7 @@ 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); @@ -98,59 +83,8 @@ public HornClause(final ManagedScript script, final HCSymbolTable symbolTable, mHeadPredicate = headPred; mBodyPreds = bodyPreds; - -// mBodyPredToHCInVars = new ArrayList<>(); -// mBodyPredToIProgramVar = new ArrayList<>(); - -// mHeadPredProgramVariables = new ArrayList<>(); - -// /* -// * build the TransFormula -// */ -// final Map 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 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 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 headVars, @@ -158,19 +92,11 @@ public HornClause(final ManagedScript script, final HCSymbolTable symbolTable, 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 getBodyPredicates() { - // return mBodyPredToTermVariables.keySet(); return mBodyPreds; } @@ -190,22 +116,10 @@ public List> getBodyPredToTermVariables() { return Collections.unmodifiableList(mBodyPredToTermVariables); } -// public List getHCInVarsForPredPos(int predPos) { -// return mBodyPredToHCInVars.get(predPos); -// } - -// public List getProgramVarsForPredPos(int predPos) { -// return mBodyPredToIProgramVar.get(predPos); -// } - public List getTermVariablesForHeadPred() { return mHeadPredTermVariables; } -// public List getProgramVarsForHeadPred() { -// return mHeadPredProgramVariables; -// } - @Override public String toString() { // String cobody = ""; @@ -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; } @@ -264,7 +162,6 @@ public int getRank() { return 1; } return mBodyPreds.size();// mTransitionFormula.getInVars().size(); - //return mBodyPreds.size(); } public Term getFormula() { return mFormula; diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCHoareTripleChecker.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCHoareTripleChecker.java index 8a6b713632d..481ad207876 100644 --- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCHoareTripleChecker.java +++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCHoareTripleChecker.java @@ -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; @@ -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, @@ -107,41 +109,10 @@ public Validity check(List 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++) { @@ -151,7 +122,8 @@ public Validity check(List 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())); @@ -170,7 +142,19 @@ private Term close(Term term, HCSymbolTable symbolTable) { final Map 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); @@ -181,25 +165,21 @@ private Term unify(IPredicate iPredicate, List termVariablesForPre final Map 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 substitution = new HashMap<>(); -// assert false; -//// for (Entry en : term.getInVars().entrySet()) { -//// substitution.put(en.getValue(), en.getKey().getDefaultConstant()); -//// } -//// for (Entry 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) @@ -232,7 +212,6 @@ private Term substitutePredicateFormula(final IPredicate predicate, final List substitution = new HashMap<>(); for (TermVariable fv : formula.getFreeVars()) { @@ -242,7 +221,6 @@ private Term replaceFreeVarsWithFreshConstants(Term formula) { return new Substitution(mManagedScript, substitution).transform(formula); } - private Map sortHCOutVars(IPredicate pred) { Map result = new HashMap<>(); for (IProgramVar var : pred.getVars()) { @@ -252,7 +230,6 @@ private Map sortHCOutVars(IPredicate pred) { return result; } - public Validity check(TreeAutomatonRule rule) { return check(rule.getSource(), rule.getLetter(), rule.getDest()); } 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 67ac1efdf90..677f146da0b 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 @@ -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;