From 33777002b7ccd15af322160aa4afce15c6dcc4e9 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 11 Aug 2015 18:27:16 +0200
Subject: [PATCH] Remove toString, rely on asString instead when printing stuff
---
.../scala/leon/datagen/VanuatooDataGen.scala | 10 ++++-----
.../leon/evaluators/RecursiveEvaluator.scala | 22 ++++++++++---------
.../frontends/scalac/CodeExtraction.scala | 2 +-
.../frontends/scalac/LeonExtraction.scala | 2 +-
.../leon/purescala/CheckADTFieldsTypes.scala | 2 +-
src/main/scala/leon/purescala/Common.scala | 13 ++++++++---
src/main/scala/leon/purescala/Types.scala | 2 ++
src/main/scala/leon/repair/rules/Focus.scala | 4 ++--
src/main/scala/leon/repair/rules/Split.scala | 4 ++--
.../leon/solvers/smtlib/SMTLIBSolver.scala | 16 +++++++-------
.../leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
.../scala/leon/synthesis/FileInterface.scala | 7 +++---
src/main/scala/leon/synthesis/Problem.scala | 8 -------
src/main/scala/leon/synthesis/Rules.scala | 6 +++--
src/main/scala/leon/synthesis/Solution.scala | 2 --
.../scala/leon/synthesis/graph/Graph.scala | 8 ++++---
.../scala/leon/synthesis/graph/Search.scala | 8 +++----
.../scala/leon/synthesis/rules/ADTDual.scala | 1 -
.../leon/synthesis/rules/ADTInduction.scala | 2 +-
.../synthesis/rules/ADTLongInduction.scala | 2 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
.../scala/leon/synthesis/rules/Assert.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 7 +++---
.../scala/leon/synthesis/rules/CEGLESS.scala | 7 +++---
.../leon/synthesis/rules/DetupleInput.scala | 3 +--
.../synthesis/rules/EquivalentInputs.scala | 2 +-
.../synthesis/utils/ExpressionGrammar.scala | 10 ++++-----
.../SynthesisProblemExtractionPhase.scala | 2 +-
.../leon/verification/DefaultTactic.scala | 2 +-
.../leon/verification/InductionTactic.scala | 6 ++---
src/main/scala/leon/verification/Tactic.scala | 2 ++
.../test/synthesis/StablePrintingSuite.scala | 4 ++--
.../leon/test/synthesis/SynthesisSuite.scala | 2 +-
.../leon/test/helpers/WithLikelyEq.scala | 8 +++++--
34 files changed, 97 insertions(+), 85 deletions(-)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 013b8d870..1751a1e55 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -66,7 +66,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
(1 to size).map(i => sub).toList,
at,
s => finiteArray(s, None, sub),
- at.toString+"@"+size
+ at.asString(ctx)+"@"+size
)
}
constructors += at -> cs
@@ -80,7 +80,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
(1 to size).map(i => sub).toList,
st,
s => FiniteSet(s.toSet, sub),
- st.toString+"@"+size
+ st.asString(ctx)+"@"+size
)
}
constructors += st -> cs
@@ -89,7 +89,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case tt @ TupleType(parts) =>
constructors.getOrElse(tt, {
- val cs = List(Constructor[Expr, TypeTree](parts, tt, s => tupleWrap(s), tt.toString))
+ val cs = List(Constructor[Expr, TypeTree](parts, tt, s => tupleWrap(s), tt.asString(ctx)))
constructors += tt -> cs
cs
})
@@ -99,7 +99,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val cs = for (size <- List(0, 1, 2, 5)) yield {
val subs = (1 to size).flatMap(i => List(from, to)).toList
- Constructor[Expr, TypeTree](subs, mt, s => FiniteMap(s.grouped(2).map(t => (t(0), t(1))).toSeq, from, to), mt.toString+"@"+size)
+ Constructor[Expr, TypeTree](subs, mt, s => FiniteMap(s.grouped(2).map(t => (t(0), t(1))).toSeq, from, to), mt.asString(ctx)+"@"+size)
}
constructors += mt -> cs
cs
@@ -117,7 +117,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
IfExpr(Equals(argsTuple, tupleWrap(t.init)), t.last, elze)
}
Lambda(args.map(id => ValDef(id)), body)
- }, ft.toString + "@" + size)
+ }, ft.asString(ctx) + "@" + size)
}
constructors += ft -> cs
cs
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 1eb6398ea..4c4340848 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -19,6 +19,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val name = "evaluator"
val description = "Recursive interpreter for PureScala expressions"
+ private implicit val ctx0 = ctx
+
type RC <: RecContext
type GC <: GlobalContext
@@ -80,7 +82,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Some(v) =>
v
case None =>
- throw EvalError("No value for identifier " + id.asString(ctx) + " in mapping.")
+ throw EvalError("No value for identifier " + id.asString + " in mapping.")
}
case Application(caller, args) =>
@@ -90,7 +92,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val mapping = l.paramSubst(newArgs)
e(body)(rctx.withNewVars(mapping), gctx)
case f =>
- throw EvalError("Cannot apply non-lambda function " + f)
+ throw EvalError("Cannot apply non-lambda function " + f.asString)
}
case Tuple(ts) =>
@@ -153,7 +155,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
e(tfd.precondition.get)(frame, gctx) match {
case BooleanLiteral(true) =>
case BooleanLiteral(false) =>
- throw RuntimeError("Precondition violation for " + tfd.id.name + " reached in evaluation.: " + tfd.precondition.get)
+ throw RuntimeError("Precondition violation for " + tfd.id.asString + " reached in evaluation.: " + tfd.precondition.get.asString)
case other =>
throw RuntimeError(typeErrorMsg(other, BooleanType))
}
@@ -170,7 +172,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Some(post) =>
e(application(post, Seq(callResult)))(frame, gctx) match {
case BooleanLiteral(true) =>
- case BooleanLiteral(false) => throw RuntimeError("Postcondition violation for " + tfd.id.name + " reached in evaluation.")
+ case BooleanLiteral(false) => throw RuntimeError("Postcondition violation for " + tfd.id.asString + " reached in evaluation.")
case other => throw EvalError(typeErrorMsg(other, BooleanType))
}
case None =>
@@ -517,7 +519,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case g @ MapGet(m,k) => (e(m), e(k)) match {
case (FiniteMap(ss, _, _), e) => ss.find(_._1 == e) match {
case Some((_, v0)) => v0
- case None => throw RuntimeError("Key not found: " + e)
+ case None => throw RuntimeError("Key not found: " + e.asString)
}
case (l,r) => throw EvalError(typeErrorMsg(l, MapType(r.getType, g.getType)))
}
@@ -577,7 +579,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val total = System.currentTimeMillis-tStart
ctx.reporter.debug("Synthesis took "+total+"ms")
- ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
+ ctx.reporter.debug("Finished synthesis with "+leonRes.asString)
clpCache += (choose, ins) -> leonRes
leonRes
@@ -599,14 +601,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Some(Some((c, mappings))) =>
e(c.rhs)(rctx.withNewVars(mappings), gctx)
case _ =>
- throw RuntimeError("MatchError: "+rscrut+" did not match any of the cases")
+ throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases")
}
case l : Literal[_] => l
case other =>
- context.reporter.error(other.getPos, "Error: don't know how to handle " + other + " in Evaluator ("+other.getClass+").")
- throw EvalError("Unhandled case in Evaluator : " + other)
+ context.reporter.error(other.getPos, "Error: don't know how to handle " + other.asString + " in Evaluator ("+other.getClass+").")
+ throw EvalError("Unhandled case in Evaluator : " + other.asString)
}
def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Map[Identifier, Expr])] = {
@@ -683,6 +685,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
}
- def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected $expected, found $tree."
+ def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected ${expected.asString}, found ${tree.asString}."
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index cda2d5fae..e96ad2d5f 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1349,7 +1349,7 @@ trait CodeExtraction extends ASTExtractors {
Not(Equals(rl, InfiniteIntegerLiteral(v)))
case (IsTyped(_, rt), IsTyped(_, lt)) =>
- outOfSubsetError(tr, "Invalid comparison: (_: "+rt+") != (_: "+lt+")")
+ outOfSubsetError(tr, "Invalid comparison: (_: "+rt.asString+") != (_: "+lt.asString+")")
}
}
diff --git a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
index 1de899e28..3bc1a0d05 100644
--- a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
@@ -12,7 +12,7 @@ trait LeonExtraction extends SubComponent with CodeExtraction {
var units: List[CompilationUnit] = Nil
- val ctx: LeonContext
+ implicit val ctx: LeonContext
var imports : Map[RefTree,List[Import]] = Map()
diff --git a/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala b/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala
index ee78b4b5f..a62837f00 100644
--- a/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala
+++ b/src/main/scala/leon/purescala/CheckADTFieldsTypes.scala
@@ -17,7 +17,7 @@ object CheckADTFieldsTypes extends UnitPhase[Program] {
for(vd <- ccd.fields) {
val tpe = vd.getType
if (bestRealType(tpe) != tpe) {
- ctx.reporter.warning("Definition of "+ccd.id+" has a field of a sub-type ("+vd+"): " +
+ ctx.reporter.warning("Definition of "+ccd.id.asString(ctx)+" has a field of a sub-type ("+vd.asString(ctx)+"): " +
"this type is not supported as-is by solvers and will be up-cast. " +
"This may cause issues such as crashes.")
}
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 764320d23..e10036a36 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -17,9 +17,7 @@ object Common {
this
}
- override def toString: String = {
- PrettyPrinter(this)
- }
+ // @EK: toString is considered harmful for non-internal things. Use asString(ctx) instead.
def asString(implicit ctx: LeonContext): String = {
ScalaPrinter(this, ctx)
@@ -60,6 +58,15 @@ object Common {
}
+ implicit object IdentifierOrdering extends Ordering[Identifier] {
+ def compare(a: Identifier, b: Identifier) = {
+ val ord = implicitly[Ordering[Tuple3[String, Int, Int]]]
+
+ ord.compare((a.name, a.id, a.globalId),
+ (b.name, b.id, b.globalId))
+ }
+ }
+
private object UniqueCounter {
private var globalId = -1
private var nameIds = Map[String, Int]().withDefaultValue(-1)
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 775a82c19..b780cfb69 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -15,6 +15,8 @@ object Types {
trait Typed {
val getType: TypeTree
def isTyped : Boolean = getType != Untyped
+
+ def asString(implicit ctx: LeonContext): String
}
class TypeErrorException(msg: String) extends Exception(msg)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index e4a5e3404..edf5cdcf3 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -109,7 +109,7 @@ case object Focus extends PreprocessingRule("Focus") {
// Focus on condition
val np = Problem(p.as, ws(c), p.pc, letTuple(p.xs, IfExpr(cx.toVariable, thn, els), p.phi), List(cx), p.eb.stripOuts)
- Some(decomp(List(np), termWrap(IfExpr(_, thn, els)), s"Focus on if-cond '$c'")(p))
+ Some(decomp(List(np), termWrap(IfExpr(_, thn, els)), s"Focus on if-cond '${c.asString}'")(p))
case _ =>
// Try to focus on branches
@@ -173,7 +173,7 @@ case object Focus extends PreprocessingRule("Focus") {
decomp(List(np), termWrap(x => MatchExpr(scrut, cases.map {
case `c` => c.copy(rhs = x)
case c2 => c2
- }), cond), s"Focus on match-case '${c.pattern}'")(p)
+ }), cond), s"Focus on match-case '${c.pattern.asString}'")(p)
)
)
diff --git a/src/main/scala/leon/repair/rules/Split.scala b/src/main/scala/leon/repair/rules/Split.scala
index 94b7ff24b..da066cefa 100644
--- a/src/main/scala/leon/repair/rules/Split.scala
+++ b/src/main/scala/leon/repair/rules/Split.scala
@@ -60,7 +60,7 @@ case object Split extends Rule("Split") {
None
}
- Some(decomp(List(sub1, sub2), onSuccess, s"Guided If-Split on '$c'"))
+ Some(decomp(List(sub1, sub2), onSuccess, s"Guided If-Split on '${c.asString}'"))
case m @ MatchExpr(scrut, cases) =>
@@ -112,7 +112,7 @@ case object Split extends Rule("Split") {
}
Some(
- decomp(infos.map(_._2).toList, onSuccess, s"Split match on '$scrut'")
+ decomp(infos.map(_._2).toList, onSuccess, s"Split match on '${scrut.asString}'")
)
case e =>
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 8bfb6d92f..5a4450e58 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -163,8 +163,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
protected def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
case SetType(base) =>
if (r.default != BooleanLiteral(false)) {
- reporter.warning("Co-finite sets are not supported.")
- throw new IllegalArgumentException
+ unsupported("Co-finite sets are not supported.")
}
require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
@@ -180,8 +179,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
// We expect a RawArrayValue with keys in from and values in Option[to],
// with default value == None
if (r.default.getType != library.noneType(to)) {
- reporter.warning("Co-finite maps are not supported. (Default was "+r.default+")")
- throw new IllegalArgumentException
+ unsupported("Co-finite maps are not supported.")
}
require(r.keyTpe == from, s"Type error in solver model, expected $from, found ${r.keyTpe}")
@@ -195,7 +193,10 @@ abstract class SMTLIBSolver(val context: LeonContext,
unsupported("Unable to extract from raw array for "+tpe)
}
- protected def unsupported(str: Any) = reporter.fatalError(s"Unsupported in smt-$targetName: $str")
+ protected def unsupported(str: String) = {
+ reporter.warning(s"Unsupported in smt-$targetName: $str")
+ throw new IllegalArgumentException(str)
+ }
protected def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
@@ -563,8 +564,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
)
}
case o =>
- reporter.warning(s"Unsupported Tree in smt-$targetName: $o")
- throw new IllegalArgumentException
+ unsupported(s"Tree ${o.asString}")
}
}
@@ -604,7 +604,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case cct: CaseClassType =>
CaseClass(cct, Nil)
case t =>
- unsupported("woot? for a single constructor for non-case-object: "+t)
+ unsupported("woot? for a single constructor for non-case-object: "+t.asString)
}
case (SimpleSymbol(s), tpe) if lets contains s =>
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index d24b88473..11cf31b27 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -82,7 +82,7 @@ trait AbstractZ3Solver
def genericValueToDecl(gv: GenericValue): Z3FuncDecl = {
generics.cachedB(gv) {
- z3.mkFreshFuncDecl(gv.tp.toString+"#"+gv.id+"!val", Seq(), typeToSort(gv.tp))
+ z3.mkFreshFuncDecl(gv.tp.id.uniqueName+"#"+gv.id+"!val", Seq(), typeToSort(gv.tp))
}
}
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index d94f78268..251c6af0e 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -15,7 +15,7 @@ import leon.utils.RangePosition
import java.io.File
class FileInterface(reporter: Reporter) {
- def updateFile(origFile: File, solutions: Map[ChooseInfo, Expr]) {
+ def updateFile(origFile: File, solutions: Map[ChooseInfo, Expr])(implicit ctx: LeonContext) {
import java.io.{File, BufferedWriter, FileWriter}
val FileExt = """^(.+)\.([^.]+)$""".r
@@ -70,9 +70,10 @@ class FileInterface(reporter: Reporter) {
}
- def substitute(str: String, fromTree: Tree, toTree: Tree): String = {
+ def substitute(str: String, fromTree: Tree, toTree: Tree)(implicit ctx: LeonContext): String = {
substitute(str, fromTree, (indent: Int) => {
- val p = new ScalaPrinter(PrinterOptions(), None)
+ val opts = PrinterOptions.fromContext(ctx)
+ val p = new ScalaPrinter(opts, None)
p.pp(toTree)(PrinterContext(toTree, Nil, indent, p))
p.toString
})
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 4ae607f81..08e9c25d3 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -33,14 +33,6 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List
"⟦ "+as.map(_.asString).mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws.asString+" ≺ " else "")+" ⟨ "+phi.asString+" ⟩ "+xs.map(_.asString).mkString(";")+" ⟧ "+ebInfo
}
- override def toString = {
- val pcws = and(ws, pc)
-
- val ebInfo = "/"+eb.valids.size+","+eb.invalids.size+"/"
-
- "⟦ "+as.mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "+ebInfo
- }
-
// Qualified example bank, allows us to perform operations (e.g. filter) with expressions
def qeb(implicit sctx: SearchContext) = QualifiedExampleBank(this.as, this.xs, eb)
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 908b753d9..e9c3fdcae 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -20,7 +20,9 @@ abstract class Rule(val name: String) extends RuleDSL {
implicit val thisRule = this
- override def toString = name
+ implicit def hctxToCtx(implicit hctx: SearchContext): LeonContext = hctx.sctx.context
+
+ def asString(implicit ctx: LeonContext) = name
}
abstract class NormalizingRule(name: String) extends Rule(name) {
@@ -75,7 +77,7 @@ abstract class RuleInstantiation(val description: String,
def apply(hctx: SearchContext): RuleApplication
- override def toString = description
+ def asString(implicit ctx: LeonContext) = description
}
/**
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 812b75353..3a44131eb 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -20,8 +20,6 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
"⟨ "+pre.asString+" | "+defs.map(_.asString).mkString(" ")+" "+term.asString+" ⟩"
}
- override def toString = "⟨ "+pre+" | "+defs.mkString(" ")+" "+term+" ⟩"
-
def guardedTerm = {
if (pre == BooleanLiteral(true)) {
term
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index aac4d2fd2..b4db0e471 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -30,6 +30,8 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
var parents: List[Node] = parent.toList
var descendants: List[Node] = Nil
+ def asString(implicit ctx: LeonContext): String
+
// indicates whether this particular node has already been expanded
var isExpanded: Boolean = false
def expand(hctx: SearchContext)
@@ -98,7 +100,7 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) extends Node(cm, parent) {
val p = ri.problem
- override def toString = "\u2227 "+ri
+ override def asString(implicit ctx: LeonContext) = "\u2227 "+ri.asString
def expand(hctx: SearchContext): Unit = {
require(!isExpanded)
@@ -172,7 +174,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(cm, parent) {
- override def toString = "\u2228 "+p
+ override def asString(implicit ctx: LeonContext) = "\u2228 "+p.asString
def getInstantiations(hctx: SearchContext): List[RuleInstantiation] = {
val rules = hctx.sctx.rules
@@ -181,7 +183,7 @@ class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(c
for ((_, rs) <- rulesPrio) {
val results = rs.flatMap{ r =>
- hctx.context.timers.synthesis.instantiations.get(r.toString).timed {
+ hctx.context.timers.synthesis.instantiations.get(r.asString(hctx.sctx.context)).timed {
r.instantiateOn(hctx, p)
}
}.toList
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index 9f1726d98..d63bca0b5 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -21,7 +21,7 @@ abstract class Search(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: C
ctx.timers.synthesis.step.timed {
n match {
case an: AndNode =>
- ctx.timers.synthesis.applications.get(an.ri.toString).timed {
+ ctx.timers.synthesis.applications.get(an.ri.asString(sctx.context)).timed {
an.expand(SearchContext(sctx, ci, an, this))
}
@@ -214,15 +214,15 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
def displayNode(n: Node): String = n match {
case an: AndNode =>
- val app = an.ri
+ val app = an.ri.asString(ctx)
s"(${n.cost.asString}) ${indent(app)}"
case on: OrNode =>
val p = on.p.asString(ctx)
s"(${n.cost.asString}) ${indent(p)}"
}
- def indent(a: Any): String = {
- a.toString.replaceAll("\n", "\n"+(" "*12))
+ def indent(a: String): String = {
+ a.replaceAll("\n", "\n"+(" "*12))
}
def pathToString(cd: List[Int]): String = {
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index ddf37760e..59fcabb3b 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -16,7 +16,6 @@ case object ADTDual extends NormalizingRule("ADTDual") {
val TopLevelAnds(exprs) = p.phi
-
val (toRemove, toAdd) = exprs.collect {
case eq @ Equals(cc @ CaseClass(ct, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) & xs).nonEmpty =>
(eq, IsInstanceOf(ct, e) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 45509bdb7..3b6df4524 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -113,7 +113,7 @@ case object ADTInduction extends Rule("ADT Induction") {
}
}
- Some(decomp(subProblemsInfo.map(_._1).toList, onSuccess, s"ADT Induction on '$origId'"))
+ Some(decomp(subProblemsInfo.map(_._1).toList, onSuccess, s"ADT Induction on '${origId.asString}'"))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 3f39582e3..093897196 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -162,7 +162,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
}
}
- Some(decomp(subProblemsInfo.map(_._1), onSuccess, s"ADT Long Induction on '$origId'"))
+ Some(decomp(subProblemsInfo.map(_._1), onSuccess, s"ADT Long Induction on '${origId.asString}'"))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index a57cdfb15..5d0ab6ce1 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -87,7 +87,7 @@ case object ADTSplit extends Rule("ADT Split.") {
Some(Solution(orJoin(globalPre), sols.flatMap(_.defs).toSet, matchExpr(Variable(id), cases), sols.forall(_.isTrusted)))
}
- decomp(subInfo.map(_._2).toList, onSuccess, s"ADT Split on '$id'")
+ decomp(subInfo.map(_._2).toList, onSuccess, s"ADT Split on '${id.asString}'")
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 270392aa1..4cdb0fbf2 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -24,7 +24,7 @@ case object Assert extends NormalizingRule("Assert") {
Some(decomp(List(sub), {
case (s @ Solution(pre, defs, term)) :: Nil => Some(Solution(andJoin(exprsA :+ pre), defs, term, s.isTrusted))
case _ => None
- }, "Assert "+andJoin(exprsA)))
+ }, "Assert "+andJoin(exprsA).asString))
}
} else {
None
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index c78750adc..386148ce6 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -43,7 +43,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val nProgramsLimit = 100000
val sctx = hctx.sctx
- implicit val ctx = sctx.context
+ val ctx = sctx.context
// CEGIS Flags to activate or deactivate features
@@ -125,7 +125,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private var slots = Map[SizedLabel[T], Int]().withDefaultValue(0)
private def streamOf(t: SizedLabel[T]): Stream[Identifier] = {
- FreshIdentifier(t.toString, t.getType, true) #:: streamOf(t)
+ FreshIdentifier(t.asString, t.getType, true) #:: streamOf(t)
}
def rewind(): Unit = {
@@ -285,7 +285,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// Define all C-def
for ((c, alts) <- cTree) yield {
- cToFd += c -> new FunDef(FreshIdentifier(c.toString, alwaysShowUniqueID = true),
+ cToFd += c -> new FunDef(FreshIdentifier(c.asString, alwaysShowUniqueID = true),
Seq(),
c.getType,
p.as.map(id => ValDef(id)))
@@ -641,6 +641,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
def apply(hctx: SearchContext): RuleApplication = {
var result: Option[RuleApplication] = None
val sctx = hctx.sctx
+ implicit val ctx = sctx.context
val ndProgram = new NonDeterministicProgram(p)
ndProgram.init()
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index 31484628a..c19a4203e 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -13,9 +13,10 @@ import Witnesses._
case object CEGLESS extends CEGISLike[Label[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
}
@@ -23,9 +24,9 @@ case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
val inputs = p.as.map(_.toVariable)
sctx.reporter.ifDebug { printer =>
- printer("Guides available:")
+ printer("Guides available:")
for (g <- guides) {
- printer(" - "+g)
+ printer(" - "+g.asString(ctx))
}
}
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index bb0f1b4ba..ed68fbfac 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -72,7 +72,6 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
}
val newAs = subAs.flatten
- //sctx.reporter.warning("newOuts: " + newOuts.toString)
// Recompose CaseClasses and Tuples.
// E.g. Cons(l.head, l.tail) ~~> l
@@ -83,7 +82,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
case (CaseClassSelector(ct, e, id), field) if field.id == id => (ct, e)
case _ => return e
}.unzip
-
+
if (cts.distinct.size == 1 && es.distinct.size == 1) {
es.head
} else {
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 10ba905b8..4754f6bc5 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -84,7 +84,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
_:Expr
)
- val substString = substs.map { case (f, t) => f+" -> "+t }
+ val substString = substs.map { case (f, t) => f.asString+" -> "+t.asString }
List(decomp(List(sub), forwardMap(subst), "Equivalent Inputs ("+substString.mkString(", ")+")"))
} else {
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 0aad97735..82c6552fe 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -50,9 +50,9 @@ abstract class ExpressionGrammar[T <% Typed] {
}
- final def printProductions(printer: String => Unit) {
+ final def printProductions(printer: String => Unit)(implicit ctx: LeonContext) {
for ((t, gs) <- cache; g <- gs) {
- val subs = g.subTrees.map { t => FreshIdentifier(Console.BOLD+t.toString+Console.RESET, t.getType).toVariable}
+ val subs = g.subTrees.map { t => FreshIdentifier(Console.BOLD+t.asString+Console.RESET, t.getType).toVariable}
val gen = g.builder(subs)
printer(f"${Console.BOLD}$t%30s${Console.RESET} ::= $gen")
@@ -210,7 +210,7 @@ object ExpressionGrammars {
case class Label[T](t: TypeTree, l: T, depth: Option[Int] = None) extends Typed {
val getType = t
- override def toString = t.toString+"#"+l+depth.map(d => "@"+d).getOrElse("")
+ override def asString(implicit ctx: LeonContext) = t.asString+"#"+l+depth.map(d => "@"+d).getOrElse("")
}
case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[Label[String]] {
@@ -356,7 +356,7 @@ object ExpressionGrammars {
val res = rec(e, gl)
//for ((t, g) <- res) {
- // val subs = g.subTrees.map { t => FreshIdentifier(t.toString, t.getType).toVariable}
+ // val subs = g.subTrees.map { t => FreshIdentifier(t.asString, t.getType).toVariable}
// val gen = g.builder(subs)
// println(f"$t%30s ::= "+gen)
@@ -435,7 +435,7 @@ object ExpressionGrammars {
case class SizedLabel[T <% Typed](underlying: T, size: Int) extends Typed {
val getType = underlying.getType
- override def toString = underlying.toString+"|"+size+"|"
+ override def asString(implicit ctx: LeonContext) = underlying.asString+"|"+size+"|"
}
case class SizeBoundedGrammar[T <% Typed](g: ExpressionGrammar[T]) extends ExpressionGrammar[SizedLabel[T]] {
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index ae4632031..7aa46f7a0 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -13,7 +13,7 @@ object SynthesisProblemExtractionPhase extends LeonPhase[Program, (Program, Map[
def run(ctx: LeonContext)(p: Program): (Program, Map[FunDef, Seq[ChooseInfo]]) = {
// Look for choose()
- val results = for (f <- funDefsFromMain(p).toSeq.sortBy(_.id.toString) if f.body.isDefined) yield {
+ val results = for (f <- funDefsFromMain(p).toSeq.sortBy(_.id) if f.body.isDefined) yield {
f -> ChooseInfo.extractFromFunction(ctx, p, f)
}
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 43ef19dfd..11de3159c 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -33,7 +33,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
val pre2 = tfd.withParamSubst(args, pre)
val vc = implies(and(precOrTrue(fd), path), pre2)
- val fiS = sizeLimit(fi.toString, 40)
+ val fiS = sizeLimit(fi.asString, 40)
VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
}
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 8ce88e490..878b902ce 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -44,7 +44,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
implies(andJoin(subCases), application(post, Seq(body)))
)
- VC(vc, fd, VCKinds.Info(VCKinds.Postcondition, s"ind. on ${arg.id} / ${cct.classDef.id}"), this).setPos(fd)
+ VC(vc, fd, VCKinds.Info(VCKinds.Postcondition, s"ind. on ${arg.asString} / ${cct.classDef.id.asString}"), this).setPos(fd)
}
case (body, _, post) =>
@@ -82,9 +82,9 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
)
// Crop the call to display it properly
- val fiS = sizeLimit(fi.toString, 25)
+ val fiS = sizeLimit(fi.asString, 25)
- VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS, ind. on ($arg : ${cct.classDef.id})"), this).setPos(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS, ind. on (${arg.asString} : ${cct.classDef.id.asString})"), this).setPos(fi)
}
case (body, _) =>
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 105c61d61..2295cb191 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -10,6 +10,8 @@ import purescala.ExprOps._
abstract class Tactic(vctx: VerificationContext) {
val description : String
+ implicit val ctx = vctx.context
+
def generateVCs(fd: FunDef): Seq[VC] = {
generatePostconditions(fd) ++
generatePreconditions(fd) ++
diff --git a/src/regression/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/regression/scala/leon/test/synthesis/StablePrintingSuite.scala
index aec2a04a3..d602a05a2 100644
--- a/src/regression/scala/leon/test/synthesis/StablePrintingSuite.scala
+++ b/src/regression/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -84,7 +84,7 @@ class StablePrintingSuite extends LeonTestSuite {
val search = synthesizer.getSearch
val hctx = SearchContext(sctx, ci, search.g.root, search)
val problem = ci.problem
- info(j.info("synthesis "+problem))
+ info(j.info("synthesis "+problem.asString(sctx.context)))
val apps = sctx.rules flatMap { _.instantiateOn(hctx, problem)}
for (a <- apps) {
@@ -101,7 +101,7 @@ class StablePrintingSuite extends LeonTestSuite {
p.toString
})
- workList push Job(newContent, (i to i+sub.size).toSet, a.toString :: j.rules)
+ workList push Job(newContent, (i to i+sub.size).toSet, a.asString(ctx) :: j.rules)
case None =>
}
}
diff --git a/src/regression/scala/leon/test/synthesis/SynthesisSuite.scala b/src/regression/scala/leon/test/synthesis/SynthesisSuite.scala
index a4804afeb..e949f139d 100644
--- a/src/regression/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/regression/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -76,7 +76,7 @@ class SynthesisSuite extends LeonTestSuite {
def matchingDesc(app: RuleInstantiation, n: String): Boolean = {
import java.util.regex.Pattern
val pattern = Pattern.quote(n).replace("*", "\\E.*\\Q")
- app.toString.matches(pattern)
+ app.asString(ctx).matches(pattern)
}
}
diff --git a/src/test/scala/leon/test/helpers/WithLikelyEq.scala b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
index aee9e7671..c998591f5 100644
--- a/src/test/scala/leon/test/helpers/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
@@ -38,7 +38,9 @@ trait WithLikelyEq {
val r1 = evaluator.eval(e1)
val r2 = evaluator.eval(e2)
- assert(r1 === r2, s"'$e1' != '$e2' ('$r1' != '$r2')")
+ if (r1 != r2) {
+ fail(s"'${e1.asString(ctx)}' != '${e2.asString(ctx)}' ('$r1' != '$r2')")
+ }
} else {
val allValues = freeVars.map(id => values.get(id).map(Seq(_)).getOrElse(typesValues(id.getType)))
@@ -57,7 +59,9 @@ trait WithLikelyEq {
val r1 = evaluator.eval(e1, m)
val r2 = evaluator.eval(e2, m)
- assert(r1 === r2, s"'$e1' != '$e2' with '$m' ('$r1' != '$r2')")
+ if (r1 != r2) {
+ fail(s"'${e1.asString(ctx)}' != '${e2.asString(ctx)}' with '$m' ('$r1' != '$r2')")
+ }
}
}
}
--
GitLab