diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala index 9dcd782a3323138e5bfe4c68822fba614e2065e7..9fe9fab5c3e8b3597d34f8730ddbf3cbf9db2415 100644 --- a/src/main/scala/leon/repair/Repairman.scala +++ b/src/main/scala/leon/repair/Repairman.scala @@ -4,15 +4,12 @@ package leon package repair import leon.datagen.GrammarDataGen -import purescala.Common._ import purescala.Definitions._ import purescala.Expressions._ import purescala.Extractors._ import purescala.ExprOps._ -import purescala.Types._ import purescala.DefOps._ import purescala.Constructors._ -import purescala.Extractors.unwrapTuple import evaluators._ import solvers._ @@ -101,7 +98,6 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou } reporter.ifDebug { printer => - import java.io.FileWriter import java.text.SimpleDateFormat import java.util.Date @@ -112,15 +108,15 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou case fd: FunDef => 1 + fd.params.size + formulaSize(fd.fullBody) } - val pSize = defs.sum; + val pSize = defs.sum val fSize = formulaSize(fd.body.get) def localizedExprs(n: graph.Node): List[Expr] = { n match { case on: graph.OrNode => - on.selected.map(localizedExprs).flatten + on.selected.flatMap(localizedExprs) case an: graph.AndNode if an.ri.rule == Focus => - an.selected.map(localizedExprs).flatten + an.selected.flatMap(localizedExprs) case an: graph.AndNode => val TopLevelAnds(clauses) = an.p.ws @@ -132,7 +128,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou } } - val locSize = localizedExprs(search.g.root).map(formulaSize).sum; + val locSize = localizedExprs(search.g.root).map(formulaSize).sum val (solSize, proof) = solutions.headOption match { case Some((sol, trusted)) => @@ -187,13 +183,9 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou val guide = Guide(origBody) val pre = fd.precOrTrue - val ci = SourceInfo( - fd = fd, - pc = andJoin(Seq(pre, guide, term)), - source = origBody, - spec = fd.postOrTrue, - eb = eb - ) + val prob = Problem.fromSpec(fd.postOrTrue, andJoin(Seq(pre, guide, term)), eb, Some(fd)) + + val ci = SourceInfo(fd, origBody, prob) // Return synthesizer for this choose val so0 = SynthesisPhase.processOptions(ctx) diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala index 9aacbb0a21f0a3f7123cd56a44d00e97e5cc2315..a842e0c0e61338f1c3a11fd6adacb6c94d402d17 100644 --- a/src/main/scala/leon/synthesis/Problem.scala +++ b/src/main/scala/leon/synthesis/Problem.scala @@ -3,12 +3,13 @@ package leon package synthesis -import leon.purescala.Expressions._ -import leon.purescala.ExprOps._ -import leon.purescala.Types._ -import leon.purescala.Common._ -import leon.purescala.Constructors._ -import leon.purescala.Extractors._ +import purescala.Expressions._ +import purescala.ExprOps._ +import purescala.Types._ +import purescala.Common._ +import purescala.Constructors._ +import purescala.Extractors._ +import purescala.Definitions.FunDef import Witnesses._ /** Defines a synthesis triple of the form: @@ -30,19 +31,25 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List val ebInfo = "/"+eb.valids.size+","+eb.invalids.size+"/" - s"""|⟦ ${if (as.nonEmpty) as.map(_.asString).mkString(", ") else "<No input variables>"} + s"""|⟦ ${if (as.nonEmpty) as.map(_.asString).mkString(", ") else "()"} | ${pcws.asString} ≺ | ⟨ ${phi.asString} ⟩ - | ${xs.map(_.asString).mkString(";")} + | ${if (xs.nonEmpty) xs.map(_.asString).mkString(", ") else "()"} |⟧ """.stripMargin + ebInfo } // Qualified example bank, allows us to perform operations (e.g. filter) with expressions def qeb(implicit sctx: SearchContext) = QualifiedExamplesBank(this.as, this.xs, eb) + } object Problem { - def fromSpec(spec: Expr, pc: Expr = BooleanLiteral(true), eb: ExamplesBank = ExamplesBank.empty): Problem = { + def fromSpec( + spec: Expr, + pc: Expr = BooleanLiteral(true), + eb: ExamplesBank = ExamplesBank.empty, + fd: Option[FunDef] = None + ): Problem = { val xs = { val tps = spec.getType.asInstanceOf[FunctionType].from tps map (FreshIdentifier("x", _, alwaysShowUniqueID = true)) @@ -51,6 +58,13 @@ object Problem { val phi = application(simplifyLets(spec), xs map { _.toVariable}) val as = (variablesOf(And(pc, phi)) -- xs).toList.sortBy(_.name) + val sortedAs = fd match { + case None => as + case Some(fd) => + val argsIndex = fd.params.map(_.id).zipWithIndex.toMap.withDefaultValue(100) + as.sortBy(a => argsIndex(a)) + } + val TopLevelAnds(clauses) = pc val (pcs, wss) = clauses.partition { @@ -58,15 +72,7 @@ object Problem { case _ => true } - Problem(as, andJoin(wss), andJoin(pcs), phi, xs, eb) + Problem(sortedAs, andJoin(wss), andJoin(pcs), phi, xs, eb) } - def fromSourceInfo(ci: SourceInfo): Problem = { - // Same as fromChoose, but we order the input variables by the arguments of - // the functions, so that tests are compatible - val p = fromSpec(ci.spec, ci.pc, ci.eb) - val argsIndex = ci.fd.params.map(_.id).zipWithIndex.toMap.withDefaultValue(100) - - p.copy( as = p.as.sortBy(a => argsIndex(a))) - } } diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala index 8ab07929d78479656f18ce1fd652cfa7ef870e17..af78f227531217a1fbd3411130ecf4243df80add 100644 --- a/src/main/scala/leon/synthesis/SourceInfo.scala +++ b/src/main/scala/leon/synthesis/SourceInfo.scala @@ -9,14 +9,7 @@ import purescala.Expressions._ import purescala.ExprOps._ import Witnesses._ -case class SourceInfo(fd: FunDef, - pc: Expr, - source: Expr, - spec: Expr, - eb: ExamplesBank) { - - val problem = Problem.fromSourceInfo(this) -} +case class SourceInfo(fd: FunDef, source: Expr, problem: Problem) object SourceInfo { @@ -68,12 +61,15 @@ object SourceInfo { ExamplesBank.empty } - val ci = SourceInfo(fd, and(path, term), ch, ch.pred, outerEb) + val p = Problem.fromSpec(ch.pred, and(path, term), outerEb, Some(fd)) + + val pcEb = eFinder.generateForPC(p.as, path, 20) + val chooseEb = eFinder.extractFromProblem(p) + val eb = (outerEb union chooseEb) union pcEb - val pcEb = eFinder.generateForPC(ci.problem.as, path, 20) - val chooseEb = eFinder.extractFromProblem(ci.problem) + val betterP = p.copy(eb = eb) - ci.copy(eb = (outerEb union chooseEb) union pcEb) + SourceInfo(fd, ch, betterP) } } }