From 7982a944a9a3f48a4dad433dccbcdf10071f2e26 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 26 Nov 2014 16:00:09 +0100
Subject: [PATCH] remove buggy optimizations
---
.../synthesis/rules/IntegerInequalities.scala | 41 +++++++++----------
1 file changed, 20 insertions(+), 21 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 7cae2a735..182f29676 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -20,8 +20,6 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val TopLevelAnds(exprs) = problem.phi
-
-
//assume that we only have inequalities
var lhsSides: List[Expr] = Nil
var exprNotUsed: List[Expr] = Nil
@@ -73,25 +71,26 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val L = if(upperBounds.isEmpty && lowerBounds.isEmpty) -1 else lcm((upperBounds ::: lowerBounds).map(_._2))
//optimization when coef = 1 and when ub - lb is a constant greater than LCM
- upperBounds = upperBounds.filterNot{case (ub, uc) => if(uc == 1) {
- exprNotUsed ++= lowerBounds.map{case (lb, lc) => LessEquals(lb, Times(IntLiteral(lc), ub))}
- true
- } else
- false
- }
- lowerBounds = lowerBounds.filterNot{case (lb, lc) => if(lc == 1) {
- exprNotUsed ++= upperBounds.map{case (ub, uc) => LessEquals(Times(IntLiteral(uc), lb), ub)}
- true
- } else
- false
- }
- upperBounds = upperBounds.filterNot{case (ub, uc) => {
- lowerBounds.forall{case (lb, lc) => {
- expandAndSimplifyArithmetic(Minus(ub, lb)) match {
- case IntLiteral(n) => L - 1 <= n
- case _ => false
- }}}
- }}
+ //upperBounds = upperBounds.filterNot{case (ub, uc) => if(uc == 1) {
+ // exprNotUsed ++= lowerBounds.map{case (lb, lc) => LessEquals(lb, Times(IntLiteral(lc), ub))}
+ // true
+ // } else
+ // false
+ //}
+ //lowerBounds = lowerBounds.filterNot{case (lb, lc) => if(lc == 1) {
+ // exprNotUsed ++= upperBounds.map{case (ub, uc) => LessEquals(Times(IntLiteral(uc), lb), ub)}
+ // true
+ // } else
+ // false
+ //}
+ //upperBounds = upperBounds.filterNot{case (ub, uc) => {
+ // lowerBounds.forall{case (lb, lc) => {
+ // expandAndSimplifyArithmetic(Minus(ub, lb)) match {
+ // case IntLiteral(n) => L - 1 <= n
+ // case _ => false
+ // }}}
+ //}}
+
//define max function
val maxValDefs: Seq[ValDef] = lowerBounds.map(_ => ValDef(FreshIdentifier("b"), Int32Type))
--
GitLab