package leon package synthesis import purescala.Trees._ import heuristics._ object Heuristics { def all = Set[Synthesizer => Rule]( new IntInduction(_) //new OptimisticInjection(_), //new SelectiveInlining(_), // new ADTInduction(_) ) } trait Heuristic { this: Rule => override def toString = "H: "+name } object HeuristicStep { def verifyPre(synth: Synthesizer, problem: Problem)(s: Solution): (Solution, Boolean) = { synth.solver.solveSAT(And(Not(s.pre), problem.phi)) match { case (Some(true), model) => synth.reporter.warning("Heuristic failed to produce weakest precondition:") synth.reporter.warning(" - problem: "+problem) synth.reporter.warning(" - precondition: "+s.pre) (s, false) case _ => (s, true) } } def apply(synth: Synthesizer, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = { RuleMultiSteps(subProblems, Nil, onSuccess.andThen(verifyPre(synth, problem))) } } object HeuristicOneStep { def apply(synth: Synthesizer, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = { RuleAlternatives(Set(HeuristicStep(synth, problem, subProblems, onSuccess))) } }