From e36ef7c4412d5cda57bf98a596fae7533a0c3ed6 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 3 Aug 2016 15:04:10 +0200
Subject: [PATCH] Add CollectorWithPC constructor
---
.../inox/transformers/CollectorWithPC.scala | 26 +++++++++++++++++++
.../inox/transformers/TransformerWithPC.scala | 3 ---
2 files changed, 26 insertions(+), 3 deletions(-)
create mode 100644 src/main/scala/inox/transformers/CollectorWithPC.scala
diff --git a/src/main/scala/inox/transformers/CollectorWithPC.scala b/src/main/scala/inox/transformers/CollectorWithPC.scala
new file mode 100644
index 000000000..771fab6f8
--- /dev/null
+++ b/src/main/scala/inox/transformers/CollectorWithPC.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package transformers
+
+/** A [[Collector]] that collects path conditions */
+trait CollectorWithPC extends TransformerWithPC with Collector
+
+object CollectorWithPC {
+ def apply[T](p: Program)(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]) = {
+ new CollectorWithPC {
+
+ type R = T
+ val trees: p.trees.type = p.trees
+ val symbols: p.symbols.type = p.symbols
+ import trees.Expr
+ import symbols.Path
+ val initEnv: Path = Path.empty
+
+ protected def step(e: Expr, env: Path): List[(T, Path)] = {
+ f.lift((e, env)).map((_, env)).toList
+ }
+
+ }
+ }
+}
diff --git a/src/main/scala/inox/transformers/TransformerWithPC.scala b/src/main/scala/inox/transformers/TransformerWithPC.scala
index fd0709898..ecda40920 100644
--- a/src/main/scala/inox/transformers/TransformerWithPC.scala
+++ b/src/main/scala/inox/transformers/TransformerWithPC.scala
@@ -95,6 +95,3 @@ trait TransformerWithPC extends Transformer {
}
}
-
-/** A [[Collector]] that collects path conditions */
-trait CollectorWithPC extends TransformerWithPC with Collector
--
GitLab