diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala index b9adc1fbee214f8962f223b30bf4d77aa721e048..8afdf96bfe53ac1dfc97f198f85f9d24e53e320d 100644 --- a/src/main/scala/leon/synthesis/Heuristics.scala +++ b/src/main/scala/leon/synthesis/Heuristics.scala @@ -97,9 +97,9 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) val postCondGT = substAll(postXsMap + (origId -> Minus(Variable(inductOn), IntLiteral(1))), p.phi) val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi) - val subBase = Problem(List(), subst(origId -> IntLiteral(0), p.phi), p.xs) - val subGT = Problem(inductOn :: postXs, And(Seq(newPhi, GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT)), p.xs) - val subLT = Problem(inductOn :: postXs, And(Seq(newPhi, LessThan(Variable(inductOn), IntLiteral(0)), postCondLT)), p.xs) + val subBase = Problem(List(), p.c, subst(origId -> IntLiteral(0), p.phi), p.xs) + val subGT = Problem(inductOn :: postXs, p.c, And(Seq(newPhi, GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT)), p.xs) + val subLT = Problem(inductOn :: postXs, p.c, And(Seq(newPhi, LessThan(Variable(inductOn), IntLiteral(0)), postCondLT)), p.xs) val onSuccess: List[Solution] => Solution = { case List(base, gt, lt) => diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala index 6ff18ecde43ec9367f2be3b3c174eccb028595d9..e34db5cdfe86fe3a41faeb584abf5e0378147f61 100644 --- a/src/main/scala/leon/synthesis/Problem.scala +++ b/src/main/scala/leon/synthesis/Problem.scala @@ -5,9 +5,9 @@ import leon.purescala.Trees._ import leon.purescala.Common._ // Defines a synthesis triple of the form: -// ⟦ as ⟨ phi ⟩ xs ⟧ -case class Problem(as: List[Identifier], phi: Expr, xs: List[Identifier]) { - override def toString = "⟦ "+as.mkString(";")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ " +// ⟦ as ⟨ C | phi ⟩ xs ⟧ +case class Problem(as: List[Identifier], c: Expr, phi: Expr, xs: List[Identifier]) { + override def toString = "⟦ "+as.mkString(";")+" ⟨ "+c+" | "+phi+" ⟩ "+xs.mkString(";")+" ⟧ " val complexity: ProblemComplexity = ProblemComplexity(this) } diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala index bef01caf45d2617bd2a03bbca994c7b41e20aa4f..071cad7f9e13457eaffa0712e768ddd8b4495a4b 100644 --- a/src/main/scala/leon/synthesis/Rules.scala +++ b/src/main/scala/leon/synthesis/Rules.scala @@ -62,7 +62,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) { val others = exprs.filter(_ != eq) val oxs = p.xs.filter(_ != x) - val newProblem = Problem(p.as, subst(x -> e, And(others)), oxs) + val newProblem = Problem(p.as, p.c, subst(x -> e, And(others)), oxs) val onSuccess: List[Solution] => Solution = { case List(Solution(pre, term)) => @@ -108,8 +108,8 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) { val p = task.problem p.phi match { case Or(Seq(o1, o2)) => - val sub1 = Problem(p.as, o1, p.xs) - val sub2 = Problem(p.as, o2, p.xs) + val sub1 = Problem(p.as, p.c, o1, p.xs) + val sub2 = Problem(p.as, p.c, o2, p.xs) val onSuccess: List[Solution] => Solution = { case List(Solution(p1, t1), Solution(p2, t2)) => Solution(Or(p1, p2), IfExpr(p1, t1, t2)) @@ -183,7 +183,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy val sub = p.copy(xs = p.xs.filterNot(unconstr)) val onSuccess: List[Solution] => Solution = { - case List(s) => + case List(s) => Solution(s.pre, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(Variable(id)) else Variable(id))))) case _ => Solution.none diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index b493a50ded11a0130fb364c9a34a5b3777e94475..983b4ec6ff88707966e8fb450643012007833892 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -88,7 +88,7 @@ class Synthesizer(val r: Reporter, val as = (variablesOf(pred)--xs).toList val phi = pred - val sol = synthesize(Problem(as, phi, xs), rules) + val sol = synthesize(Problem(as, BooleanLiteral(true), phi, xs), rules) solutions = (ch -> sol) :: solutions