From d8fc644ef75618592a07df4309f925583a991dbc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 14 Nov 2012 15:07:03 +0100
Subject: [PATCH] .. I guess this time should be good
---
src/main/scala/leon/synthesis/LinearEquations.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 8 ++++----
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index a3ebe75da..3d9eb6230 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -10,7 +10,7 @@ object LinearEquations {
//eliminate one variable from normalizedEquation t + a1*x1 + ... + an*xn = 0
//return a mapping for each of the n variables in (pre, map, freshVars)
def elimVariable(as: Set[Identifier], normalizedEquation: List[Expr]): (Expr, List[Expr], List[Identifier]) = {
- println("elim in normalized: " + normalizedEquation)
+ require(normalizedEquation.size > 1)
require(normalizedEquation.tail.forall{case IntLiteral(i) if i != 0 => true case _ => false})
val t: Expr = normalizedEquation.head
val coefsVars: List[Int] = normalizedEquation.tail.map{case IntLiteral(i) => i}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 201aeb826..ed0cb1553 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -578,17 +578,17 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
case Some(normalizedEq0) => {
val (neqxs, normalizedEq) = eqxs.zip(normalizedEq0.tail).filterNot{ case (_, IntLiteral(0)) => true case _ => false}.unzip
- if(normalizedEq.size == 1) {
+ //if(normalizedEq.size == 1) {
- } else {
+ //} else {
val (eqPre, eqWitness, eqFreshVars) = elimVariable(eqas, normalizedEq)
val eqSubstMap: Map[Expr, Expr] = neqxs.zip(eqWitness).map{case (id, e) => (Variable(id), simplify(e))}.toMap
val freshFormula = simplify(replace(eqSubstMap, And(allOthers)))
- }
- (eqPre, freshFormula)
+ //}
+ //(eqPre, freshFormula)
val newProblem = Problem(as, And(eqPre, p.c), freshFormula, eqFreshVars)
--
GitLab