From caf0f1333d9b8fb65a278d5c27e44bbc6973e596 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 4 Feb 2015 19:00:20 +0100
Subject: [PATCH] Correct computation of sizes
---
runTests.sh | 2 +-
src/main/scala/leon/purescala/TreeOps.scala | 15 +++++++++++++++
2 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/runTests.sh b/runTests.sh
index d7ca90f21..e792db1f3 100755
--- a/runTests.sh
+++ b/runTests.sh
@@ -36,7 +36,7 @@ echo "# Category, File, function, p.S, fuS
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_pad testcases/repair/List/List1.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_++ testcases/repair/List/List2.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_ap testcases/repair/List/List3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --functions=_drop testcases/repair/List/List4.scala | tee -a $fullLog
+#./leon --repair --timeout=30 --functions=_drop testcases/repair/List/List4.scala | tee -a $fullLog
./leon --repair --timeout=30 --functions=_replace testcases/repair/List/List5.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_count testcases/repair/List/List6.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_find testcases/repair/List/List7.scala | tee -a $fullLog
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 8cc5f31fa..ebba57547 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1372,10 +1372,25 @@ object TreeOps {
simplePreTransform(pre)(expr)
}
+ def patternSize(p: Pattern): Int = p match {
+ case wp: WildcardPattern =>
+ 1
+ case _ =>
+ p.subPatterns.foldLeft(1 + (if(p.binder.isDefined) 1 else 0)) {
+ case (s, p) => s + patternSize(p)
+ }
+ }
+
def formulaSize(e: Expr): Int = e match {
case t: Terminal =>
1
+ case ml: MatchLike =>
+ ml.cases.foldLeft(formulaSize(ml.scrutinee)) {
+ case (s, MatchCase(p, og, rhs)) =>
+ s + formulaSize(rhs) + og.map(formulaSize).getOrElse(0) + patternSize(p)
+ }
+
case UnaryOperator(e, builder) =>
formulaSize(e)+1
--
GitLab