From eb8a68051d4445c6756d1e512ee18950cccc9b21 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 22 Nov 2012 14:52:01 +0100
Subject: [PATCH] optimization when coefficient is one
---
.../synthesis/rules/IntegerInequalities.scala | 20 +++++++++++++++++--
1 file changed, 18 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index b2c767771..56795de12 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -35,9 +35,7 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
val processedVar = candidateVars.head
val otherVars: List[Identifier] = problem.xs.filterNot(_ == processedVar)
- println("lhsSides: " + lhsSides)
val normalizedLhs: List[List[Expr]] = lhsSides.map(linearArithmeticForm(_, Array(processedVar)).toList)
- println("normalized: " + normalizedLhs.mkString("\n"))
var upperBounds: List[(Expr, Int)] = Nil // (t, c) means c*x <= t
var lowerBounds: List[(Expr, Int)] = Nil // (t, c) means t <= c*x
normalizedLhs.foreach{
@@ -48,6 +46,24 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
case err => sys.error("unexpected from normal form: " + err)
}
+ //optimization when coef = 1
+ 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 }
+
+ println("lowerBounds: " + lowerBounds)
+ println("upperBounds: " + upperBounds)
+ println("exprNotUsed: " + exprNotUsed)
+
+ //lowerBounds.exists{case (lb, lc) => {
+ // if(uc == 1)
+ //}}}
+
//define max function
val maxVarDecls: Seq[VarDecl] = lowerBounds.map(_ => VarDecl(FreshIdentifier("b"), Int32Type))
val maxFun = new FunDef(FreshIdentifier("max"), Int32Type, maxVarDecls)
--
GitLab