package leon package synthesis import leon.purescala.Trees._ import leon.purescala.TreeOps._ // Defines a synthesis solution of the form: // ⟨ P | T ⟩ class Solution(val pre: Expr, val term: Expr) { override def toString = "⟨ "+pre+" | "+term+" ⟩" lazy val complexity: SolutionComplexity = new ConcreteSolutionComplexity(this) def toExpr = { if (pre == BooleanLiteral(true)) { term } else if (pre == BooleanLiteral(false)) { Error("Impossible program").setType(term.getType) } else { IfExpr(pre, term, Error("Precondition failed").setType(term.getType)) } } } object Solution { def choose(p: Problem): Solution = new Solution(BooleanLiteral(true), Choose(p.xs, p.phi)) def basic(p: Problem): Solution = new Solution(BooleanLiteral(true), Tuple(p.xs.map(id => simplestValue(id.getType)))) def none: Solution = throw new Exception("Unexpected failure to construct solution") def simplify(e: Expr) = simplifyLets(e) def apply(pre: Expr, term: Expr) = { new Solution(simplify(pre), simplify(term)) } def unapply(s: Solution): Option[(Expr, Expr)] = if (s eq null) None else Some((s.pre, s.term)) }