Merge pull request #135 from jad-hamza/fix-115

Implement @samarion's fix for issue 115 with lambda pointers

Author: samarion

src/it/resources/regression/tip/UNSAT/LambdaPointers-Issue115.tip

@@ -0,0 +1,6 @@
+(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
+(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
+(declare-datatypes () ((T (TT (body S)))))
+(define-fun t () T (TT (C 22 5)))
+(assert (not (let ((g f)) (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ g r2))) g) 22) 5))))
+(check-sat)

src/main/scala/inox/solvers/unrolling/Templates.scala

@@ -514,23 +514,32 @@ trait Templates
 
   object Template {
 
-    def lambdaPointers(encoder: Expr => Encoded)(expr: Expr): Map[Encoded, Encoded] = {
-      def collectSelectors(expr: Expr, ptr: Expr): Seq[(Expr, Variable)] = expr match {
-        case adt @ ADT(id, tps, es) => (adt.getConstructor.fields zip es).flatMap {
-          case (vd, e) => collectSelectors(e, ADTSelector(ptr, vd.id))
-        }
+    private def collectSelectors(expr: Expr, ptr: Expr): Seq[(Expr, Variable)] = expr match {
+      case adt @ ADT(id, tps, es) => (adt.getConstructor.fields zip es).flatMap {
+        case (vd, e) => collectSelectors(e, ADTSelector(ptr, vd.id))
+      }
 
-        case Tuple(es) => es.zipWithIndex.flatMap {
-          case (e, i) => collectSelectors(e, TupleSelect(ptr, i + 1))
-        }
+      case Tuple(es) => es.zipWithIndex.flatMap {
+        case (e, i) => collectSelectors(e, TupleSelect(ptr, i + 1))
+      }
+
+      case IsTyped(v: Variable, _: FunctionType) => Seq(ptr -> v)
+      case _ => Seq.empty
+    }
 
-        case IsTyped(v: Variable, _: FunctionType) => Seq(ptr -> v)
-        case _ => Seq.empty
+    private def resultPointers(encoder: Expr => Encoded)(expr: Expr): Map[Encoded, Encoded] = {
+      val pointers = expr match {
+        case Equals(v @ (_: Variable | _: FunctionInvocation | _: Application), e) => collectSelectors(e, v).toMap
+        case Equals(e, v @ (_: Variable | _: FunctionInvocation | _: Application)) => collectSelectors(e, v).toMap
+        case _ => Map.empty[Expr, Variable]
       }
 
+      pointers.map(p => encoder(p._1) -> encoder(p._2))
+    }
+
+    def lambdaPointers(encoder: Expr => Encoded)(expr: Expr): Map[Encoded, Encoded] = {
+
       val pointers = exprOps.collect {
-        case Equals(v @ (_: Variable | _: FunctionInvocation | _: Application), e) => collectSelectors(e, v).toSet
-        case Equals(e, v @ (_: Variable | _: FunctionInvocation | _: Application)) => collectSelectors(e, v).toSet
         case FunctionInvocation(_, _, es) => es.flatMap(e => collectSelectors(e, e)).toSet
         case Application(_, es) => es.flatMap(e => collectSelectors(e, e)).toSet
         case e: Tuple => collectSelectors(e, e).toSet
@@ -661,6 +670,10 @@ trait Templates
           if (matchs.nonEmpty) matchers += bp -> matchs
         }
 
+        for (e <- guardedExprs.getOrElse(pv, Set.empty)) {
+          pointers ++= resultPointers(encoder)(e)
+        }
+
         clauses ++= (for ((b,es) <- guardedExprs; e <- es) yield encoder(Implies(b, e)))
         clauses ++= eqs.map(encoder)