From e69edd4dc9faed7d46bb4f10dd72197584ec4ab5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Tue, 22 Mar 2016 15:54:30 +0100
Subject: [PATCH] ExamplesAdder.scala now simplifies the postcondition before
adding examples to it.
---
.../scala/leon/synthesis/disambiguation/ExamplesAdder.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 7c73a5b91..8f0eb70cd 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -11,6 +11,7 @@ import purescala.Definitions.{ FunDef, Program, ValDef }
import purescala.ExprOps
import purescala.Extractors.TopLevelAnds
import purescala.Expressions._
+import leon.utils.Simplifiers
/**
* @author Mikael
@@ -54,7 +55,8 @@ class ExamplesAdder(ctx0: LeonContext, program: Program) {
private def filterCases(cases: Seq[MatchCase]) = cases.filter(c => c.optGuard != Some(BooleanLiteral(false)))
- def addToExpr(post: Expr, id: Identifier, inputVariables: Expr, newCases: Seq[MatchCase]): Expr = {
+ def addToExpr(_post: Expr, id: Identifier, inputVariables: Expr, newCases: Seq[MatchCase]): Expr = {
+ val post= Simplifiers.bestEffort(ctx0, program)(_post)
if(purescala.ExprOps.exists(_.isInstanceOf[Passes])(post)) {
post match {
case TopLevelAnds(exprs) =>
--
GitLab