From a4873bf5317d60a12120dc5885dcb632a9883776 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 20 Nov 2012 20:05:16 +0100
Subject: [PATCH] switch order of sub variables, seems to generate code that is
easier to read
---
.../scala/leon/synthesis/rules/IntegerInequalities.scala | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index d3fb488de..3249c9289 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -109,7 +109,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
case ((b, k), l) => Equals(b, Plus(Times(IntLiteral(L), Variable(l)), Variable(k))) ::
newLowerBounds.map(lbound => LessEquals(Variable(k), Minus(b, lbound)))
} ++ exprNotUsed))
- val subProblemxs: List[Identifier] = otherVars ++ quotientIds
+ val subProblemxs: List[Identifier] = quotientIds ++ otherVars
val subProblem = Problem(problem.as ++ remainderIds, problem.c, subProblemFormula, subProblemxs)
def onSuccess(sols: List[Solution]): Solution = sols match {
@@ -127,7 +127,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
Tuple(problem.xs.map(Variable(_))))))
} else if(upperBounds.isEmpty || lowerBounds.isEmpty) {
Solution(pre, defs,
- LetTuple(otherVars++quotientIds, term,
+ LetTuple(subProblemxs, term,
Let(processedVar, witness,
Tuple(problem.xs.map(Variable(_))))))
} else if(upperBounds.size > 1) {
@@ -145,7 +145,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
Error("No solution exists"),
IfExpr(
concretePre,
- LetTuple(otherVars++quotientIds, concreteTerm,
+ LetTuple(subProblemxs, concreteTerm,
Let(processedVar, witness,
Tuple(problem.xs.map(Variable(_))))
),
--
GitLab