From 33b63e07356383cc62ddbb9a4365704cdd1b2cca Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 4 Dec 2014 17:08:15 +0100
Subject: [PATCH] Stop unfolding if grammar is closed, which it is for CEGLESS
---
src/main/scala/leon/synthesis/rules/CegisLike.scala | 4 ++++
src/main/scala/leon/synthesis/rules/Cegless.scala | 2 +-
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index 12fd6299e..5d2e203f0 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -561,6 +561,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
solver1.assertCnstr(clause)
solver2.assertCnstr(clause)
+
+ if (clauses.isEmpty) {
+ unfolding = maxUnfoldings
+ }
}
// Compute all programs that have not been excluded yet
diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/Cegless.scala
index 4d8ebb86c..d5fbb2619 100644
--- a/src/main/scala/leon/synthesis/rules/Cegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegless.scala
@@ -13,7 +13,7 @@ import utils._
import utils.ExpressionGrammars._
case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
- override val maxUnfoldings = 3;
+ override val maxUnfoldings = 1000;
def getGrammar(sctx: SynthesisContext, p: Problem) = {
--
GitLab