Merge pull request #704 from viperproject/meilers_qp_hints

Function application as QP hints

Author: marcoeilers

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1723,7 +1723,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       arguments.flatMap {
         case SeqAt(seq, _) => Some(seq)
         case MapLookup(map, _) => Some(map)
-        // TODO: Add a case for (domain or heap-dep.) function applications, i.e. fun(_)
+        case App(f, _) => Some(AppHint(f))
         case _ => None
       }
 

src/main/scala/state/Terms.scala

@@ -244,6 +244,13 @@ object App extends ((Applicable, Seq[Term]) => App) {
   def unapply(app: App) = Some((app.applicable, app.args))
 }
 
+/*
+ * Applicable without arguments, only to be used as a hint for quantified chunks.
+ */
+case class AppHint(applicable: Applicable) extends Term {
+  val sort = applicable.resultSort
+}
+
 /*
  * Terms
  */