From 8f564c6dc51a50bef1910e5e393b080a9c7c5cf1 Mon Sep 17 00:00:00 2001 From: katharina99wa Date: Mon, 20 Feb 2023 16:17:18 +0100 Subject: [PATCH] Removed unnecessary variable declerations --- .../quantifier/DualJunctionDml.java | 32 ++----------------- 1 file changed, 3 insertions(+), 29 deletions(-) diff --git a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java index 57e4628522a..69178f6dc5f 100644 --- a/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java +++ b/trunk/source/Library-SmtLibUtils/src/de/uni_freiburg/informatik/ultimate/lib/smtlibutils/quantifier/DualJunctionDml.java @@ -189,14 +189,7 @@ private EliminationResult applyModElimination(final EliminationTask inputEt, fin final Term divisorAsTerm = SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), pmt.getDivisor()); final Term inverseAsTerm = SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), - pmt.getInverse()); - final Term aAsTerm = SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), pmt.getA()); - // product3 = a*x - final Term product3 = SmtUtils.mul(mScript, SmtSortUtils.getIntSort(mScript), aAsTerm, pmt.getEliminate()); - // sum2 = a*x + b - final Term sum2 = SmtUtils.sum(mScript, SmtSortUtils.getIntSort(mScript), product3, pmt.getB()); - // mod1 = a*x + b mod k - final Term mod1 = SmtUtils.mod(mScript, sum2, divisorAsTerm); + pmt.getInverse()); final Term modTermReplacement; if (SmtUtils.tryToConvertToLiteral(pmt.getB()) != null && SmtUtils.tryToConvertToLiteral(pmt.getB()).equals(Rational.ZERO)) { @@ -216,7 +209,7 @@ private EliminationResult applyModElimination(final EliminationTask inputEt, fin final Term zeroAsTerm = SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), zeroAsBigInteger); final Map sub3 = new HashMap(); - sub3.put(mod1, modTermReplacement); + sub3.put(pmt.getDmlSubterm(), modTermReplacement); Term termAfterFirstSubstitution = QuantifierUtils.getAbsorbingElement(mScript, inputEt.getQuantifier()); for (final Term conjunct : juncts) { if (conjunct == pmt.getContainingDualJunct()) { @@ -343,18 +336,9 @@ private EliminationResult applyDivEliminationWithSmallA(final EliminationTask in SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), pmt.getA()), y); // sum2 = ay + (b div k) final Term sum2 = SmtUtils.sum(mScript, SmtSortUtils.getIntSort(mScript), product2, div1); - // product3 = ax - final Term product3 = SmtUtils.mul(mScript, SmtSortUtils.getIntSort(mScript), - SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), pmt.getA()), - pmt.getEliminate()); - // sum4 = ax + b - final Term sum4 = SmtUtils.sum(mScript, SmtSortUtils.getIntSort(mScript), product3, pmt.getB()); - // div2 = ax + b div k - final Term div2 = SmtUtils.divInt(mScript, sum4, - SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), pmt.getDivisor())); List termJunctSubstList = new ArrayList<>(); if (aAsInt > 0) { - for (int i = 0; i < (aAsInt + 1); i++) { + for (int i = 0; i < aAsInt; i++) { BigInteger iAsBigInteger = BigInteger.valueOf(i); Term iAsTerm = SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), iAsBigInteger); // sum3 = ay + (b div k) + i @@ -419,11 +403,6 @@ private EliminationResult applyDivEliminationWithSmallRemainder(final Eliminatio final Term product3 = SmtUtils.mul(mScript, SmtSortUtils.getIntSort(mScript), nAsTerm, z); // sumBeforeFinal = ay + (b div k) + nz final Term sumBeforeFinal = SmtUtils.sum(mScript, SmtSortUtils.getIntSort(mScript), sum2, product3); - // sum4 = ax + b - final Term sum4 = SmtUtils.sum(mScript, SmtSortUtils.getIntSort(mScript), product3, pmt.getB()); - // div2 = ax + b div k - final Term div2 = SmtUtils.divInt(mScript, sum4, - SmtUtils.constructIntegerValue(mScript, SmtSortUtils.getIntSort(mScript), pmt.getDivisor())); List termJunctSubstList = new ArrayList<>(); for (int i = 0; i < absIntRemainderG + 1; i++) { BigInteger iAsBigInteger = BigInteger.valueOf(i); @@ -435,13 +414,8 @@ private EliminationResult applyDivEliminationWithSmallRemainder(final Eliminatio Term divConjunctSub = Substitution.apply(mMgdScript, subJunct, pmt.getContainingDualJunct()); termJunctSubstList.add(divConjunctSub); } - //QuantifierUtils.applyDualFiniteConnective - //final Term termJunctSubst = QuantifierUtils.applyDualFiniteConnective(mScript, inputEt.getQuantifier(), - // termJunctSubstList); final Term termJunctSubst = QuantifierUtils.applyCorrespondingFiniteConnective(mScript, inputEt.getQuantifier(), termJunctSubstList); - //final Map sub3 = new HashMap(); - //sub3.put(div2, termJunctSubst); final EliminationResult resultWithoutXInDiv = helpReturnForEliminatingDiv(inputEt, pmt, sub1, termJunctSubst, y, z); return resultWithoutXInDiv; }