From 8a01b7f1eb8a741a112aa79dce13ee411c63dd16 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 11 Nov 2014 15:50:15 +0100
Subject: [PATCH] Apply matchToIfThenElse before compiling expressions in CEGIS
---
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 0b740adf7..7ced27bff 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -240,7 +240,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
val forArray = replace(substMap, simplerRes)
// We trust arrays to be fast...
- val eval = evaluator.compile(forArray, ba +: p.as)
+ val eval = evaluator.compile(matchToIfThenElse(forArray), ba +: p.as)
eval.map{e => { case (bss, ins) =>
e(FiniteArray(bss).setType(ArrayType(BooleanType)) +: ins)
@@ -248,7 +248,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
}
def compileWithArgs(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
- val eval = evaluator.compile(simplerRes, bssOrdered ++ p.as)
+ val eval = evaluator.compile(matchToIfThenElse(simplerRes), bssOrdered ++ p.as)
eval.map{e => { case (bss, ins) =>
e(bss ++ ins)
--
GitLab