From acd77b90a2a87af763498162ab887a14e073321a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 22 Nov 2012 19:17:06 +0100
Subject: [PATCH] heuristic to remove variable in inequality with lower lcm
---
.../scala/leon/synthesis/rules/IntegerEquation.scala | 2 +-
.../leon/synthesis/rules/IntegerInequalities.scala | 12 ++++++++++--
2 files changed, 11 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index ef830dc0b..1561520d5 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -11,7 +11,7 @@ import purescala.TypeTrees._
import purescala.Definitions._
import LinearEquations.elimVariable
-class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth, 300) {
+class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth, 600) {
def attemptToApplyOn(problem: Problem): RuleResult = if(!problem.xs.exists(_.getType == Int32Type)) RuleInapplicable else {
val TopLevelAnds(exprs) = problem.phi
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index bee26bf88..5faa28594 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -12,7 +12,7 @@ import purescala.Definitions._
import LinearEquations.elimVariable
import leon.synthesis.Algebra.lcm
-class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities", synth, 300) {
+class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities", synth, 600) {
def attemptToApplyOn(problem: Problem): RuleResult = {
val TopLevelAnds(exprs) = problem.phi
@@ -31,8 +31,16 @@ class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities
val ineqVars = lhsSides.foldLeft(Set[Identifier]())((acc, lhs) => acc ++ variablesOf(lhs))
val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains(_))
+
if(candidateVars.isEmpty) RuleInapplicable else {
- val processedVar = candidateVars.head
+ val processedVar: Identifier = candidateVars.map(v => {
+ val normalizedLhs: List[List[Expr]] = lhsSides.map(linearArithmeticForm(_, Array(v)).toList)
+ if(normalizedLhs.isEmpty)
+ (v, 0)
+ else
+ (v, lcm(normalizedLhs.map{ case List(t, IntLiteral(i)) => if(i == 0) 1 else i.abs case _ => sys.error("shouldn't happen") }))
+ }).toList.sortWith((t1, t2) => t1._2 <= t2._2).head._1
+
val otherVars: List[Identifier] = problem.xs.filterNot(_ == processedVar)
val normalizedLhs: List[List[Expr]] = lhsSides.map(linearArithmeticForm(_, Array(processedVar)).toList)
--
GitLab