From c292984cf2f0a42ae7c3106de1215c98983b3f58 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 17 Dec 2014 15:21:15 +0100
Subject: [PATCH] Cost models decide which rules can be applied depending on
graph
---
library/lang/synthesis/package.scala | 1 -
src/main/scala/leon/repair/RepairCostModel.scala | 9 +++++----
src/main/scala/leon/repair/Repairman.scala | 4 ++--
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/library/lang/synthesis/package.scala b/library/lang/synthesis/package.scala
index 62e08280c..1f5f749b6 100644
--- a/library/lang/synthesis/package.scala
+++ b/library/lang/synthesis/package.scala
@@ -45,5 +45,4 @@ package object synthesis {
@library
@witness
def guide[T](e: T): Boolean = true
-
}
diff --git a/src/main/scala/leon/repair/RepairCostModel.scala b/src/main/scala/leon/repair/RepairCostModel.scala
index c658b93e1..e9b1a8163 100644
--- a/src/main/scala/leon/repair/RepairCostModel.scala
+++ b/src/main/scala/leon/repair/RepairCostModel.scala
@@ -17,10 +17,11 @@ case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("
val h = cm.andNode(an, subs).minSize
Cost(an.ri.rule match {
- case rules.GuidedDecomp => h/3
- case rules.GuidedCloser => h/3
- case rules.CEGLESS => h/2
- case _ => h
+ case rules.GuidedDecomp => h/2
+ case rules.GuidedCloser => 0
+ case rules.CEGLESS => 0
+ case rules.TEGLESS => 1
+ case _ => h+1
})
}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index fa4aa5685..97fc1b86e 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -109,8 +109,8 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
functionsToIgnore = soptions0.functionsToIgnore + fd,
costModel = RepairCostModel(soptions0.costModel),
rules = (soptions0.rules ++ Seq(
- //GuidedDecomp,
- //GuidedCloser,
+ GuidedDecomp,
+ GuidedCloser,
CEGLESS,
TEGLESS
)) diff Seq(ADTInduction)
--
GitLab