diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index 39b0a77005e7e50ac290bda0b1eb094191fa1805..dcad10769bab3a9101e9ee4fb215cdd225acdcb4 100644 --- a/src/main/scala/leon/purescala/TreeOps.scala +++ b/src/main/scala/leon/purescala/TreeOps.scala @@ -1303,8 +1303,13 @@ object TreeOps { rec(expr, Nil) } - def valuateWithModel(expr: Expr, vars: Set[Identifier], model: Map[Identifier, Expr]) = { - replace(vars.map(id => Variable(id) -> model.getOrElse(id, simplestValue(id.getType))).toMap, expr) + def valuateWithModel(model: Map[Identifier, Expr])(id: Identifier): Expr = { + model.getOrElse(id, simplestValue(id.getType)) + } + + def valuateWithModelIn(expr: Expr, vars: Set[Identifier], model: Map[Identifier, Expr]): Expr = { + val valuator = valuateWithModel(model) _ + replace(vars.map(id => Variable(id) -> valuator(id)).toMap, expr) } } diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala index 2bcdc96d3dc908998a38d2ab5485c7c1df8012a2..ace65b430e334de3a80730e14a6e2eda3eb83c83 100644 --- a/src/main/scala/leon/synthesis/Rules.scala +++ b/src/main/scala/leon/synthesis/Rules.scala @@ -32,6 +32,7 @@ abstract class Rule(val name: String, val synth: Synthesizer, val priority: Prio def applyOn(task: Task): RuleResult def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in) + def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in) val forward: List[Solution] => Solution = { case List(s) => s @@ -90,7 +91,7 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) { synth.solveSAT(p.phi) match { case (Some(true), model) => - RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(id => model.getOrElse(id, simplestValue(Variable(id))))).setType(tpe))) + RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))) case (Some(false), model) => RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))) case _ => @@ -124,15 +125,15 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn case (Some(true), satModel) => val satXsModel = satModel.filterKeys(xss) - val newPhi = valuateWithModel(phi, xss, satModel) + val newPhi = valuateWithModelIn(phi, xss, satModel) synth.solveSAT(Not(newPhi)) match { case (Some(true), invalidModel) => // Found as such as the xs break, refine predicates - predicates = valuateWithModel(phi, ass, invalidModel) +: predicates + predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates case (Some(false), _) => - result = Some(RuleSuccess(Solution(BooleanLiteral(true), newPhi))) + result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe)))) case _ => result = Some(RuleInapplicable) @@ -330,3 +331,22 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) { } } } + +object Heuristics { + class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) { + def applyOn(task: Task): RuleResult = { + val p = task.problem + + p.as.find(_.getType == Int32Type) match { + case Some(inductOn) => + + val subBase = Problem(p.as.filterNot(_ == inductOn), subst(inductOn -> IntLiteral(0), p.phi), p.xs) + // val subGT = Problem(p.as + tmpGT, And(Seq(p.phi, GreaterThan(Variable(inductOn), IntLiteral(0)), subst(inductOn -> IntLiteral(0), p.phi), p.xs) + + RuleDecomposed(List(subBase), forward) + case None => + RuleInapplicable + } + } + } +}