From 3d4692591821145e67dd3250035454d87ed08469 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 24 Feb 2014 12:01:27 +0100
Subject: [PATCH] Prevent IntegerEquation from generating empty sub-problems
---
src/main/scala/leon/synthesis/FileInterface.scala | 3 ---
src/main/scala/leon/synthesis/rules/IntegerEquation.scala | 8 +++++++-
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index c2bac94ca..02b5f9456 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -58,9 +58,6 @@ class FileInterface(reporter: Reporter) {
// Get base indentation of last line:
val lineChars = before.substring(before.lastIndexOf('\n')+1).toList
- println(lineChars)
- println(lineChars.takeWhile(_ == ' '))
-
val indent = lineChars.takeWhile(_ == ' ').size
val p = new ScalaPrinter(PrinterOptions())
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index efbc68ef0..b05db6949 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -110,7 +110,13 @@ case object IntegerEquation extends Rule("Integer Equation") {
None
}
- List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess, this.name))
+
+ if (subproblemxs.isEmpty) {
+ // we directly solve
+ List(RuleInstantiation.immediateSuccess(problem, this, onSuccess(List(Solution(And(eqPre, problem.pc), Set(), Tuple(Seq())))).get))
+ } else {
+ List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess, this.name))
+ }
}
}
}
--
GitLab