From 69291b5f2c883529ef23eae68473f44326fc3b27 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 16 Nov 2012 20:48:15 +0100
Subject: [PATCH] return precondition
---
.../leon/synthesis/rules/IntegerInequality.scala | 12 +++++-------
1 file changed, 5 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequality.scala b/src/main/scala/leon/synthesis/rules/IntegerInequality.scala
index fe9b6f14a..f91358fb3 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequality.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequality.scala
@@ -96,7 +96,7 @@ class IntegerInequality(synth: Synthesizer) extends Rule("Integer Inequality", s
val pre = And(
for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds)
yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc))))
- RuleSuccess(Solution(BooleanLiteral(true), Set(), IfExpr(pre, witness, Error("precondition violation"))))
+ RuleSuccess(Solution(pre, Set(), witness))
} else {
val L = GCD.lcm((upperBounds ::: lowerBounds).map(_._2))
val newUpperBounds: List[Expr] = upperBounds.map{case (bound, coef) => Times(IntLiteral(L/coef), bound)}
@@ -122,12 +122,10 @@ class IntegerInequality(synth: Synthesizer) extends Rule("Integer Inequality", s
val newPre = And(
for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds)
yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc))))
- Solution(pre, defs,
- IfExpr(newPre,
- LetTuple(subProblemxs, term,
- Let(processedVar, witness,
- Tuple(problem.xs.map(Variable(_))))),
- Error("Precondition violation")))
+ Solution(And(newPre, pre), defs,
+ LetTuple(subProblemxs, term,
+ Let(processedVar, witness,
+ Tuple(problem.xs.map(Variable(_))))))
} else if(upperBounds.isEmpty || lowerBounds.isEmpty) {
Solution(pre, defs,
LetTuple(otherVars++quotientIds, term,
--
GitLab