From b043306917e71eee0be7286b79d610560b65353d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 18 Feb 2016 16:45:35 +0100
Subject: [PATCH] Refactor the various contexts
---
src/main/scala/leon/LeonContext.scala | 9 +-
src/main/scala/leon/genc/CConverter.scala | 2 +-
.../leon/purescala/SelfPrettyPrinter.scala | 44 +++++----
src/main/scala/leon/repair/rules/Focus.scala | 7 +-
.../scala/leon/synthesis/ExamplesBank.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 2 -
src/main/scala/leon/synthesis/Search.scala | 6 +-
.../scala/leon/synthesis/SearchContext.scala | 17 ++--
.../leon/synthesis/SynthesisContext.scala | 22 +++--
.../scala/leon/synthesis/graph/Graph.scala | 17 ++--
.../leon/synthesis/rules/ADTInduction.scala | 2 +-
.../synthesis/rules/ADTLongInduction.scala | 2 +-
.../leon/synthesis/rules/BottomUpTegis.scala | 12 +--
.../leon/synthesis/rules/CEGISLike.scala | 95 +++++++++----------
.../scala/leon/synthesis/rules/CEGLESS.scala | 4 +-
.../synthesis/rules/EquivalentInputs.scala | 2 +-
.../scala/leon/synthesis/rules/Ground.scala | 2 +-
.../synthesis/rules/IntegerEquation.scala | 2 +-
.../synthesis/rules/IntroduceRecCall.scala | 10 +-
.../synthesis/rules/OptimisticGround.scala | 2 +-
.../leon/synthesis/rules/StringRender.scala | 78 ++++++++-------
.../leon/synthesis/rules/SygusCVC4.scala | 4 +-
.../leon/synthesis/rules/TEGISLike.scala | 19 ++--
.../solvers/StringRenderSuite.scala | 55 +++--------
.../leon/regression/repair/RepairSuite.scala | 2 +-
.../synthesis/StablePrintingSuite.scala | 4 +-
26 files changed, 193 insertions(+), 230 deletions(-)
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index ca3fdd676..000e785b0 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -9,7 +9,7 @@ import java.io.File
import scala.reflect.ClassTag
/** Everything that is part of a compilation unit, except the actual program tree.
- * Contexts are immutable, and so should all their fields (with the possible
+ * LeonContexts are immutable, and so should all their fields (with the possible
* exception of the reporter).
*/
case class LeonContext(
@@ -36,8 +36,11 @@ object LeonContext {
}
def printNames = {
- empty.copy(options =
- Seq(LeonOption[Set[DebugSection]](SharedOptions.optDebug)(Set(DebugSectionTrees)))
+ val reporter = new DefaultReporter(Set())
+ LeonContext(
+ reporter,
+ new InterruptManager(reporter),
+ options = Seq(LeonOption[Set[DebugSection]](SharedOptions.optDebug)(Set(DebugSectionTrees)))
)
}
}
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index a979fd8dd..e7795adbe 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -156,7 +156,7 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
val extraParams = funCtx.toParams
val params = extraParams ++ stdParams
- // Function Context:
+ // Function LeonContext:
// 1) Save the variables of the current context for later function invocation
// 2) Lift & augment funCtx with the current function's arguments
// 3) Propagate it to the current function's body
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index d1cc5f86c..e34b0a4a3 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -34,8 +34,7 @@ object SelfPrettyPrinter {
/** This pretty-printer uses functions defined in Leon itself.
* If not pretty printing function is defined, return the default value instead
- * @param The list of functions which should be excluded from pretty-printing (to avoid rendering counter-examples of toString methods using the method itself)
- * @return a user defined string for the given typed expression. */
+ */
class SelfPrettyPrinter {
implicit val section = leon.utils.DebugSectionEvaluation
private var allowedFunctions = Set[FunDef]()
@@ -49,16 +48,18 @@ class SelfPrettyPrinter {
/** Returns a list of possible lambdas that can transform the input type to a String.
* At this point, it does not consider yet the inputType. Only [[prettyPrinterFromCandidate]] will consider it. */
def prettyPrintersForType(inputType: TypeTree/*, existingPp: Map[TypeTree, List[Lambda]] = Map()*/)(implicit ctx: LeonContext, program: Program): Stream[Lambda] = {
- program.definedFunctions.toStream flatMap {
- fd =>
- val isCandidate = fd.returnType == StringType &&
- fd.params.length >= 1 &&
+ program.definedFunctions.toStream flatMap { fd =>
+ val isCandidate =
+ fd.returnType == StringType &&
+ fd.params.nonEmpty &&
!excluded(fd) &&
- (allowedFunctions(fd) || (
- fd.id.name.toLowerCase().endsWith("tostring")))
- if(isCandidate) {
- prettyPrinterFromCandidate(fd, inputType)
- } else Stream.Empty
+ (allowedFunctions(fd) || fd.id.name.toLowerCase().endsWith("tostring"))
+
+ if(isCandidate) {
+ prettyPrinterFromCandidate(fd, inputType)
+ } else {
+ Stream.Empty
+ }
}
}
@@ -88,19 +89,24 @@ class SelfPrettyPrinter {
case None => Stream.empty
}
}
-
-
- /** Actually prints the expression with as alternative the given orElse */
+
+
+ /** Actually prints the expression with as alternative the given orElse
+ * @param excluded The list of functions which should be excluded from pretty-printing
+ * (to avoid rendering counter-examples of toString methods using the method itself)
+ * @return a user defined string for the given typed expression.
+ **/
def print(v: Expr, orElse: =>String, excluded: Set[FunDef] = Set())(implicit ctx: LeonContext, program: Program): String = {
this.excluded = excluded
val s = prettyPrintersForType(v.getType) // TODO: Included the variable excluded if necessary.
- s.take(100).find(l => l match { // Limit the number of pretty-printers.
+ s.take(100).find {
+ // Limit the number of pretty-printers.
case Lambda(_, FunctionInvocation(TypedFunDef(fd, _), _)) =>
- (program.callGraph.transitiveCallees(fd) + fd).forall { fde =>
- !ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
- }
+ (program.callGraph.transitiveCallees(fd) + fd).forall { fde =>
+ !ExprOps.exists(_.isInstanceOf[Choose])(fde.fullBody)
+ }
case _ => false
- }) match {
+ } match {
case None => orElse
case Some(l) =>
ctx.reporter.debug("Executing pretty printer for type " + v.getType + " : " + l + " on " + v)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 93520c5ea..b625ab7d3 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -32,10 +32,9 @@ case object Focus extends PreprocessingRule("Focus") {
}
val fd = hctx.ci.fd
- val ctx = hctx.sctx.context
- val program = hctx.sctx.program
+ val program = hctx.program
- val evaluator = new DefaultEvaluator(ctx, program)
+ val evaluator = new DefaultEvaluator(hctx, program)
// Check how an expression behaves on tests
// - returns Some(true) if for all tests e evaluates to true
@@ -97,7 +96,7 @@ case object Focus extends PreprocessingRule("Focus") {
case c if c eq cond => Some(not(cond))
case _ => None
}(fdSpec)
- forAllTests(ndSpec, Map(), new AngelicEvaluator(new RepairNDEvaluator(ctx, program, cond)))
+ forAllTests(ndSpec, Map(), new AngelicEvaluator(new RepairNDEvaluator(hctx, program, cond)))
}
guides.flatMap {
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 265b35a5e..89e018b5e 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -177,7 +177,7 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
/** Filter inputs throught expr which is an expression evaluating to a boolean */
def filterIns(expr: Expr): ExamplesBank = {
- filterIns(m => hctx.sctx.defaultEvaluator.eval(expr, m).result == Some(BooleanLiteral(true)))
+ filterIns(m => hctx.defaultEvaluator.eval(expr, m).result == Some(BooleanLiteral(true)))
}
/** Filters inputs through the predicate pred, with an assignment of input variables to expressions. */
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 1e3cb8717..abbe45fb2 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -20,8 +20,6 @@ abstract class Rule(val name: String) extends RuleDSL {
implicit val thisRule = this
- implicit def hctxToCtx(implicit hctx: SearchContext): LeonContext = hctx.sctx.context
-
def asString(implicit ctx: LeonContext) = name
}
diff --git a/src/main/scala/leon/synthesis/Search.scala b/src/main/scala/leon/synthesis/Search.scala
index 4700d7e33..cb7ecf048 100644
--- a/src/main/scala/leon/synthesis/Search.scala
+++ b/src/main/scala/leon/synthesis/Search.scala
@@ -23,12 +23,12 @@ class Search(val ctx: LeonContext, ci: SourceInfo, p: Problem, val strat: Strate
ctx.timers.synthesis.step.timed {
n match {
case an: AndNode =>
- ctx.timers.synthesis.applications.get(an.ri.asString(sctx.context)).timed {
- an.expand(SearchContext(sctx, ci, an, this))
+ ctx.timers.synthesis.applications.get(an.ri.asString(sctx)).timed {
+ an.expand(new SearchContext(sctx, ci, an, this))
}
case on: OrNode =>
- on.expand(SearchContext(sctx, ci, on, this))
+ on.expand(new SearchContext(sctx, ci, on, this))
}
}
}
diff --git a/src/main/scala/leon/synthesis/SearchContext.scala b/src/main/scala/leon/synthesis/SearchContext.scala
index 1ee7361d5..c782f35ed 100644
--- a/src/main/scala/leon/synthesis/SearchContext.scala
+++ b/src/main/scala/leon/synthesis/SearchContext.scala
@@ -9,15 +9,17 @@ import graph._
* This is context passed down rules, and include search-wise context, as well
* as current search location information
*/
-case class SearchContext (
+class SearchContext (
sctx: SynthesisContext,
- ci: SourceInfo,
- currentNode: Node,
- search: Search
+ val ci: SourceInfo,
+ val currentNode: Node,
+ val search: Search
+) extends SynthesisContext(
+ sctx,
+ sctx.settings,
+ sctx.functionContext,
+ sctx.program
) {
- val context = sctx.context
- val reporter = sctx.reporter
- val program = sctx.program
def searchDepth = {
def depthOf(n: Node): Int = n.parent match {
@@ -29,4 +31,5 @@ case class SearchContext (
}
def parentNode: Option[Node] = currentNode.parent
+
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 5b2a9a9f1..1d0a6b5e9 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -10,28 +10,32 @@ import evaluators._
/**
* This is global information per entire search, contains necessary information
*/
-case class SynthesisContext(
+class SynthesisContext(
context: LeonContext,
- settings: SynthesisSettings,
- functionContext: FunDef,
- program: Program
+ val settings: SynthesisSettings,
+ val functionContext: FunDef,
+ val program: Program
+) extends LeonContext(
+ context.reporter,
+ context.interruptManager,
+ context.options,
+ context.files,
+ context.classDir,
+ context.timers
) {
- val reporter = context.reporter
-
- val rules = settings.rules
-
val solverFactory = SolverFactory.getFromSettings(context, program)
lazy val defaultEvaluator = {
new DefaultEvaluator(context, program)
}
+
}
object SynthesisContext {
def fromSynthesizer(synth: Synthesizer) = {
- SynthesisContext(
+ new SynthesisContext(
synth.context,
synth.settings,
synth.ci.fd,
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 295f7b4c9..3bb9fbff9 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -35,7 +35,7 @@ sealed abstract class Node(val parent: Option[Node]) {
// indicates whether this particular node has already been expanded
var isExpanded: Boolean = false
- def expand(hctx: SearchContext)
+ def expand(implicit hctx: SearchContext)
val p: Problem
@@ -64,7 +64,6 @@ sealed abstract class Node(val parent: Option[Node]) {
}
/** Represents the conjunction of search nodes.
- * @param cm The cost model used when prioritizing, evaluating and expanding
* @param parent Some node. None if it is the root node.
* @param ri The rule instantiation that created this AndNode.
**/
@@ -73,7 +72,7 @@ class AndNode(parent: Option[Node], val ri: RuleInstantiation) extends Node(pare
override def asString(implicit ctx: LeonContext) = "\u2227 "+ri.asString
- def expand(hctx: SearchContext): Unit = {
+ def expand(implicit hctx: SearchContext): Unit = {
require(!isExpanded)
isExpanded = true
@@ -83,9 +82,7 @@ class AndNode(parent: Option[Node], val ri: RuleInstantiation) extends Node(pare
prefix + lines.head + "\n" + lines.tail.map(padding + _).mkString("\n")
}
- implicit val ctx = hctx.sctx.context
-
- import hctx.sctx.reporter.info
+ import hctx.reporter.info
val prefix = f"[${Option(ri.rule).getOrElse("?")}%-20s] "
@@ -158,15 +155,15 @@ class OrNode(parent: Option[Node], val p: Problem) extends Node(parent) {
implicit val debugSection = DebugSectionSynthesis
def getInstantiations(hctx: SearchContext): List[RuleInstantiation] = {
- val rules = hctx.sctx.rules
+ val rules = hctx.settings.rules
val rulesPrio = rules.groupBy(_.priority).toSeq.sortBy(_._1)
for ((prio, rs) <- rulesPrio) {
val results = rs.flatMap{ r =>
- hctx.context.reporter.ifDebug(printer => printer("Testing rule: " + r))
- hctx.context.timers.synthesis.instantiations.get(r.asString(hctx.sctx.context)).timed {
+ hctx.reporter.ifDebug(printer => printer("Testing rule: " + r))
+ hctx.timers.synthesis.instantiations.get(r.asString(hctx)).timed {
r.instantiateOn(hctx, p)
}
}.toList
@@ -181,7 +178,7 @@ class OrNode(parent: Option[Node], val p: Problem) extends Node(parent) {
Nil
}
- def expand(hctx: SearchContext): Unit = {
+ def expand(implicit hctx: SearchContext): Unit = {
require(!isExpanded)
val ris = getInstantiations(hctx)
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 9787811b7..2c0bd4439 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -17,7 +17,7 @@ case object ADTInduction extends Rule("ADT Induction") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
/* All input variables which are inductive in the post condition, along with their abstract data type. */
val candidates = p.as.collect {
- case IsTyped(origId, act: AbstractClassType) if isInductiveOn(hctx.sctx.solverFactory)(p.pc, origId) => (origId, act)
+ case IsTyped(origId, act: AbstractClassType) if isInductiveOn(hctx.solverFactory)(p.pc, origId) => (origId, act)
}
val instances = for (candidate <- candidates) yield {
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 66b27a66a..3d031db44 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -15,7 +15,7 @@ import purescala.Definitions._
case object ADTLongInduction extends Rule("ADT Long Induction") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
val candidates = p.as.collect {
- case IsTyped(origId, act @ AbstractClassType(cd, tpe)) if isInductiveOn(hctx.sctx.solverFactory)(p.pc, origId) => (origId, act)
+ case IsTyped(origId, act @ AbstractClassType(cd, tpe)) if isInductiveOn(hctx.solverFactory)(p.pc, origId) => (origId, act)
}
val instances = for (candidate <- candidates) yield {
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 4c12f5822..2f4eee0d6 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -37,16 +37,13 @@ abstract class BottomUpTEGISLike[T <: Typed](name: String) extends Rule(name) {
if (tests.nonEmpty) {
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
- val sctx = hctx.sctx
-
- implicit val ctx = sctx.context
val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
//val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
//val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
- val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams)
+ val evaluator = new DualEvaluator(hctx, hctx.program, evalParams)
- val grammar = getGrammar(sctx, p)
+ val grammar = getGrammar(hctx, p)
val nTests = tests.size
@@ -108,7 +105,7 @@ abstract class BottomUpTEGISLike[T <: Typed](name: String) extends Rule(name) {
val wrappedTests = tests.map { case (is, os) => (is, tupleWrap(os))}
val enum = new BottomUpEnumerator[T, Expr, Expr, ProductionRule[T, Expr]](
- grammar.getProductions,
+ grammar.getProductions(_)(hctx),
wrappedTests,
{ (vecs, gen) =>
compile(gen)(vecs)
@@ -116,9 +113,6 @@ abstract class BottomUpTEGISLike[T <: Typed](name: String) extends Rule(name) {
3
)
-
- val timers = sctx.context.timers.synthesis.rules.tegis
-
val matches = enum.iterator(getRootLabel(targetType))
if (matches.hasNext) {
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index e51a3c30e..b0052a372 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -42,24 +42,21 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
// Track non-deterministic programs up to 100'000 programs, or give up
val nProgramsLimit = 100000
- val sctx = hctx.sctx
- val ctx = sctx.context
-
- val timers = ctx.timers.synthesis.cegis
+ val timers = hctx.timers.synthesis.cegis
// CEGIS Flags to activate or deactivate features
- val useOptTimeout = sctx.settings.cegisUseOptTimeout
- val useVanuatoo = sctx.settings.cegisUseVanuatoo
+ val useOptTimeout = hctx.settings.cegisUseOptTimeout
+ val useVanuatoo = hctx.settings.cegisUseVanuatoo
// The factor by which programs need to be reduced by testing before we validate them individually
val testReductionRatio = 10
- val interruptManager = sctx.context.interruptManager
+ val interruptManager = hctx.interruptManager
- val params = getParams(sctx, p)
+ val params = getParams(hctx, p)
// If this CEGISLike forces a maxSize, take it, otherwise find it in the settings
- val maxSize = params.maxSize.getOrElse(sctx.settings.cegisMaxSize)
+ val maxSize = params.maxSize.getOrElse(hctx.settings.cegisMaxSize)
if (maxSize == 0) {
return Nil
@@ -141,7 +138,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
// Update the c-tree after an increase in termsize
def updateCTree(): Unit = {
- ctx.timers.synthesis.cegis.updateCTree.start()
+ hctx.timers.synthesis.cegis.updateCTree.start()
def freshB() = {
val id = FreshIdentifier("B", BooleanType, true)
bs += id
@@ -183,7 +180,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
c
}
- sctx.reporter.ifDebug { printer =>
+ hctx.reporter.ifDebug { printer =>
printer("Grammar so far:")
grammar.printProductions(printer)
printer("")
@@ -195,7 +192,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
excludedPrograms = Set()
prunedPrograms = allPrograms().toSet
- ctx.timers.synthesis.cegis.updateCTree.stop()
+ hctx.timers.synthesis.cegis.updateCTree.stop()
}
// Returns a count of all possible programs
@@ -223,7 +220,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val allCount = allProgramsCount()
if (allCount > nProgramsLimit) {
- ctx.reporter.debug(s"Exceeded program limit: $allCount > $nProgramsLimit")
+ hctx.reporter.debug(s"Exceeded program limit: $allCount > $nProgramsLimit")
return Seq()
}
@@ -284,10 +281,10 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val outerSolution = {
new PartialSolution(hctx.search.strat, true)
.solutionAround(hctx.currentNode)(FunctionInvocation(solFd.typed, p.as.map(_.toVariable)))
- .getOrElse(ctx.reporter.fatalError("Unable to get outer solution"))
+ .getOrElse(hctx.reporter.fatalError("Unable to get outer solution"))
}
- val program0 = addFunDefs(sctx.program, Seq(cTreeFd, solFd, phiFd) ++ outerSolution.defs, hctx.ci.fd)
+ val program0 = addFunDefs(hctx.program, Seq(cTreeFd, solFd, phiFd) ++ outerSolution.defs, hctx.ci.fd)
cTreeFd.body = None
@@ -396,7 +393,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
cTreeFd.body = Some(cExpr)
programCTree = addFunDefs(innerProgram, newFds, cTreeFd)
- evaluator = new DefaultEvaluator(sctx.context, programCTree)
+ evaluator = new DefaultEvaluator(hctx, programCTree)
//println("-- "*30)
//println(programCTree.asString)
@@ -482,11 +479,11 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
println(err)
println()
}*/
- sctx.reporter.debug("RE testing CE: "+err)
+ hctx.reporter.debug("RE testing CE: "+err)
false
case EvaluationResults.EvaluatorError(err) =>
- sctx.reporter.debug("Error testing CE: "+err)
+ hctx.reporter.debug("Error testing CE: "+err)
false
}
@@ -525,7 +522,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val cnstr = and(innerPc, letTuple(p.xs, innerSol, Not(innerPhi)))
- val eval = new DefaultEvaluator(ctx, innerProgram)
+ val eval = new DefaultEvaluator(hctx, innerProgram)
if (cexs exists (cex => eval.eval(cnstr, p.as.zip(cex).toMap).result == Some(BooleanLiteral(true)))) {
//println(s"Program $outerSol fails!")
@@ -534,7 +531,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
} else {
//println("Solving for: "+cnstr.asString)
- val solverf = SolverFactory.getFromSettings(ctx, innerProgram).withTimeout(cexSolverTo)
+ val solverf = SolverFactory.getFromSettings(hctx, innerProgram).withTimeout(cexSolverTo)
val solver = solverf.getNewSolver()
try {
solver.assertCnstr(cnstr)
@@ -559,7 +556,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
case None =>
if (useOptTimeout) {
// Interpret timeout in CE search as "the candidate is valid"
- sctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
+ hctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
// Optimistic valid solution
return Right(Solution(BooleanLiteral(true), Set(), outerSol, false))
}
@@ -608,7 +605,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
* First phase of CEGIS: discover potential programs (that work on at least one input)
*/
def solveForTentativeProgram(): Option[Option[Set[Identifier]]] = {
- val solverf = SolverFactory.getFromSettings(ctx, programCTree).withTimeout(exSolverTo)
+ val solverf = SolverFactory.getFromSettings(hctx, programCTree).withTimeout(exSolverTo)
val solver = solverf.getNewSolver()
val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
@@ -670,7 +667,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
* might timeout instead of returning Some(false). We might still
* benefit from unfolding further
*/
- ctx.reporter.debug("Timeout while getting tentative program!")
+ hctx.reporter.debug("Timeout while getting tentative program!")
Some(None)
}
} finally {
@@ -683,7 +680,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
* Second phase of CEGIS: verify a given program by looking for CEX inputs
*/
def solveForCounterExample(bs: Set[Identifier]): Option[Option[Seq[Expr]]] = {
- val solverf = SolverFactory.getFromSettings(ctx, programCTree).withTimeout(cexSolverTo)
+ val solverf = SolverFactory.getFromSettings(hctx, programCTree).withTimeout(cexSolverTo)
val solver = solverf.getNewSolver()
val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
@@ -724,19 +721,19 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
var result: Option[RuleApplication] = None
- val sctx = hctx.sctx
- implicit val ctx = sctx.context
val ndProgram = NonDeterministicProgram
ndProgram.init()
- sctx.reporter.debug("Acquiring initial list of examples")
+ implicit val ic = hctx
+
+ hctx.reporter.debug("Acquiring initial list of examples")
// To the list of known examples, we add an additional one produced by the solver
val solverExample = if (p.pc == BooleanLiteral(true)) {
InExample(p.as.map(a => simplestValue(a.getType)))
} else {
- val solverf = sctx.solverFactory
+ val solverf = hctx.solverFactory
val solver = solverf.getNewSolver().setTimeout(exSolverTo)
solver.assertCnstr(p.pc)
@@ -748,12 +745,12 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
InExample(p.as.map(a => model.getOrElse(a, simplestValue(a.getType))))
case Some(false) =>
- sctx.reporter.debug("Path-condition seems UNSAT")
+ hctx.reporter.debug("Path-condition seems UNSAT")
return RuleFailed()
case None =>
if (!interruptManager.isInterrupted) {
- sctx.reporter.warning("Solver could not solve path-condition")
+ hctx.reporter.warning("Solver could not solve path-condition")
}
return RuleFailed() // This is not necessary though, but probably wanted
}
@@ -764,7 +761,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val baseExampleInputs = p.eb.examples :+ solverExample
- sctx.reporter.ifDebug { debug =>
+ hctx.reporter.ifDebug { debug =>
baseExampleInputs.foreach { in =>
debug(" - "+in.asString)
}
@@ -776,9 +773,9 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val nTests = if (p.pc == BooleanLiteral(true)) 50 else 20
val inputGenerator: Iterator[Example] = if (useVanuatoo) {
- new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000).map(InExample)
+ new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc, nTests, 3000).map(InExample)
} else {
- val evaluator = new DualEvaluator(sctx.context, sctx.program, CodeGenParams.default)
+ val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default)
new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc, nTests, 1000).map(InExample)
}
@@ -807,7 +804,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
ndProgram.unfold()
val nInitial = ndProgram.prunedPrograms.size
- sctx.reporter.debug("#Programs: "+nInitial)
+ hctx.reporter.debug("#Programs: "+nInitial)
//sctx.reporter.ifDebug{ printer =>
// val limit = 100
@@ -828,12 +825,12 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val examples = allInputExamples()
examples.find(e => !ndProgram.testForProgram(bs)(e)).foreach { e =>
failedTestsStats(e) += 1
- sctx.reporter.debug(f" Program: ${ndProgram.getExpr(bs).asString}%-80s failed on: ${e.asString}")
+ hctx.reporter.debug(f" Program: ${ndProgram.getExpr(bs).asString}%-80s failed on: ${e.asString}")
ndProgram.excludeProgram(bs, true)
}
if (ndProgram.excludedPrograms.size+1 % 1000 == 0) {
- sctx.reporter.debug("..."+ndProgram.excludedPrograms.size)
+ hctx.reporter.debug("..."+ndProgram.excludedPrograms.size)
}
}
timers.filter.stop()
@@ -841,8 +838,8 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
def nPassing = ndProgram.prunedPrograms.size
- sctx.reporter.debug(s"#Programs passing tests: $nPassing out of $nInitial")
- sctx.reporter.ifDebug{ printer =>
+ hctx.reporter.debug(s"#Programs passing tests: $nPassing out of $nInitial")
+ hctx.reporter.ifDebug{ printer =>
for (p <- ndProgram.prunedPrograms.take(100)) {
printer(" - "+ndProgram.getExpr(p).asString)
}
@@ -850,8 +847,8 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
printer(" - ...")
}
}
- sctx.reporter.debug("#Tests: "+baseExampleInputs.size)
- sctx.reporter.ifDebug{ printer =>
+ hctx.reporter.debug("#Tests: "+baseExampleInputs.size)
+ hctx.reporter.ifDebug{ printer =>
for (e <- baseExampleInputs.take(10)) {
printer(" - "+e.asString)
}
@@ -863,12 +860,12 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
// CEGIS Loop at a given unfolding level
while (result.isEmpty && !interruptManager.isInterrupted && !ndProgram.allProgramsClosed) {
timers.loop.start()
- ctx.reporter.debug("Programs left: " + ndProgram.prunedPrograms.size)
+ hctx.reporter.debug("Programs left: " + ndProgram.prunedPrograms.size)
// Phase 0: If the number of remaining programs is small, validate them individually
if (nInitial / nPassing > testReductionRatio || nPassing <= 10) {
val programsToValidate = ndProgram.prunedPrograms
- sctx.reporter.debug(s"Will send ${programsToValidate.size} program(s) to validate individually")
+ hctx.reporter.debug(s"Will send ${programsToValidate.size} program(s) to validate individually")
ndProgram.validatePrograms(programsToValidate) match {
case Right(sol) =>
// Found solution! Exit CEGIS
@@ -879,18 +876,18 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
val newCexs = cexs.map(InExample)
gi ++= newCexs
}
- ctx.reporter.debug(s"#Programs after validating individually: ${ndProgram.prunedPrograms.size}")
+ hctx.reporter.debug(s"#Programs after validating individually: ${ndProgram.prunedPrograms.size}")
}
if (result.isEmpty && !ndProgram.allProgramsClosed) {
// Phase 1: Find a candidate program that works for at least 1 input
ndProgram.solveForTentativeProgram() match {
case Some(Some(bs)) =>
- sctx.reporter.debug(s"Found tentative model ${ndProgram.getExpr(bs)}, need to validate!")
+ hctx.reporter.debug(s"Found tentative model ${ndProgram.getExpr(bs)}, need to validate!")
// Phase 2: Validate candidate model
ndProgram.solveForCounterExample(bs) match {
case Some(Some(inputsCE)) =>
- sctx.reporter.debug("Found counter-example:" + inputsCE)
+ hctx.reporter.debug("Found counter-example:" + inputsCE)
val ce = InExample(inputsCE)
// Found counterexample! Exclude this program
gi += ce
@@ -912,10 +909,10 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
case None =>
// We are not sure
- sctx.reporter.debug("Unknown")
+ hctx.reporter.debug("Unknown")
if (useOptTimeout) {
// Interpret timeout in CE search as "the candidate is valid"
- sctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
+ hctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
val expr = ndProgram.getExpr(bs)
result = Some(RuleClosed(Solution(BooleanLiteral(true), Set(), expr, isTrusted = false)))
} else {
@@ -927,7 +924,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
}
case Some(None) =>
- sctx.reporter.debug("There exists no candidate program!")
+ hctx.reporter.debug("There exists no candidate program!")
ndProgram.prunedPrograms foreach (ndProgram.excludeProgram(_, true))
case None =>
@@ -944,7 +941,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
} catch {
case e: Throwable =>
- sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
+ hctx.reporter.warning("CEGIS crashed: "+e.getMessage)
e.printStackTrace()
RuleFailed()
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index 36cc7f9e6..8f30f229f 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -15,8 +15,6 @@ case object CEGLESS extends CEGISLike[NonTerminal[String]]("CEGLESS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
val TopLevelAnds(clauses) = p.ws
- val ctx = sctx.context
-
val guides = clauses.collect {
case Guide(e) => e
}
@@ -26,7 +24,7 @@ case object CEGLESS extends CEGISLike[NonTerminal[String]]("CEGLESS") {
sctx.reporter.ifDebug { printer =>
printer("Guides available:")
for (g <- guides) {
- printer(" - "+g.asString(ctx))
+ printer(" - "+g.asString(sctx))
}
}
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 6b2f9e858..a4e01064c 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -73,7 +73,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
}
if (substs.nonEmpty) {
- val simplifier = Simplifiers.bestEffort(hctx.context, hctx.program) _
+ val simplifier = Simplifiers.bestEffort(hctx, hctx.program) _
val sub = p.copy(ws = replaceSeq(substs, p.ws),
pc = simplifier(andJoin(replaceSeq(substs, p.pc) +: postsToInject)),
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index a385bb126..e5eb75463 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -15,7 +15,7 @@ case object Ground extends NormalizingRule("Ground") {
if (p.as.isEmpty) {
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
- val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(10.seconds))
+ val solver = SimpleSolverAPI(hctx.solverFactory.withTimeout(10.seconds))
val result = solver.solveSAT(p.phi) match {
case (Some(true), model) =>
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 8aaa89ee1..a668f26fc 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -23,7 +23,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
var candidates: Seq[Expr] = eqs
var allOthers: Seq[Expr] = others
- val evaluator = new DefaultEvaluator(hctx.context, hctx.program)
+ val evaluator = new DefaultEvaluator(hctx, hctx.program)
var vars: Set[Identifier] = Set()
var eqxs: List[Identifier] = List()
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala
index c93846666..95892b4a0 100644
--- a/src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala
+++ b/src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala
@@ -25,7 +25,7 @@ case object IntroduceRecCall extends Rule("Introduce rec. calls") {
}
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val evaluator = new NoChooseEvaluator(hctxToCtx, hctx.program)
+ val evaluator = new NoChooseEvaluator(hctx, hctx.program)
val calls = terminatingCalls(hctx.program, p.ws, p.pc, None, false)
@@ -56,11 +56,11 @@ case object IntroduceRecCall extends Rule("Introduce rec. calls") {
val psol = new PartialSolution(hctx.search.strat, true)
.solutionAround(hctx.currentNode)(Error(p.outType, "Encountered choose!"))
- .getOrElse(hctx.sctx.context.reporter.fatalError("Unable to get outer solution"))
+ .getOrElse(hctx.reporter.fatalError("Unable to get outer solution"))
.term
- val origImpl = hctx.sctx.functionContext.fullBody
- hctx.sctx.functionContext.fullBody = psol
+ val origImpl = hctx.functionContext.fullBody
+ hctx.functionContext.fullBody = psol
def mapExample(e: Example): List[Example] = {
val res = evaluator.eval(newCall, p.as.zip(e.ins).toMap)
@@ -79,7 +79,7 @@ case object IntroduceRecCall extends Rule("Introduce rec. calls") {
eb = p.eb.map(mapExample)
)
- hctx.sctx.functionContext.fullBody = origImpl
+ hctx.functionContext.fullBody = origImpl
RuleExpanded(List(newProblem))
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 679e49e38..f99ae625a 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -18,7 +18,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
val res = new RuleInstantiation(this.name) {
def apply(hctx: SearchContext) = {
- val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
+ val solver = SimpleSolverAPI(hctx.solverFactory.withTimeout(50.millis))
val xss = p.xs.toSet
val ass = p.as.toSet
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 715d54385..1244dc6df 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -6,10 +6,8 @@ package rules
import scala.annotation.tailrec
import scala.collection.mutable.ListBuffer
-import bonsai.enumerators.MemoizedEnumerator
-import evaluators.DefaultEvaluator
import evaluators.AbstractEvaluator
-import purescala.Definitions.{FunDef, ValDef, Program, TypedFunDef, CaseClassDef, AbstractClassDef}
+import purescala.Definitions._
import purescala.Common._
import purescala.Types._
import purescala.Constructors._
@@ -19,14 +17,10 @@ import purescala.TypeOps
import purescala.DefOps
import purescala.ExprOps
import purescala.SelfPrettyPrinter
-import solvers.Model
import solvers.ModelBuilder
import solvers.string.StringSolver
-import synthesis.programsets.DirectProgramSet
-import synthesis.programsets.JoinProgramSet
-import leon.utils.DebugSectionSynthesis
-
-
+import programsets.DirectProgramSet
+import programsets.JoinProgramSet
/** A template generator for a given type tree.
@@ -148,7 +142,8 @@ case object StringRender extends Rule("StringRender") {
/** Returns a stream of assignments compatible with input/output examples for the given template */
def findAssignments(p: Program, inputs: Seq[Identifier], examples: ExamplesBank, template: Expr)(implicit hctx: SearchContext): Stream[Map[Identifier, String]] = {
- val e = new AbstractEvaluator(hctx.context, p)
+
+ val e = new AbstractEvaluator(hctx, p)
@tailrec def gatherEquations(s: List[InOutExample], acc: ListBuffer[Equation] = ListBuffer()): Option[SProblem] = s match {
case Nil => Some(acc.toList)
@@ -201,7 +196,7 @@ case object StringRender extends Rule("StringRender") {
def computeSolutions(funDefsBodies: Seq[(FunDef, WithIds[Expr])], template: WithIds[Expr]): Stream[Assignment] = {
val funDefs = for((funDef, body) <- funDefsBodies) yield { funDef.body = Some(body._1); funDef }
- val newProgram = DefOps.addFunDefs(hctx.program, funDefs, hctx.sctx.functionContext)
+ val newProgram = DefOps.addFunDefs(hctx.program, funDefs, hctx.functionContext)
findAssignments(newProgram, p.as.filter{ x => !x.getType.isInstanceOf[FunctionType] }, examples, template._1)
}
@@ -327,9 +322,9 @@ case object StringRender extends Rule("StringRender") {
/** Creates an empty function definition for the dependent type */
def createEmptyFunDef(ctx: StringSynthesisContext, tpe: DependentType)(implicit hctx: SearchContext): FunDef = {
def defaultFunName(t: TypeTree) = t match {
- case AbstractClassType(c, d) => c.id.asString(hctx.context)
- case CaseClassType(c, d) => c.id.asString(hctx.context)
- case t => t.asString(hctx.context)
+ case AbstractClassType(c, d) => c.id.asString(hctx)
+ case CaseClassType(c, d) => c.id.asString(hctx)
+ case t => t.asString(hctx)
}
val funName2 = tpe.caseClassParent match {
@@ -339,10 +334,9 @@ case object StringRender extends Rule("StringRender") {
val funName3 = funName2.replaceAll("[^a-zA-Z0-9_]","")
val funName = funName3(0).toLower + funName3.substring(1)
val funId = FreshIdentifier(ctx.freshFunName(funName), alwaysShowUniqueID = true)
- val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
- val tparams = hctx.sctx.functionContext.tparams
- val fd = new FunDef(funId, tparams, ValDef(argId) :: ctx.provided_functions.map(ValDef(_)).toList, StringType) // Empty function.
- fd
+ val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx).toLowerCase()(0).toString, tpe.typeToConvert)
+ val tparams = hctx.functionContext.tparams
+ new FunDef(funId, tparams, ValDef(argId) :: ctx.provided_functions.map(ValDef).toList, StringType) // Empty function.
}
/** Pre-updates of the function definition */
@@ -354,7 +348,7 @@ case object StringRender extends Rule("StringRender") {
}
/** Assembles multiple MatchCase to a singleMatchExpr using the function definition fd */
- private val mergeMatchCases = (fd: FunDef) => (cases: Seq[WithIds[MatchCase]]) => (MatchExpr(Variable(fd.params(0).id), cases.map(_._1)), cases.map(_._2).flatten.toList)
+ private val mergeMatchCases = (fd: FunDef) => (cases: Seq[WithIds[MatchCase]]) => (MatchExpr(Variable(fd.params(0).id), cases.map(_._1)), cases.flatMap(_._2).toList)
/** Returns a (possibly recursive) template which can render the inputs in their order.
* Returns an expression and path-dependent pretty printers which can be used.
@@ -414,23 +408,23 @@ case object StringRender extends Rule("StringRender") {
result: ListBuffer[Stream[WithIds[Expr]]] = ListBuffer()): (List[Stream[WithIds[Expr]]], StringSynthesisResult) = inputs match {
case Nil => (result.toList, ctx.result)
case input::q =>
- val dependentType = DependentType(ctx.currentCaseClassParent, input.asString(hctx.program)(hctx.context), input.getType)
+ val dependentType = DependentType(ctx.currentCaseClassParent, input.asString(hctx.program)(hctx), input.getType)
ctx.result.adtToString.get(dependentType) match {
case Some(fd) =>
gatherInputs(ctx, q, result += Stream((functionInvocation(fd._1, input::ctx.provided_functions.toList.map(Variable)), Nil)))
case None => // No function can render the current type.
// We should not rely on calling the original function on the first line of the body of the function itself.
val exprs1s = (new SelfPrettyPrinter)
- .allowFunction(hctx.sctx.functionContext)
- .excludeFunction(hctx.sctx.functionContext)
- .prettyPrintersForType(input.getType)(hctx.context, hctx.program)
+ .allowFunction(hctx.functionContext)
+ .excludeFunction(hctx.functionContext)
+ .prettyPrintersForType(input.getType)(hctx, hctx.program)
.map(l => (application(l, Seq(input)), List[Identifier]())) // Use already pre-defined pretty printers.
- val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(fd, _)), _) if fd == hctx.sctx.functionContext => 0 case _ => 1}
+ val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(fd, _)), _) if fd == hctx.functionContext => 0 case _ => 1}
val exprs2 = ctx.abstractStringConverters.getOrElse(input.getType, Nil).map(f => (f(input), List[Identifier]()))
val defaultConverters: Stream[WithIds[Expr]] = exprs1.toStream #::: exprs2.toStream
val recursiveConverters: Stream[WithIds[Expr]] =
(new SelfPrettyPrinter)
- .prettyPrinterFromCandidate(hctx.sctx.functionContext, input.getType)(hctx.context, hctx.program)
+ .prettyPrinterFromCandidate(hctx.functionContext, input.getType)(hctx, hctx.program)
.map(l => (application(l, Seq(input)), List[Identifier]()))
def mergeResults(templateConverters: =>Stream[WithIds[Expr]]): Stream[WithIds[Expr]] = {
@@ -457,7 +451,7 @@ case object StringRender extends Rule("StringRender") {
case WithStringconverter(converter) => // Base case
gatherInputs(ctx, q, result += mergeResults(Stream((converter(input), Nil))))
case t: ClassType =>
- if(enforceDefaultStringMethodsIfAvailable && !defaultConverters.isEmpty) {
+ if(enforceDefaultStringMethodsIfAvailable && defaultConverters.nonEmpty) {
gatherInputs(ctx, q, result += defaultConverters)
} else {
// Create the empty function body and updates the assignments parts.
@@ -467,10 +461,10 @@ case object StringRender extends Rule("StringRender") {
case act@AbstractClassType(acd@AbstractClassDef(id, tparams, parent), tps) =>
// Create a complete FunDef body with pattern matching
- val allKnownDescendantsAreCCAndHaveZeroArgs = act.knownCCDescendants.forall { x => x match {
+ val allKnownDescendantsAreCCAndHaveZeroArgs = act.knownCCDescendants.forall {
case CaseClassType(ccd@CaseClassDef(id, tparams, parent, isCaseObject), tparams2) => ccd.fields.isEmpty
case _ => false
- }}
+ }
//TODO: Test other templates not only with Wilcard patterns, but more cases options for non-recursive classes (e.g. Option, Boolean, Finite parameterless case classes.)
val (ctx3, cases) = ((ctx2, ListBuffer[Stream[WithIds[MatchCase]]]()) /: act.knownCCDescendants) {
@@ -542,18 +536,19 @@ case object StringRender extends Rule("StringRender") {
//hctx.reporter.debug("StringRender:Output variables="+p.xs+", their types="+p.xs.map(_.getType))
p.xs match {
case List(IsTyped(v, StringType)) =>
- val description = "Creates a standard string conversion function"
+ val examplesFinder = new ExamplesFinder(hctx, hctx.program)
+ .setKeepAbstractExamples(true)
+ .setEvaluationFailOnChoose(true)
- val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
- .setKeepAbstractExamples(true)
- .setEvaluationFailOnChoose(true)
val examples = examplesFinder.extractFromProblem(p)
- val abstractStringConverters: StringConverters =
- (p.as.flatMap { case x => x.getType match {
- case FunctionType(Seq(aType), StringType) => List((aType, (arg: Expr) => application(Variable(x), Seq(arg))))
+ val abstractStringConverters: StringConverters = p.as.flatMap { case x =>
+ x.getType match {
+ case FunctionType(Seq(aType), StringType) =>
+ List((aType, (arg: Expr) => application(Variable(x), Seq(arg))))
case _ => Nil
- }}).groupBy(_._1).mapValues(_.map(_._2))
+ }
+ }.groupBy(_._1).mapValues(_.map(_._2))
val (inputVariables, functionVariables) = p.as.partition ( x => x.getType match {
case f: FunctionType => false
@@ -564,11 +559,12 @@ case object StringRender extends Rule("StringRender") {
val originalInputs = inputVariables.map(Variable)
ruleInstantiations += RuleInstantiation("String conversion") {
val (expr, synthesisResult) = createFunDefsTemplates(
- StringSynthesisContext.empty(
- abstractStringConverters,
- originalInputs.toSet,
- functionVariables
- ), originalInputs)
+ StringSynthesisContext.empty(
+ abstractStringConverters,
+ originalInputs.toSet,
+ functionVariables
+ ), originalInputs
+ )
val funDefs = synthesisResult.adtToString
/*val toDebug: String = (("\nInferred functions:" /: funDefs)( (t, s) =>
diff --git a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
index bf6f57616..72c267b28 100644
--- a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
+++ b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
@@ -11,9 +11,7 @@ case object SygusCVC4 extends Rule("SygusCVC4") {
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
- val sctx = hctx.sctx
-
- val s = new CVC4SygusSolver(sctx.context, sctx.program, p)
+ val s = new CVC4SygusSolver(hctx, hctx.program, p)
s.checkSynth() match {
case Some(expr) =>
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 93e97de6f..62145f7ca 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -32,21 +32,18 @@ abstract class TEGISLike[T <: Typed](name: String) extends Rule(name) {
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
- val sctx = hctx.sctx
-
- implicit val ctx = sctx.context
-
- val params = getParams(sctx, p)
+ implicit val ci = hctx
+ val params = getParams(hctx, p)
val grammar = params.grammar
val nTests = if (p.pc == BooleanLiteral(true)) 50 else 20
- val useVanuatoo = sctx.settings.cegisUseVanuatoo
+ val useVanuatoo = hctx.settings.cegisUseVanuatoo
val inputGenerator: Iterator[Seq[Expr]] = if (useVanuatoo) {
- new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000)
+ new VanuatooDataGen(hctx, hctx.program).generateFor(p.as, p.pc, nTests, 3000)
} else {
- val evaluator = new DualEvaluator(sctx.context, sctx.program, CodeGenParams.default)
+ val evaluator = new DualEvaluator(hctx, hctx.program, CodeGenParams.default)
new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc, nTests, 1000)
}
@@ -66,13 +63,13 @@ abstract class TEGISLike[T <: Typed](name: String) extends Rule(name) {
if (gi.nonEmpty) {
val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
- val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams)
+ val evaluator = new DualEvaluator(hctx, hctx.program, evalParams)
val enum = new MemoizedEnumerator[T, Expr, ProductionRule[T, Expr]](grammar.getProductions)
val targetType = tupleTypeWrap(p.xs.map(_.getType))
- val timers = sctx.context.timers.synthesis.rules.tegis
+ val timers = hctx.timers.synthesis.rules.tegis
val allExprs = enum.iterator(params.rootLabel(targetType))
@@ -113,7 +110,7 @@ abstract class TEGISLike[T <: Typed](name: String) extends Rule(name) {
RuleClosed(toStream)
} else {
- sctx.reporter.debug("No test available")
+ hctx.reporter.debug("No test available")
RuleFailed()
}
}
diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
index cd6bd2ee7..fb3f1ecae 100644
--- a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
@@ -1,46 +1,26 @@
-package leon.integration.solvers
+package leon
+package integration
+package solvers
+import leon.test.LeonTestSuiteWithProgram
-import org.scalatest.FunSuite
-import org.scalatest.Matchers
-import leon.test.helpers.ExpressionsDSL
-import leon.solvers.string.StringSolver
import leon.purescala.Common.FreshIdentifier
-import leon.purescala.Common.Identifier
import leon.purescala.Expressions._
import leon.purescala.Definitions._
import leon.purescala.DefOps
import leon.purescala.ExprOps
import leon.purescala.Types._
-import leon.purescala.TypeOps
import leon.purescala.Constructors._
+
+import leon.synthesis._
import leon.synthesis.rules.{StringRender, TypedTemplateGenerator}
-import scala.collection.mutable.{HashMap => MMap}
-import scala.concurrent.Future
-import scala.concurrent.ExecutionContext.Implicits.global
-import org.scalatest.concurrent.Timeouts
-import org.scalatest.concurrent.ScalaFutures
-import org.scalatest.time.SpanSugar._
-import org.scalatest.FunSuite
-import org.scalatest.concurrent.Timeouts
-import org.scalatest.concurrent.ScalaFutures
-import org.scalatest.time.SpanSugar._
-import leon.purescala.Types.Int32Type
-import leon.test.LeonTestSuiteWithProgram
-import leon.synthesis.SourceInfo
-import leon.synthesis.CostModels
-import leon.synthesis.graph.SimpleSearch
+import leon.synthesis.strategies.CostBasedStrategy
import leon.synthesis.graph.AndNode
-import leon.synthesis.SearchContext
-import leon.synthesis.Synthesizer
-import leon.synthesis.SynthesisSettings
-import leon.synthesis.RuleApplication
-import leon.synthesis.RuleClosed
+
import leon.evaluators._
-import leon.LeonContext
-import leon.synthesis.rules.DetupleInput
-import leon.synthesis.Rules
-import leon.solvers.ModelBuilder
+
+import org.scalatest.concurrent.ScalaFutures
+import org.scalatest.Matchers
import scala.language.implicitConversions
class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures {
@@ -102,11 +82,11 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
def applyStringRenderOn(functionName: String): (FunDef, Program) = {
val ci = synthesisInfos(functionName)
- val search = new SimpleSearch(ctx, ci, ci.problem, CostModels.default, Some(200))
+ val search = new Search(ctx, ci, ci.problem, new CostBasedStrategy(ctx, CostModels.default))
val synth = new Synthesizer(ctx, program, ci, SynthesisSettings(rules = Seq(StringRender)))
val orNode = search.g.root
if (!orNode.isExpanded) {
- val hctx = SearchContext(synth.sctx, synth.ci, orNode, search)
+ val hctx = new SearchContext(synth.sctx, synth.ci, orNode, search)
orNode.expand(hctx)
}
val andNodes = orNode.descendants.collect {
@@ -115,11 +95,6 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
}
val rulesApps = (for ((t, i) <- andNodes.zipWithIndex) yield {
- val status = if (t.isDeadEnd) {
- "closed"
- } else {
- "open"
- }
t.ri.asString -> i
}).toMap
rulesApps should contain key "String conversion"
@@ -129,7 +104,7 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
val solutions = (search.traversePath(path) match {
case Some(an: AndNode) =>
- val hctx = SearchContext(synth.sctx, synth.ci, an, search)
+ val hctx = new SearchContext(synth.sctx, synth.ci, an, search)
an.ri.apply(hctx)
case _ => throw new Exception("Was not an and node")
}) match {
@@ -241,7 +216,6 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
def synthesizeAndTest(functionName: String, tests: (Seq[Expr], String)*) {
val (fd, program) = applyStringRenderOn(functionName)
val when = new DefaultEvaluator(ctx, program)
- val args = getFunctionArguments(functionName)
for((in, out) <- tests) {
val expr = functionInvocation(fd, in)
when.eval(expr) match {
@@ -254,7 +228,6 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal
def synthesizeAndAbstractTest(functionName: String)(tests: (FunDef, Program) => Seq[(Seq[Expr], Expr)]) {
val (fd, program) = applyStringRenderOn(functionName)
val when_abstract = new AbstractEvaluator(ctx, program)
- val args = getFunctionArguments(functionName)
for((in, out) <- tests(fd, program)) {
val expr = functionInvocation(fd, in)
when_abstract.eval(expr) match {
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 6301f4ea1..5f9861362 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -34,7 +34,7 @@ class RepairSuite extends LeonRegressionSuite {
val reporter = new TestSilentReporter
//val reporter = new DefaultReporter(Set(utils.DebugSectionRepair))
- val ctx = LeonContext(
+ val ctx = new LeonContext(
reporter = reporter,
interruptManager = new InterruptManager(reporter),
options = Seq(
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index c8bfc2688..61bbe1deb 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -104,9 +104,9 @@ class StablePrintingSuite extends LeonRegressionSuite {
val sctx = synthesizer.sctx
try {
val search = synthesizer.getSearch
- val hctx = SearchContext(sctx, ci, search.g.root, search)
+ val hctx = new SearchContext(sctx, ci, search.g.root, search)
val problem = ci.problem
- info(j.info("synthesis "+problem.asString(sctx.context)))
+ info(j.info("synthesis "+problem.asString(sctx)))
val apps = decompRules flatMap { _.instantiateOn(hctx, problem)}
for (a <- apps) {
--
GitLab