Skip to content
Snippets Groups Projects
Commit 56a5fcc4 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Update repair

Repair uses the same Cost as synthesis
Fix repair rules ordering
parent 5f5c8c02
No related branches found
No related tags found
No related merge requests found
/* Copyright 2009-2015 EPFL, Lausanne */
package leon
package repair
import synthesis._
import synthesis.rules._
import repair.rules._
case class RepairCostModel(cm: CostModel) extends WrappedCostModel(cm, "Repair("+cm.name+")") {
// FIXME: Implement this in repair strategy
/*override def andNode(an: AndNode, subs: Option[Seq[Cost]]) = {
val h = cm.andNode(an, subs).minSize
Cost(an.ri.rule match {
case Focus => -10
case CEGLESS => 0
case TEGLESS => 1
case _ => h+1
})
}*/
}
...@@ -192,12 +192,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou ...@@ -192,12 +192,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val soptions = so0.copy( val soptions = so0.copy(
functionsToIgnore = so0.functionsToIgnore + fd, functionsToIgnore = so0.functionsToIgnore + fd,
costModel = RepairCostModel(so0.costModel), rules = Seq(Focus, CEGLESS) ++ so0.rules
rules = (so0.rules ++ Seq(
Focus,
CEGLESS
//TEGLESS
)) diff Seq(ADTInduction, TEGIS, IntegerInequalities, IntegerEquation)
) )
new Synthesizer(ctx, program, ci, soptions) new Synthesizer(ctx, program, ci, soptions)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment