From 160c0ae5daccf2feda06072ea786bfd4100c4ef8 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 19 Nov 2012 13:43:09 +0100
Subject: [PATCH] Unroll more, keep predicates
---
src/main/scala/leon/synthesis/rules/Cegis.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 52691946d..0f16842ed 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -118,7 +118,8 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
var lastF = TentativeFormula(p.c, p.phi, BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
var currentF = lastF.unroll
var unrolings = 0
- val maxUnrolings = 2
+ val maxUnrolings = 3
+ var predicates: Seq[Expr] = Seq()
do {
//println("="*80)
//println("Was: "+lastF.entireFormula)
@@ -127,7 +128,6 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
val tpe = TupleType(p.xs.map(_.getType))
val bss = currentF.bss
- var predicates: Seq[Expr] = Seq()
var continue = true
while (result.isEmpty && continue) {
--
GitLab