Skip to content
Snippets Groups Projects
Commit c292984c authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Cost models decide which rules can be applied depending on graph

parent 51e01a87
Branches
Tags
No related merge requests found
...@@ -45,5 +45,4 @@ package object synthesis { ...@@ -45,5 +45,4 @@ package object synthesis {
@library @library
@witness @witness
def guide[T](e: T): Boolean = true def guide[T](e: T): Boolean = true
} }
...@@ -17,10 +17,11 @@ case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair(" ...@@ -17,10 +17,11 @@ case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("
val h = cm.andNode(an, subs).minSize val h = cm.andNode(an, subs).minSize
Cost(an.ri.rule match { Cost(an.ri.rule match {
case rules.GuidedDecomp => h/3 case rules.GuidedDecomp => h/2
case rules.GuidedCloser => h/3 case rules.GuidedCloser => 0
case rules.CEGLESS => h/2 case rules.CEGLESS => 0
case _ => h case rules.TEGLESS => 1
case _ => h+1
}) })
} }
......
...@@ -109,8 +109,8 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout ...@@ -109,8 +109,8 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
functionsToIgnore = soptions0.functionsToIgnore + fd, functionsToIgnore = soptions0.functionsToIgnore + fd,
costModel = RepairCostModel(soptions0.costModel), costModel = RepairCostModel(soptions0.costModel),
rules = (soptions0.rules ++ Seq( rules = (soptions0.rules ++ Seq(
//GuidedDecomp, GuidedDecomp,
//GuidedCloser, GuidedCloser,
CEGLESS, CEGLESS,
TEGLESS TEGLESS
)) diff Seq(ADTInduction) )) diff Seq(ADTInduction)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment