From 9bf1c4d1e31d5b398233c2b3f0a1aca1b06e2cab Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 1 Oct 2016 19:03:26 +0200
Subject: [PATCH] Removed certain unecessary ordering clauses for lambda
equality
---
.../solvers/unrolling/LambdaTemplates.scala | 23 +------------------
1 file changed, 1 insertion(+), 22 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index a31bdc567..1194bcea1 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -239,16 +239,6 @@ trait LambdaTemplates { self: Templates =>
clauses ++ super.instantiate(b, args)
}
- override def instantiate(substMap: Map[Encoded, Arg]): Clauses = {
- val substituter = mkSubstituter(substMap.mapValues(_.encoded))
-
- val clauses: Clauses = (for (template <- lambdas) yield {
- registerClosure(substituter(start), ids._2 -> tpe, substituter(template.ids._2) -> template.tpe)
- }).flatten
-
- clauses ++ super.instantiate(substMap)
- }
-
private lazy val str : String = stringRepr()
override def toString : String = str
}
@@ -407,18 +397,7 @@ trait LambdaTemplates { self: Templates =>
registerParent(typeBlocker, firstB)
val symClauses = registerSymbol(typeBlocker, encoded, to)
- def orderClauses(tpe: FunctionType, caller: Encoded, args: Seq[Encoded]): Clauses = tpe match {
- case FunctionType(from, to: FunctionType) =>
- val (curr, rest) = args.splitAt(from.size)
- val newCaller = mkApp(caller, tpe, curr)
- registerClosure(typeBlocker, caller -> tpe, newCaller -> to) ++ orderClauses(to, newCaller, rest)
- case _ => Seq.empty[Encoded]
- }
-
- orderClauses(tpe, caller, args.map(_.encoded)) ++
- symClauses :+
- extClause :+
- mkImplies(firstB, typeBlocker)
+ symClauses :+ extClause :+ mkImplies(firstB, typeBlocker)
}
applications += tpe -> (applications(tpe) + key)
--
GitLab