diff --git a/src/main/scala/inox/ast/DSL.scala b/src/main/scala/inox/ast/DSL.scala
index edb08f59bd6378e0d1408347e5235970ac88017a..cc50665036714da651d1b8e25fec4d449164bc68 100644
--- a/src/main/scala/inox/ast/DSL.scala
+++ b/src/main/scala/inox/ast/DSL.scala
@@ -191,6 +191,7 @@ trait DSL {
/* Types */
def T(tp1: Type, tp2: Type, tps: Type*) = TupleType(tp1 :: tp2 :: tps.toList)
def T(id: Identifier) = new IdToClassType(id)
+ def T(str: String) = TypeParameter.fresh(str)
class IdToClassType(id: Identifier) {
def apply(tps: Type*) = ClassType(id, tps.toSeq)
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index dc51473ff30f8cf7fb455d1817bc5b274b744cf4..43b0f7db53cf0a76cfa216c13aa234b8d7699e88 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -26,13 +26,19 @@ package object inox {
object InoxProgram {
def apply(ictx: InoxContext,
functions: Seq[inox.trees.FunDef],
- classes: Seq[inox.trees.ClassDef]) = new Program {
+ classes: Seq[inox.trees.ClassDef]): InoxProgram = new Program {
val trees = inox.trees
val ctx = ictx
val symbols = new inox.trees.Symbols(
functions.map(fd => fd.id -> fd).toMap,
classes.map(cd => cd.id -> cd).toMap)
}
+
+ def apply(ictx: InoxContext, sym: inox.trees.Symbols): InoxProgram = new Program {
+ val trees = inox.trees
+ val ctx = ictx
+ val symbols = sym
+ }
}
object trees extends ast.Trees {
diff --git a/src/main/scala/inox/solvers/EnumerationSolver.scala b/src/main/scala/inox/solvers/EnumerationSolver.scala
index c15e0939315d7ca3ac340f584b24fa6790668775..1863547a872fbb3f3ff62a1a56c96c078dd87d42 100644
--- a/src/main/scala/inox/solvers/EnumerationSolver.scala
+++ b/src/main/scala/inox/solvers/EnumerationSolver.scala
@@ -52,8 +52,8 @@ trait EnumerationSolver extends Solver { self =>
datagen = None
}
- def check(config: Configuration): config.Response[Model, Cores] = config.cast {
- val res: SolverResponse[Model, Cores] = try {
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions] = config.cast {
+ val res: SolverResponse[Model, Assumptions] = try {
datagen = Some(new GrammarDataGen {
val grammars: self.grammars.type = self.grammars
val evaluator: DeterministicEvaluator { val program: self.program.type } = self.evaluator
@@ -80,11 +80,7 @@ trait EnumerationSolver extends Solver { self =>
} else {
val cardinalities = allFreeVars.map(vd => typeCardinality(vd.tpe))
if (cardinalities.forall(_.isDefined) && cardinalities.flatten.product < maxTried) {
- if (config.withCores) {
- UnsatWithCores(Set.empty)
- } else {
- Unsat
- }
+ Unsat
} else {
Unknown
}
@@ -98,10 +94,15 @@ trait EnumerationSolver extends Solver { self =>
res
}
- def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Cores] = {
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = {
push()
for (c <- assumptions) assertCnstr(c)
- val res = check(config)
+ val res: config.Response[Model, Assumptions] = config.cast {
+ (check(Model min config) : SolverResponse[Model, Assumptions]) match {
+ case Unsat if config.withUnsatAssumptions => UnsatWithAssumptions(Set.empty)
+ case c => c
+ }
+ }
pop()
res
}
diff --git a/src/main/scala/inox/solvers/SimpleSolverAPI.scala b/src/main/scala/inox/solvers/SimpleSolverAPI.scala
index cd96dca50b5587a1ec806066fb559004275bd41f..2215e7a5011c4ea21482e59bedb0c52e2223e4e1 100644
--- a/src/main/scala/inox/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/inox/solvers/SimpleSolverAPI.scala
@@ -32,8 +32,8 @@ trait SimpleSolverAPI {
}
}
- def solveSATWithCores(expression: Expr, assumptions: Set[Expr]):
- ResponseWithModelAndCores[Map[ValDef, Expr], Set[Expr]] = {
+ def solveSATWithUnsatAssumptions(expression: Expr, assumptions: Set[Expr]):
+ ResponseWithModelAndAssumptions[Map[ValDef, Expr], Set[Expr]] = {
val s = factory.getNewSolver()
try {
s.assertCnstr(expression)
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 03dffbcac13bd6620ec3108ce833768899682530..ac419f0978da1033aafdc71314a55dc11bc0404f 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -11,7 +11,7 @@ object SolverOptions {
optSilentErrors,
unrolling.optUnrollFactor,
unrolling.optFeelingLucky,
- unrolling.optUnrollCores,
+ unrolling.optUnrollAssumptions,
smtlib.optCVC4Options
)
}
@@ -34,7 +34,7 @@ trait AbstractSolver extends Interruptible {
type Trees
type Model
- type Cores
+ type Assumptions = Set[Trees]
import SolverResponses._
@@ -66,8 +66,8 @@ trait AbstractSolver extends Interruptible {
def assertCnstr(expression: Trees): Unit
- def check(config: Configuration): config.Response[Model, Cores]
- def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Cores]
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions]
+ def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Assumptions]
def free(): Unit
@@ -89,7 +89,6 @@ trait Solver extends AbstractSolver {
type Trees = Expr
type Model = Map[ValDef, Expr]
- type Cores = Set[Expr]
def getResultSolver: Option[Solver] = Some(this)
}
diff --git a/src/main/scala/inox/solvers/SolverResponses.scala b/src/main/scala/inox/solvers/SolverResponses.scala
index d2ffdbdb251a0e63aa9d0351d94d84e88dda0d3e..94f375cf69c28af14e9c5b393e7f79cfe7114bd1 100644
--- a/src/main/scala/inox/solvers/SolverResponses.scala
+++ b/src/main/scala/inox/solvers/SolverResponses.scala
@@ -7,19 +7,20 @@ import scala.language.higherKinds
import scala.language.implicitConversions
object SolverResponses {
- sealed trait SolverResponse[+Model,+Cores]
+ sealed trait SolverResponse[+Model,+Assumptions]
sealed trait Satisfiable
sealed trait Unsatisfiable
+ sealed trait CheckResponse
- sealed trait SimpleResponse extends SolverResponse[Nothing, Nothing]
- sealed trait ResponseWithModel[+Model] extends SolverResponse[Model, Nothing]
- sealed trait ResponseWithCores[+Cores] extends SolverResponse[Nothing, Cores]
- sealed trait ResponseWithModelAndCores[+Model,+Cores] extends SolverResponse[Model, Cores]
+ sealed trait SimpleResponse extends SolverResponse[Nothing, Nothing] with CheckResponse
+ sealed trait ResponseWithModel[+Model] extends SolverResponse[Model, Nothing] with CheckResponse
+ sealed trait ResponseWithUnsatAssumptions[+Assumptions] extends SolverResponse[Nothing, Assumptions]
+ sealed trait ResponseWithModelAndAssumptions[+Model,+Assumptions] extends SolverResponse[Model, Assumptions]
case object Sat extends Satisfiable
with SimpleResponse
- with ResponseWithCores[Nothing]
+ with ResponseWithUnsatAssumptions[Nothing]
case object Unsat extends Unsatisfiable
with SimpleResponse
@@ -27,19 +28,19 @@ object SolverResponses {
case class SatWithModel[Model](model: Model) extends Satisfiable
with ResponseWithModel[Model]
- with ResponseWithModelAndCores[Model, Nothing]
+ with ResponseWithModelAndAssumptions[Model, Nothing]
- case class UnsatWithCores[Cores](cores: Cores) extends Unsatisfiable
- with ResponseWithCores[Cores]
- with ResponseWithModelAndCores[Nothing, Cores]
+ case class UnsatWithAssumptions[Trees](assumptions: Set[Trees]) extends Unsatisfiable
+ with ResponseWithUnsatAssumptions[Set[Trees]]
+ with ResponseWithModelAndAssumptions[Nothing, Set[Trees]]
case object Unknown extends SimpleResponse
with ResponseWithModel[Nothing]
- with ResponseWithCores[Nothing]
- with ResponseWithModelAndCores[Nothing, Nothing]
+ with ResponseWithUnsatAssumptions[Nothing]
+ with ResponseWithModelAndAssumptions[Nothing, Nothing]
object Check {
- def unapply[Core,Model](resp: SolverResponse[Core,Model]): Option[Boolean] = resp match {
+ def unapply[Model,Assumptions](resp: SolverResponse[Model,Assumptions]): Option[Boolean] = resp match {
case _: Satisfiable => Some(true)
case _: Unsatisfiable => Some(false)
case Unknown => None
@@ -49,17 +50,17 @@ object SolverResponses {
sealed trait Configuration {
type Response[+M,+C] <: SolverResponse[M,C]
def withModel: Boolean
- def withCores: Boolean
+ def withUnsatAssumptions: Boolean
def max(that: Configuration): Configuration = (this, that) match {
case (All , _ ) => All
case (_ , All ) => All
- case (Model, Cores) => All
- case (Cores, Model) => All
+ case (Model, UnsatAssumptions) => All
+ case (UnsatAssumptions, Model) => All
case (Model, _ ) => Model
case (_ , Model) => Model
- case (Cores, _ ) => Cores
- case (_ , Cores) => Cores
+ case (UnsatAssumptions, _ ) => UnsatAssumptions
+ case (_ , UnsatAssumptions) => UnsatAssumptions
case _ => Simple
}
@@ -67,61 +68,68 @@ object SolverResponses {
case (o1, o2) if o1 == o2 => o1
case (Simple, _) => Simple
case (_, Simple) => Simple
- case (Model, Cores) => Simple
- case (Cores, Model) => Simple
+ case (Model, UnsatAssumptions) => Simple
+ case (UnsatAssumptions, Model) => Simple
case (All, o) => o
case (o, All) => o
}
def cast[M, C](resp: SolverResponse[M,C]): Response[M,C] = ((this, resp) match {
- case (_, Unknown) => Unknown
- case (Simple | Cores, Sat) => Sat
- case (Model | All , s @ SatWithModel(_)) => s
- case (Simple | Model, Unsat) => Unsat
- case (Cores | All , u @ UnsatWithCores(_)) => u
+ case (_, Unknown) => Unknown
+ case (Simple | UnsatAssumptions, Sat) => Sat
+ case (Model | All, s @ SatWithModel(_)) => s
+ case (Simple | Model, Unsat) => Unsat
+ case (UnsatAssumptions | All, u @ UnsatWithAssumptions(_)) => u
case _ => throw FatalError("Unexpected response " + resp + " for configuration " + this)
}).asInstanceOf[Response[M,C]]
- def convert[M1,C1,M2,C2](resp: Response[M1,C1], cm: M1 => M2, cc: C1 => C2): Response[M2,C2] =
- cast(resp.asInstanceOf[SolverResponse[M1,C1]] match {
+ def convert[M1,T1,M2,T2](resp: Response[M1,Set[T1]], cm: M1 => M2, cc: Set[T1] => Set[T2]): Response[M2,Set[T2]] =
+ cast(resp.asInstanceOf[SolverResponse[M1,Set[T1]]] match {
case Unknown => Unknown
case Sat => Sat
case Unsat => Unsat
case SatWithModel(model) => SatWithModel(cm(model))
- case UnsatWithCores(cores) => UnsatWithCores(cc(cores))
+ case UnsatWithAssumptions(cores) => UnsatWithAssumptions(cc(cores))
})
}
object Configuration {
- def apply(model: Boolean = false, cores: Boolean = false): Configuration =
- if (model && cores) All
+ def apply(model: Boolean = false, unsatAssumptions: Boolean = false): Configuration =
+ if (model && unsatAssumptions) All
else if (model) Model
- else if (cores) Cores
+ else if (unsatAssumptions) UnsatAssumptions
else Simple
}
- case object Simple extends Configuration {
+ sealed trait CheckConfiguration extends Configuration {
+ type Response[+M,+C] <: SolverResponse[M,C] with CheckResponse
+
+ override def withUnsatAssumptions = false
+
+ override def min(that: Configuration): CheckConfiguration =
+ super.min(that).asInstanceOf[CheckConfiguration]
+ }
+
+ case object Simple extends CheckConfiguration {
type Response[+M,+C] = SimpleResponse
def withModel = false
- def withCores = false
}
- case object Model extends Configuration {
+ case object Model extends CheckConfiguration {
type Response[+M,+C] = ResponseWithModel[M]
def withModel = true
- def withCores = false
}
- case object Cores extends Configuration {
- type Response[+M,+C] = ResponseWithCores[C]
+ case object UnsatAssumptions extends Configuration {
+ type Response[+M,+C] = ResponseWithUnsatAssumptions[C]
def withModel = false
- def withCores = true
+ def withUnsatAssumptions = true
}
case object All extends Configuration {
- type Response[+M,+C] = ResponseWithModelAndCores[M, C]
+ type Response[+M,+C] = ResponseWithModelAndAssumptions[M, C]
def withModel = true
- def withCores = true
+ def withUnsatAssumptions = true
}
implicit def wideningConfiguration[M,C](config: Configuration)
diff --git a/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala b/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala
index 61c8b160557603cb40c766356937c3e8394c25d7..39a3d6a888072bb8f2b767b4c8f873f5b3e5aa41 100644
--- a/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala
@@ -30,10 +30,12 @@ trait PortfolioSolver extends Solver { self =>
override def dbg(msg: => Any) = solvers foreach (_.dbg(msg))
- private def genericCheck(config: Configuration)(f: SubSolver => config.Response[Model, Cores]): config.Response[Model, Cores] = {
+ private def genericCheck(config: Configuration)
+ (f: SubSolver => config.Response[Model, Assumptions]):
+ config.Response[Model, Assumptions] = {
reporter.debug("Running portfolio check")
// solving
- val fs: Seq[Future[(SubSolver, config.Response[Model, Cores])]] = solvers.map { s =>
+ val fs: Seq[Future[(SubSolver, config.Response[Model, Assumptions])]] = solvers.map { s =>
Future {
try {
val result = f(s)
@@ -69,11 +71,11 @@ trait PortfolioSolver extends Solver { self =>
}
- def check(config: Configuration): config.Response[Model, Cores] = {
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions] = {
genericCheck(config)(subSolver => subSolver.check(config))
}
- def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Cores] = {
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = {
genericCheck(config)(subSolver => subSolver.checkAssumptions(config)(assumptions))
}
diff --git a/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala b/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
index 4c74587a08f8d97cca91b80d371464e53f922f2c..e9b03ebc46ad3af55090d0d5d19f9201333dddbd 100644
--- a/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
+++ b/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
@@ -25,7 +25,7 @@ trait TimeoutSolver extends Solver {
this
}
- abstract override def check(config: Configuration) = {
+ abstract override def check(config: CheckConfiguration) = {
optTimeout match {
case Some(to) =>
ti.interruptAfter(to) {
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
index a93526a0f76a3018c5f9c2ce7a6eff3cff79af30..0d4449f40eda45254bea0250221bed31e3a68696 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
@@ -53,7 +53,7 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
}
}
- private def extractResponse(config: Configuration, res: SExpr): config.Response[Model, Cores] =
+ private def extractResponse(config: Configuration, res: SExpr): config.Response[Model, Assumptions] =
config.cast(res match {
case CheckSatStatus(SatStatus) =>
if (config.withModel) {
@@ -88,12 +88,12 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
Sat
}
case CheckSatStatus(UnsatStatus) =>
- if (config.withCores) {
- emit(GetUnsatCore()) match {
- case GetUnsatCoreResponseSuccess(syms) =>
- UnsatWithCores(Set.empty) // FIXME
+ if (config.withUnsatAssumptions) {
+ emit(GetUnsatAssumptions()) match {
+ case GetUnsatAssumptionsResponseSuccess(syms) =>
+ UnsatWithAssumptions(syms.flatMap(s => variables.getA(s)).toSet)
case _ =>
- UnsatWithCores(Set.empty)
+ UnsatWithAssumptions(Set.empty)
}
} else {
Unsat
@@ -102,10 +102,10 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
case e => Unknown
})
- def check(config: Configuration): config.Response[Model, Cores] =
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions] =
extractResponse(config, emit(CheckSat()))
- def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Cores] = {
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = {
val props = assumptions.toSeq.map {
case Not(v: Variable) => PropLiteral(variables.toB(v), false)
case v: Variable => PropLiteral(variables.toB(v), true)
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index eda22625b4fbf2552a06e4f90d166ce850ecedb4..2b80190248574f86db0a0c6e5450dc7e4fbec157 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -34,8 +34,6 @@ trait Templates extends TemplateGenerator
def mkEquals(l: Encoded, r: Encoded): Encoded
def mkImplies(l: Encoded, r: Encoded): Encoded
- def extractNot(e: Encoded): Option[Encoded]
-
private[unrolling] lazy val trueT = mkEncoder(Map.empty)(BooleanLiteral(true))
private var currentGen: Int = 0
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 1f89dc0cd2da738edab7e9450e290263a871c3aa..fa3816fd147764c7c16ab2579ccb78c1b2cfcd21 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -10,13 +10,13 @@ import theories._
import evaluators._
object optUnrollFactor extends InoxLongOptionDef(
- "unrollfactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
+ "unrollfactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
object optFeelingLucky extends InoxFlagOptionDef(
- "feelinglucky", "Use evaluator to find counter-examples early", false)
+ "feelinglucky", "Use evaluator to find counter-examples early", false)
-object optUnrollCores extends InoxFlagOptionDef(
- "unrollcores", "Use unsat-cores to drive unfolding while remaining fair", false)
+object optUnrollAssumptions extends InoxFlagOptionDef(
+ "unrollassumptions", "Use unsat-assumptions to drive unfolding while remaining fair", false)
trait AbstractUnrollingSolver
extends Solver {
@@ -43,16 +43,15 @@ trait AbstractUnrollingSolver
protected val underlying: AbstractSolver {
val program: AbstractUnrollingSolver.this.theories.targetProgram.type
type Trees = Encoded
- type Cores = Set[Encoded]
}
- lazy val checkModels = options.findOptionOrDefault(optCheckModels)
+ lazy val checkModels = options.findOptionOrDefault(optCheckModels)
lazy val silentErrors = options.findOptionOrDefault(optSilentErrors)
lazy val unrollFactor = options.findOptionOrDefault(optUnrollFactor)
lazy val feelingLucky = options.findOptionOrDefault(optFeelingLucky)
- lazy val unrollCores = options.findOptionOrDefault(optUnrollCores)
+ lazy val unrollAssumptions = options.findOptionOrDefault(optUnrollAssumptions)
- def check(config: Configuration): config.Response[Model, Cores] =
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions] =
checkAssumptions(config)(Set.empty)
private val constraints = new IncrementalSeq[Expr]()
@@ -256,7 +255,7 @@ trait AbstractUnrollingSolver
}
}
- def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Cores] = {
+ def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = {
val assumptionsSeq : Seq[Expr] = assumptions.toSeq
val encodedAssumptions : Seq[Encoded] = assumptionsSeq.map { expr =>
@@ -265,7 +264,7 @@ trait AbstractUnrollingSolver
}
val encodedToAssumptions : Map[Encoded, Expr] = (encodedAssumptions zip assumptionsSeq).toMap
- def encodedCoreToCore(core: Set[Encoded]): Set[Expr] = {
+ def decodeAssumptions(core: Set[Encoded]): Set[Expr] = {
core.flatMap(ast => encodedToAssumptions.get(ast) match {
case Some(n @ Not(_: Variable)) => Some(n)
case Some(v: Variable) => Some(v)
@@ -276,7 +275,7 @@ trait AbstractUnrollingSolver
import SolverResponses._
sealed abstract class CheckState
- class CheckResult(val response: config.Response[Model, Cores]) extends CheckState
+ class CheckResult(val response: config.Response[Model, Assumptions]) extends CheckState
case class Validate(model: Map[ValDef, Expr]) extends CheckState
case object ModelCheck extends CheckState
case object FiniteRangeCheck extends CheckState
@@ -285,11 +284,11 @@ trait AbstractUnrollingSolver
case object Unroll extends CheckState
object CheckResult {
- def cast(resp: SolverResponse[underlying.Model, underlying.Cores]): CheckResult =
- new CheckResult(config.convert(config.cast(resp), extractSimpleModel, encodedCoreToCore))
+ def cast(resp: SolverResponse[underlying.Model, Set[underlying.Trees]]): CheckResult =
+ new CheckResult(config.convert(config.cast(resp), extractSimpleModel, decodeAssumptions))
- def apply[M <: Model, C <: Cores](resp: config.Response[M, C]) = new CheckResult(resp)
- def unapply(res: CheckResult): Option[config.Response[Model, Cores]] = Some(res.response)
+ def apply[M <: Model, A <: Assumptions](resp: config.Response[M, A]) = new CheckResult(resp)
+ def unapply(res: CheckResult): Option[config.Response[Model, Assumptions]] = Some(res.response)
}
object Abort {
@@ -306,11 +305,11 @@ trait AbstractUnrollingSolver
reporter.debug(" - Running search...")
val checkConfig = config
- .min(Configuration(model = !templates.requiresFiniteRangeCheck, cores = true))
- .max(Configuration(model = false, cores = unrollCores))
+ .min(Configuration(model = !templates.requiresFiniteRangeCheck, unsatAssumptions = true))
+ .max(Configuration(model = false, unsatAssumptions = unrollAssumptions))
val timer = ctx.timers.solvers.check.start()
- val res: SolverResponse[underlying.Model, underlying.Cores] =
+ val res: SolverResponse[underlying.Model, Set[underlying.Trees]] =
underlying.checkAssumptions(checkConfig)(
encodedAssumptions.toSet ++ templates.satisfactionAssumptions
)
@@ -334,11 +333,8 @@ trait AbstractUnrollingSolver
case _: Unsatisfiable if !templates.canUnroll =>
CheckResult.cast(res)
- case UnsatWithCores(cores) if unrollCores =>
- for (c <- cores) templates.extractNot(c) match {
- case Some(b) => templates.promoteBlocker(b)
- case None => reporter.fatalError("Unexpected blocker polarity for unsat core unrolling: " + c)
- }
+ case UnsatWithAssumptions(assumptions) if unrollAssumptions =>
+ for (b <- assumptions) templates.promoteBlocker(b)
ProofCheck
case _ =>
@@ -355,7 +351,7 @@ trait AbstractUnrollingSolver
for (cl <- encodedAssumptions.toSeq ++ templates.satisfactionAssumptions ++ clauses) {
underlying.assertCnstr(cl)
}
- val res: SolverResponse[underlying.Model, underlying.Cores] = underlying.check(config min Model)
+ val res: SolverResponse[underlying.Model, Set[underlying.Trees]] = underlying.check(Model min config)
underlying.pop()
timer.stop()
@@ -406,7 +402,7 @@ trait AbstractUnrollingSolver
}
val timer = ctx.timers.solvers.check.start()
- val res: SolverResponse[underlying.Model, underlying.Cores] =
+ val res: SolverResponse[underlying.Model, Set[underlying.Trees]] =
underlying.checkAssumptions(config max Configuration(model = feelingLucky))(
encodedAssumptions.toSet ++ templates.refutationAssumptions
)
@@ -472,7 +468,6 @@ trait UnrollingSolver extends AbstractUnrollingSolver {
val program: theories.targetProgram.type
type Trees = Expr
type Model = Map[ValDef, Expr]
- type Cores = Set[Expr]
}
override val name = "U:"+underlying.name
@@ -500,11 +495,6 @@ trait UnrollingSolver extends AbstractUnrollingSolver {
def mkAnd(es: Expr*) = andJoin(es)
def mkEquals(l: Expr, r: Expr) = Equals(l, r)
def mkImplies(l: Expr, r: Expr) = implies(l, r)
-
- def extractNot(e: Expr): Option[Expr] = e match {
- case Not(b) => Some(b)
- case _ => None
- }
}
protected def declareVariable(v: Variable): Variable = v
diff --git a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
index cffc247a4e3874348d4cf366fd14863b63d9f816..cda80fdbe99c30665d8c3b8ff76b7e4fafc4cf5e 100644
--- a/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/AbstractZ3Solver.scala
@@ -685,13 +685,20 @@ trait AbstractZ3Solver
else Sat
case Some(false) =>
- if (config.withCores) UnsatWithCores(solver.getUnsatCore.toSet)
+ if (config.withUnsatAssumptions) UnsatWithAssumptions(
+ solver.getUnsatCore.toSet.flatMap((c: Z3AST) => z3.getASTKind(c) match {
+ case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
+ case OpNot => Some(args.head)
+ case _ => None
+ }
+ case _ => None
+ }))
else Unsat
case None => Unknown
})
- def check(config: Configuration) = extractResult(config)(solver.check)
+ def check(config: CheckConfiguration) = extractResult(config)(solver.check)
def checkAssumptions(config: Configuration)(assumptions: Set[Z3AST]) =
extractResult(config)(solver.checkAssumptions(assumptions.toSeq : _*))
@@ -712,7 +719,7 @@ trait AbstractZ3Solver
}).map(v.toVal -> _)
}
- def extractCores(cores: Set[Z3AST]): Set[Expr] = {
+ def extractUnsatAssumptions(cores: Set[Z3AST]): Set[Expr] = {
cores.flatMap { c =>
variables.getA(c).orElse(z3.getASTKind(c) match {
case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
diff --git a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
index a7ce7e3fbe8fd8b65e9448da595e24a30da6991a..8ac204fcc8382926b7861fdb39c0919e987c7692 100644
--- a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
@@ -57,14 +57,6 @@ trait NativeZ3Solver
def mkAnd(es: Z3AST*) = z3.mkAnd(es : _*)
def mkEquals(l: Z3AST, r: Z3AST) = z3.mkEq(l, r)
def mkImplies(l: Z3AST, r: Z3AST) = z3.mkImplies(l, r)
-
- def extractNot(l: Z3AST): Option[Z3AST] = z3.getASTKind(l) match {
- case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
- case OpNot => Some(args.head)
- case _ => None
- }
- case ast => None
- }
}
override def reset(): Unit = {
diff --git a/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
index 8f10f1fb25e03f0269bf9392621b9ae8c8796822..5f5b7175db5d1db5c39bb24c00860f8dccd77121 100644
--- a/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/UninterpretedZ3Solver.scala
@@ -62,14 +62,14 @@ trait UninterpretedZ3Solver
private def completeModel(model: Map[ValDef, Expr]): Map[ValDef, Expr] =
freeVars.map(v => v.toVal -> model.getOrElse(v.toVal, simplestValue(v.getType))).toMap
- def check(config: Configuration): config.Response[Model, Cores] =
+ def check(config: CheckConfiguration): config.Response[Model, Assumptions] =
config.convert(underlying.check(config),
(model: Z3Model) => completeModel(underlying.extractModel(model)),
- underlying.extractCores)
+ underlying.extractUnsatAssumptions)
override def checkAssumptions(config: Configuration)
- (assumptions: Set[Expr]): config.Response[Model, Cores] =
+ (assumptions: Set[Expr]): config.Response[Model, Assumptions] =
config.convert(underlying.checkAssumptions(config)(assumptions.map(underlying.toZ3Formula(_))),
(model: Z3Model) => completeModel(underlying.extractModel(model)),
- underlying.extractCores)
+ underlying.extractUnsatAssumptions)
}
diff --git a/src/test/scala/inox/InoxTestSuite.scala b/src/test/scala/inox/InoxTestSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1e80c083b7546ff3027e9e6a509dfda0a840b12d
--- /dev/null
+++ b/src/test/scala/inox/InoxTestSuite.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+
+import org.scalatest._
+import org.scalatest.concurrent._
+
+trait InoxTestSuite extends FunSuite with Timeouts {
+ type FixtureParam = InoxContext
+
+ val configurations: Seq[Seq[InoxOption[Any]]] = Seq(Seq.empty)
+
+ protected def test(name: String, tags: Tag*)(test: InoxContext => Outcome): Unit = {
+ for (config <- configurations) {
+ val reporter = new TestSilentReporter
+ val ctx = InoxContext(reporter, new InterruptManager(reporter), InoxOptions(config))
+ try {
+ test(ctx)
+ } catch {
+ case err: FatalError =>
+ reporter.lastErrors ++= err.msg
+ Failed(new exceptions.TestFailedException(reporter.lastErrors.mkString("\n"), err, 5))
+ }
+ }
+ }
+}
diff --git a/src/test/scala/inox/SolvingTestSuite.scala b/src/test/scala/inox/SolvingTestSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bcc837762636b561e0d7c0827dc1addab68b2408
--- /dev/null
+++ b/src/test/scala/inox/SolvingTestSuite.scala
@@ -0,0 +1,20 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+
+trait SolvingTestSuite extends InoxTestSuite {
+ import solvers._
+
+ override val configurations = for {
+ solverName <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4")
+ checkModels <- Seq(true, false)
+ feelingLucky <- Seq(true, false)
+ unrollCores <- Seq(true, false)
+ } yield Seq(
+ InoxOption(InoxOptions.optSelectedSolver)(Set(solverName)),
+ InoxOption(optCheckModels)(checkModels),
+ InoxOption(unrolling.optFeelingLucky)(feelingLucky),
+ InoxOption(unrolling.optUnrollCores)(unrollCores),
+ InoxOption(InoxOptions.optTimeout)(300)
+ )
+}
diff --git a/src/test/scala/leon/test/TestSilentReporter.scala b/src/test/scala/inox/TestSilentReporter.scala
similarity index 92%
rename from src/test/scala/leon/test/TestSilentReporter.scala
rename to src/test/scala/inox/TestSilentReporter.scala
index a7b3535a26c9d10d2c40b1df18f2f8b970be96e8..6ecd70be9dfd086160a85a82fe01e6ac598535ea 100644
--- a/src/test/scala/leon/test/TestSilentReporter.scala
+++ b/src/test/scala/inox/TestSilentReporter.scala
@@ -1,8 +1,8 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon.test
+package inox
-import leon.DefaultReporter
+import DefaultReporter
class TestSilentReporter extends DefaultReporter(Set()) {
var lastErrors: List[String] = Nil
diff --git a/src/test/scala/inox/regression/SimpleQuantifiersSuite.scala b/src/test/scala/inox/regression/SimpleQuantifiersSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..026c325342420b4f8ed8d3850a9f3db8fec0c131
--- /dev/null
+++ b/src/test/scala/inox/regression/SimpleQuantifiersSuite.scala
@@ -0,0 +1,97 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package regression
+
+class SimpleQuantifiersSuite extends SolvingTestSuite {
+ import inox.trees._
+ import dsl._
+
+ val isAssociativeID = FreshIdentifier("isAssociative")
+ val isAssociative = mkFunDef(isAssociativeID)("A") { case Seq(aT) =>
+ Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
+ forall("x" :: aT, "y" :: aT, "z" :: aT)((x,y,z) => f(f(x,y),z) === f(x,f(y,z)))
+ }
+ }
+
+ val isCommutativeID = FreshIdentifier("isCommutative")
+ val isCommutative = mkFunDef(isCommutativeID)("A") { case Seq(aT) =>
+ Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
+ forall("x" :: aT, "y" :: aT)((x,y) => f(x,y) === f(y,x))
+ }
+ }
+
+ val isRotateID = FreshIdentifier("isRotate")
+ val isRotate = mkFunDef(isRotateID)("A") { case Seq(aT) =>
+ Seq("f" :: (T(aT, aT) =>: aT)), BooleanType, { case Seq(f) =>
+ forall("x" :: aT, "y" :: aT, "z" :: aT)((x,y,z) => f(f(x,y),z) === f(f(y,z),x))
+ }
+ }
+
+ val symbols = new Symbols(Map(
+ isAssociativeID -> isAssociative,
+ isCommutativeID -> isCommutative,
+ isRotateID -> isRotate
+ ), Map.empty)
+
+ test("Pair of associative ==> associative pair") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val (aT,bT) = (T("A"), T("B"))
+ val Seq(f1,f2) = Seq("f1" :: (T(aT, aT) =>: aT), "f2" :: (T(bT, bT) =>: bT))
+ val clause = isAssociative(aT)(f1) && isAssociative(bT)(f2) && !isAssociative(T(aT,bT)) {
+ \("p1" :: T(aT,bT), "p2" :: T(aT, bT))((p1,p2) => E(f1(p1._1,p2._1), f2(p1._2,p2._2)))
+ }
+
+ val sf = SolverFactory.default(program)
+ val api = SimpleSolverAPI(sf)
+ api.solveVALID(clause) should be (Some(false))
+ }
+
+ test("Commutative and rotate ==> associative") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val aT = T("A")
+ val f = "f" :: (T(aT, aT) =>: aT)
+ val clause = isCommutative(aT)(f) && isRotate(aT)(f) && !isAssociative(aT)(f)
+
+ val sf = SolverFactory.default(program)
+ val api = SimpleSolverAPI(sf)
+ api.solveVALID(clause) should be (Some(false))
+ }
+
+ test("Commutative and rotate ==> associative (integer type)") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val f = "f" :: (T(IntegerType, IntegerType) =>: IntegerType)
+ val clause = isCommutative(IntegerType)(f) && isRotate(IntegerType)(f) && !isAssociative(IntegerType)(f)
+
+ val sf = SolverFactory.default(program)
+ val api = SimpleSolverAPI(sf)
+ api.solveVALID(clause) should be (Some(false))
+ }
+
+ test("Associatve =!=> commutative") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val aT = T("A")
+ val f = "f" :: (T(aT, aT) =>: aT)
+ val clause = isAssociative(aT)(f) && !isCommutative(aT)(f)
+
+ val sf = SolverFactory.default(program)
+ val api = SimpleSolverAPI(sf)
+ api.solveVALID(clause) should be (Some(true))
+ }
+
+ test("Commutative =!=> associative") { ctx =>
+ val program = InoxProgram(ctx, symbols)
+
+ val aT = T("A")
+ val f = "f" :: (T(aT, aT) =>: aT)
+ val clause = isCommutative(aT)(f) && !isAssociative(aT)(f)
+
+ val sf = SolverFactory.default(program)
+ val api = SimpleSolverAPI(sf)
+ api.solveVALID(clause) should be (Some(true))
+ }
+}
diff --git a/src/test/scala/inox/regression/SimpleSolversSuite.scala b/src/test/scala/inox/regression/SimpleSolversSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..175cdab263759f6500ed2f0147e28dbbcdd58865
--- /dev/null
+++ b/src/test/scala/inox/regression/SimpleSolversSuite.scala
@@ -0,0 +1,9 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package regression
+
+class SimpleSolversSuite extends InoxTestSuite {
+
+
+}
diff --git a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala b/src/test/scala/inox/unit/evaluators/EvaluatorSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
rename to src/test/scala/inox/unit/evaluators/EvaluatorSuite.scala
diff --git a/src/test/scala/leon/unit/orb/OrbUnitTestSuite.scala b/src/test/scala/inox/unit/orb/OrbUnitTestSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/orb/OrbUnitTestSuite.scala
rename to src/test/scala/inox/unit/orb/OrbUnitTestSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala b/src/test/scala/inox/unit/purescala/DefinitionTransformerSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/DefinitionTransformerSuite.scala
rename to src/test/scala/inox/unit/purescala/DefinitionTransformerSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/DependencyFinderSuite.scala b/src/test/scala/inox/unit/purescala/DependencyFinderSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/DependencyFinderSuite.scala
rename to src/test/scala/inox/unit/purescala/DependencyFinderSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/ExprOpsSuite.scala b/src/test/scala/inox/unit/purescala/ExprOpsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/ExprOpsSuite.scala
rename to src/test/scala/inox/unit/purescala/ExprOpsSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/ExtractorsSuite.scala b/src/test/scala/inox/unit/purescala/ExtractorsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/ExtractorsSuite.scala
rename to src/test/scala/inox/unit/purescala/ExtractorsSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/SimplifyLetsSuite.scala b/src/test/scala/inox/unit/purescala/SimplifyLetsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/SimplifyLetsSuite.scala
rename to src/test/scala/inox/unit/purescala/SimplifyLetsSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/TreeNormalizationsSuite.scala b/src/test/scala/inox/unit/purescala/TreeNormalizationsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/TreeNormalizationsSuite.scala
rename to src/test/scala/inox/unit/purescala/TreeNormalizationsSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/TreeTestsSuite.scala b/src/test/scala/inox/unit/purescala/TreeTestsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/TreeTestsSuite.scala
rename to src/test/scala/inox/unit/purescala/TreeTestsSuite.scala
diff --git a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala b/src/test/scala/inox/unit/purescala/TypeOpsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
rename to src/test/scala/inox/unit/purescala/TypeOpsSuite.scala
diff --git a/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala b/src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/solvers/SolverPoolSuite.scala
rename to src/test/scala/inox/unit/solvers/SolverPoolSuite.scala
diff --git a/src/test/scala/leon/unit/synthesis/AlgebraSuite.scala b/src/test/scala/inox/unit/synthesis/AlgebraSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/synthesis/AlgebraSuite.scala
rename to src/test/scala/inox/unit/synthesis/AlgebraSuite.scala
diff --git a/src/test/scala/leon/unit/synthesis/LinearEquationsSuite.scala b/src/test/scala/inox/unit/synthesis/LinearEquationsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/synthesis/LinearEquationsSuite.scala
rename to src/test/scala/inox/unit/synthesis/LinearEquationsSuite.scala
diff --git a/src/test/scala/leon/unit/utils/BijectionSuite.scala b/src/test/scala/inox/unit/utils/BijectionSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/utils/BijectionSuite.scala
rename to src/test/scala/inox/unit/utils/BijectionSuite.scala
diff --git a/src/test/scala/leon/unit/utils/FunctionClosureSuite.scala b/src/test/scala/inox/unit/utils/FunctionClosureSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/utils/FunctionClosureSuite.scala
rename to src/test/scala/inox/unit/utils/FunctionClosureSuite.scala
diff --git a/src/test/scala/leon/unit/utils/GraphsSuite.scala b/src/test/scala/inox/unit/utils/GraphsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/utils/GraphsSuite.scala
rename to src/test/scala/inox/unit/utils/GraphsSuite.scala
diff --git a/src/test/scala/leon/unit/utils/IncrementalBijectionSuite.scala b/src/test/scala/inox/unit/utils/IncrementalBijectionSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/utils/IncrementalBijectionSuite.scala
rename to src/test/scala/inox/unit/utils/IncrementalBijectionSuite.scala
diff --git a/src/test/scala/leon/unit/utils/StreamsSuite.scala b/src/test/scala/inox/unit/utils/StreamsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/utils/StreamsSuite.scala
rename to src/test/scala/inox/unit/utils/StreamsSuite.scala
diff --git a/src/test/scala/leon/unit/utils/UtilsSuite.scala b/src/test/scala/inox/unit/utils/UtilsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/utils/UtilsSuite.scala
rename to src/test/scala/inox/unit/utils/UtilsSuite.scala
diff --git a/src/test/scala/leon/unit/xlang/EffectsAnalysisSuite.scala b/src/test/scala/inox/unit/xlang/EffectsAnalysisSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/xlang/EffectsAnalysisSuite.scala
rename to src/test/scala/inox/unit/xlang/EffectsAnalysisSuite.scala
diff --git a/src/test/scala/leon/unit/xlang/ExprOpsSuite.scala b/src/test/scala/inox/unit/xlang/ExprOpsSuite.scala
similarity index 100%
rename from src/test/scala/leon/unit/xlang/ExprOpsSuite.scala
rename to src/test/scala/inox/unit/xlang/ExprOpsSuite.scala
diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
deleted file mode 100644
index 58ee74149ff3e5a00f938ea1087478acdfe5a1ae..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/genc/GenCSuite.scala
+++ /dev/null
@@ -1,219 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package genc
-
-import leon.test.LeonRegressionSuite
-
-import leon.frontends.scalac.ExtractionPhase
-import leon.regression.verification.XLangVerificationSuite
-import leon.purescala.Definitions.Program
-import leon.utils.{ PreprocessingPhase, UniqueCounter }
-
-import scala.concurrent._
-import ExecutionContext.Implicits.global
-import scala.sys.process._
-
-import org.scalatest.{ Args, Status }
-
-import java.io.ByteArrayInputStream
-import java.nio.file.{ Files, Path }
-
-class GenCSuite extends LeonRegressionSuite {
-
- private val testDir = "regression/genc/"
- private lazy val tmpDir = Files.createTempDirectory("genc")
- private val ccflags = "-std=c99 -g -O0"
- private val maxExecutionTime = 2 // seconds
-
- private val counter = new UniqueCounter[Unit]
- counter.nextGlobal // Start with 1
-
- private case class ExtendedContext(leon: LeonContext, tmpDir: Path, progName: String)
-
- // Tests are run as follows:
- // - before mkTest is run, all valid test are verified using XLangVerificationSuite
- // - The classic ExtractionPhase & PreprocessingPhase are run on all input files
- // (this way the libraries are evaluated only once)
- // - A Program is constructed for each input file
- // - At this point no error should have occurred or something would be wrong
- // with the extraction phases
- // - For each Program P:
- // + if P is expected to be convertible to C, then we make sure that:
- // * the GenerateCPhase run without trouble,
- // * the generated C code compiles using a C99 compiler without error,
- // * and that, when run, the exit code is 0
- // + if P is expected to be non-convertible to C, then we make sure that:
- // * the GenerateCPhase fails
- private def mkTest(files: List[String], cat: String)(block: (ExtendedContext, Program) => Unit) = {
- val extraction =
- ExtractionPhase andThen
- new PreprocessingPhase(genc = true)
-
- val ctx = createLeonContext(files:_*)
-
- try {
- val (_, ast) = extraction.run(ctx, files)
-
- val programs = {
- val (user, lib) = ast.units partition { _.isMainUnit }
- user map ( u => Program(u :: lib) )
- }
-
- for { prog <- programs } {
- val name = prog.units.head.id.name
- val ctx = createLeonContext(s"--o=$tmpDir/$name.c")
- val xCtx = ExtendedContext(ctx, tmpDir, name)
-
- val displayName = s"$cat/$name.scala"
- val index = counter.nextGlobal
-
- test(f"$index%3d: $displayName") {
- block(xCtx, prog)
- }
- }
- } catch {
- case fe: LeonFatalError =>
- test("Compilation") {
- fail(ctx, "Unexpected fatal error while setting up tests", fe)
- }
- }
- }
-
- // Run a process with a timeout and return the status code
- private def runProcess(pb: ProcessBuilder): Int = runProcess(pb.run)
- private def runProcess(p: Process): Int = {
- val f = Future(blocking(p.exitValue()))
- try {
- Await.result(f, duration.Duration(maxExecutionTime, "sec"))
- } catch {
- case _: TimeoutException =>
- p.destroy()
- throw LeonFatalError("timeout reached")
- }
- }
-
- // Determine which C compiler is available
- private def detectCompiler: Option[String] = {
- val testCode = "int main() { return 0; }"
- val testBinary = s"$tmpDir/test"
-
- // NOTE this code might print error on stderr when a non-existing compiler
- // is used. It seems that even with a special ProcessLogger the RuntimeException
- // is printed for some reason.
-
- def testCompiler(cc: String): Boolean = try {
- def input = new ByteArrayInputStream(testCode.getBytes())
- val process = s"$cc $ccflags -o $testBinary -xc -" #< input #&& s"$testBinary"
- runProcess(process) == 0
- } catch {
- case _: java.lang.RuntimeException => false
- }
-
- val knownCompiler = "cc" :: "clang" :: "gcc" :: "mingw" :: Nil
- // Note that VS is not in the list as we cannot specify C99 dialect
-
- knownCompiler find testCompiler
- }
-
- private def convert(xCtx: ExtendedContext)(prog: Program) = {
- try {
- GenerateCPhase(xCtx.leon, prog)
- } catch {
- case fe: LeonFatalError =>
- fail(xCtx.leon, "Convertion to C unexpectedly failed", fe)
- }
- }
-
- private def saveToFile(xCtx: ExtendedContext)(cprog: CAST.Prog) = {
- CFileOutputPhase(xCtx.leon, cprog)
- }
-
- private def compile(xCtx: ExtendedContext, cc: String)(unused: Unit) = {
- val basename = s"${xCtx.tmpDir}/${xCtx.progName}"
- val sourceFile = s"$basename.c"
- val compiledProg = basename
-
- val process = Process(s"$cc $ccflags $sourceFile -o $compiledProg")
- val status = runProcess(process)
-
- assert(status == 0, "Compilation of converted program failed")
- }
-
- private def evaluate(xCtx: ExtendedContext)(unused: Unit) = {
- val compiledProg = s"${xCtx.tmpDir}/${xCtx.progName}"
-
- // TODO memory limit
- val process = Process(compiledProg)
-
- val status = runProcess(process)
- assert(status == 0, s"Evaluation of converted program failed with status [$status]")
- }
-
- private def forEachFileIn(cat: String)(block: (ExtendedContext, Program) => Unit) {
- val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
-
- fs foreach { file =>
- assert(file.exists && file.isFile && file.canRead,
- s"Benchmark ${file.getName} is not a readable file")
- }
-
- val files = fs map { _.getPath }
-
- mkTest(files, cat)(block)
- }
-
- protected def testDirectory(cc: String, dir: String) = forEachFileIn(dir) { (xCtx, prog) =>
- val converter = convert(xCtx) _
- val saver = saveToFile(xCtx) _
- val compiler = compile(xCtx, cc) _
- val evaluator = evaluate(xCtx) _
-
- val pipeline = converter andThen saver andThen compiler andThen evaluator
-
- pipeline(prog)
- }
-
- protected def testValid(cc: String) = testDirectory(cc, "valid")
- protected def testUnverified(cc: String) = testDirectory(cc, "unverified");
-
- protected def testInvalid() = forEachFileIn("invalid") { (xCtx, prog) =>
- intercept[LeonFatalError] {
- GenerateCPhase(xCtx.leon, prog)
- }
- }
-
- class AltVerificationSuite(override val testDir: String) extends XLangVerificationSuite {
- override def testAll() = testValid() // Test only the valid ones
-
- override def suiteName = "Verification Suite For GenC"
-
- // Add a timeout for the verification
- override val optionVariants = List(List("--solvers=smt-z3,ground"))
- }
-
- // Run verification suite as a nested suite
- override def nestedSuites = {
- // Use our test dir and not the one from XLangVerificationSuite
- scala.collection.immutable.IndexedSeq(new AltVerificationSuite(testDir))
- }
-
- protected def testAll() = {
- // Set C compiler according to the platform we're currently running on
- detectCompiler match {
- case Some(cc) =>
- testValid(cc)
- testUnverified(cc)
- case None =>
- test("dectecting C compiler") { fail("no C compiler found") }
- }
-
- testInvalid()
- }
-
- override def run(testName: Option[String], args: Args): Status = {
- testAll()
- super.run(testName, args)
- }
-}
-
diff --git a/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala
deleted file mode 100644
index 12bc15f0a07128f1f1569a5c8cd63c02b3dd27cb..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala
+++ /dev/null
@@ -1,113 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.evaluators
-
-import leon.test._
-import helpers.ExpressionsDSLProgram
-import leon.evaluators._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import org.scalatest.Matchers
-
-class AbstractEvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSLProgram with Matchers {
- //override def a = super[ExpressionsDSL].a
-
- val sources = List("""
-import leon.lang._
-
-object AbstractTests {
- abstract class Tree
- case class Node(w: Tree, x: Int, y: Tree) extends Tree
- case class Leaf() extends Tree
-
- def param(x: String) = x + x
-
- def test() = {
- val x = "19"
- val w = 9
- val y = () => w*w+5
- val z = y().toString
- val res = param(x) + z
- res
- }
-
- def test2(right: Boolean, c: Tree): Int = {
- if(right) {
- c match {
- case Leaf() => 0
- case Node(_, a, Leaf()) => a
- case Node(_, _, n) => test2(right, n)
- }
- } else {
- c match {
- case Leaf() => 0
- case Node(Leaf(), a, _) => a
- case Node(n, _, _) => test2(right, n)
- }
- }
- }
-}""")
-
- test("Abstract evaluator should keep track of variables") { implicit fix =>
- val testFd = funDef("AbstractTests.test")
-
- val ae = new AbstractEvaluator(fix._1, fix._2)
-
- val res = ae.eval(FunctionInvocation(testFd.typed, Seq()))
-
- res.result match {
- case Some((e, expr)) =>
- e should equal (StringLiteral("191986"))
- expr should equal (StringConcat(StringConcat(StringLiteral("19"), StringLiteral("19")), Int32ToString(BVPlus(BVTimes(IntLiteral(9), IntLiteral(9)), IntLiteral(5)))))
- case None =>
- fail("No result!")
- }
- }
-
-
- test("AbstractOnly evaluator should keep track of variables") { implicit fix =>
- val testFd = funDef("AbstractTests.test")
-
- val aeOnly = new AbstractOnlyEvaluator(fix._1, fix._2)
-
- val res2 = aeOnly.eval(FunctionInvocation(testFd.typed, Seq()))
-
- res2.result match {
- case Some(expr) =>
- expr should equal (StringConcat(StringConcat(StringLiteral("19"), StringLiteral("19")), Int32ToString(BVPlus(BVTimes(IntLiteral(9), IntLiteral(9)), IntLiteral(5)))))
- case None =>
- fail("No result!")
- }
- }
-
- test("Abstract evaluator should correctly handle boolean and recursive") { implicit fix =>
- val testFd = funDef("AbstractTests.test2")
- val Leaf = cc("AbstractTests.Leaf")()
- def Node(left: Expr, n: Expr, right: Expr) = cc("AbstractTests.Node")(left, n, right)
- val NodeDef = classDef("AbstractTests.Node")
- val NodeType = classType("AbstractTests.Node", Seq()).asInstanceOf[CaseClassType]
-
- val ae = new AbstractEvaluator(fix._1, fix._2)
- ae.evaluateCaseClassSelector = false
-
- val input = Node(Leaf, IntLiteral(5), Leaf)
-
- val res = ae.eval(FunctionInvocation(testFd.typed, Seq(BooleanLiteral(true), input))).result match {
- case Some((e, expr)) =>
- e should equal (IntLiteral(5))
- expr should equal (CaseClassSelector(NodeType, input, NodeDef.fieldsIds(1)))
- case None =>
- fail("No result!")
- }
- val a = id("a", Int32Type)
- val input2 = Node(Leaf, Variable(a), Leaf)
- ae.eval(FunctionInvocation(testFd.typed, Seq(BooleanLiteral(true), input2))).result match {
- case Some((e, expr)) =>
- e should equal (Variable(a))
- expr should equal (CaseClassSelector(NodeType, input2, NodeDef.fieldsIds(1)))
- case None =>
- fail("No result!")
- }
- }
-}
diff --git a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
deleted file mode 100644
index e0e1b2b85b35b03170660730c41ea06183eaaf0a..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/evaluators/CodegenEvaluatorSuite.scala
+++ /dev/null
@@ -1,349 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.evaluators
-
-import leon.test._
-import leon.evaluators._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.codegen._
-
-class CodegenEvaluatorSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL{
-
- val sources = List("""
- import leon.lang._
-
- object simple {
- abstract class Abs
- case class Conc(x : Int) extends Abs
- def test = {
- val c = Conc(1)
- c.x
-
- }
- }
- object simple2 {
- abstract class Abs
- case class Conc(x : BigInt) extends Abs
- def test = {
- val c = Conc(1)
- c.x
- }
- }
- object eager {
- abstract class Abs() {
- val foo = 42
- }
- case class Conc(x : Int) extends Abs()
- def foo = {
- val c = Conc(1)
- c.foo + c.x
- }
- def test = foo
- }
- object thiss {
-
- case class Bar() {
- def boo = this
- def toRet = 42
- }
-
- def test = Bar().boo.toRet
- }
- object oldStuff {
- def test = 1
- case class Bar() {
- def boo = 2
- }
- }
- object methSimple {
-
- sealed abstract class Ab {
- def f2(x : Int) = x + 5
- }
- case class Con() extends Ab { }
-
- def test = Con().f2(5)
- }
- object methSimple2 {
-
- val x: BigInt = 42
-
- def test = x
-
- }
- object methSimple3 {
-
- sealed abstract class Ab {
- def f2(x : BigInt): BigInt = x + 5
- }
- case class Con() extends Ab { }
-
- def test = Con().f2(5)
- }
- object methSimple4 {
-
- sealed abstract class Ab {
- def f2(x : BigInt): BigInt = x + BigInt(2000000000)
- }
- case class Con() extends Ab { }
-
- def test = Con().f2(2000000000)
- }
- object bigint1 {
-
- def f(x: BigInt): BigInt = ((x * 2) - 10)/2
-
- def test = f(12)
- }
- object bigint2 {
-
- def f(x: BigInt): Boolean = x == BigInt(17)
-
- def test = f(17)
- }
- object bigint3 {
-
- def f(x: BigInt): BigInt = if(x <= 0) -x else x
-
- def test = f(-17)
- }
- object bigint4 {
-
- def f(x: BigInt): BigInt = if(x < 0) -x else x
-
- def test = f(-12)
- }
- object bigint5 {
-
- def f(x: BigInt): BigInt = if(x >= 0) -x else x
-
- def test = f(-7)
- }
- object methods {
- def f1 = 4
- sealed abstract class Ab {
- def f2(x : Int) = Cs().f3(1,2) + f1 + x + 5
- }
- case class Con() extends Ab {}
- case class Cs() {
- def f3(x : Int, y : Int) = x + y
- }
- def test = Con().f2(3)
- }
- object lazyFields {
- def foo = 1
- sealed abstract class Ab {
- lazy val x : Int = this match {
- case Conc(t) => t + 1
- case Conc2(t) => t+2
- }
- }
- case class Conc(t : Int) extends Ab { }
- case class Conc2(t : Int) extends Ab { }
- def test = foo + Conc(5).x + Conc2(6).x
- }
- object modules {
- def foo = 1
- val bar = 2
- lazy val baz = 0
- def test = foo + bar + baz
- }
- object lazyISLazy {
- abstract class Ab { lazy val x : Int = foo; def foo : Int = foo }
- case class Conc() extends Ab { }
- def test = { val willNotLoop = Conc(); 42 }
- }
- object ListWithSize {
- abstract class List[T] {
- val length : Int = this match {
- case Nil() => 0
- case Cons (_, xs ) => 1 + xs.length
- }
-
- }
- case class Cons[T](hd : T, tl : List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
-
- val l = Cons(1, Cons(2, Cons(3, Nil())))
-
- def test = l.length + Nil[Int]().length
- }
- object ListWithSumMono {
- abstract class List
- case class Cons(hd : Int, tl : List) extends List
- case class Nil() extends List
-
- def sum (l : List) : Int = l match {
- case Nil() => 0
- case Cons(x, xs) => x + sum(xs)
- }
-
- val l = Cons(1, Cons(2, Cons(3, Nil())))
-
- def test = sum(l)
- }
- object poly {
- case class Poly[T](poly : T)
- def ex = Poly(42)
- def test = ex.poly
- }
- object ListHead {
- abstract class List[T]
- case class Cons[T](hd : T, tl : List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
- def l = Cons(1, Cons(2, Cons(3, Nil())))
-
- def test = l.hd
- }
- object ListWithSum {
- abstract class List[T]
- case class Cons[T](hd : T, tl : List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
- def sum (l : List[Int]) : Int = l match {
- case Nil() => 0
- case Cons(x, xs) => x + sum(xs)
- }
-
- val l = Cons(1, Cons(2, Cons(3, Nil())))
-
- def test = sum(l)
- }
- object lazyLoops {
- abstract class Ab { lazy val x : Int = foo; def foo : Int = foo }
- case class Conc() extends Ab { }
- def test = Conc().x
- }
- object Lazier {
- import leon.lang._
- abstract class List[T] {
- lazy val tail = this match {
- case Nil() => error[List[T]]("Nil.tail")
- case Cons(_, tl) => tl
- }
- }
- case class Cons[T](hd : T, tl : List[T]) extends List[T]
- case class Nil[T]() extends List[T]
-
- def sum (l : List[Int]) : Int = l match {
- case Nil() => 0
- case c : Cons[Int] => c.hd + sum(c.tail)
- }
-
- val l = Cons(1, Cons(2, Cons(3, Nil())))
-
- def test = sum(l)
- }
- object SetToList {
- import leon.collection._
- def test = {
- val s = Set(1, 2, 3, 4, 5)
- val s2 = setToList(s).content
- s == s2
- }
- }
- object Overrides1 {
- abstract class A {
- def x = true
- }
- case class B() extends A {
- override def x = false
- }
- case class C() extends A
-
- def test = (B().x, C().x)
- }
- object Overrides2 {
- abstract class A {
- val x = true
- }
- case class B() extends A {
- override val x = false
- }
- case class C() extends A
-
- def test = (B().x, C().x)
- }
- object Arrays1 {
- def test = {
- val x = 1
- val y = 42
- val a = Array.fill(y)(x)
- a(0) + a(41)
- }
- }
-
- object Arrays2 {
- def test = {
- val x = 1
- val a = Array(x, x+1, x+2, x+3)
- a(0) + a(1) + a(2) + a(3)
- }
- }
- """)
-
- val results = Seq(
- "simple" -> IntLiteral(1),
- "simple2" -> InfiniteIntegerLiteral(1),
- "eager" -> IntLiteral(43),
- "thiss" -> IntLiteral(42) ,
- "oldStuff" -> IntLiteral(1),
- "methSimple" -> IntLiteral(10),
- "methSimple2" -> InfiniteIntegerLiteral(42),
- "methSimple3" -> InfiniteIntegerLiteral(10),
- "methSimple4" -> InfiniteIntegerLiteral(BigInt("4000000000")),
- "bigint1" -> InfiniteIntegerLiteral(BigInt(7)),
- "bigint2" -> BooleanLiteral(true),
- "bigint3" -> InfiniteIntegerLiteral(BigInt(17)),
- "bigint4" -> InfiniteIntegerLiteral(BigInt(12)),
- "bigint5" -> InfiniteIntegerLiteral(BigInt(-7)),
- "methods" -> IntLiteral(15),
- "lazyFields" -> IntLiteral(1 + 5 + 1 + 6 + 2),
- "modules" -> IntLiteral(1 + 2 + 0),
- "lazyISLazy" -> IntLiteral(42),
- "ListWithSize" -> IntLiteral(3),
- "ListWithSumMono" -> IntLiteral(1 + 2 + 3),
- "poly" -> IntLiteral(42),
- "ListHead" -> IntLiteral(1),
- "ListWithSum" -> IntLiteral(1 + 2 + 3),
- "lazyLoops" -> Error(Untyped, "Looping"),// This one loops!
- "Lazier" -> IntLiteral(1 + 2 + 3),
- "SetToList" -> BooleanLiteral(true),
- "Overrides1" -> Tuple(Seq(BooleanLiteral(false), BooleanLiteral(true))),
- "Overrides2" -> Tuple(Seq(BooleanLiteral(false), BooleanLiteral(true))),
- "Arrays1" -> IntLiteral(2),
- "Arrays2" -> IntLiteral(10)
- )
-
- for {
- (name, exp) <- results
- requireMonitor <- Seq(false, true)
- doInstrument <- Seq(false,true)
- } {
- val opts = (if(requireMonitor) "monitor " else "") +
- (if(doInstrument) "instrument" else "")
-
- val testName = f"$name%-20s $opts%-18s"
-
- test("Evaluation of "+testName) { implicit fix =>
- val eval = new CodeGenEvaluator(fix._1, fix._2, params = CodeGenParams(
- maxFunctionInvocations = if (requireMonitor) 1000 else -1, // Monitor calls and abort execution if more than X calls
- checkContracts = true, // Generate calls that checks pre/postconditions
- doInstrument = doInstrument // Instrument reads to case classes (mainly for vanuatoo)
- ))
-
- (eval.eval(fcall(name + ".test")()).result, exp) match {
- case (Some(res), exp) =>
- assert(res === exp)
- case (None, Error(_, _)) =>
- // OK
- case _ =>
- fail("")
- }
- }
- }
-}
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
deleted file mode 100644
index e0c1537166cdca38c05c430df0f6bd3e5a5621d0..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ /dev/null
@@ -1,500 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.evaluators
-
-import leon._
-import leon.test._
-import leon.test.helpers._
-import leon.evaluators.{Evaluator => _, DeterministicEvaluator => Evaluator, _}
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.codegen._
-
-class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
-
- val sources = List(
- """|object CaseClasses {
- | sealed abstract class List
- | case class Nil() extends List
- | case class Cons(head : Int, tail : List) extends List
- |
- | case class MySingleton(i : Int)
- |
- | def size(l : List) : Int = l match {
- | case Nil() => 0
- | case Cons(_, xs) => 1 + size(xs)
- | }
- |
- | def compare(l1 : List, l2 : List) : Boolean = (l1 == l2)
- |
- | def head(l : List) : Int = l match {
- | case Cons(h, _) => h
- | }
- |
- | def wrap(i : Int) : MySingleton = MySingleton(i)
- |}""".stripMargin,
-
- """|import leon.lang._
- |object Sets {
- | sealed abstract class List
- | case class Nil() extends List
- | case class Cons(head : Int, tail : List) extends List
- |
- | def content(l : List) : Set[Int] = l match {
- | case Nil() => Set.empty[Int]
- | case Cons(x, xs) => Set(x) ++ content(xs)
- | }
- |
- | def finite() : Set[Int] = Set(1, 2, 3)
- | def build(x : Int, y : Int, z : Int) : Set[Int] = Set(x, y, z)
- | def add(s1 : Set[Int], e: Int) : Set[Int] = s1 + e
- | def union(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 ++ s2
- | def inter(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 & s2
- | def diff(s1 : Set[Int], s2 : Set[Int]) : Set[Int] = s1 -- s2
- |}""".stripMargin,
-
- """|import leon.lang._
- |object Bags {
- | sealed abstract class List
- | case class Nil() extends List
- | case class Cons(head : Int, tail : List) extends List
- |
- | def content(l : List) : Bag[Int] = l match {
- | case Nil() => Bag.empty[Int]
- | case Cons(x, xs) => content(xs) + x
- | }
- |
- | def finite() : Bag[Int] = Bag((1, 1), (2, 2), (3, 3))
- | def add(s1 : Bag[Int], e: Int) : Bag[Int] = s1 + e
- | def union(s1 : Bag[Int], s2 : Bag[Int]) : Bag[Int] = s1 ++ s2
- | def inter(s1 : Bag[Int], s2 : Bag[Int]) : Bag[Int] = s1 & s2
- | def diff(s1 : Bag[Int], s2 : Bag[Int]) : Bag[Int] = s1 -- s2
- |}""".stripMargin,
-
- """|import leon.lang._
- |object Maps {
- | sealed abstract class PList
- | case class PNil() extends PList
- | case class PCons(headfst : Int, headsnd : Int, tail : PList) extends PList
- |
- | def toMap(pl : PList) : Map[Int,Int] = pl match {
- | case PNil() => Map.empty[Int,Int]
- | case PCons(f,s,xs) => toMap(xs).updated(f, s)
- | }
- |
- | def finite0() : Map[Int,Int] = Map[Int, Int]()
- | def finite1() : Map[Int,Int] = Map(1 -> 2)
- | def finite2() : Map[Int,Int] = Map(2 -> 3, 1 -> 2)
- | def finite3() : Map[Int,Int] = finite1().updated(2, 3)
- |}""".stripMargin,
-
- """|import leon.lang._
- |object Sets2 {
- | case class MyPair(x : Int, y : Boolean)
- |
- | def buildPairCC(x : Int, y : Boolean) : MyPair = MyPair(x,y)
- | def mkSingletonCC(p : MyPair) : Set[MyPair] = Set(p)
- | def containsCC(s : Set[MyPair], p : MyPair) : Boolean = s.contains(p)
- |
- | def buildPairT(x : Int, y : Boolean) : (Int,Boolean) = (x,y)
- | def mkSingletonT(p : (Int,Boolean)) : Set[(Int,Boolean)] = Set(p)
- | def containsT(s : Set[(Int,Boolean)], p : (Int,Boolean)) : Boolean = s.contains(p)
- |}""".stripMargin,
-
- """|import leon.lang._
- |import leon.lang.synthesis._
- |object Choose {
- | def c(i : Int) : Int = choose { (j : Int) => j > i && j < i + 2 }
- |}
- |""".stripMargin,
-
- """|import leon.lang._
- |object Recursion {
- | import leon.lang._
- |
- | def c(i : Int) : Int = c(i-1)
- |}
- |""".stripMargin,
-
- """|import leon.lang._
- |object Contracts {
- |
- | def c(i : Int) : Int = {
- | require(i > 0);
- | c(i-1)
- | }
- |}
- |""".stripMargin,
-
- """|import leon.lang._
- |object PatMat {
- | abstract class List;
- | case class Cons(h: Int, t: List) extends List;
- | case object Nil extends List;
- |
- | def f1: Int = (Cons(1, Nil): List) match {
- | case Cons(h, t) => h
- | case Nil => 0
- | }
- |
- | def f2: Int = (Cons(1, Nil): List) match {
- | case Cons(h, _) => h
- | case Nil => 0
- | }
- |
- | def f3: Int = (Nil: List) match {
- | case _ => 1
- | }
- |
- | def f4: Int = (Cons(1, Cons(2, Nil)): List) match {
- | case a: Cons => 1
- | case _ => 0
- | }
- |
- | def f5: Int = ((Cons(1, Nil), Nil): (List, List)) match {
- | case (a: Cons, _) => 1
- | case _ => 0
- | }
- |
- | def f6: Int = (Cons(2, Nil): List) match {
- | case Cons(h, t) if h > 0 => 1
- | case _ => 0
- | }
- |}""".stripMargin,
-
- """import leon.lang._
- |object Lambda {
- | val foo1 = (x: BigInt) => x
- | val foo2 = {
- | val a = BigInt(1)
- | (x: BigInt) => a + x
- | }
- | val foo3 = {
- | val f1 = (x: BigInt) => x + 1
- | val f2 = (x: BigInt) => x + 2
- | (x: BigInt, y: BigInt) => f1(x) + f2(y)
- | }
- | def foo4(x: BigInt) = (i: BigInt) => i + x
- |}""".stripMargin,
-
- """object Methods {
- | abstract class A
- |
- | abstract class B extends A {
- | def foo(i: BigInt) = {
- | require(i > 0)
- | i + 1
- | } ensuring ( _ >= 0 )
- | }
- |
- | case class C(x: BigInt) extends B {
- | val y = BigInt(42)
- | override def foo(i: BigInt) = {
- | x + y + (if (i>0) i else -i)
- | } ensuring ( _ >= x )
- | }
- |
- | case class D() extends A
- |
- | def f1 = {
- | val c = C(42)
- | (if (c.foo(0) + c.x > 0) c else D()).isInstanceOf[B]
- | }
- | def f2 = D().isInstanceOf[B]
- | def f3 = C(42).isInstanceOf[A]
- |}""".stripMargin,
-
- """import leon.lang._
- |import leon.collection._
- |
- |object Foo {
- | def unapply(i: BigInt): Option[BigInt] = if (i > 0) Some(i) else None()
- |}
- |
- |object Unapply {
- | def foo =
- | (BigInt(1) match {
- | case Foo(i) => i
- | case _ => BigInt(0)
- | }) + (BigInt(-12) match {
- | case Foo(i) => i
- | case _ => BigInt(2)
- | })
- |
- | def size[A](l: List[A]): BigInt = l match {
- | case _ :: _ :: _ :: Nil() => 3
- | case _ :: _ :: Nil() => 2
- | case _ :: Nil() => 1
- | case Nil() => 0
- | case _ :: _ => 42
- | }
- |
- | def s1 = size(1 :: 2 :: 3 :: Nil[Int]())
- | def s2 = size(Nil[Int]())
- | def s3 = size(List(1,2,3,4,5,6,7,8))
- |
- |}
- """.stripMargin,
-
- """object Casts1 {
- | abstract class Foo
- | case class Bar1(v: BigInt) extends Foo
- | case class Bar2(v: BigInt) extends Foo
- | case class Bar3(v: BigInt) extends Foo
- |
- | def test(a: Foo): BigInt = {
- | if (a.isInstanceOf[Bar1]) {
- | a.asInstanceOf[Bar1].v
- | } else {
- | a.asInstanceOf[Bar2].v
- | }
- | }
- |}""".stripMargin
- )
-
- def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
- List(
- new DefaultEvaluator(ctx, pgm),
- new AngelicEvaluator(new StreamEvaluator(ctx, pgm))
- )
- }
-
- def codegenEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
- List(
- new CodeGenEvaluator(ctx, pgm)
- )
- }
-
- def allEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
- normalEvaluators ++ codegenEvaluators
- }
-
- test("Case classes") { implicit fix =>
- val nil = cc("CaseClasses.Nil")()
- def cons(es: Expr*) = cc("CaseClasses.Cons")(es: _*)
-
- val cons12a = cons(i(1), cons(i(2), nil))
- val cons12b = cons(i(1), cons(i(2), nil))
- val sing1 = cc("CaseClasses.MySingleton")(i(1))
-
- for(e <- allEvaluators) {
- eval(e, fcall("CaseClasses.size")(nil)) === i(0)
- eval(e, fcall("CaseClasses.size")(cons12a)) === i(2)
- eval(e, fcall("CaseClasses.compare")(nil, cons12a)) === F
- eval(e, fcall("CaseClasses.compare")(cons12a, cons12b)) === T
- eval(e, fcall("CaseClasses.head")(cons12a)) === i(1)
-
- eval(e, Equals(fcall("CaseClasses.wrap")(i(1)), sing1)) === T
-
- // Match error
- eval(e, fcall("CaseClasses.head")(nil)).failed
- }
- }
-
- test("Sets") { implicit fix =>
- val nil = cc("Sets.Nil")()
- def cons(es: Expr*) = cc("Sets.Cons")(es: _*)
-
- val cons12 = cons(i(1), cons(i(2), nil))
-
- val es = FiniteSet(Set(), Int32Type)
- val s2 = FiniteSet(Set(i(2)), Int32Type)
- val s12 = FiniteSet(Set(i(1), i(2)), Int32Type)
- val s13 = FiniteSet(Set(i(1), i(3)), Int32Type)
- val s46 = FiniteSet(Set(i(4), i(6)), Int32Type)
- val s123 = FiniteSet(Set(i(1), i(2), i(3)), Int32Type)
- val s246 = FiniteSet(Set(i(2), i(4), i(6)), Int32Type)
- val s12346 = FiniteSet(Set(i(1), i(2), i(3), i(4), i(6)), Int32Type)
-
- for(e <- allEvaluators) {
- eval(e, fcall("Sets.finite")()) === s123
- eval(e, fcall("Sets.content")(nil)) === es
- eval(e, fcall("Sets.content")(cons12)) === s12
- eval(e, fcall("Sets.build")(i(1), i(2), i(3))) === s123
- eval(e, fcall("Sets.build")(i(1), i(2), i(2))) === s12
- eval(e, fcall("Sets.add")(s12, i(2))) === s12
- eval(e, fcall("Sets.add")(s12, i(3))) === s123
- eval(e, fcall("Sets.union")(s123, s246)) === s12346
- eval(e, fcall("Sets.union")(s246, s123)) === s12346
- eval(e, fcall("Sets.inter")(s123, s246)) === s2
- eval(e, fcall("Sets.inter")(s246, s123)) === s2
- eval(e, fcall("Sets.diff")(s123, s246)) === s13
- eval(e, fcall("Sets.diff")(s246, s123)) === s46
-
- eval(e, Equals(fcall("Sets.union")(s123, s246), fcall("Sets.union")(s246, s123))) === T
- eval(e, Equals(fcall("Sets.inter")(s123, s246), fcall("Sets.inter")(s246, s123))) === T
- eval(e, Equals(fcall("Sets.diff")(s123, s246), fcall("Sets.diff")(s246, s123))) === F
- }
- }
-
- test("Bags") { implicit fix =>
- val nil = cc("Bags.Nil")()
- def cons(es: Expr*) = cc("Bags.Cons")(es: _*)
-
- val cons12 = cons(i(1), cons(i(2), nil))
- val cons122 = cons(i(1), cons(i(2), cons(i(2), nil)))
-
- def fb(is: (Int, Int)*) = FiniteBag(is.map(p => i(p._1) -> bi(p._2)).toMap, Int32Type)
-
- val b12 = fb(1 -> 1, 2 -> 1)
- val b123 = fb(1 -> 1, 2 -> 1, 3 -> 1)
- val b246 = fb(2 -> 1, 4 -> 1, 6 -> 1)
- val b1223 = fb(1 -> 1, 2 -> 2, 3 -> 1)
-
- for(e <- allEvaluators) {
- eval(e, fcall("Bags.finite")()) === fb(1 -> 1, 2 -> 2, 3 -> 3)
- eval(e, fcall("Bags.content")(nil)) === fb()
- eval(e, fcall("Bags.content")(cons12)) === fb(1 -> 1, 2 -> 1)
- eval(e, fcall("Bags.content")(cons122)) === fb(1 -> 1, 2 -> 2)
- eval(e, fcall("Bags.add")(b12, i(2))) === fb(1 -> 1, 2 -> 2)
- eval(e, fcall("Bags.add")(b12, i(3))) === fb(1 -> 1, 2 -> 1, 3 -> 1)
- eval(e, fcall("Bags.union")(b123, b246)) === fb(1 -> 1, 2 -> 2, 3 -> 1, 4 -> 1, 6 -> 1)
- eval(e, fcall("Bags.union")(b246, b123)) === fb(1 -> 1, 2 -> 2, 3 -> 1, 4 -> 1, 6 -> 1)
- eval(e, fcall("Bags.inter")(b123, b246)) === fb(2 -> 1)
- eval(e, fcall("Bags.inter")(b246, b123)) === fb(2 -> 1)
- eval(e, fcall("Bags.inter")(b1223, b123)) === b123
- eval(e, fcall("Bags.diff")(b123, b246)) === fb(1 -> 1, 3 -> 1)
- eval(e, fcall("Bags.diff")(b246, b123)) === fb(4 -> 1, 6 -> 1)
- eval(e, fcall("Bags.diff")(b1223, b123)) === fb(2 -> 1)
- eval(e, fcall("Bags.diff")(b123, b1223)) === fb()
- }
- }
-
- test("Maps") { implicit fix =>
- val cons1223 = cc("Maps.PCons")(i(1), i(2), cc("Maps.PCons")(i(2), i(3), cc("Maps.PNil")()))
-
- def eqMap(a: Expr, m: Map[Expr, Expr]) = a match {
- case FiniteMap(es1, _, _) =>
- es1.toMap === m
- case e =>
- fail("Expected FiniteMap, got "+e)
- }
-
- for(e <- allEvaluators) {
- eqMap(eval(e, fcall("Maps.finite0")()).res, Map())
- eqMap(eval(e, fcall("Maps.finite1")()).res, Map(i(1) -> i(2)))
- eqMap(eval(e, fcall("Maps.finite2")()).res, Map(i(1) -> i(2), i(2) -> i(3)))
- eqMap(eval(e, fcall("Maps.toMap")(cons1223)).res, Map(i(1) -> i(2), i(2) -> i(3)))
-
- eval(e, Equals(fcall("Maps.finite1")(), fcall("Maps.finite2")())) === F
- eval(e, Equals(fcall("Maps.finite2")(), fcall("Maps.finite3")())) === T
- eval(e, MapIsDefinedAt(fcall("Maps.finite2")(), i(2))) === T
- eval(e, MapIsDefinedAt(fcall("Maps.finite2")(), i(3))) === F
- }
- }
-
- test("Sets and maps of structures") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, fcall("Sets2.containsCC")(fcall("Sets2.mkSingletonCC")(fcall("Sets2.buildPairCC")(i(42), T)), fcall("Sets2.buildPairCC")(i(42), T))) === T
- eval(e, fcall("Sets2.containsT")(fcall("Sets2.mkSingletonT")(fcall("Sets2.buildPairT")(i(42), T)), fcall("Sets2.buildPairT")(i(42), T))) === T
- }
- }
-
- test("Executing Chooses") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, fcall("Choose.c")(i(42))) === i(43)
- }
- }
-
- test("Infinite Recursion") { implicit fix =>
- val e = new CodeGenEvaluator(fix._1, fix._2, params = CodeGenParams.default.copy(maxFunctionInvocations = 32))
-
- eval(e, fcall("Recursion.c")(i(42))).failed
- }
-
- test("Wrong Contracts") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, fcall("Contracts.c")(i(-42))).failed
- }
- }
-
- test("Pattern Matching") { implicit fix =>
- for(e <- allEvaluators) {
- // Some simple math.
- eval(e, fcall("PatMat.f1")()) === i(1)
- eval(e, fcall("PatMat.f2")()) === i(1)
- eval(e, fcall("PatMat.f3")()) === i(1)
- eval(e, fcall("PatMat.f4")()) === i(1)
- eval(e, fcall("PatMat.f5")()) === i(1)
- eval(e, fcall("PatMat.f6")()) === i(1)
- }
- }
-
- test("Lambda functions") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, Application(fcall("Lambda.foo1")(), Seq(bi(1)))) === bi(1)
- eval(e, Application(fcall("Lambda.foo2")(), Seq(bi(1)))) === bi(2)
- eval(e, Application(fcall("Lambda.foo3")(), Seq(bi(1), bi(2)))) === bi(6)
- eval(e, Application(fcall("Lambda.foo4")(bi(2)), Seq(bi(1)))) === bi(3)
- }
- }
-
- test("Methods") { implicit fix =>
- for(e <- allEvaluators) {
- // Some simple math.
- eval(e, fcall("Methods.f1")()) === T
- eval(e, fcall("Methods.f2")()) === F
- eval(e, fcall("Methods.f3")()) === T
- }
- }
-
- test("Unapply") { implicit fix =>
- for(e <- allEvaluators) {
- eval(e, fcall("Unapply.foo")()) === bi(3)
- eval(e, fcall("Unapply.s1")()) === bi(3)
- eval(e, fcall("Unapply.s2")()) === bi(0)
- eval(e, fcall("Unapply.s3")()) === bi(42)
- }
- }
-
- test("Casts1") { implicit fix =>
- def bar1(es: Expr*) = cc("Casts1.Bar1")(es: _*)
- def bar2(es: Expr*) = cc("Casts1.Bar2")(es: _*)
- def bar3(es: Expr*) = cc("Casts1.Bar3")(es: _*)
-
- val b42 = bi(42)
-
- for(e <- allEvaluators) {
- eval(e, fcall("Casts1.test")(bar1(b42))) === b42
- eval(e, fcall("Casts1.test")(bar2(b42))) === b42
- eval(e, fcall("Casts1.test")(bar3(b42))).failed
- }
- }
-
- abstract class EvalDSL {
- def res: Expr
- def ===(res: Expr): Unit
- def failed: Unit = {}
- def success: Expr = res
- }
-
- case class Success(expr: Expr, env: Map[Identifier, Expr], evaluator: Evaluator, res: Expr) extends EvalDSL {
- override def failed = {
- fail(s"Evaluation of '$expr' with '$evaluator' (and env $env) should have failed")
- }
-
- def ===(exp: Expr) = {
- assert(res === exp)
- }
- }
-
- case class Failed(expr: Expr, env: Map[Identifier, Expr], evaluator: Evaluator, err: String) extends EvalDSL {
- override def success = {
- fail(s"Evaluation of '$expr' with '$evaluator' (and env $env) should have succeeded but failed with $err")
- }
-
- def res = success
-
- def ===(res: Expr) = success
- }
-
- def eval(e: Evaluator, toEval: Expr, env: Map[Identifier, Expr] = Map()): EvalDSL = {
- e.eval(toEval, env) match {
- case EvaluationResults.Successful(res) => Success(toEval, env, e, res)
- case EvaluationResults.RuntimeError(err) => Failed(toEval, env, e, err)
- case EvaluationResults.EvaluatorError(err) => Failed(toEval, env, e, err)
- }
- }
-}
diff --git a/src/test/scala/leon/integration/grammars/SimilarToSuite.scala b/src/test/scala/leon/integration/grammars/SimilarToSuite.scala
deleted file mode 100644
index bdabd5bee810661cb88c6401afaccf4786c7b298..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/grammars/SimilarToSuite.scala
+++ /dev/null
@@ -1,238 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.grammars
-
-import leon._
-import leon.test._
-import leon.test.helpers._
-import leon.purescala.Path
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Constructors._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.codegen._
-import synthesis._
-import bonsai.enumerators._
-import leon.grammars._
-import leon.grammars.aspects.SimilarTo
-
-class SimilarToSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
-
- val sources = List(
- """|import leon.lang._
- |import leon.annotation._
- |import leon.collection._
- |import leon._
- |
- |object Trees {
- | abstract class Expr
- | case class Plus(lhs: Expr, rhs: Expr) extends Expr
- | case class Minus(lhs: Expr, rhs: Expr) extends Expr
- | case class LessThan(lhs: Expr, rhs: Expr) extends Expr
- | case class And(lhs: Expr, rhs: Expr) extends Expr
- | case class Or(lhs: Expr, rhs: Expr) extends Expr
- | case class Not(e : Expr) extends Expr
- | case class Eq(lhs: Expr, rhs: Expr) extends Expr
- | case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
- | case class IntLiteral(v: BigInt) extends Expr
- | case class BoolLiteral(b : Boolean) extends Expr
- |}
- |object STrees {
- | abstract class Expr
- | case class Plus(lhs : Expr, rhs : Expr) extends Expr
- | case class Neg(arg : Expr) extends Expr
- | case class Ite(cond : Expr, thn : Expr, els : Expr) extends Expr
- | case class Eq(lhs : Expr, rhs : Expr) extends Expr
- | case class LessThan(lhs : Expr, rhs : Expr) extends Expr
- | case class Literal(i : BigInt) extends Expr
- |}
- |
- |object Desugar {
- | def desugar(e: Trees.Expr): STrees.Expr = {
- | STrees.Literal(0)
- | }
- |} """.stripMargin,
-
- """|import leon.lang._
- |import leon.collection._
- |
- |object Heaps {
- |
- | sealed abstract class Heap {
- | val rank : BigInt = this match {
- | case Leaf() => 0
- | case Node(_, l, r) =>
- | 1 + max(l.rank, r.rank)
- | }
- | def content : Set[BigInt] = this match {
- | case Leaf() => Set[BigInt]()
- | case Node(v,l,r) => l.content ++ Set(v) ++ r.content
- | }
- | }
- | case class Leaf() extends Heap
- | case class Node(value:BigInt, left: Heap, right: Heap) extends Heap
- |
- | def max(i1 : BigInt, i2 : BigInt) = if (i1 >= i2) i1 else i2
- |
- | def hasHeapProperty(h : Heap) : Boolean = h match {
- | case Leaf() => true
- | case Node(v, l, r) =>
- | ( l match {
- | case Leaf() => true
- | case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
- | }) &&
- | ( r match {
- | case Leaf() => true
- | case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
- | })
- | }
- |
- | def hasLeftistProperty(h: Heap) : Boolean = h match {
- | case Leaf() => true
- | case Node(_,l,r) =>
- | hasLeftistProperty(l) &&
- | hasLeftistProperty(r) &&
- | l.rank >= r.rank
- | }
- |
- | def heapSize(t: Heap): BigInt = { t match {
- | case Leaf() => BigInt(0)
- | case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
- | }} ensuring(_ >= 0)
- |
- | private def merge(h1: Heap, h2: Heap) : Heap = {
- | require(
- | hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
- | hasHeapProperty(h1) && hasHeapProperty(h2)
- | )
- | (h1,h2) match {
- | case (Leaf(), _) => h2
- | case (_, Leaf()) => h1
- | case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
- | //if(v1 >= v2) // FIXME
- | makeN(v1, l1, merge(r1, h2))
- | //else
- | // makeN(v2, l2, merge(h1, r2))
- | }
- | } ensuring { res =>
- | hasLeftistProperty(res) && hasHeapProperty(res) &&
- | heapSize(h1) + heapSize(h2) == heapSize(res) &&
- | h1.content ++ h2.content == res.content
- | }
- |
- | private def makeN(value: BigInt, left: Heap, right: Heap) : Heap = {
- | require(
- | hasLeftistProperty(left) && hasLeftistProperty(right)
- | )
- | if(left.rank >= right.rank)
- | Node(value, left, right)
- | else
- | Node(value, right, left)
- | } ensuring { res =>
- | hasLeftistProperty(res) }
- |}""".stripMargin
-
- )
-
- def runTests(tests: List[(List[Variable], Expr, Expr)], ofd: Option[FunDef] = None)(implicit fix: (LeonContext, Program)): Unit = {
- for ((vs, from, exp) <- tests) {
- // SimilarTo(<from>) should produce <exp>
-
- val g = OneOf(vs)
- val enum = new MemoizedEnumerator[Label, Expr, ProductionRule[Label, Expr]](g.getProductions)
- val exprs = enum.iterator(Label(exp.getType).withAspect(SimilarTo(Seq(from))))
-
- //println(s"SimilarTo(${from.asString}):")
-
- if (!exprs.contains(exp)) {
- info("Productions: ")
- g.printProductions(info(_))
-
- fail(s"Unable to find ${exp.asString} in SimilarTo(${from.asString})")
- }
- }
- }
-
- test("Basic") { implicit fix =>
-
- def _None = CaseClass(caseClassDef("leon.lang.None").typed(Seq(IntegerType)), Nil)
- def _Some(e: Expr) = CaseClass(caseClassDef("leon.lang.Some").typed(Seq(IntegerType)), List(e))
-
- val tests = List[(List[Variable], Expr, Expr)](
- (List(x, y), GreaterThan(x, y), GreaterThan(y, x)),
- (List(x, y), GreaterThan(x, y), not(GreaterThan(x, y))),
- (List(x, y), equality(x, y), not(equality(x, y))),
- (List(x, y), x, y),
- (List(x), _Some(x), _Some(Plus(x, bi(1)))),
- (List(x), _Some(Plus(x, bi(2))), _Some(Plus(x, bi(1))))
- )
-
- runTests(tests)
- }
-
- test("Desugar") { implicit fix =>
- val e = id("e", "Trees.Expr").toVariable
- val cond = id("cond", "Trees.Expr").toVariable
- val thn = id("thn", "Trees.Expr").toVariable
- val els = id("els", "Trees.Expr").toVariable
-
- def Ite(es: Expr*) = cc("STrees.Ite")(es: _*)
- def Literal(es: Expr*) = cc("STrees.Literal")(es: _*)
-
- val desugarfd = funDef("Desugar.desugar")
- def desugar(es: Expr*) = fcall("Desugar.desugar")(es: _*)
-
- val tests = List[(List[Variable], Expr, Expr)](
- (List(cond, thn, els),
- Ite(desugar(cond), desugar(els), desugar(thn)),
- Ite(desugar(cond), desugar(thn), desugar(els))
- ),
- (List(e),
- Ite(desugar(e), Literal(bi(1)), Literal(bi(1))),
- Ite(desugar(e), Literal(bi(0)), Literal(bi(1)))
- )
- )
-
- runTests(tests, Some(desugarfd))
- }
-
- test("Heap") { implicit fix =>
- val v1 = id("v1", IntegerType).toVariable
- val h1 = id("h1", "Heaps.Heap").toVariable
- val l1 = id("l1", "Heaps.Heap").toVariable
- val r1 = id("r1", "Heaps.Heap").toVariable
-
- val v2 = id("v2", IntegerType).toVariable
- val h2 = id("h2", "Heaps.Heap").toVariable
- val l2 = id("l2", "Heaps.Heap").toVariable
- val r2 = id("r2", "Heaps.Heap").toVariable
-
- val mergefd = funDef("Heaps.merge")
- def merge(es: Expr*) = fcall("Heaps.merge")(es: _*)
-
- def makeN(es: Expr*) = fcall("Heaps.makeN")(es: _*)
-
- def Node(es: Expr*) = cc("Heaps.Node")(es: _*)
- def Leaf(es: Expr*) = cc("Heaps.Leaf")(es: _*)
-
- def rank(es: Expr*) = fcall("Heap.rank")(es: _*)
-
- val tests = List[(List[Variable], Expr, Expr)](
- (List(h1, v1, l1, r1, h2, v2, l2, r2),
- makeN(v2, l1, merge(h1, r2)),
- makeN(v2, l2, merge(h1, r2))
- ),
- (List(v1, h1),
- merge(Node(Plus(v1, bi(1)), Leaf(), Leaf()), h1),
- merge(Node(v1, Leaf(), Leaf()), h1)
- ),
- (List(h1, h2),
- GreaterThan(rank(h1), Plus(rank(h2), bi(42))),
- GreaterThan(rank(h1), Minus(Plus(rank(h2), bi(42)), bi(1)))
- )
- )
-
- runTests(tests, Some(mergefd))
- }
-}
diff --git a/src/test/scala/leon/integration/purescala/CallGraphSuite.scala b/src/test/scala/leon/integration/purescala/CallGraphSuite.scala
deleted file mode 100644
index 1d9fa2124c977ecffcececd745d7fd80862fa242..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/purescala/CallGraphSuite.scala
+++ /dev/null
@@ -1,27 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.purescala
-
-import leon.test._
-
-import leon.purescala.Definitions.Program
-
-class CallGraphSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
-
- val sources = List(
- """object Matches {
- | import leon.collection._
- | def aMatch(a: List[Int]) = a match {
- | case _ :: _ => 0
- | }
- |}""".stripMargin
- )
-
- test("CallGraph tracks dependency to unapply pattern") { implicit fix =>
- val fd1 = funDef("Matches.aMatch")
- val fd2 = funDef("leon.collection.::.unapply")
-
- assert(implicitly[Program].callGraph.calls(fd1, fd2))
- }
-
-}
diff --git a/src/test/scala/leon/integration/purescala/DataGenSuite.scala b/src/test/scala/leon/integration/purescala/DataGenSuite.scala
deleted file mode 100644
index 050176ef54ce165af558c638cb2ed7d607120472..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/purescala/DataGenSuite.scala
+++ /dev/null
@@ -1,103 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.purescala
-
-import leon.test._
-
-import leon.purescala.Common._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.datagen._
-
-import leon.evaluators._
-
-class DataGenSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
- val sources = List(
- """|import leon.lang._
- |object Program {
- | sealed abstract class List
- | case class Cons(head: Int, tail: List) extends List
- | case object Nil extends List
- |
- | def size(lst: List): BigInt = lst match {
- | case Cons(_, xs) => 1 + size(xs)
- | case Nil => BigInt(0)
- | }
- |
- | def isSorted(lst: List) : Boolean = lst match {
- | case Nil => true
- | case Cons(_, Nil) => true
- | case Cons(x, xs @ Cons(y, ys)) => x < y && isSorted(xs)
- | }
- |
- | def content(lst: List) : Set[Int] = lst match {
- | case Nil => Set.empty[Int]
- | case Cons(x, xs) => Set(x) ++ content(xs)
- | }
- |
- | def insertSpec(elem: Int, list: List, res: List) : Boolean = {
- | isSorted(res) && content(res) == (content(list) ++ Set(elem))
- | }
- |}""".stripMargin
- )
-
- test("Lists") { implicit fix =>
-
- val ctx = fix._1
- val pgm = fix._2
-
- val eval = new DefaultEvaluator(ctx, pgm)
- val generator = new GrammarDataGen(eval)
-
- generator.generate(BooleanType).toSet.size === 2
- generator.generate(TupleType(Seq(BooleanType,BooleanType))).toSet.size === 4
-
- // Make sure we target our own lists
-
- val listType = classDef("Program.List").typed(Seq())
-
- assert(generator.generate(listType).take(100).toSet.size === 100, "Should be able to generate 100 different lists")
-
- val l1 = FreshIdentifier("l1", listType).toVariable
- val l2 = FreshIdentifier("l2", listType).toVariable
-
- def size(x: Expr) = fcall("Program.size")(x)
- def content(x: Expr) = fcall("Program.content")(x)
- def sorted(x: Expr) = fcall("Program.isSorted")(x)
-
- def spec(elem: Expr, list: Expr, res: Expr) = fcall("Program.insertSpec")(elem, list, res)
- def cons(h: Expr, t: Expr) = cc("Program.Cons")(h, t)
-
- assert(generator.generateFor(
- Seq(l1.id),
- GreaterThan(size(l1), bi(0)),
- 10,
- 500
- ).size === 10, "Should find 10 non-empty lists in the first 500 enumerated")
-
- assert(generator.generateFor(
- Seq(l1.id, l2.id),
- And(Equals(content(l1), content(l2)), sorted(l2)),
- 10,
- 500
- ).size === 10, "Should find 2x 10 lists with same content in the first 500 enumerated")
-
- assert(generator.generateFor(
- Seq(l1.id, l2.id),
- And(Seq(Equals(content(l1), content(l2)), sorted(l1), sorted(l2), Not(Equals(l1, l2)))),
- 1,
- 500
- ).isEmpty, "There should be no models for this problem")
-
- assert(generator.generateFor(
- Seq(l1.id, l2.id, b.id, a.id),
- And(Seq(
- LessThan(a, b),
- sorted(cons(a, l1)),
- spec(b, l1, l2)
- )),
- 10,
- 500
- ).size >= 5, "There should be at least 5 models for this problem.")
- }
-}
diff --git a/src/test/scala/leon/integration/purescala/DefOpsSuite.scala b/src/test/scala/leon/integration/purescala/DefOpsSuite.scala
deleted file mode 100644
index 7c7b82b13864b587800a0b9bb36d3e73730143f5..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/purescala/DefOpsSuite.scala
+++ /dev/null
@@ -1,108 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.purescala
-
-import leon.test._
-
-import leon.purescala.Definitions._
-import leon.purescala.DefOps._
-
-class DefOpsSuite extends LeonTestSuiteWithProgram {
-
- val sources = List(
- """ |package foo.bar.baz
- |import other.hello.world.Foo
- |import other.hello.world.Foo._
- |import other.hello.world.!!!._
- |import other.hello.world.m
- |object Bar {
- | val x = 42
- | abstract class A
- | case class C(i : Int) extends A
- |}
- |
- |object Foo {
- | import Bar.C
- | case class FooC()
- | val m = Bar.x + y + x
- | val ? = C(m)
- | val fooC = ? match {
- | case C(i) if i == 0 => FooC()
- | case _ => FooC()
- | }
- |}""".stripMargin,
-
- """ |package other.hello.world
- |
- |object !!! { val m = 42 }
- |object m { val x = 0 }
- |
- |object Foo {
- | val y = 0
- |}""".stripMargin,
-
- """ |package foo.bar
- |package object baz {
- | val x = 42
- |}""".stripMargin,
-
- """ |package foo.bar.baz.and.some.more
- |object InSubpackage {}
- |""".stripMargin,
-
- """ object InEmpty { def arrayLookup(a : Array[Int], i : Int) = a(i) } """
- )
-
- def fooC(implicit pgm: Program) = {
- pgm.lookup("foo.bar.baz.Foo.fooC")
- }
-
-
- test("Find base definition"){ case (ctx, pgm) =>
- assert(fooC(pgm).isDefined)
- }
-
-
- test("In empty package") { case (ctx, pgm) =>
- implicit val program = pgm
- val name = "InEmpty.arrayLookup"
- val df = pgm.lookup(name)
- assert(df.isDefined)
- assert{fullName(df.get) == name }
- }
-
- // Search by full name
-
- def mustFind(name: String, msg: String) = test(msg) { case (ctx, pgm) =>
- assert(searchRelative(name, fooC(pgm).get)(pgm).nonEmpty)
- }
-
- def mustFail(name: String, msg: String) = test(msg) { case (ctx, pgm) =>
- assert(searchRelative(name, fooC(pgm).get)(pgm).isEmpty)
- }
-
- mustFind("fooC", "Find yourself")
- mustFind("FooC", "Find a definition in the same scope 1")
- mustFind("?", "Find a definition in the same scope 2")
- mustFind("m", "Find a definition in the same scope 3")
- mustFind("Foo", "Find an enclosing definition")
- mustFind("Bar", "Find a definition in an enclosing scope")
-
- mustFind("Bar.A", "Find a definition in an object 1")
- mustFind("Foo.fooC", "Find a definition in an object 2")
-
- mustFind("y", "Find imported definition 1")
- mustFind("x", "Find imported definition 2")
-
- mustFind("other.hello.world.Foo", "Find a definition in another package")
- mustFind("and.some.more.InSubpackage","Find a definition in a subpackage")
- mustFind("InEmpty.arrayLookup", "Find a definition in the empty package")
-
- mustFail("nonExistent", "Don't find non-existent definition")
- mustFail("A", "Don't find definition in another object")
- mustFail("InSubpackage", "Don't find definition in another package")
- mustFail("hello.world.Foo","Don't find definition in non-visible nested package")
- mustFail("!!!", "Don't find definition that is root of a wildcard import")
- mustFail("m.x", "Don't find imported definition shadowed by local definition")
-
-}
diff --git a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
deleted file mode 100644
index 28238bb59513394d103be161ac6b80162baaa5ba..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
+++ /dev/null
@@ -1,137 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.purescala
-
-import leon.test._
-
-import leon.purescala.Constructors._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps._
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-
-class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
-
- val sources = List(
- """object Casts1 {
- | abstract class Foo
- | case class Bar1(v: BigInt) extends Foo
- | case class Bar2(v: BigInt) extends Foo
- | case class Bar3(v: BigInt) extends Foo
- | case class Bar4(i: Foo) extends Foo
- |
- | def aMatch(a: Foo) = a match {
- | case b1 @ Bar4(b2: Bar3) => b2
- | }
- |}""".stripMargin,
-
- """object Nested {
- | def foo = {
- | def bar = {
- | def baz = 42
- | baz
- | }
- | def zoo = 42
- | }
- |}
- |
- """.stripMargin
- )
-
- test("mapForPattern introduces casts"){ implicit fix =>
- funDef("Casts1.aMatch").body match {
- case Some(MatchExpr(scrut, Seq(MatchCase(p, None, b)))) =>
- val bar3 = caseClassDef("Casts1.Bar3").typed
- val bar4 = caseClassDef("Casts1.Bar4").typed
- val i = caseClassDef("Casts1.Bar4").fields.head.id
-
- for ((id, v) <- mapForPattern(scrut, p)) {
- if (id.name == "b1") {
- assert(v === AsInstanceOf(scrut, bar4))
- } else if (id.name == "b2") {
- assert(v === AsInstanceOf(CaseClassSelector(bar4, AsInstanceOf(scrut, bar4), i), bar3))
- } else {
- fail("Map contained unknown entry "+id.asString)
- }
- }
-
- case b =>
- fail("unexpected test shape: "+b)
- }
- }
-
- test("matchToIfThenElse introduces casts"){ implicit fix =>
- funDef("Casts1.aMatch").body match {
- case Some(b) =>
- assert(exists {
- case AsInstanceOf(_, _) => true
- case _ => false
- }(matchToIfThenElse(b)), "Could not find AsInstanceOf in the result of matchToIfThenElse")
-
- case b =>
- fail("unexpected test shape: "+b)
- }
- }
-
- test("asInstOf simplifies trivial casts") { implicit fix =>
- val cct = caseClassDef("Casts1.Bar1").typed
- val cc = CaseClass(cct, Seq(bi(42)))
- assert(asInstOf(cc, cct) === cc)
- }
-
- test("asInstOf leaves unknown casts") { implicit fix =>
- val act = classDef("Casts1.Foo").typed
- val cct = caseClassDef("Casts1.Bar1").typed
-
- val cc = CaseClass(cct, Seq(bi(42)))
- val id = FreshIdentifier("tmp", act)
- val expr = Let(id, cc, id.toVariable)
-
- assert(asInstOf(expr, cct) === AsInstanceOf(expr, cct))
- }
-
- test("closing functions") { implicit fix =>
- val nested = moduleDef("Nested")
- assert(nested.definedFunctions.size === 4)
- }
-
- test("simplestValue") { implicit fix =>
- import leon.purescala.TypeOps.isSubtypeOf
- val act = classDef("Casts1.Foo").typed
- val cct = caseClassDef("Casts1.Bar1").typed
-
- assert(isSubtypeOf(simplestValue(act).getType, act))
- assert(simplestValue(cct).getType == cct)
- }
-
- test("canBeHomomorphic") { implicit fix =>
- import leon.purescala.ExprOps.canBeHomomorphic
- import leon.purescala.Types._
- import leon.purescala.Definitions._
- val d = FreshIdentifier("d", IntegerType)
- val x = FreshIdentifier("x", IntegerType)
- val y = FreshIdentifier("y", IntegerType)
- assert(canBeHomomorphic(Variable(d), Variable(x)).isEmpty)
- val l1 = Lambda(Seq(ValDef(x)), Variable(x))
- val l2 = Lambda(Seq(ValDef(y)), Variable(y))
- assert(canBeHomomorphic(l1, l2).nonEmpty)
- val fType = FunctionType(Seq(IntegerType), IntegerType)
- val f = FreshIdentifier("f",
- FunctionType(Seq(IntegerType, fType, fType), IntegerType))
- val farg1 = FreshIdentifier("arg1", IntegerType)
- val farg2 = FreshIdentifier("arg2", fType)
- val farg3 = FreshIdentifier("arg3", fType)
-
- val fdef = new FunDef(f, Seq(), Seq(ValDef(farg1), ValDef(farg2), ValDef(farg3)), IntegerType)
-
- // Captured variables should be silent, even if they share the same identifier in two places of the code.
- assert(canBeHomomorphic(
- FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l2)),
- FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l1))).nonEmpty)
-
- assert(canBeHomomorphic(
- StringLiteral("1"),
- StringLiteral("2")).isEmpty)
- }
-
-}
diff --git a/src/test/scala/leon/integration/purescala/InliningSuite.scala b/src/test/scala/leon/integration/purescala/InliningSuite.scala
deleted file mode 100644
index 973dd579a32f8d6f00f22caae943cb4fef9a9d1b..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/purescala/InliningSuite.scala
+++ /dev/null
@@ -1,68 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.purescala
-
-import leon.test._
-import leon.purescala.Expressions._
-
-class InliningSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
- val sources = List(
- """|
- |import leon.lang._
- |import leon.annotation._
- |
- |object InlineGood {
- |
- | @inline
- | def foo(a: BigInt) = true
- |
- | def bar(a: BigInt) = foo(a)
- |
- |} """.stripMargin,
-
- """|import leon.lang._
- |import leon.annotation._
- |
- |object InlineBad {
- |
- | @inline
- | def foo(a: BigInt): BigInt = if (a > 42) foo(a-1) else 0
- |
- | def bar(a: BigInt) = foo(a)
- |
- |}""".stripMargin,
-
- """|import leon.lang._
- |import leon.annotation._
- |
- |object InlineGood2 {
- |
- | @inline
- | def foo(a: BigInt) = true
- |
- | @inline
- | def bar(a: BigInt) = foo(a)
- |
- | def baz(a: BigInt) = bar(a)
- |
- |}""".stripMargin
- )
-
-
- test("Simple Inlining") { implicit fix =>
- assert(funDef("InlineGood.bar").fullBody == BooleanLiteral(true), "Function not inlined?")
- }
-
- test("Recursive Inlining") { implicit fix =>
- funDef("InlineBad.bar").fullBody match {
- case FunctionInvocation(tfd, args) if tfd.id.name == "foo" => // OK, not inlined
- case b =>
- fail(s"Resultig body should be a call to 'foo', got '$b'")
- }
- }
-
- test("Double Inlining") { implicit fix =>
- assert(funDef("InlineGood2.baz").fullBody == BooleanLiteral(true), "Inlined function invocation not inlined in turn?")
- }
-
-}
diff --git a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
deleted file mode 100644
index c95b75e3ea3603ff773e9621498c30095c16e033..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
+++ /dev/null
@@ -1,101 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.purescala
-
-import leon.test._
-
-import leon._
-import leon.solvers._
-import leon.solvers.z3.UninterpretedZ3Solver
-import leon.purescala.Definitions.Program
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.Common._
-import leon.purescala.ExprOps
-
-class SimplifyPathsSuite extends LeonTestSuite {
- val a = FreshIdentifier("a", BooleanType)
- val aV = a.toVariable
- val b = FreshIdentifier("b", BooleanType)
- val bV = b.toVariable
- val c = FreshIdentifier("c", BooleanType)
- val cV = b.toVariable
-
- val l1 = InfiniteIntegerLiteral(1)
- val l2 = InfiniteIntegerLiteral(2)
-
- def simplifyPaths(ctx: LeonContext, expr: Expr): Expr = {
- val uninterpretedZ3 = SolverFactory.getFromName(ctx, Program.empty)("nativez3-u")
- try {
- ExprOps.simplifyPaths(uninterpretedZ3)(expr)
- } finally {
- uninterpretedZ3.shutdown()
- }
- }
-
- test("Simplify Paths 01 - if(true)") { ctx =>
- val in = IfExpr(BooleanLiteral(true), l1, l2)
- val exp = l1
-
- val out = simplifyPaths(ctx, in)
- assert(out === exp)
- }
-
- test("Simplify Paths 02 - expr match { .. }") { ctx =>
- val x = FreshIdentifier("x", BooleanType)
- val xV = x.toVariable
-
- val in = MatchExpr(Equals(And(aV, Not(bV)), Not(Or(Not(aV), bV))), Seq(
- MatchCase(LiteralPattern(Some(x), BooleanLiteral(true)), None, And(xV, cV)),
- MatchCase(LiteralPattern(None, BooleanLiteral(false)), None, Not(cV))
-
- ))
-
- val out = simplifyPaths(ctx, in)
- assert(out.asInstanceOf[MatchExpr].cases.size == 1)
- }
-
- test("Simplify Paths 03 - ") { ctx =>
- val a = FreshIdentifier("a", IntegerType)
- val aV = a.toVariable
- val x = FreshIdentifier("x", IntegerType)
- val y = FreshIdentifier("y", IntegerType)
- val z = FreshIdentifier("y", IntegerType)
- val w = FreshIdentifier("y", IntegerType)
- val o = FreshIdentifier("o", IntegerType)
-
- val l0 = InfiniteIntegerLiteral(0)
- val l42 = InfiniteIntegerLiteral(42)
-
- val in = MatchExpr(aV, Seq(
- MatchCase(LiteralPattern(None, l0), None, l0),
- MatchCase(WildcardPattern(Some(x)), Some(GreaterEquals(x.toVariable, l42)), Plus(x.toVariable, l42)),
- MatchCase(WildcardPattern(Some(y)), Some(GreaterThan(y.toVariable, l42)), Minus(x.toVariable, l42)),
- MatchCase(WildcardPattern(Some(z)), Some(GreaterThan(z.toVariable, l0)), Plus(z.toVariable, l42)),
- MatchCase(WildcardPattern(Some(w)), Some(LessThan(w.toVariable, l0)), Minus(w.toVariable, l42)),
- MatchCase(WildcardPattern(Some(o)), None, InfiniteIntegerLiteral(1000))
- ))
-
- val exp = MatchExpr(aV, Seq(
- MatchCase(LiteralPattern(None, l0), None, l0),
- MatchCase(WildcardPattern(Some(x)), Some(GreaterEquals(x.toVariable, l42)), Plus(x.toVariable, l42)),
- MatchCase(WildcardPattern(Some(z)), Some(GreaterThan(z.toVariable, l0)), Plus(z.toVariable, l42)),
- MatchCase(WildcardPattern(Some(w)), None, Minus(w.toVariable, l42))
- ))
-
- val out = simplifyPaths(ctx, in)
- assert(out === exp)
- }
-
- test("Simplify Paths 04 - error - 1") { ctx =>
- val in = And(Error(BooleanType, ""), aV)
- val out = simplifyPaths(ctx, in)
- assert(out === in)
- }
-
- test("Simplify Paths 05 - error - 2") { ctx =>
- val in = And(BooleanLiteral(false), Error(BooleanType, ""))
- val out = simplifyPaths(ctx, in)
- assert(out === BooleanLiteral(false))
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/ContextGrammarSuite.scala b/src/test/scala/leon/integration/solvers/ContextGrammarSuite.scala
deleted file mode 100644
index a2b2317acb78c448d2a8db879d84cf6a50e2cfe5..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/ContextGrammarSuite.scala
+++ /dev/null
@@ -1,314 +0,0 @@
-package leon
-package integration.solvers
-
-import synthesis.grammars.ContextGrammar
-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 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 org.scalatest.matchers.Matcher
-import org.scalatest.matchers.MatchResult
-
-trait CustomGrammarEqualMatcher[U, V] extends ContextGrammar[U, V] {
- def indexDifference(s1: String, s2: String): Int = {
- def rec(min: Int, max: Int): Int = if(max-min <= 1) min else {
- val mid = (min+max)/2
- val s1mid = s1.substring(0, mid)
- val s2mid = s2.substring(0, mid)
- if(s1mid != s2mid) rec(min, mid) else rec(mid, max)
- }
- rec(0, Math.min(s1.length, s2.length))
- }
-
- class EqualGrammarMatcher(expectedGrammar: Grammar) extends Matcher[Grammar] {
- def apply(left: Grammar) = {
- val leftString = grammarToString(left)
- val expected = grammarToString(expectedGrammar)
- val problem = indexDifference(leftString, expected)
- val msg1 = leftString.substring(0, problem) + "***got***" + leftString.substring(problem)
- val msg2 = expected.substring(0, problem) + "***expected***" + expected.substring(problem)
- MatchResult(
- left == expectedGrammar,
- s"$msg1\n ***did not equal*** \n$msg2",
- s"${grammarToString(left)}\n ***equaled*** \n${grammarToString(expectedGrammar)}"
- )
- }
- }
-
- def equalGrammar(grammar: Grammar) = new EqualGrammarMatcher(grammar)
-}
-
-class ContextGrammarString extends ContextGrammar[String, String] with CustomGrammarEqualMatcher[String, String]
-
-/**
- * @author Mikael
- */
-class ContextGrammarSuite extends FunSuite with Matchers with ScalaFutures {
- val ctx = new ContextGrammarString
- import ctx._
-
- val A = NonTerminal("A")
- val B = NonTerminal("B")
- val C = NonTerminal("C")
- val D = NonTerminal("D")
- val E = NonTerminal("E")
- val F = NonTerminal("F")
- val x = Terminal("x")("")
- val y = Terminal("y")("")
- val z = Terminal("z")("")
- val w = Terminal("w")("")
-
- test("Horizontal Markovization Simple") {
- val xA = A.copy(hcontext = List(x))
- val xB = B.copy(hcontext = List(x))
- val xC = C.copy(hcontext = List(x))
- val xAA = A.copy(hcontext = List(x, A))
- val xAB = B.copy(hcontext = List(x, A))
- val xAC = C.copy(hcontext = List(x, A))
- val AA = A.copy(hcontext = List(A))
- val AB = B.copy(hcontext = List(A))
- val AC = C.copy(hcontext = List(A))
-
- val grammar1 =
- Grammar(List(A, A), Map(A -> VerticalRHS(Seq(B, C)),
- B -> HorizontalRHS(x, Seq(A, A)),
- C -> HorizontalRHS(y, Nil)))
-
- val grammar2 =
- Grammar(List(A, AA), Map(A -> VerticalRHS(Seq(B, C)),
- B -> HorizontalRHS(x, Seq(xA, xAA)),
- C -> HorizontalRHS(y, Nil),
- xA -> VerticalRHS(Seq(xB, xC)),
- xB -> HorizontalRHS(x, Seq(xA, xAA)),
- xC -> HorizontalRHS(y, Nil),
- AA -> VerticalRHS(Seq(AB, AC)),
- AB -> HorizontalRHS(x, Seq(xA, xAA)),
- AC -> HorizontalRHS(y, Nil),
- xAA -> VerticalRHS(Seq(xAB, xAC)),
- xAB -> HorizontalRHS(x, Seq(xA, xAA)),
- xAC -> HorizontalRHS(y, Nil)
- ))
-
- grammar1.markovize_horizontal() should equalGrammar (grammar2)
- }
-
- test("Horizontal Markovization filtered") {
- val BA = A.copy(hcontext = List(B))
- val AB = B.copy(hcontext = List(A))
-
- val grammar1 =
- Grammar(List(A, B),
- Map(A -> Expansion(List(List(B, A), List(y))),
- B -> Expansion(List(List(x)))
- ))
- val grammar2 =
- Grammar(List(A, AB),
- Map(A -> Expansion(List(List(B, A), List(y))),
- B -> Expansion(List(List(x))),
- AB -> Expansion(List(List(x)))
- ))
-
- grammar1.markovize_horizontal_filtered(_.tag == "B", false) should equalGrammar (grammar2)
- grammar2.markovize_horizontal_filtered(_.tag == "B", false) should equalGrammar (grammar2)
- }
-
- test("Vertical Markovization simple") {
- val AA = A.copy(vcontext = List(A))
- val AAA = A.copy(vcontext = List(AA, A))
- val grammar1 =
- Grammar(List(A), Map(A -> Expansion(List(List(x, A), List(y)))))
- val grammar2 =
- Grammar(List(A),
- Map(A -> Expansion(List(List(x, AA), List(y))),
- AA -> Expansion(List(List(x, AA), List(y)))))
- val grammar3 =
- Grammar(List(A),
- Map(A -> Expansion(List(List(x, AA), List(y))),
- AA -> Expansion(List(List(x, AAA), List(y))),
- AAA -> Expansion(List(List(x, AAA), List(y)))))
-
- grammar1.markovize_vertical() should equalGrammar (grammar2)
- grammar2.markovize_vertical() should equalGrammar (grammar3)
- }
-
- test("Vertical Markovization double") {
- val AA = A.copy(vcontext = List(A))
- val BA = A.copy(vcontext = List(B))
- val AB = B.copy(vcontext = List(A))
- val BB = B.copy(vcontext = List(B))
-
- val grammar1 =
- Grammar(List(A),
- Map(A -> Expansion(List(List(x, B), List(y))),
- B -> Expansion(List(List(z, A), List(x)))))
-
- val grammar2 =
- Grammar(List(A),
- Map(A -> Expansion(List(List(x, AB), List(y))),
- BA -> Expansion(List(List(x, AB), List(y))),
- AB -> Expansion(List(List(z, BA), List(x)))))
-
- grammar1.markovize_vertical() should equalGrammar (grammar2)
- }
-
- test("Vertical Markovization triple") {
- val AA = A.copy(vcontext = List(A))
- val BA = A.copy(vcontext = List(B))
- val AB = B.copy(vcontext = List(A))
- val BB = B.copy(vcontext = List(B))
-
- val grammar1 =
- Grammar(List(A),
- Map(A -> Expansion(List(List(x, B), List(y))),
- B -> Expansion(List(List(z, A), List(z, B), List(x)))))
-
- val grammar2 =
- Grammar(List(A),
- Map(A -> Expansion(List(List(x, AB), List(y))),
- BA -> Expansion(List(List(x, AB), List(y))),
- AB -> Expansion(List(List(z, BA), List(z, BB), List(x))),
- BB -> Expansion(List(List(z, BA), List(z, BB), List(x)))
- ))
-
- grammar1.markovize_vertical() should equalGrammar (grammar2)
- }
-
- // Extend the grammar by taking the unique vertical context of an abstract class, not directly vertical.
- // In this context: A -> A -> B -> B -> B -> A should remind only A -> B -> A
- test("Abstract vertical Markovization") {
- val Alist = NonTerminal("Alist")
- val Acons = NonTerminal("Acons")
- val Anil = NonTerminal("Anil")
- val acons = Terminal("acons")("")
- val anil = Terminal("anil")("")
-
- val Blist = NonTerminal("Blist")
- val Bcons = NonTerminal("Bcons")
- val Bnil = NonTerminal("Bnil")
- val bcons = Terminal("bcons")("")
- val bnil = Terminal("bnil")("")
- val grammar =
- Grammar(List(Alist),
- Map(Alist -> Expansion(List(List(Acons), List(Anil))),
- Acons -> Expansion(List(List(acons, Blist, Alist))),
- Anil -> Expansion(List(List(anil, x))),
- Blist -> Expansion(List(List(Bcons), List(Bnil))),
- Bcons -> Expansion(List(List(bcons, Alist, Blist))),
- Bnil -> Expansion(List(List(bnil, y)))))
-
- val AconsB = Acons.copy(vcontext = List(Blist))
- val AnilB = Anil.copy(vcontext = List(Blist))
- val AlistB = Alist.copy(vcontext = List(Blist))
- val AconsA = Acons.copy(vcontext = List(Alist))
- val AnilA = Anil.copy(vcontext = List(Alist))
- val AlistA = Alist.copy(vcontext = List(Alist))
- val BconsA = Bcons.copy(vcontext = List(Alist))
- val BnilA = Bnil.copy(vcontext = List(Alist))
- val BlistA = Blist.copy(vcontext = List(Alist))
-
- val grammar2 =
- Grammar(List(Alist),
- Map(Alist -> Expansion(List(List(Acons), List(Anil))),
- Acons -> Expansion(List(List(acons, BlistA, AlistA))),
- Anil -> Expansion(List(List(anil, x))),
- AlistA -> Expansion(List(List(AconsA), List(AnilA))),
- AconsA -> Expansion(List(List(acons, BlistA, AlistA))),
- AnilA -> Expansion(List(List(anil, x))),
- AlistB -> Expansion(List(List(AconsB), List(AnilB))),
- AconsB -> Expansion(List(List(acons, BlistA, AlistB))),
- AnilB -> Expansion(List(List(anil, x))),
- BlistA -> Expansion(List(List(BconsA), List(BnilA))),
- BconsA -> Expansion(List(List(bcons, AlistB, BlistA))),
- BnilA -> Expansion(List(List(bnil, y)))))
-
- grammar.markovize_abstract_vertical() should equalGrammar (grammar2)
- }
-
- // Extend the grammar by taking the unique vertical context of an abstract class, not directly vertical.
- // In this context: A -> A -> B -> B -> B -> A should remind only A -> B -> A
- test("Abstract vertical Markovization Filtered") {
- val Alist = NonTerminal("Alist")
- val Acons = NonTerminal("Acons")
- val Anil = NonTerminal("Anil")
- val acons = Terminal("acons")("")
- val anil = Terminal("anil")("")
-
- val Blist = NonTerminal("Blist")
- val Bcons = NonTerminal("Bcons")
- val Bnil = NonTerminal("Bnil")
- val bcons = Terminal("bcons")("")
- val bnil = Terminal("bnil")("")
- val grammar =
- Grammar(List(Alist),
- Map(Alist -> Expansion(List(List(Acons), List(Anil))),
- Acons -> Expansion(List(List(acons, Blist, Alist))),
- Anil -> Expansion(List(List(anil, x))),
- Blist -> Expansion(List(List(Bcons), List(Bnil))),
- Bcons -> Expansion(List(List(bcons, Alist, Blist))),
- Bnil -> Expansion(List(List(bnil, y)))))
-
- val BconsA = Bcons.copy(vcontext = List(Alist))
- val BconsB = Bcons.copy(vcontext = List(Blist))
- val BnilA = Bnil.copy(vcontext = List(Alist))
- val BnilB = Bnil.copy(vcontext = List(Blist))
- val BlistA = Blist.copy(vcontext = List(Alist))
- val BlistB = Blist.copy(vcontext = List(Blist))
-
- val grammar2 =
- Grammar(List(Alist),
- Map(Alist -> Expansion(List(List(Acons), List(Anil))),
- Acons -> Expansion(List(List(acons, BlistA, Alist))),
- Anil -> Expansion(List(List(anil, x))),
- BlistA -> Expansion(List(List(BconsA), List(BnilA))),
- BconsA -> Expansion(List(List(bcons, Alist, BlistA))),
- BnilA -> Expansion(List(List(bnil, y)))))
-
- grammar.markovize_abstract_vertical_filtered(_.tag == "Blist") should equalGrammar (grammar2)
- }
-
- test("Vertical Markovization on self structures") {
- val Alist = NonTerminal("Alist")
- val Acons = NonTerminal("Acons")
- val Anil = NonTerminal("Anil")
- val acons = Terminal("acons")("")
- val anil = Terminal("anil")("")
- val T = NonTerminal("T")
- val t = Terminal("t")("")
-
- val grammar =
- Grammar(List(Alist),
- Map(Alist -> Expansion(List(List(Acons), List(Anil))),
- Acons -> Expansion(List(List(acons, T, T, Alist))),
- Anil -> Expansion(List(List(anil, x))),
- T -> Expansion(List(List(t)))))
-
- val AconsA = Acons.copy(vcontext = List(Alist))
- val AlistA = Alist.copy(vcontext = List(Alist))
- val AnilA = Anil.copy(vcontext = List(Alist))
-
- val grammar2 =
- Grammar(List(Alist),
- Map(Alist -> Expansion(List(List(Acons), List(Anil))),
- Acons -> Expansion(List(List(acons, T, T, AlistA))),
- Anil -> Expansion(List(List(anil, x))),
- AlistA -> Expansion(List(List(AconsA), List(AnilA))),
- AconsA -> Expansion(List(List(acons, T, T, AlistA))),
- AnilA -> Expansion(List(List(anil, x))),
- T -> Expansion(List(List(t)))))
-
-
- grammar.markovize_abstract_vertical_filtered(_.tag == "Alist") should equalGrammar (grammar2)
- }
-}
\ No newline at end of file
diff --git a/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala b/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
deleted file mode 100644
index cd3f846e8ada4e44a4a1f636e0425d498d2c3fb5..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.LeonContext
-
-class EnumerationSolverSuite extends LeonSolverSuite {
- def getSolver(implicit ctx: LeonContext, pgm: Program) = {
- new EnumerationSolver(ctx.toSctx, pgm)
- }
-
- val sources = Nil
-
- test("EnumerationSolver 1 (true)") { implicit fix =>
- sat(BooleanLiteral(true))
- }
-
- test("EnumerationSolver 2 (x == 1)") { implicit fix =>
- val x = FreshIdentifier("x", IntegerType).toVariable
-
- sat(Equals(x, InfiniteIntegerLiteral(0)))
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala b/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
deleted file mode 100644
index 6901791ad92a5620d04f0e1d7e2d80abc5922671..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
+++ /dev/null
@@ -1,71 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.LeonContext
-
-import leon.solvers.z3._
-
-class FairZ3SolverTests extends LeonSolverSuite {
-
- val sources = List(
- """|import leon.lang._
- |
- |object Minimal {
- | def f(x: BigInt) = x + 1
- |}""".stripMargin
- )
-
- def getSolver(implicit ctx: LeonContext, pgm: Program) = {
- new FairZ3Solver(ctx.toSctx, pgm)
- }
-
- test("Tautology 1") { implicit fix =>
- valid(BooleanLiteral(true))
- }
-
- test("Tautology 2") { implicit fix =>
- val x = FreshIdentifier("x", IntegerType).toVariable
- valid(Equals(Plus(x, x), Times(InfiniteIntegerLiteral(2), x)))
- }
-
- // This one contains a function invocation but is valid regardless of its
- // interpretation, so should be proved anyway.
- test("Tautology 3") { implicit fix =>
- val pgm = fix._2
- val fd = pgm.lookup("Minimal.f").collect {
- case fd: FunDef => fd
- }.get
-
- def f(e: Expr) = FunctionInvocation(fd.typed, Seq(e))
- val x = FreshIdentifier("x", IntegerType).toVariable
- val y = FreshIdentifier("y", IntegerType).toVariable
-
- valid(Implies(Not(Equals(f(x), f(y))), Not(Equals(x, y))))
- }
-
- test("Wrong 1") { implicit fix =>
- invalid(BooleanLiteral(false))
- }
-
- test("Wrong 2") { implicit fix =>
- val x = FreshIdentifier("x", IntegerType).toVariable
- unsat(And(GreaterThan(x, InfiniteIntegerLiteral(0)), Equals(Plus(x, x), Times(InfiniteIntegerLiteral(3), x))))
- }
-
- test("Correct after unfolding") { implicit fix =>
- val pgm = fix._2
- val fd = pgm.lookup("Minimal.f").collect {
- case fd: FunDef => fd
- }.get
-
- def f(e: Expr) = FunctionInvocation(fd.typed, Seq(e))
- val x = FreshIdentifier("x", IntegerType).toVariable
-
- valid(Equals(f(x), Plus(x, InfiniteIntegerLiteral(1))))
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala b/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala
deleted file mode 100644
index 1e8fc65d1126075c63ba87c764a7db063850aab7..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala
+++ /dev/null
@@ -1,68 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.test._
-import leon.test.helpers._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.ExprOps._
-import leon.purescala.Constructors._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.LeonContext
-
-import leon.solvers._
-import leon.solvers.smtlib._
-import leon.solvers.unrolling._
-import leon.solvers.z3._
-
-class GlobalVariablesSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
-
- val sources = List(
- """|import leon.lang._
- |import leon.annotation._
- |
- |object GlobalVariables {
- |
- | def test(i: BigInt): BigInt = {
- | 0 // will be replaced
- | }
- |} """.stripMargin
- )
-
- val solverNames: Seq[String] = {
- (if (SolverFactory.hasNativeZ3) Seq("fairz3") else Nil) ++
- (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
- (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
- }
-
- // Check that we correctly extract several types from solver models
- for (sname <- solverNames) {
- test(s"Global Variables in $sname") { implicit fix =>
- val ctx = fix._1
- val pgm = fix._2
-
- pgm.lookup("GlobalVariables.test") match {
- case Some(fd: FunDef) =>
- val b0 = FreshIdentifier("B", BooleanType);
- fd.body = Some(IfExpr(b0.toVariable, bi(1), bi(-1)))
-
- val cnstr = LessThan(FunctionInvocation(fd.typed, Seq(bi(42))), bi(0))
- val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
- solver.assertCnstr(And(b0.toVariable, cnstr))
-
- try {
- if (solver.check != Some(false)) {
- fail("Global variables not correctly handled.")
- }
- } finally {
- solver.free()
- }
- case _ =>
- fail("Function with global body not found")
- }
-
- }
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
deleted file mode 100644
index 7bb6f2e31a041840e40927f2433e7b414963eaab..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/InputCoverageSuite.scala
+++ /dev/null
@@ -1,307 +0,0 @@
-package leon.integration.solvers
-
-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.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.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 scala.language.implicitConversions
-import leon.LeonContext
-import leon.test.LeonTestSuiteWithProgram
-import leon.test.helpers.ExpressionsDSL
-import leon.synthesis.disambiguation.InputCoverage
-import leon.test.helpers.ExpressionsDSLProgram
-import leon.test.helpers.ExpressionsDSLVariables
-import leon.purescala.Extractors._
-import org.scalatest.PrivateMethodTester.PrivateMethod
-import org.scalatest.PrivateMethodTester
-
-class InputCoverageSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures with ExpressionsDSLProgram with ExpressionsDSLVariables with PrivateMethodTester {
-
- //override a because it comes from both Matchers and ExpressionsDSLVariables
- override val a = null
-
- override val leonOpts = List("--solvers=smt-cvc4")
-
- val sources = List("""
- |import leon.lang._
- |import leon.collection._
- |import leon.lang.synthesis._
- |import leon.annotation._
- |
- |object InputCoverageSuite {
- | def dummy = 2
- | def withIf(cond: Boolean) = {
- | if(cond) {
- | 1
- | } else {
- | 2
- | }
- | }
- |
- | def withIfInIf(cond: Boolean) = {
- | if(if(cond) false else true) {
- | 1
- | } else {
- | 2
- | }
- | }
- |
- | sealed abstract class A
- | case class B() extends A
- | case class C(a: String, tail: A) extends A
- | case class D(a: String, tail: A, b: String) extends A
- |
- | def withMatch(a: A): String = {
- | a match {
- | case B() => "B"
- | case C(a, C(b, tail)) => b.toString + withMatch(tail) + a.toString
- | case C(a, tail) => withMatch(tail) + a.toString
- | case D(a, tail, b) => a + withMatch(tail) + b
- | }
- | }
- |
- | def withCoveredFun1(input: Int) = {
- | withCoveredFun2(input - 5) + withCoveredFun2(input + 5)
- | }
- |
- | def withCoveredFun2(input: Int) = {
- | if(input > 0) {
- | 2
- | } else {
- | 0
- | }
- | }
- |
- | def withCoveredFun3(input: Int) = {
- | withCoveredFun2(withCoveredFun2(input + 5))
- | }
- |
- | def coveredCond(a: Boolean, b: Boolean, c: Boolean, d: Boolean) = {
- | if(a || b) {
- | if(c && d) {
- | 1
- | } else if(c) {
- | 2
- | } else {
- | 3
- | }
- | } else if(!a && c) {
- | 4
- | } else 5
- | }
- |
- |}""".stripMargin)
-
- val wrapBranch = PrivateMethod[(Expr, Some[Seq[Identifier]])]('wrapBranch)
- val markBranches = PrivateMethod[(Expr, Option[Seq[Identifier]])]('markBranches)
-
- test("wrapBranch should wrap expressions if they are not already containing wrapped calls"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val dummy = funDef("InputCoverageSuite.dummy")
- val coverage = new InputCoverage(dummy, Set(dummy))
- val simpleExpr = Plus(IntLiteral(1), b)
- coverage invokePrivate wrapBranch((simpleExpr, Some(Seq(p.id, q.id)))) should equal ((simpleExpr, Some(Seq(p.id, q.id))))
- coverage invokePrivate wrapBranch((simpleExpr, None)) match {
- case (covered, Some(ids)) =>
- ids should have size 1
- covered should equal (Tuple(Seq(simpleExpr, Variable(ids.head))))
- case _ =>
- fail("No ids added")
- }
- }
-
- test("If-coverage should work"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withIf = funDef("InputCoverageSuite.withIf")
- val coverage = new InputCoverage(withIf, Set(withIf))
- val expr = withIf.body.get
-
- coverage invokePrivate markBranches(expr) match {
- case (res, Some(ids)) =>
- ids should have size 2
- expr match {
- case IfExpr(cond, thenn, elze) =>
- res should equal (IfExpr(cond, Tuple(Seq(thenn, Variable(ids(0)))), Tuple(Seq(elze, Variable(ids(1))))))
- case _ => fail(s"$expr is not an IfExpr")
- }
- case _ =>
- fail("No ids added")
- }
- }
-
- test("If-cond-coverage should work"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withIfInIf = funDef("InputCoverageSuite.withIfInIf")
- val coverage = new InputCoverage(withIfInIf, Set(withIfInIf))
- val expr = withIfInIf.body.get
-
- coverage invokePrivate markBranches(expr) match {
- case (res, None) => fail("No ids added")
- case (res, Some(ids)) =>
- ids should have size 4
- expr match {
- case IfExpr(IfExpr(cond, t1, e1), t2, e2) =>
- res match {
- case MatchExpr(IfExpr(c, t1, e1), Seq(MatchCase(TuplePattern(None, s), None, IfExpr(c2, t2, e2)))) if s.size == 2 =>
- case _ => fail("should have a shape like (if() else ) match { case (a, b) => if(...) else }")
- }
- case _ => fail(s"$expr is not an IfExpr")
- }
- }
- }
-
- test("Match coverage should work with recursive functions") { ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withMatch = funDef("InputCoverageSuite.withMatch")
- val coverage = new InputCoverage(withMatch, Set(withMatch))
- val expr = withMatch.body.get
-
- coverage invokePrivate markBranches(expr) match {
- case (res, None) => fail("No ids added")
- case (res, Some(ids)) =>
- withClue(res.toString) {
- ids should have size 4
- }
- }
- }
-
- test("fundef combination-coverage should work"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withCoveredFun1 = funDef("InputCoverageSuite.withCoveredFun1")
- val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
- val coverage = new InputCoverage(withCoveredFun1, Set(withCoveredFun1, withCoveredFun2))
- val expr = withCoveredFun1.body.get
-
- coverage invokePrivate markBranches(expr) match {
- case (res, Some(ids)) if ids.size > 0 =>
- withClue(res.toString) {
- fail(s"Should have not added any ids, but got $ids")
- }
- case (res, _) =>
- }
- }
-
- test("fundef composition-coverage should work"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
- val withCoveredFun3 = funDef("InputCoverageSuite.withCoveredFun3")
- val coverage = new InputCoverage(withCoveredFun3, Set(withCoveredFun3, withCoveredFun2))
- val expr = withCoveredFun3.body.get
-
- coverage invokePrivate markBranches(expr) match {
- case (res, None) => fail("No ids added")
- case (res, Some(ids)) =>
- }
- }
-
- test("input coverage for booleans should find all of them") { ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withIf = funDef("InputCoverageSuite.withIf")
- val coverage = new InputCoverage(withIf, Set(withIf))
- coverage.result().toSet should equal (Set(Seq(b(true)), Seq(b(false))))
- }
-
- test("input coverage for ADT should find all of them") { ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withMatch = funDef("InputCoverageSuite.withMatch")
- val coverage = new InputCoverage(withMatch, Set(withMatch))
- coverage.minimizeExamples = false
- val res = coverage.result().toSet
- res should have size 4
-
- coverage.minimizeExamples = true
- val res2 = coverage.result().toSet
- res2 should have size 3
- }
-
- test("input coverage for boolean, disjunctions and conjunctions should find all of them") { ctxprogram =>
- implicit val (c, p) = ctxprogram
- val coveredCond = funDef("InputCoverageSuite.coveredCond")
- val coverage = new InputCoverage(coveredCond, Set(coveredCond))
- coverage.minimizeExamples = true
- val res2 = coverage.result().toSet
- res2 should have size 5
- }
-
- test("input coverage for combined functions should find all of them") { ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withCoveredFun1 = funDef("InputCoverageSuite.withCoveredFun1")
- val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
- val coverage = new InputCoverage(withCoveredFun1, Set(withCoveredFun1, withCoveredFun2))
- val res = coverage.result().toSet.toSeq
- if(res.size == 1) {
- val Seq(IntLiteral(a)) = res(0)
- withClue(s"a=$a") {
- assert(a + 5 > 0 || a - 5 > 0, "At least one of the two examples should cover the positive case")
- assert(a + 5 <= 0 || a - 5 <= 0, "At least one of the two examples should cover the negative case")
- }
- } else {
- res should have size 2
- val Seq(IntLiteral(a)) = res(0)
- val Seq(IntLiteral(b)) = res(1)
- withClue(s"a=$a, b=$b") {
- assert(a + 5 > 0 || b + 5 > 0 || a - 5 > 0 || b - 5 > 0 , "At least one of the two examples should cover the positive case")
- assert(a + 5 <= 0 || b + 5 <= 0 || a - 5 <= 0 || b - 5 <= 0 , "At least one of the two examples should cover the negative case")
- }
- }
- }
-
- test("input coverage for composed functions should find all of them") { ctxprogram =>
- implicit val (c, p) = ctxprogram
- val withCoveredFun3 = funDef("InputCoverageSuite.withCoveredFun3")
- val withCoveredFun2 = funDef("InputCoverageSuite.withCoveredFun2")
- val coverage = new InputCoverage(withCoveredFun3, Set(withCoveredFun3, withCoveredFun2))
- val res = coverage.result().toSet.toSeq
- def withCoveredFun2Impl(i: Int) = if(i > 0) 2 else 0
- if(res.size == 1) {
- val Seq(IntLiteral(a)) = res(0)
- withClue(s"a=$a") {
- assert(a + 5 > 0 || withCoveredFun2Impl(a + 5) > 0, "At least one of the two examples should cover the positive case")
- assert(a + 5 <= 0 || withCoveredFun2Impl(a + 5) <= 0, "At least one of the two examples should cover the negative case")
- }
- } else {
- res should have size 2
- val Seq(IntLiteral(a)) = res(0)
- val Seq(IntLiteral(b)) = res(1)
- withClue(s"a=$a, b=$b") {
- assert(a + 5 > 0 || withCoveredFun2Impl(a + 5) > 0 || b + 5 > 0 || withCoveredFun2Impl(b + 5) > 0, "At least one of the two examples should cover the positive case")
- assert(a + 5 <= 0 || withCoveredFun2Impl(a + 5) <= 0 || b + 5 <= 0 || withCoveredFun2Impl(b + 5) <= 0, "At least one of the two examples should cover the negative case")
- }
- }
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/InputPatternCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputPatternCoverageSuite.scala
deleted file mode 100644
index 2a1696cce7ec583bac4c48e975af12921528956c..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/InputPatternCoverageSuite.scala
+++ /dev/null
@@ -1,146 +0,0 @@
-package leon.integration.solvers
-
-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.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.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 scala.language.implicitConversions
-import leon.LeonContext
-import leon.test.LeonTestSuiteWithProgram
-import leon.test.helpers.ExpressionsDSL
-import leon.synthesis.disambiguation.InputPatternCoverage
-import leon.test.helpers.ExpressionsDSLProgram
-import leon.test.helpers.ExpressionsDSLVariables
-import leon.purescala.Extractors._
-import org.scalatest.PrivateMethodTester.PrivateMethod
-import org.scalatest.PrivateMethodTester
-import org.scalatest.matchers.Matcher
-import org.scalatest.matchers.MatchResult
-
-class InputPatternCoverageSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures with ExpressionsDSLProgram with ExpressionsDSLVariables with PrivateMethodTester {
- override val a = null
-
- override val leonOpts = List[String]("--solvers=smt-cvc4")
-
- val sources = List("""
- |import leon.lang._
- |import leon.collection._
- |import leon.lang.synthesis._
- |import leon.annotation._
- |
- |object InputPatternCoverageSuite {
- | def dummy = 2
- | def f(l: List[String]): String = l match { case Nil() => "[]" case Cons(a, b) => "[" + a + frec(b) }
- | def frec(l: List[String]): String = l match { case Nil() => "" case Cons(a, b) => "," + a + frec(b) }
- |
- | // Slightly different version of f with one inversion not caught by just covering examples.
- | def g(l: List[String]): String = l match { case Nil() => "[]" case Cons(a, b) => "[" + a + grec(b) }
- | def grec(l: List[String]): String = l match { case Nil() => "" case Cons(a, b) => "," + grec(b) + a }
- |
- | // Testing buildMarkableValue
- | abstract class A
- | case class B() extends A
- | case class C(i: String) extends A
- |
- | abstract class AA
- | case class E(i: Boolean) extends AA
- | case class F(a: A) extends AA
- |
- | abstract class L
- | case class Co(b: Boolean, l: L) extends L
- | case class Ni() extends L
- |
- | def h(a: A, l: L): String = hA(a) + hL(l)
- | def hA(a: A): String = a match { case B() => "b" case C(i) => i }
- | def hL(l: L): String= l match { case Co(b, tail) => b.toString + "," + hL(tail) case Ni() => "]" }
- |}
- |object CornerExamples {
- | abstract class A
- | case class R(a: A) extends A
- | case class L(a: A) extends A
- | case class C(a: A) extends A
- | case class E() extends A
- |
- | def f(a: A): String = a match {
- | case R(a) => f(a) + "."
- | case L(a) => "." + f(a)
- | case C(a) => f(a)
- | case E() => "A"
- | }
- | def h(a: List[A]): String = a match{
- | case Nil() => ""
- | case Cons(a, t) => f(a) + h(t)
- | }
- |}""".stripMargin)
-
-
- def haveOneWhich[T](pred: T => Boolean, predStr: String = "")(implicit m: Manifest[Iterable[T]]) = Matcher { (left: Iterable[T]) =>
- MatchResult(
- left exists pred,
- s"No element $predStr among ${left.mkString(", ")}",
- s"All elements of ${left.mkString(", ")} $predStr")
- }
-
- def eval(f: FunDef)(e: Seq[Expr])(implicit ctx: LeonContext, program: Program): Expr = {
- val d = new DefaultEvaluator(ctx, program)
- d.eval(functionInvocation(f, e)).result.get
- }
-
- test("InputPatternCoverage should expand covering examples."){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val f = funDef("InputPatternCoverageSuite.f")
- val reccoverage = new InputPatternCoverage(f.typed)
- reccoverage.result() should have size 3
- }
-
- test("InputPatternCoverage on multiple arguments should work"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val h = funDef("InputPatternCoverageSuite.h")
- val reccoverage = new InputPatternCoverage(h.typed)
- reccoverage.result() should have size 4
- }
-
- test("InputPatternCoverage should exhaustively find arguments"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
-
- val h = funDef("CornerExamples.h")
-
- val reccoverage = new InputPatternCoverage(h.typed)
- reccoverage.result() should have size 5
- }
-}
\ No newline at end of file
diff --git a/src/test/scala/leon/integration/solvers/InputRecCoverageSuite.scala b/src/test/scala/leon/integration/solvers/InputRecCoverageSuite.scala
deleted file mode 100644
index 037e114019e3a400bddf07bb998423f13ceed6dc..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/InputRecCoverageSuite.scala
+++ /dev/null
@@ -1,177 +0,0 @@
-package leon.integration.solvers
-
-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.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.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 scala.language.implicitConversions
-import leon.LeonContext
-import leon.test.LeonTestSuiteWithProgram
-import leon.test.helpers.ExpressionsDSL
-import leon.synthesis.disambiguation.InputRecCoverage
-import leon.test.helpers.ExpressionsDSLProgram
-import leon.test.helpers.ExpressionsDSLVariables
-import leon.purescala.Extractors._
-import org.scalatest.PrivateMethodTester.PrivateMethod
-import org.scalatest.PrivateMethodTester
-import org.scalatest.matchers.Matcher
-import org.scalatest.matchers.MatchResult
-
-class InputRecCoverageSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures with ExpressionsDSLProgram with ExpressionsDSLVariables with PrivateMethodTester {
- override val a = null
-
- override val leonOpts = List[String]("--solvers=smt-cvc4")
-
- val sources = List("""
- |import leon.lang._
- |import leon.collection._
- |import leon.lang.synthesis._
- |import leon.annotation._
- |
- |object InputRecCoverageSuite {
- | def dummy = 2
- | def f(l: List[String]): String = l match { case Nil() => "[]" case Cons(a, b) => "[" + a + frec(b) }
- | def frec(l: List[String]): String = l match { case Nil() => "" case Cons(a, b) => "," + a + frec(b) }
- |
- | // Slightly different version of f with one inversion not caught by just covering examples.
- | def g(l: List[String]): String = l match { case Nil() => "[]" case Cons(a, b) => "[" + a + grec(b) }
- | def grec(l: List[String]): String = l match { case Nil() => "" case Cons(a, b) => "," + grec(b) + a }
- |
- | // Testing buildMarkableValue
- | abstract class A
- | case class B() extends A
- | case class C(i: String) extends A
- |
- | abstract class AA
- | case class E(i: Boolean) extends AA
- | case class F(a: A) extends AA
- |
- | abstract class L
- | case class Co(b: Boolean, l: L) extends L
- | case class Ni() extends L
- |
- | def h(a: A, l: L): String = hA(a) + hL(l)
- | def hA(a: A): String = a match { case B() => "b" case C(i) => i }
- | def hL(l: L): String= l match { case Co(b, tail) => b.toString + "," + hL(tail) case Ni() => "]" }
- |}
- |object CornerExamples {
- | abstract class A
- | case class R(a: A) extends A
- | case class L(a: A) extends A
- | case class C(a: A) extends A
- | case class E() extends A
- |
- | def f(a: A): String = a match {
- | case R(a) => f(a) + "."
- | case L(a) => "." + f(a)
- | case C(a) => f(a)
- | case E() => "A"
- | }
- | def h(a: List[A]): String = a match{
- | case Nil() => ""
- | case Cons(a, t) => f(a) + h(t)
- | }
- |}""".stripMargin)
-
- // Since InputRecCoverage is not sufficient, we will soon remove these tests.
- /*
- def haveOneWhich[T](pred: T => Boolean, predStr: String = "")(implicit m: Manifest[Iterable[T]]) = Matcher { (left: Iterable[T]) =>
- MatchResult(
- left exists pred,
- s"No element $predStr among ${left.mkString(", ")}",
- s"All elements of ${left.mkString(", ")} $predStr")
- }
-
- def eval(f: FunDef)(e: Seq[Expr])(implicit ctx: LeonContext, program: Program): Expr = {
- val d = new DefaultEvaluator(ctx, program)
- d.eval(functionInvocation(f, e)).result.get
- }
-
- test("InputRecCoverage should expand covering examples to make them rec-covering."){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val f = funDef("InputRecCoverageSuite.f")
- val frec = funDef("InputRecCoverageSuite.frec")
- val g = funDef("InputRecCoverageSuite.g")
- val reccoverage = new InputRecCoverage(f, Set(f, frec))
- reccoverage.result().map(x => x(0)) should haveOneWhich({(input: Expr) =>
- eval(f)(Seq(input)) != eval(g)(Seq(input))
- }, "make f and g differ")
- }
-
- val buildMarkableValue = PrivateMethod[Option[Expr]]('buildMarkableValue)
-
- test("buildMarkableValue should build markable values if possible") { ctxprogram =>
- implicit val (ctx, program) = ctxprogram
- val dummy = funDef("InputRecCoverageSuite.dummy")
- val reccoverage = new InputRecCoverage(dummy, Set(dummy))
- reccoverage invokePrivate buildMarkableValue(classType("InputRecCoverageSuite.AA")) match {
- case None => fail("Could not find a markable value of type AA but F(C(\"\")) is one !")
- case Some(v) => v match {
- case CaseClass(cct, Seq(c)) => cct should equal (classType("InputRecCoverageSuite.F"))
- c match {
- case CaseClass(cct, Seq(s)) => cct should equal (classType("InputRecCoverageSuite.C"))
- case _ => fail(s"$c is not of the type C")
- }
- case _ => fail(s"$v is not of the type F")
- }
- }
-
- reccoverage invokePrivate buildMarkableValue(classType("InputRecCoverageSuite.E")) should be('empty)
-
- reccoverage invokePrivate buildMarkableValue(classType("InputRecCoverageSuite.L")) should be('empty)
- }
-
- test("InputRecCoverage on multiple arguments should work"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
- val h = funDef("InputRecCoverageSuite.h")
- val hA = funDef("InputRecCoverageSuite.hA")
- val hL = funDef("InputRecCoverageSuite.hL")
- val reccoverage = new InputRecCoverage(h, Set(h, hA, hL))
- reccoverage.assertIsRecCovering(reccoverage.result())
- }
-
- test("InputRecCoverage should exhaustively find arguments"){ ctxprogram =>
- implicit val (c, p) = ctxprogram
-
- val f = funDef("CornerExamples.f")
- val h = funDef("CornerExamples.h")
-
- val reccoverage = new InputRecCoverage(h, Set(h, f))
- reccoverage.assertIsRecCovering(reccoverage.result())
- }*/
-}
\ No newline at end of file
diff --git a/src/test/scala/leon/integration/solvers/LeonSolverSuite.scala b/src/test/scala/leon/integration/solvers/LeonSolverSuite.scala
deleted file mode 100644
index 62b343df6c108d48e762e14b3ff655923cb0dfa8..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/LeonSolverSuite.scala
+++ /dev/null
@@ -1,94 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.LeonContext
-
-import leon.solvers._
-import leon.solvers.z3._
-
-trait LeonSolverSuite extends LeonTestSuiteWithProgram {
- def getSolver(implicit ctx: LeonContext, pgm: Program): Solver
-
- case class SolverDSL(res: Option[Boolean], solver: Solver) {
- val resToString = res match {
- case Some(true) => "sat"
- case Some(false) => "unsat"
- case None => "unknown"
- }
-
- def sat: Unit = {
- if (res != Some(true)) {
- fail(s"Expected 'sat', got '$resToString' from $solver")
- }
- }
-
- def unsat: Unit = {
- if (res != Some(false)) {
- fail(s"Expected 'unsat', got '$resToString' from $solver")
- }
- }
- def unknown: Unit = {
- if (res != None) {
- fail(s"Expected 'unknown', got '$resToString' from $solver")
- }
- }
- }
-
- def satToString(res: Option[Boolean]) = res match {
- case Some(true) => "sat"
- case Some(false) => "unsat"
- case None => "unknown"
- }
-
- def validToString(res: Option[Boolean]) = res match {
- case Some(true) => "invalid"
- case Some(false) => "valid"
- case None => "unknown"
- }
-
- def check(cnstr: Expr)(implicit ctx: LeonContext, pgm: Program): Option[Boolean] = {
- val solver = getSolver
-
- try {
- solver.assertCnstr(cnstr)
- solver.check
- } finally {
- solver.free()
- }
- }
-
- def sat(cnstr: Expr)(implicit ctx: LeonContext, pgm: Program): Unit = {
- val res = check(cnstr)
- if (res != Some(true)) {
- fail("Expected '"+satToString(Some(true))+"', got '"+satToString(res)+"'")
- }
- }
-
- def unsat(cnstr: Expr)(implicit ctx: LeonContext, pgm: Program): Unit = {
- val res = check(cnstr)
- if (res != Some(false)) {
- fail("Expected '"+satToString(Some(false))+"', got '"+satToString(res)+"'")
- }
- }
-
- def valid(cnstr: Expr)(implicit ctx: LeonContext, pgm: Program): Unit = {
- val res = check(Not(cnstr))
- if (res != Some(false)) {
- fail("Expected '"+validToString(Some(false))+"', got '"+validToString(res)+"'")
- }
- }
-
- def invalid(cnstr: Expr)(implicit ctx: LeonContext, pgm: Program): Unit = {
- val res = check(Not(cnstr))
- if (res != Some(true)) {
- fail("Expected '"+validToString(Some(true))+"', got '"+validToString(res)+"'")
- }
- }
-
-}
diff --git a/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala b/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
deleted file mode 100644
index 3d56b31ccb663171dff9c6d84e91795b00209baf..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
+++ /dev/null
@@ -1,192 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.test._
-import leon.test.helpers._
-import leon._
-import leon.solvers._
-import leon.utils._
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.evaluators._
-import leon.purescala.Expressions._
-
-class ModelEnumerationSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
- val sources = List(
- """|import leon.lang._
- |import leon.annotation._
- |
- |object List1 {
- | abstract class List
- | case class Cons(h: BigInt, t: List) extends List
- | case object Nil extends List
- |
- | def size(l: List): BigInt = {
- | l match {
- | case Cons(h, t) => BigInt(1) + size(t)
- | case Nil => BigInt(0)
- | }
- | } ensuring { _ >= 0 }
- |
- | def sum(l: List): BigInt = l match {
- | case Cons(h, t) => h + size(t)
- | case Nil => 0
- | }
- |
- | def sumAndSize(l: List) = (size(l), sum(l))
- |
- |} """.stripMargin
- )
-
- def getModelEnum(implicit ctx: LeonContext, pgm: Program) = {
- val sf = SolverFactory.default
- new ModelEnumerator(ctx, pgm, sf)
- }
-
- test("Simple model enumeration 1") { implicit fix =>
- val tpe = classDef("List1.List").typed
- val l = FreshIdentifier("l", tpe)
-
- val cnstr = GreaterThan(fcall("List1.size")(l.toVariable), bi(2))
-
- val me = getModelEnum
- val enum = me.enumSimple(Seq(l), cnstr)
-
- val models = enum.take(5).toList
-
- assert(models.size === 5, "We can enumerate at least 5 lists of size 3+")
- assert(models.toSet.size === 5, "Models are distinct")
- }
-
- test("Simple model enumeration 2") { implicit fix =>
- val tpe = classDef("List1.List").typed
- val l = FreshIdentifier("l", tpe)
-
- val cnstr = Equals(fcall("List1.size")(l.toVariable), bi(0))
-
- val me = getModelEnum
-
- val enum = me.enumSimple(Seq(l), cnstr)
-
- assert(enum.take(5).toList.size === 1, "We can only enumerate one list of size 0")
- }
-
- test("Varying model enumeration 1") { implicit fix =>
- val tpe = classDef("List1.List").typed
- val l = FreshIdentifier("l", tpe)
-
- // 0 < list.size < 3
- val cnstr = And(GreaterThan(fcall("List1.size")(l.toVariable), bi(0)),
- LessThan(fcall("List1.size")(l.toVariable), bi(3)))
-
- val car = fcall("List1.size")(l.toVariable)
-
- val evaluator = new DefaultEvaluator(fix._1, fix._2)
- val me = getModelEnum
-
- // 1 model of each size
- val enum1 = me.enumVarying(Seq(l), cnstr, car)
-
- assert(enum1.toList.size === 2, "We can enumerate 2 lists of varying size 0 < .. < 3")
-
- // 3 models of each size
- val enum2 = me.enumVarying(Seq(l), cnstr, car, 3)
-
- assert(enum2.toList.size === 6, "We can enumerate 6 lists of varying size 0 < .. < 3 with 3 per size")
-
-
- val car2 = fcall("List1.sum")(l.toVariable)
-
- // 1 model of each sum
- val enum3 = me.enumVarying(Seq(l), cnstr, car2)
- val models3 = enum3.take(4).toList
-
- assert(models3.size === 4, "We can enumerate >=4 lists of varying sum, with 0 < .. < 3")
-
- val carResults3 = models3.groupBy(m => evaluator.eval(car2, m).result.get)
- assert(carResults3.size === 4, "We should have 4 distinct sums")
- assert(carResults3.forall(_._2.size === 1), "We should have 1 model per sum")
-
- // 2 model of each sum
- val enum4 = me.enumVarying(Seq(l), cnstr, car2, 2)
- val models4 = enum4.take(4).toList
-
- assert(models4.size === 4, "We can enumerate >=4 lists of varying sum, with 0 < .. < 3")
-
- val carResults4 = models4.groupBy(m => evaluator.eval(car2, m).result.get)
- assert(carResults4.size >= 2, "We should have at least 2 distinct sums")
- assert(carResults4.forall(_._2.size <= 2), "We should have at most 2 models per sum")
-
- }
-
- test("Varying model enumeration 2") { implicit fix =>
- val tpe = classDef("List1.List").typed
- val l = FreshIdentifier("l", tpe)
-
- // 0 < list.size < 3
- val cnstr = And(GreaterThan(fcall("List1.size")(l.toVariable), bi(0)),
- LessThan(fcall("List1.size")(l.toVariable), bi(3)))
-
- val car = Equals(fcall("List1.size")(l.toVariable), bi(1))
-
- val me = getModelEnum
-
- // 1 model of each caracteristic (which is a boolean, so only two possibilities)
- val enum3 = me.enumVarying(Seq(l), cnstr, car)
- val models3 = enum3.take(10).toList
-
- assert(models3.size === 2, "We can enumerate only 2 lists of varying size==0")
-
-
- // 1 model of each caracteristic (which is a boolean, so only two possibilities)
- val enum4 = me.enumVarying(Seq(l), cnstr, car, 2)
- val models4 = enum4.take(10).toList
-
- assert(models4.size === 4, "We can enumerate only 4 lists of varying size==0 (2 each)")
- }
-
- test("Maximizing size") { implicit fix =>
- val tpe = classDef("List1.List").typed
- val l = FreshIdentifier("l", tpe)
-
- val cnstr = LessThan(fcall("List1.size")(l.toVariable), bi(5))
-
- val car = fcall("List1.size")(l.toVariable)
-
- val evaluator = new DefaultEvaluator(fix._1, fix._2)
- val me = getModelEnum
-
- val enum1 = me.enumMaximizing(Seq(l), cnstr, car)
- val models1 = enum1.take(5).toList
-
- assert(models1.size < 5, "It took less than 5 models to reach max")
- assert(evaluator.eval(car, models1.last).result === Some(bi(4)), "Max should be 4")
-
- val enum2 = me.enumMaximizing(Seq(l), BooleanLiteral(true), car)
- val models2 = enum2.take(4).toList
-
- assert(models2.size == 4, "Unbounded search yields models")
- // in 4 steps, it should reach lists of size > 10
- assert(evaluator.eval(GreaterThan(car, bi(10)), models2.last).result === Some(T), "Progression should be efficient")
- }
-
- test("Minimizing size") { implicit fix =>
- val tpe = classDef("List1.List").typed
- val l = FreshIdentifier("l", tpe)
-
- val cnstr = LessThan(fcall("List1.size")(l.toVariable), bi(5))
-
- val car = fcall("List1.size")(l.toVariable)
-
- val evaluator = new DefaultEvaluator(fix._1, fix._2)
- val me = getModelEnum
-
- val enum1 = me.enumMinimizing(Seq(l), cnstr, car)
- val models1 = enum1.take(5).toList
-
- assert(models1.size < 5, "It took less than 5 models to reach min")
- assert(evaluator.eval(car, models1.last).result === Some(bi(0)), "Min should be 0")
- }
-
-}
diff --git a/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala b/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
deleted file mode 100644
index f50eb57c72ec467dd906811e4d1003a9d187d6d5..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/QuantifierSolverSuite.scala
+++ /dev/null
@@ -1,141 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Constructors._
-import leon.purescala.Types._
-import leon.LeonContext
-import leon.LeonOption
-
-import leon.solvers._
-import leon.solvers.smtlib._
-import leon.solvers.cvc4._
-import leon.solvers.z3._
-
-class QuantifierSolverSuite extends LeonTestSuiteWithProgram {
-
- val sources = List()
-
- override val leonOpts = List("--checkmodels")
-
- val solverNames: Seq[String] = {
- (if (SolverFactory.hasNativeZ3) Seq("fairz3") else Nil) ++
- (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
- (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
- }
-
- val f1: Identifier = FreshIdentifier("f1", FunctionType(Seq(IntegerType, IntegerType), IntegerType))
- val A = TypeParameter.fresh("A")
- val f2: Identifier = FreshIdentifier("f2", FunctionType(Seq(A, A), A))
-
- def app(f: Expr, args: Expr*): Expr = Application(f, args)
- def bi(i: Int): Expr = InfiniteIntegerLiteral(i)
-
- def associative(f: Expr): Expr = {
- val FunctionType(Seq(t1, t2), _) = f.getType
- assert(t1 == t2, "Can't specify associativity for type " + f.getType)
-
- val ids @ Seq(x, y, z) = Seq("x", "y", "z").map(name => FreshIdentifier(name, t1, true))
- Forall(ids.map(ValDef(_)), Equals(
- app(f, app(f, Variable(x), Variable(y)), Variable(z)),
- app(f, Variable(x), app(f, Variable(y), Variable(z)))))
- }
-
- def commutative(f: Expr): Expr = {
- val FunctionType(Seq(t1, t2), _) = f.getType
- assert(t1 == t2, "Can't specify commutativity for type " + f.getType)
-
- val ids @ Seq(x, y) = Seq("x", "y").map(name => FreshIdentifier(name, t1, true))
- Forall(ids.map(ValDef(_)), Equals(
- app(f, Variable(x), Variable(y)), app(f, Variable(y), Variable(x))))
- }
-
- def idempotent(f: Expr): Expr = {
- val FunctionType(Seq(t1, t2), _) = f.getType
- assert(t1 == t2, "Can't specify idempotency for type " + f.getType)
-
- val ids @ Seq(x, y, z) = Seq("x", "y", "z").map(name => FreshIdentifier(name, t1, true))
- Forall(ids.map(ValDef(_)), Equals(
- app(f, Variable(x), Variable(y)),
- app(f, Variable(x), app(f, Variable(x), Variable(y)))))
- }
-
- def rotative(f: Expr): Expr = {
- val FunctionType(Seq(t1, t2), _) = f.getType
- assert(t1 == t2, "Can't specify associativity for type " + f.getType)
-
- val ids @ Seq(x, y, z) = Seq("x", "y", "z").map(name => FreshIdentifier(name, t1, true))
- Forall(ids.map(ValDef(_)), Equals(
- app(f, app(f, Variable(x), Variable(y)), Variable(z)),
- app(f, app(f, Variable(y), Variable(z)), Variable(x))))
- }
-
- val satisfiable = List(
- "paper 1" -> and(associative(Variable(f1)),
- Not(Equals(app(Variable(f1), app(Variable(f1), bi(1), bi(2)), bi(3)),
- app(Variable(f1), bi(1), app(Variable(f1), bi(2), bi(2)))))),
- "paper 2" -> and(commutative(Variable(f1)), idempotent(Variable(f1)),
- Not(Equals(app(Variable(f1), app(Variable(f1), bi(1), bi(2)), bi(2)),
- app(Variable(f1), bi(1), app(Variable(f1), bi(2), app(Variable(f1), bi(1), bi(3))))))),
- "assoc not comm int" -> and(associative(Variable(f1)), Not(commutative(Variable(f1)))),
- "assoc not comm generic" -> and(associative(Variable(f2)), Not(commutative(Variable(f2)))),
- "comm not assoc int" -> and(commutative(Variable(f1)), Not(associative(Variable(f1)))),
- "comm not assoc generic" -> and(commutative(Variable(f2)), Not(associative(Variable(f2))))
- )
-
- val unification: Expr = {
- val ids @ Seq(x, y) = Seq("x", "y").map(name => FreshIdentifier(name, IntegerType, true))
- Forall(ids.map(ValDef(_)), Not(Equals(app(Variable(f1), Variable(x), Variable(y)), app(Variable(f1), Variable(y), Variable(x)))))
- }
-
- val unsatisfiable = List(
- "comm + rotate = assoc int" -> and(commutative(Variable(f1)), rotative(Variable(f1)), Not(associative(Variable(f1)))),
- "comm + rotate = assoc generic" -> and(commutative(Variable(f2)), rotative(Variable(f2)), Not(associative(Variable(f2)))),
- "unification" -> unification
- )
-
- def checkSolver(solver: Solver, expr: Expr, sat: Boolean)(implicit fix: (LeonContext, Program)): Unit = {
- try {
- solver.assertCnstr(expr)
- solver.check match {
- case Some(true) if sat && fix._1.reporter.warningCount > 0 =>
- fail(s"Solver $solver - Constraint ${expr.asString} doesn't guarantee model validity!?")
- case Some(true) if sat => // checkmodels ensures validity
- case Some(false) if !sat => // we were looking for unsat
- case res => fail(s"Solver $solver - Constraint ${expr.asString} has result $res!?")
- }
- } finally {
- solver.free()
- }
- }
-
- for (sname <- solverNames; (ename, expr) <- satisfiable) {
- test(s"Satisfiable quantified formula $ename in $sname") { implicit fix =>
- val (ctx, pgm) = fix
- val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
- checkSolver(solver, expr, true)
- }
-
- /*
- test(s"Satisfiable quantified formula $ename in $sname with partial models") { implicit fix =>
- val (ctx, pgm) = fix
- val newCtx = ctx.copy(options = ctx.options.filter(_ != UnrollingProcedure.optPartialModels) :+
- LeonOption(UnrollingProcedure.optPartialModels)(true))
- val solver = sf(newCtx, pgm)
- checkSolver(solver, expr, true)
- }
- */
- }
-
- for (sname <- solverNames; (ename, expr) <- unsatisfiable) {
- test(s"Unsatisfiable quantified formula $ename in $sname") { implicit fix =>
- val (ctx, pgm) = fix
- val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
- checkSolver(solver, expr, false)
- }
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala
deleted file mode 100644
index 5f987a1454f4c025d8a44864a13c24523a904138..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/SolversSuite.scala
+++ /dev/null
@@ -1,100 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.test._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.ExprOps._
-import leon.purescala.Constructors._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.LeonContext
-
-import leon.solvers._
-import leon.solvers.smtlib._
-import leon.solvers.z3._
-
-class SolversSuite extends LeonTestSuiteWithProgram {
-
- val sources = List()
-
- val solverNames: Seq[String] = {
- (if (SolverFactory.hasNativeZ3) Seq("fairz3") else Nil) ++
- (if (SolverFactory.hasZ3) Seq("smt-z3") else Nil) ++
- (if (SolverFactory.hasCVC4) Seq("smt-cvc4") else Nil)
- }
-
- val types = Seq(
- BooleanType,
- UnitType,
- CharType,
- RealType,
- IntegerType,
- Int32Type,
- StringType,
- TypeParameter.fresh("T"),
- SetType(IntegerType),
- BagType(IntegerType),
- MapType(IntegerType, IntegerType),
- FunctionType(Seq(IntegerType), IntegerType),
- TupleType(Seq(IntegerType, BooleanType, Int32Type))
- )
-
- val vs = types.map(FreshIdentifier("v", _).toVariable)
-
- // We need to make sure models are not co-finite
- val cnstrs = vs.map(v => v.getType match {
- case UnitType =>
- Equals(v, simplestValue(v.getType))
- case SetType(base) =>
- Not(ElementOfSet(simplestValue(base), v))
- case BagType(base) =>
- Not(Equals(MultiplicityInBag(simplestValue(base), v), simplestValue(IntegerType)))
- case MapType(from, to) =>
- Not(Equals(MapApply(v, simplestValue(from)), simplestValue(to)))
- case FunctionType(froms, to) =>
- Not(Equals(Application(v, froms.map(simplestValue)), simplestValue(to)))
- case _ =>
- not(Equals(v, simplestValue(v.getType)))
- })
-
- def checkSolver(solver: Solver, vs: Set[Variable], cnstr: Expr)(implicit fix: (LeonContext, Program)): Unit = {
- try {
- solver.assertCnstr(cnstr)
-
- solver.check match {
- case Some(true) =>
- val model = solver.getModel
- for (v <- vs) {
- if (model.isDefinedAt(v.id)) {
- assert(model(v.id).getType === v.getType, s"Solver $solver - Extracting value of type "+v.getType)
- } else {
- fail(s"Solver $solver - Model does not contain "+v.id.uniqueName+" of type "+v.getType)
- }
- }
- case res =>
- fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!? Solver was "+solver.getClass)
- }
- } finally {
- solver.free()
- }
- }
-
- // Check that we correctly extract several types from solver models
- for (sname <- solverNames) {
- test(s"Model Extraction in $sname") { implicit fix =>
- val ctx = fix._1
- val pgm = fix._2
- val solver = SolverFactory.getFromName(ctx, pgm)(sname).getNewSolver()
- checkSolver(solver, vs.toSet, andJoin(cnstrs))
- }
- }
-
- test(s"Data generation in enum solver") { implicit fix =>
- for ((v,cnstr) <- vs zip cnstrs) {
- val solver = new EnumerationSolver(fix._1.toSctx, fix._2)
- checkSolver(solver, Set(v), cnstr)
- }
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
deleted file mode 100644
index 0543fa60094ee00daf985e085dd95b332794487e..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala
+++ /dev/null
@@ -1,496 +0,0 @@
-package leon
-package integration
-package solvers
-
-import leon.test.LeonTestSuiteWithProgram
-
-import leon.purescala.Common.FreshIdentifier
-import leon.purescala.Expressions._
-import leon.purescala.Definitions._
-import leon.purescala.DefOps
-import leon.purescala.ExprOps
-import leon.purescala.Types._
-import leon.purescala.Constructors._
-
-import leon.synthesis._
-import leon.synthesis.rules.{StringRender, TypedTemplateGenerator}
-import leon.synthesis.strategies.CostBasedStrategy
-import leon.synthesis.graph.AndNode
-
-import leon.evaluators._
-
-import org.scalatest.concurrent.ScalaFutures
-import org.scalatest.Matchers
-import scala.language.implicitConversions
-
-class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with ScalaFutures {
-
- override val leonOpts = List("--solvers=smt-cvc4")
-
- test("Template Generator simple"){ case (ctx: LeonContext, program: Program) =>
- val TTG = new TypedTemplateGenerator(IntegerType) {}
- val e = TTG(hole => Plus(hole, hole))
- val (expr, vars) = e.instantiateWithVars
- vars should have length 2
- expr shouldEqual Plus(Variable(vars(0)), Variable(vars(1)))
-
- val f = TTG.nested(hole => (Minus(hole, expr), vars))
- val (expr2, vars2) = f.instantiateWithVars
- vars2 should have length 3
- vars2(0) shouldEqual vars(0)
- vars2(1) shouldEqual vars(1)
- expr2 shouldEqual Minus(Variable(vars2(2)), expr)
- }
-
- trait withSymbols {
- val x = FreshIdentifier("x", StringType)
- val y = FreshIdentifier("y", StringType)
- val i = FreshIdentifier("i", IntegerType)
- val f = FreshIdentifier("f", FunctionType(Seq(IntegerType), StringType))
- val fd = new FunDef(f, Nil, Seq(ValDef(i)), StringType)
- val fdi = FunctionInvocation(fd.typed, Seq(Variable(i)))
- }
-
- test("toEquations working"){ case (ctx: LeonContext, program: Program) =>
- import StringRender._
- new withSymbols {
- val lhs = RegularStringFormToken(Left("abc"))::RegularStringFormToken(Right(x))::OtherStringFormToken(fdi)::Nil
- val rhs = RegularStringChunk("abcdef")::OtherStringChunk(fdi)::Nil
- val p = toEquations(lhs, rhs)
- p should not be 'empty
- p.get should have length 1
- }
- }
-
- test("toEquations working 2"){ case (ctx: LeonContext, program: Program) =>
- import StringRender._
- new withSymbols {
- val lhs = RegularStringFormToken(Left("abc"))::RegularStringFormToken(Right(x))::OtherStringFormToken(fdi)::RegularStringFormToken(Right(y))::Nil
- val rhs = RegularStringChunk("abcdef")::OtherStringChunk(fdi)::RegularStringChunk("123")::Nil
- val p = toEquations(lhs, rhs)
- p should not be 'empty
- p.get should have length 2
- }
- }
-
- test("toEquations failing"){ case (ctx: LeonContext, program: Program) =>
- import StringRender._
- new withSymbols {
- val lhs = RegularStringFormToken(Left("abc"))::RegularStringFormToken(Right(x))::RegularStringFormToken(Right(y))::Nil
- val rhs = RegularStringChunk("abcdef")::OtherStringChunk(fdi)::RegularStringChunk("123")::Nil
- val p = toEquations(lhs, rhs)
- p should be ('empty)
- }
- }
-
- def applyStringRenderOn(functionName: String): (FunDef, Program) = {
- val ci = synthesisInfos(functionName)
- val search = new Search(ctx, ci, 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 = new SearchContext(synth.sctx, synth.ci.source, orNode, search)
- orNode.expand(hctx)
- }
- val andNodes = orNode.descendants.collect {
- case n: AndNode =>
- n
- }
-
- val rulesApps = (for ((t, i) <- andNodes.zipWithIndex) yield {
- t.ri.asString -> i
- }).toMap
- rulesApps should contain key "String conversion"
-
- val rid = rulesApps("String conversion")
- val path = List(rid)
-
- val solutions = (search.traversePath(path) match {
- case Some(an: AndNode) =>
- val hctx = new SearchContext(synth.sctx, synth.ci.source, an, search)
- an.ri.apply(hctx)
- case _ => throw new Exception("Was not an and node")
- }) match {
- case RuleClosed(solutions) => solutions
- case _ => fail("no solution found")
- }
- solutions should not be 'empty
- val newProgram = DefOps.addFunDefs(synth.program, solutions.head.defs, synth.sctx.functionContext)
- val newFd = ci.fd.duplicate()
- newFd.body = Some(solutions.head.term)
- val newProgram2 = DefOps.transformProgram(DefOps.funDefReplacer { fd =>
- if(fd == ci.fd) Some(newFd) else None
- }, newProgram)
- (newFd, newProgram2)
- }
-
- def getFunctionArguments(functionName: String) = {
- program.lookupFunDef("StringRenderSuite." + functionName) match {
- case Some(fd) => fd.params
- case None =>
- fail("Could not find function " + functionName + " in sources. Other functions:" + program.definedFunctions.map(_.id.name).sorted)
- }
- }
-
- implicit class StringUtils(s: String) {
- def replaceByExample: String =
- s.replaceAll("\\((\\w+):(.*) by example", "\\($1:$2 ensuring { (res: String) => ($1, res) passes { case _ if false => \"\" } }")
- }
-
- val sources = List("""
- |import leon.lang._
- |import leon.collection._
- |import leon.lang.synthesis._
- |import leon.annotation._
- |
- |object StringRenderSuite {
- | def literalSynthesis(i: Int): String = ??? ensuring { (res: String) => (i, res) passes { case 42 => ":42." } }
- |
- | def booleanSynthesis(b: Boolean): String = ??? ensuring { (res: String) => (b, res) passes { case true => "yes" case false => "no" } }
- | def booleanSynthesis2(b: Boolean): String = ??? ensuring { (res: String) => (b, res) passes { case true => "B: true" } }
- | //def stringEscape(s: String): String = ??? ensuring { (res: String) => (s, res) passes { case "\n" => "done...\\n" } }
- |
- | case class Dummy(s: String)
- | def dummyToString(d: Dummy): String = "{" + d.s + "}"
- |
- | case class Dummy2(s: String)
- | def dummy2ToString(d: Dummy2): String = "<" + d.s + ">"
- |
- | case class Config(i: BigInt, t: (Int, String))
- |
- | def configToString(c: Config): String = ??? ensuring { (res: String) => (c, res) passes { case Config(BigInt(1), (2, "3")) => "1: 2 -> 3" } }
- | def configToString2(c: Config): String = ??? ensuring { (res: String) => (c, res) passes { case Config(BigInt(1), (2, "3")) => "3: 1 -> 2" } }
- |
- | sealed abstract class Tree
- | case class Knot(left: Tree, right: Tree) extends Tree
- | case class Bud(v: String) extends Tree
- |
- | def treeToString(t: Tree): String = ???[String] ensuring {
- | (res : String) => (t, res) passes {
- | case Knot(Knot(Bud("17"), Bud("14")), Bud("23")) =>
- | "<<17Y14>Y23>"
- | case Bud("foo") =>
- | "foo"
- | case Knot(Bud("foo"), Bud("foo")) =>
- | "<fooYfoo>"
- | case Knot(Bud("foo"), Knot(Bud("bar"), Bud("foo"))) =>
- | "<fooY<barYfoo>>"
- | }
- | }
- |
- | sealed abstract class BList[T]
- | case class BCons[T](head: (T, T), tail: BList[T]) extends BList[T]
- | case class BNil[T]() extends BList[T]
- |
- | def bListToString[T](b: BList[T], f: T => String) = ???[String] ensuring
- | { (res: String) => (b, res) passes { case BNil() => "[]" case BCons(a, BCons(b, BCons(c, BNil()))) => "[" + f(a._1) + "-" + f(a._2) + ", " + f(b._1) + "-" + f(b._2) + ", " + f(c._1) + "-" + f(c._2) + "]" }}
- |
- | // Handling one rendering function at a time.
- | case class BConfig(flags: BList[Dummy])
- | def bConfigToString(b: BConfig): String = ???[String] ensuring
- | { (res: String) => (b, res) passes { case BConfig(BNil()) => "Config" + bListToString[Dummy](BNil(), (x: Dummy) => dummyToString(x)) } }
- |
- | def customListToString[T](l: List[T], f: T => String): String = ???[String] ensuring
- | { (res: String) => (l, res) passes { case _ if false => "" } }
- |
- | // Handling multiple rendering functions at the same time.
- | case class DConfig(dums: List[Dummy], dums2: List[Dummy2])
- | def dConfigToString(dc: DConfig): String = ???[String] ensuring
- | { (res: String) => (dc, res) passes {
- | case DConfig(Nil(), Nil()) =>
- | "Solution:\n " + customListToString[Dummy](List[Dummy](), (x : Dummy) => dummyToString(x)) + "\n " + customListToString[Dummy2](List[Dummy2](), (x: Dummy2) => dummy2ToString(x)) } }
- |
- | case class Node(tag: String, l: List[Edge])
- | case class Edge(start: Node, end: Node)
- |
- | def nodeToString(n: Node): String = ??? by example
- | def edgeToString(e: Edge): String = ??? by example
- | def listEdgeToString(l: List[Edge]): String = ??? by example
- |
- | // Test if it can infer functions based on sealed classes.
- | abstract class ThreadId
- | case object T1 extends ThreadId
- | case object T2 extends ThreadId
- | case object T3 extends ThreadId
- | case object T4 extends ThreadId
- | case object T5 extends ThreadId
- |
- | case class ThreadConfig(t: ThreadId, push: Option[Int])
- |
- | def threadConfigToString(t: ThreadConfig): String = ???[String] ensuring {
- | (res: String) => (t, res) passes {
- | case ThreadConfig(T1, Some(2)) => "T1: Push 2"
- | case ThreadConfig(T2, None()) => "T2: Skip"
- | }
- | }
- |
- | def doubleOptionToString(pushed: Option[Int], pulled: Option[Int]): String = {
- | ???[String]
- | } ensuring {
- | (res : String) => ((pushed, pulled), res) passes {
- | case (None(), None()) =>
- | "Config: "
- | case (None(), Some(0)) =>
- | "Config: pulled 0"
- | case (Some(0), None()) =>
- | "Config: pushed 0 "
- | }
- | }
- |
- | case class MultipleConfig(i: Int, next: Option[MultipleConfig])
- |
- | def multipleConfigToString(m: MultipleConfig): String = {
- | ???[String]
- | } ensuring {
- | (res: String) => (m, res) passes {
- | case MultipleConfig(0, None()) => "MultipleConfig: 0"
- | case MultipleConfig(0, Some(MultipleConfig(1, None()))) => "MultipleConfig: 0\nMultipleConfig: 1"
- | }
- | }
- |
- | def setToString(in : Set[String]): String = {
- | ???[String]
- | } ensuring {
- | (res : String) => (in, res) passes {
- | case s if s == Set[String]("1", "2", "0") =>
- | "{0 | 1 | 2}"
- | case s if s == Set[String]() =>
- | "{}"
- | }
- | }
- |}
- """.stripMargin.replaceByExample)
-
- implicit val (ctx, program) = getFixture()
-
- val synthesisInfos = SourceInfo.extractFromProgram(ctx, program).map(si => si.fd.id.name -> si).toMap
-
- def synthesizeAndTest(functionName: String, tests: (Seq[Expr], String)*) {
- val (fd, program) = applyStringRenderOn(functionName)
- val when = new DefaultEvaluator(ctx, program)
- for((in, out) <- tests) {
- val expr = functionInvocation(fd, in)
- when.eval(expr) match {
- case EvaluationResults.Successful(value) => value shouldEqual StringLiteral(out)
- case EvaluationResults.EvaluatorError(msg) => fail(/*program + "\n" + */msg)
- case EvaluationResults.RuntimeError(msg) => fail(/*program + "\n" + */"Runtime: " + msg)
- }
- }
- }
- def synthesizeAndAbstractTest(functionName: String)(tests: (FunDef, Program) => Seq[(Seq[Expr], Expr)]) {
- val (fd, program) = applyStringRenderOn(functionName)
- val when_abstract = new AbstractEvaluator(ctx, program)
- for((in, out) <- tests(fd, program)) {
- val expr = functionInvocation(fd, in)
- when_abstract.eval(expr) match {
- case EvaluationResults.Successful(value) => val m = ExprOps.canBeHomomorphic(value._1, out)
- assert(m.nonEmpty, value._1 + " was not homomorphic with " + out)
- case EvaluationResults.EvaluatorError(msg) => fail(/*program + "\n" + */msg)
- case EvaluationResults.RuntimeError(msg) => fail(/*program + "\n" + */"Runtime: " + msg)
- }
- }
- }
- abstract class CCBuilder(ccName: String, prefix: String = "StringRenderSuite.")(implicit program: Program) {
- val caseClassName = prefix + ccName
- def getType: TypeTree = program.lookupCaseClass(caseClassName).get.typed
- def apply(s: Expr*): CaseClass = {
- CaseClass(program.lookupCaseClass(caseClassName).get.typed, s.toSeq)
- }
- def apply(s: String): CaseClass = this.apply(StringLiteral(s))
- }
- abstract class ParamCCBuilder(caseClassName: String, prefix: String = "StringRenderSuite.")(implicit program: Program) {
- def apply(types: TypeTree*)(s: Expr*): CaseClass = {
- CaseClass(program.lookupCaseClass(prefix+caseClassName).get.typed(types),
- s.toSeq)
- }
- }
- def method(fName: String)(implicit program: Program) = {
- program.lookupFunDef("StringRenderSuite." + fName).get
- }
- abstract class paramMethod(fName: String)(implicit program: Program) {
- val fd = program.lookupFunDef("StringRenderSuite." + fName).get
- def apply(types: TypeTree*)(args: Expr*) =
- FunctionInvocation(fd.typed(types), args)
- }
-
- // Mimics the file above, allows construction of expressions.
- case class Constructors(program: Program) {
- implicit val p = program
- implicit def CCBuilderToType(c: CCBuilder): TypeTree = c.getType
- object Knot extends CCBuilder("Knot")
- object Bud extends CCBuilder("Bud")
- object Dummy extends CCBuilder("Dummy")
- object Dummy2 extends CCBuilder("Dummy2")
- object Cons extends ParamCCBuilder("Cons", "leon.collection.")
- object Nil extends ParamCCBuilder("Nil", "leon.collection.")
- object List {
- def apply(types: TypeTree*)(elems: Expr*): CaseClass = {
- elems.toList match {
- case scala.collection.immutable.Nil => Nil(types: _*)()
- case a::b => Cons(types: _*)(a, List(types: _*)(b: _*))
- }
- }
- }
- object Some extends ParamCCBuilder("Some", "leon.lang.")
- object None extends ParamCCBuilder("None", "leon.lang.")
-
- object BCons extends ParamCCBuilder("BCons")
- object BNil extends ParamCCBuilder("BNil")
- object BList {
- def apply(types: TypeTree*)(elems: Expr*): CaseClass = {
- elems.toList match {
- case scala.collection.immutable.Nil => BNil(types: _*)()
- case a::b => BCons(types: _*)(a, BList(types: _*)(b: _*))
- }
- }
- def helper(types: TypeTree*)(elems: (Expr, Expr)*): CaseClass = {
- this.apply(types: _*)(elems.map(x => tupleWrap(Seq(x._1, x._2))): _*)
- }
- }
- object Config extends CCBuilder("Config") {
- def apply(i: Int, b: (Int, String)): CaseClass =
- this.apply(InfiniteIntegerLiteral(i), tupleWrap(Seq(IntLiteral(b._1), StringLiteral(b._2))))
- }
- object BConfig extends CCBuilder("BConfig")
- object DConfig extends CCBuilder("DConfig")
- lazy val dummyToString = method("dummyToString")
- lazy val dummy2ToString = method("dummy2ToString")
- lazy val bListToString = method("bListToString")
- object customListToString extends paramMethod("customListToString")
- lazy val threadConfigToString = method("threadConfigToString")
- object T3 extends CCBuilder("T3")
- object ThreadConfig extends CCBuilder("ThreadConfig")
-
- lazy val doubleOptionToString = method("doubleOptionToString")
- object MultipleConfig extends CCBuilder("MultipleConfig")
- lazy val multipleConfigToString = method("multipleConfigToString")
- }
-
- test("Literal synthesis"){ case (ctx: LeonContext, program: Program) =>
- synthesizeAndTest("literalSynthesis",
- Seq(IntLiteral(156)) -> ":156.",
- Seq(IntLiteral(-5)) -> ":-5.")
- }
-
- test("boolean Synthesis"){ case (ctx: LeonContext, program: Program) =>
- synthesizeAndTest("booleanSynthesis",
- Seq(BooleanLiteral(true)) -> "yes",
- Seq(BooleanLiteral(false)) -> "no")
- }
-
- test("Boolean synthesis 2"){ case (ctx: LeonContext, program: Program) =>
- synthesizeAndTest("booleanSynthesis2",
- Seq(BooleanLiteral(true)) -> "B: true",
- Seq(BooleanLiteral(false)) -> "B: false")
- }
-
- /*test("String escape synthesis"){ case (ctx: LeonContext, program: Program) =>
- synthesizeAndTest("stringEscape",
- Seq(StringLiteral("abc")) -> "done...abc",
- Seq(StringLiteral("\t")) -> "done...\\t")
-
- }*/
-
- test("Case class synthesis"){ case (ctx: LeonContext, program: Program) =>
- val c = Constructors(program); import c._
- StringRender.enforceDefaultStringMethodsIfAvailable = false
- synthesizeAndTest("configToString",
- Seq(Config(4, (5, "foo"))) -> "4: 5 -> foo")
- }
-
- test("Out of order synthesis"){ case (ctx: LeonContext, program: Program) =>
- val c = Constructors(program); import c._
- StringRender.enforceDefaultStringMethodsIfAvailable = false
- synthesizeAndTest("configToString2",
- Seq(Config(4, (5, "foo"))) -> "foo: 4 -> 5")
- }
-
- test("Recursive case class synthesis"){ case (ctx: LeonContext, program: Program) =>
- val c = Constructors(program); import c._
- synthesizeAndTest("treeToString",
- Seq(Knot(Knot(Bud("aa"), Bud("bb")), Knot(Bud("mm"), Bud("nn")))) ->
- "<<aaYbb>Y<mmYnn>>")
- }
-
- test("Abstract synthesis"){ case (ctx: LeonContext, program: Program) =>
- val c = Constructors(program); import c._
- val d = FreshIdentifier("d", Dummy)
-
- synthesizeAndTest("bListToString",
- Seq(BList.helper(Dummy)(
- (Dummy("a"), Dummy("b")),
- (Dummy("c"), Dummy("d"))),
- Lambda(Seq(ValDef(d)), FunctionInvocation(dummyToString.typed, Seq(Variable(d)))))
- ->
- "[{a}-{b}, {c}-{d}]")
-
- }
-
-
- test("Pretty-printing using inferred not yet defined functions in argument"){ case (ctx: LeonContext, program: Program) =>
- StringRender.enforceDefaultStringMethodsIfAvailable = true
- synthesizeAndAbstractTest("bConfigToString"){ (fd: FunDef, program: Program) =>
- val c = Constructors(program); import c._
- val arg = BList.helper(Dummy)((Dummy("a"), Dummy("b")))
- val d = FreshIdentifier("d", Dummy)
- val lambdaDummyToString = Lambda(Seq(ValDef(d)), FunctionInvocation(dummyToString.typed, Seq(Variable(d))))
- val listDummyToString = functionInvocation(bListToString, Seq(arg, lambdaDummyToString))
- Seq(Seq(BConfig(arg)) ->
- StringConcat(StringLiteral("Config"), listDummyToString))
- }
- }
-
- test("Pretty-printing using an existing not yet defined parametrized function") { case (ctx: LeonContext, program: Program) =>
- StringRender.enforceDefaultStringMethodsIfAvailable = true
-
- synthesizeAndAbstractTest("dConfigToString"){ (fd: FunDef, program: Program) =>
- val c = Constructors(program); import c._
-
- val listDummy1 = c.List(Dummy)(Dummy("a"), Dummy("b"), Dummy("c"))
- val listDummy2 = c.List(Dummy2)(Dummy2("1"), Dummy2("2"))
- val arg = DConfig(listDummy1, listDummy2)
-
- val d = FreshIdentifier("d", Dummy)
- val lambdaDummyToString = Lambda(Seq(ValDef(d)), FunctionInvocation(dummyToString.typed, Seq(Variable(d))))
- val d2 = FreshIdentifier("d2", Dummy2)
- val lambdaDummy2ToString = Lambda(Seq(ValDef(d2)), FunctionInvocation(dummy2ToString.typed, Seq(Variable(d2))))
-
- Seq(Seq(arg) ->
- StringConcat(StringConcat(StringConcat(
- StringLiteral("Solution:\n "),
- customListToString(Dummy)(listDummy1, lambdaDummyToString)),
- StringLiteral("\n ")),
- customListToString(Dummy2)(listDummy2, lambdaDummy2ToString)))
- }
- }
-
- test("Pretty-printing a hierarchy of case object") { case (ctx, program) =>
- val c= Constructors(program); import c._
- synthesizeAndTest("threadConfigToString",
- Seq(c.ThreadConfig(c.T3(), c.Some(Int32Type)(IntLiteral(5)))) -> "T3: Push 5"
- )
- }
-
- test("Activating horizontal markovization should work") { case (ctx, program) =>
- val c = Constructors(program); import c._
- synthesizeAndTest("doubleOptionToString",
- Seq(c.Some(Int32Type)(IntLiteral(1)), c.Some(Int32Type)(IntLiteral(2))) -> "Config: pushed 1 pulled 2"
- )
- }
-
- test("reuse of the same function twice should work") { case (ctx, program) =>
- synthesizeAndAbstractTest("multipleConfigToString"){ (fd: FunDef, program: Program) =>
- val numOfMultipleConfig = program.definedFunctions.map(fd => ExprOps.fold[Int]{ case (StringLiteral("MultipleConfig: "), _) => 1 case (e, children) => children.sum }(fd.fullBody)).reduce(_ + _)
- numOfMultipleConfig should equal(1)
- Seq()
- }
- }
-
- test("setToString should be found") { case (ctx, program) =>
- val c= Constructors(program); import c._
- synthesizeAndTest("setToString",
- Seq(FiniteSet(Set(StringLiteral("a"), StringLiteral("c"), StringLiteral("b"), StringLiteral("e")), StringType)) ->
- "{a | b | c | e}"
- )
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
deleted file mode 100644
index 8f6f295b2075fa5d66af8f43baac631c17936aca..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ /dev/null
@@ -1,282 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-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 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._
-
-/**
- * @author Mikael
- */
-class StringSolverSuite extends FunSuite with Matchers with ScalaFutures {
- val k = new MMap[String, Identifier]
-
- val x = FreshIdentifier("x")
- val y = FreshIdentifier("y")
- val z = FreshIdentifier("z")
- val u = FreshIdentifier("u")
- val v = FreshIdentifier("v")
- val w = FreshIdentifier("w")
- k ++= List("x" -> x, "y" -> y, "z" -> z, "u" -> u, "v" -> v, "w" -> w)
-
- implicit class EquationMaker(lhs: String) {
- def convertStringToStringFrom(s: String)(implicit idMap: MMap[String, Identifier]): StringSolver.StringForm = {
- for(elem <- s.split("\\+").toList) yield {
- if(elem.startsWith("\"")) {
- Left(elem.substring(1, elem.length - 1))
- } else if(elem(0).isDigit) {
- Left(elem)
- } else {
- val id = idMap.getOrElse(elem, {
- val res = FreshIdentifier(elem)
- idMap += elem -> res
- res
- })
- Right(id)
- }
- }
- }
-
- def ===(rhs: String)(implicit k: MMap[String, Identifier]): StringSolver.Equation = {
- (convertStringToStringFrom(lhs), rhs)
- }
- def ====(rhs: String)(implicit k: MMap[String, Identifier]): StringSolver.GeneralEquation = {
- (convertStringToStringFrom(lhs), convertStringToStringFrom(rhs))
- }
- }
-
- import StringSolver._
-
- def m = MMap[String, Identifier]()
-
- test("simplifyProblem"){
- implicit val kk = k
- simplifyProblem(List("x" === "1"), Map()) should equal (Some((Nil, Map(x -> "1"))))
- simplifyProblem(List("y" === "23"), Map()) should equal (Some((Nil, Map(y -> "23"))))
- simplifyProblem(List("1" === "1"), Map()) should equal (Some((Nil, Map())))
- simplifyProblem(List("2" === "1"), Map()) should equal (None)
- simplifyProblem(List("x" === "1", "y+x" === "12"), Map()) should equal (Some((List("y+1" === "12"), Map(x -> "1"))))
- }
-
- test("noLeftRightConstants") {
- implicit val kk = k
- noLeftRightConstants(List("x" === "1"), Map()) should equal (Some((List("x" === "1"), Map())))
- noLeftRightConstants(List("y+2" === "12"), Map()) should equal (Some((List("y" === "1"), Map())))
- noLeftRightConstants(List("3+z" === "31"), Map()) should equal (Some((List("z" === "1"), Map())))
- noLeftRightConstants(List("1+u+2" === "1, 2"), Map()) should equal (Some((List("u" === ", "), Map())))
- }
- test("forwardStrategy") {
- implicit val kk = k
- forwardStrategy(List("x+3" === "123", "x+y" === "1245"), Map()) should equal (Some((Nil, Map(x -> "12", y -> "45"))))
- forwardStrategy(List("y+z" === "4567", "x+3" === "123", "x+y" === "1245"), Map()) should equal (Some((Nil, Map(x -> "12", y -> "45", z -> "67"))))
- }
-
- test("occurrences") {
- occurrences("*?)*","*?)*?)**?)*???*") should equal (List(0, 3, 7))
- }
-
- test("repartitions") {
- repartitions(List("*"), "?*???????") should equal (List(List(1)))
- repartitions(List("*","*"), "?*???????") should equal (List())
- repartitions(List("1","2"), "?*1??2???") should equal (List(List(2, 5)))
- repartitions(List("*","*"), "?*????*???*") should equal (List(List(1, 6), List(1, 10), List(6, 10)))
- }
-
- test("simpleSplit") {
- implicit val stats = Map(x -> 1, y -> 1) // Dummy stats
- simpleSplit(List(), "").toList should equal (List(Map()))
- simpleSplit(List(), "abc").toList should equal (Nil)
- simpleSplit(List(x), "abc").toList should equal (List(Map(x -> "abc")))
- simpleSplit(List(x, y), "ab").toList should equal (List(Map(x -> "", y -> "ab"), Map(x -> "ab", y -> ""), Map(x -> "a", y -> "b")))
- simpleSplit(List(x, x), "ab").toList should equal (Nil)
- simpleSplit(List(x, y, x), "aba").toList should equal (List(Map(x -> "", y -> "aba"), Map(x -> "a", y -> "b")))
- }
-
- test("simpleSplitPriority") { // Just guesses some values for y.
- implicit val stats = Map(x -> 1, y -> 2)
- simpleSplit(List(x, y, y, y), "a121212").toList should equal (List(Map(y -> "12"), Map(y -> "2"), Map(y -> "")))
- }
-
-
- test("solve switch") {
- implicit val kk = k
- solve(List("x+y" === "1234", "y+x" === "1234")).toSet should equal (Set(Map(x -> "1234", y -> ""), Map(x -> "", y -> "1234")))
- solve(List("x+y" === "1234", "y+x" === "3412")).toList should equal (List(Map(x -> "12", y -> "34")))
- solve(List("x+y" === "1234", "y+x" === "4123")).toList should equal (List(Map(x -> "123", y -> "4")))
- solve(List("x+y" === "1234", "y+x" === "2341")).toList should equal (List(Map(x -> "1", y -> "234")))
- }
-
- test("solve inner") {
- implicit val kk = k
- solve(List("x+2+y" === "123")).toList should equal (List(Map(x -> "1", y -> "3")))
- solve(List("x+2+y+z" === "123")).toSet should equal (Set(Map(x -> "1", y -> "3", z -> ""), Map(x -> "1", y -> "", z -> "3")))
- solve(List("x+2+y" === "12324")).toSet should equal (Set(Map(x -> "1", y -> "324"), Map(x -> "123", y -> "4")))
- }
-
- test("isTransitivelyBounded") {
- implicit val kk = k
- isTransitivelyBounded(List("1" ==== "2")) should be(true)
- isTransitivelyBounded(List("2" ==== "2")) should be(true)
- isTransitivelyBounded(List("x+2" ==== "2")) should be(true)
- isTransitivelyBounded(List("x+2" ==== "1")) should be(true)
- isTransitivelyBounded(List("x+2" ==== "2+x")) should be(false)
- isTransitivelyBounded(List("x+2" ==== "2+y")) should be(false)
- isTransitivelyBounded(List("x+2" ==== "2+y", "y" ==== "1")) should be(true)
- isTransitivelyBounded(List("x+2" ==== "2+x", "x" ==== "1")) should be(true)
- isTransitivelyBounded(List("x+y+z" ==== "1234", "u+v" ==== "y+42+x")) should be(true)
- }
-
- test("solveGeneralProblem") {
- implicit val kk = k
- solveGeneralProblem(List("x+y" ==== "12", "u+v" ==== "y+x")).toSet should equal (
- Set(
- Map(x -> "", y -> "12", u -> "", v -> "12"),
- Map(x -> "", y -> "12", u -> "1", v -> "2"),
- Map(x -> "", y -> "12", u -> "12", v -> ""),
- Map(x -> "1", y -> "2", u -> "", v -> "21"),
- Map(x -> "1", y -> "2", u -> "2", v -> "1"),
- Map(x -> "1", y -> "2", u -> "21", v -> ""),
- Map(x -> "12", y -> "", u -> "", v -> "12"),
- Map(x -> "12", y -> "", u -> "1", v -> "2"),
- Map(x -> "12", y -> "", u -> "12", v -> "")
- )
- )
- }
-
- test("constantPropagate") {
- implicit val kk = k
- val complexString = "abcdefmlkjsdqfmlkjqezpijbmkqjsdfmijzmajmpqjmfldkqsjmkj"
- solve(List("w+5+x+y+z+u+v" === (complexString+"5"))).toList should equal (
- List(Map(w -> complexString,
- x -> "",
- y -> "",
- z -> "",
- u -> "",
- v -> "")))
- }
-
- test("constantPropagate2") {
- implicit val kk = k
- val complexString = "abcdefmlkjsdqfmlkjqezpijbmkqjsdfmijzmajmpqjmfldkqsjmkj"
- val complexString2 = complexString.reverse
- val complexString3 = "flmqmslkjdqfmleomijgmlkqsjdmfijmqzoijdfmlqksjdofijmez"
- solve(List("w+5+x+5+z" === (complexString+"5" + complexString2 + "5" + complexString3))).toList should equal (
- List(Map(w -> complexString,
- x -> complexString2,
- z -> complexString3)))
- }
-
- test("ListInt") {
- implicit val idMap = MMap[String, Identifier]()
- val problem = List(
- """const8+const4+"12"+const5+const+"-1"+const1+const3+const2+const6+const9""" === "(12, -1)",
- """const8+const4+"1"+const5+const3+const6+const9""" === "(1)",
- """const8+const7+const9""" === "()")
- val solutions = solve(problem)
- solutions should not be 'empty
- val solution = solutions.head
- errorcheck(problem, solution) should be(None)
- }
-
- test("ListInt as List(...)") {
- implicit val idMap = MMap[String, Identifier]()
- val problem = List("const8" === "List(",
- "const8+const7+const9" === "List()",
- """const8+const4+"1"+const5+const3+const6+const9""" === "List(1)",
- """const8+const4+"12"+const5+const+"-1"+const1+const3+const2+const6+const9""" === "List(12, -1)")
- val solution = solve(problem)
- solution should not be 'empty
- val firstSolution = solution(0)
- firstSolution(idMap("const8")) should equal("List(")
- firstSolution(idMap("const4")) should equal("")
- }
-
- test("solveJadProblem") {
- val lhs = """const38+const34+const7+"T1"+const8+const3+const9+const5+"5"+const6+const10+const35+const30+const13+"T1"+const14+const31+const30+const7+"T2"+const8+const2+const9+const4+const10+const31+const30+const25+"T1"+const26+"Push"+const27+const20+"5"+const21+const28+const22+const29+const31+const30+const13+"T2"+const14+const31+const30+const25+"T2"+const26+"Pop"+const27+const19+const28+const23+"5"+const24+const29+const31+const33+const32+const32+const32+const32+const32+const36+const39=="T1: call Push(5)"""
- implicit val idMap = MMap[String, Identifier]()
-
- val expected = """T1: call Push(5)
-T1: internal
-T2: call Pop()
-T1: ret Push(5)
-T2: internal
-T2: ret Pop() -> 5"""
-
- val problem: Problem = List(lhs === expected)
-
- solve(problem) should not be 'empty
- }
-
- test("SolvePropagateEquationProblem") {
- implicit val idMap = MMap[String, Identifier]()
- val problem = List(
- "a+b+c+d" === "1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890",
- "k+a+b+c+d" === "21234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567891"
- )
- val p = Future { solve(problem) }
- assert(p.isReadyWithin(2 seconds), "Could not solve propagate")
- p.futureValue should be('empty)
- }
-
- test("SolveRightCheckingProblem") {
- implicit val idMap = MMap[String, Identifier]()
- val problem = List(
- "u+v+w+a+b+c+d" === "123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789",
- "u+v+w+k+a+k+b+c+d" === "21234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567892"
- )
- val p = Future { solve(problem) }
- assert(p.isReadyWithin(2 seconds), "Could not solve propagate")
- p.futureValue should not be('empty)
- }
-
- test("solveMinChange") {
- implicit val idMap = MMap[String, Identifier]()
- val problem = List(
- "u+v+w" === "akbc"
- )
- val u = idMap("u")
- val v = idMap("v")
- val w = idMap("w")
- val solutions = solveMinChange(problem, Map(u -> "a", v -> "b", w -> "c"))
- solutions(0) should equal (Map(u -> "ak"))
- solutions(1) should equal (Map(v -> "kb"))
- (2 to 5).toSet.map((i: Int) => solutions(i)) should equal (Set(Map(u -> "", v -> "akb")
- , Map(u -> "a", v -> "kb")
- , Map(u -> "ak", v -> "b")
- , Map(u -> "akb", v -> "")))
- }
-
- test("solveMinChange 2") {
- implicit val idMap = MMap[String, Identifier]()
- val problem = List(
- "u+v+w" === "Welcome to Implicit website builder4!",
- "a+v+b+c" === "You are looking at the page generated by the code on the left. Implicit website builder is a technology allowing you to either modify the code or the view. Try it now! Edit this paragraph!"
- )
- val u = idMap("u")
- val v = idMap("v")
- val w = idMap("w")
- val a = idMap("a")
- val b = idMap("b")
- val c = idMap("c")
- val init = Map(u -> "Welcome to ", v -> "Implicit website builder", w -> "!",
- a -> "You are looking at the page generated by the code on the left. ",
- b -> " is a technology allowing you to ",
- c -> "either modify the code or the view. Try it now! Edit this paragraph!")
- val solutions = solveMinChange(problem, init)
- solutions(0) should equal (Map(w -> "4!"))
- }
-}
\ No newline at end of file
diff --git a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala b/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
deleted file mode 100644
index ca0eaf2b71cfd04b384842d3314ce5cc22b6c9d4..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
+++ /dev/null
@@ -1,77 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon._
-import leon.test._
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-
-class TimeoutSolverSuite extends LeonTestSuite {
- private class IdioticSolver(val sctx: SolverContext, val program: Program) extends Solver with NaiveAssumptionSolver {
- val name = "Idiotic"
- val description = "Loops"
-
- var interrupted = false
-
- override def check: Option[Boolean] = {
- while(!interrupted) {
- Thread.sleep(50L)
- }
- None
- }
-
- def recoverInterrupt() {
- interrupted = false
- }
-
- def interrupt() {
- interrupted = true
- }
-
- def assertCnstr(e: Expr) = {}
-
- def push() {}
- def pop() {}
-
- def free() {}
-
- def reset() {}
-
- def getModel = ???
- }
-
- private def getTOSolver(ctx: LeonContext): SolverFactory[Solver] = {
- SolverFactory("idiotic", () => (new IdioticSolver(ctx.toSctx, Program.empty) with TimeoutSolver).setTimeout(200L))
- }
-
- private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {
- val s = sf.getNewSolver()
- s.assertCnstr(e)
- s.check
- }
-
- test("TimeoutSolver 1") { ctx =>
- val sf = getTOSolver(ctx)
- assert(check(sf, BooleanLiteral(true)) === None)
- assert(check(sf, BooleanLiteral(false)) === None)
-
- val x = Variable(FreshIdentifier("x", IntegerType))
- assert(check(sf, Equals(x, x)) === None)
-
- sf.shutdown()
- }
-
- test("TimeoutSolver 2") { ctx =>
- val sf = getTOSolver(ctx)
- val x = Variable(FreshIdentifier("x", IntegerType))
- val o = InfiniteIntegerLiteral(1)
- assert(check(sf, Equals(Plus(x, o), Plus(o, x))) === None)
- assert(check(sf, Equals(Plus(x, o), x)) === None)
-
- sf.shutdown()
- }
-}
diff --git a/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala b/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
deleted file mode 100644
index 04450dfc2eef9bdf705e8a4bb42660ddf114383c..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
+++ /dev/null
@@ -1,51 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.integration.solvers
-
-import leon.LeonContext
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.solvers._
-
-class UnrollingSolverSuite extends LeonSolverSuite {
-
- val sources = List(
- """|import leon.lang._
- |
- |object Minimal {
- | def f(x: BigInt): BigInt = {
- | if (x > 0) {
- | x + f(x-1)
- | } else {
- | BigInt(1)
- | }
- | } ensuring { _ > 0 }
- |}""".stripMargin
- )
-
- def getSolver(implicit ctx: LeonContext, pgm: Program) = {
- SolverFactory.getFromName(ctx, pgm)("unrollz3").getNewSolver()
- }
-
- test("'true' should be valid") { implicit fix =>
- valid(BooleanLiteral(true))
- }
-
- test("'false' should be invalid") { implicit fix =>
- invalid(BooleanLiteral(false))
- }
-
- test("unrolling should enable recursive definition verification") { implicit fix =>
- val pgm = fix._2
- val fd = pgm.lookup("Minimal.f").collect {
- case fd: FunDef => fd
- }.get
-
- def f(e: Expr) = FunctionInvocation(fd.typed, Seq(e))
- val x = FreshIdentifier("x", IntegerType).toVariable
-
- valid(GreaterThan(f(x), InfiniteIntegerLiteral(0)))
- }
-}
diff --git a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala b/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
deleted file mode 100644
index ba2ce427d4f052dac39a07a025ae298fb0e66156..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala
+++ /dev/null
@@ -1,37 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.isabelle
-
-import scala.concurrent._
-import scala.concurrent.duration._
-import scala.concurrent.ExecutionContext.Implicits.global
-
-import leon._
-import leon.frontends.scalac.ExtractionPhase
-import leon.purescala.Definitions._
-import leon.utils._
-import leon.solvers.isabelle._
-import leon.test._
-import leon.utils.PreprocessingPhase
-
-class IsabelleLibrarySuite extends LeonRegressionSuite {
-
- object IsabelleNoopPhase extends UnitPhase[Program] {
- val name = "isabelle-noop"
- val description = "Isabelle definitions"
-
- implicit val debugSection = DebugSectionIsabelle
-
- def apply(context: LeonContext, program: Program): Unit =
- Await.result(IsabelleEnvironment(context, program).map(_ => ()), Duration.Inf)
- }
-
- test("Define the library") {
- val pipeline = ExtractionPhase andThen new PreprocessingPhase andThen IsabelleNoopPhase
-
- val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
-
- pipeline.run(ctx, Nil)
- }
-
-}
diff --git a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala b/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
deleted file mode 100644
index 7540c296df2b26ac93a6e193466d9563602c591b..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.isabelle
-
-import leon.regression.verification.VerificationSuite
-
-class IsabelleVerificationSuite extends VerificationSuite {
-
- val testDir = "regression/verification/isabelle/"
- override val isabelle = true
-
- val optionVariants: List[List[String]] = List(List("--solvers=isabelle"))
-
-}
diff --git a/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala b/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
deleted file mode 100644
index c92c2ddcc3fff04058d916354838684d5ffc82d4..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/frontends/FrontEndsSuite.scala
+++ /dev/null
@@ -1,49 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.frontends
-
-import leon._
-import leon.test._
-import java.io.File
-
-class FrontEndsSuite extends LeonRegressionSuite {
-
- def testFrontend(f: File, forError: Boolean) = {
- val pipeline =
- frontends.scalac.ExtractionPhase andThen
- new utils.PreprocessingPhase andThen
- NoopPhase()
-
- test ("Testing " + f.getName) {
- val ctx = createLeonContext()
- if (forError) {
- intercept[LeonFatalError]{
- pipeline.run(ctx, List(f.getAbsolutePath))
- }
- } else {
- pipeline.run(ctx, List(f.getAbsolutePath))
- }
- }
- }
-
- private def forEachFileIn(path : String)(block : File => Unit) {
- val fs = filesInResourceDir(path, _.endsWith(".scala"))
-
- for(f <- fs) {
- block(f)
- }
- }
-
- val baseDir = "regression/frontends/"
-
- forEachFileIn(baseDir+"passing/") { f =>
- testFrontend(f, false)
- }
- forEachFileIn(baseDir+"error/simple/") { f =>
- testFrontend(f, true)
- }
- forEachFileIn(baseDir+"error/xlang/") { f =>
- testFrontend(f, true)
- }
-
-}
diff --git a/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala b/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala
deleted file mode 100644
index 348f93ad78166891514cfc7807d29f8ed51d5992..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala
+++ /dev/null
@@ -1,58 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.orb
-import leon.test._
-
-import leon._
-import invariant.engine._
-import laziness._
-import verification._
-
-import java.io.File
-
-class LazyEvalRegressionSuite extends LeonRegressionSuite {
- private def forEachFileIn(path: String)(block: File => Unit) {
- val fs = filesInResourceDir(path, _.endsWith(".scala"))
- for (f <- fs) {
- block(f)
- }
- }
-
- private def testLazyVerification(f: File, ctx: LeonContext) {
- val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
- new leon.utils.PreprocessingPhase
- val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
- val processPipe = LazinessEliminationPhase
- val (ctx3, report) = processPipe.run(ctx2, program)
- report.stateVerification match {
- case None => fail(s"No state verification report found!")
- case Some(rep) =>
- val fails = rep.vrs.collect{ case (vc, vr) if !vr.isValid => vc }
- if (!fails.isEmpty)
- fail(s"State verification failed for functions ${fails.map(_.fd).mkString("\n")}")
- }
- report.resourceVeri match {
- case None => fail(s"No resource verification report found!")
- case Some(rep: InferenceReport) =>
- val fails = rep.conditions.filterNot(_.prettyInv.isDefined)
- if (!fails.isEmpty)
- fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
- case Some(rep: VerificationReport) =>
- val fails = rep.vrs.collect{ case (vc, vr) if !vr.isValid => vc }
- if (!fails.isEmpty)
- fail(s"Resource verification failed for functions ${fails.map(_.fd).mkString("\n")}")
- }
- }
-/*
- forEachFileIn("regression/orb/lazy/withconst") { f =>
- test("Lazy evaluation w/o Orb: " + f.getName) {
- testLazyVerification(f, createLeonContext("--lazy", "--silent", "--timeout=30"))
- }
- }
-
- forEachFileIn("regression/orb/lazy/withorb") { f =>
- test("Lazy evaluation with Orb: " + f.getName) {
- testLazyVerification(f, createLeonContext("--lazy", "--useOrb", "--silent", "--vcTimeout=15", "--timeout=30"))
- }
- }*/
-}
diff --git a/src/test/scala/leon/regression/orb/OrbInstrumentationTestSuite.scala b/src/test/scala/leon/regression/orb/OrbInstrumentationTestSuite.scala
deleted file mode 100644
index bb4bb564e4c584c65dbdabe2d792fafcd1f5d5f8..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/orb/OrbInstrumentationTestSuite.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.orb
-import leon.test._
-import leon._
-import leon.purescala.Definitions._
-import leon.invariant.engine._
-import leon.transformations._
-import java.io.File
-import leon.purescala.Types.TupleType
-
-class OrbInstrumentationTestSuite extends LeonRegressionSuite {
-
- test("TestInstrumentation") {
- val ctx = createLeonContext("--inferInv", "--minbounds", "--timeout=" + 10)
- val testFilename = toTempFile(
- """
- import leon.annotation._
- import leon.invariant._
- import leon.instrumentation._
-
- object Test {
- sealed abstract class List
- case class Cons(tail: List) extends List
- case class Nil() extends List
-
- // proved with unrolling=0
- def size(l: List) : BigInt = (l match {
- case Nil() => BigInt(0)
- case Cons(t) => 1 + size(t)
- }) ensuring(res => tmpl(a => time <= a))
- }""")
- val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
- new leon.utils.PreprocessingPhase
- val (ctx2, program) = beginPipe.run(ctx, testFilename)
- val processPipe = InstrumentationPhase
- // check properties.
- val (ctx3, instProg) = processPipe.run(ctx2, program)
- val sizeFun = instProg.definedFunctions.find(_.id.name.startsWith("size"))
- if (!sizeFun.isDefined || !sizeFun.get.returnType.isInstanceOf[TupleType])
- fail("Error in instrumentation")
- }
-
- def toTempFile(content: String): List[String] = {
- val pipeline = leon.utils.TemporaryInputPhase
- pipeline.run(createLeonContext(), (List(content), Nil))._2
- }
-}
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
deleted file mode 100644
index a8d4113f3cc6d2dbd1129a730a0636ac76912e50..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+++ /dev/null
@@ -1,66 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.orb
-import leon.test._
-
-import leon._
-import leon.purescala.Definitions._
-import leon.invariant.engine._
-import leon.transformations._
-
-import java.io.File
-
-class OrbRegressionSuite extends LeonRegressionSuite {
- private def forEachFileIn(path: String)(block: File => Unit) {
- val fs = filesInResourceDir(path, _.endsWith(".scala"))
- for (f <- fs) {
- block(f)
- }
- }
-
- private def testInference(f: File, bound: Option[Int] = None) {
- val ctx = createLeonContext("--inferInv", "--vcTimeout=3", "--solvers=smt-z3", "--silent", "--timeout=120")
- val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
- new leon.utils.PreprocessingPhase
- val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
- val processPipe = InferInvariantsPhase
- val (ctx3, report) = processPipe.run(ctx2, program)
- if (report.conditions.isEmpty)
- fail(s"Nothing was solved")
- else {
- val fails = report.conditions.filterNot(_.prettyInv.isDefined)
- if (!fails.isEmpty)
- fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
- }
- }
-
- forEachFileIn("regression/orb/timing") { f =>
- test("Timing: " + f.getName) {
- testInference(f)
- }
- }
-
- forEachFileIn("regression/orb/stack/") { f =>
- test("Stack: " + f.getName) {
- testInference(f)
- }
- }
-
- forEachFileIn("regression/orb//depth") { f =>
- test("Depth: " + f.getName) {
- testInference(f)
- }
- }
-
- forEachFileIn("regression/orb/numerical") { f =>
- test("Numerical: " + f.getName) {
- testInference(f)
- }
- }
-
- forEachFileIn("regression/orb/combined/") { f =>
- test("Multiple Instrumentations: " + f.getName) {
- testInference(f)
- }
- }
-}
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
deleted file mode 100644
index 3724b017044b57aa80a74cbd84d092da3e9b0804..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ /dev/null
@@ -1,43 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.repair
-
-import leon.test._
-import leon.utils._
-import leon.frontends.scalac.ExtractionPhase
-import leon.repair._
-
-class RepairSuite extends LeonRegressionSuite {
- val pipeline = ExtractionPhase andThen
- new PreprocessingPhase andThen
- RepairPhase
-
- val fileToFun = Map(
- "Compiler1.scala" -> "desugar",
- "Heap3.scala" -> "merge",
- "Heap4.scala" -> "merge",
- "ListEasy.scala" -> "pad",
- "List1.scala" -> "pad",
- "Numerical1.scala" -> "power",
- "MergeSort2.scala" -> "merge"
- )
-
- for (file <- filesInResourceDir("regression/repair/", _.endsWith(".scala"))) {
-
- val path = file.getAbsoluteFile.toString
- val name = file.getName
-
- test(name) {
- if (!(fileToFun contains file.getName)) {
- fail(s"Don't know which function to repair for ${file.getName}")
- }
-
- val ctx = createLeonContext("--parallel", "--timeout=180", "--solvers=smt-z3", s"--functions=${fileToFun(name)}")
-
- pipeline.run(ctx, List(path))
- if(ctx.reporter.errorCount > 0) {
- fail("Errors during repair:\n"+ctx.reporter.asInstanceOf[TestSilentReporter].lastErrors.mkString("\n"))
- }
- }
- }
-}
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
deleted file mode 100644
index 4f3b5bafd4b6b62fe36ec266fddac88de6f78efa..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ /dev/null
@@ -1,146 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.synthesis
-
-import leon._
-import leon.test._
-
-import leon.purescala.Definitions._
-import leon.purescala.ScalaPrinter
-import leon.purescala.PrinterContext
-import leon.purescala.PrinterOptions
-import leon.synthesis._
-import leon.synthesis.rules._
-
-import scala.collection.mutable.Stack
-import scala.io.Source
-
-import java.io.File
-
-class StablePrintingSuite extends LeonRegressionSuite {
- private def forEachFileIn(path : String)(block : File => Unit) {
- val fs = filesInResourceDir(path, _.endsWith(".scala"))
-
- for(f <- fs) {
- block(f)
- }
- }
-
-
- private def testIterativeSynthesis(cat: String, f: File, depth: Int) {
-
- val decompRules = List[Rule](
- Unification.DecompTrivialClash,
- Unification.OccursCheck, // probably useless
- Disunification.Decomp,
- ADTDual,
- CaseSplit,
- IfSplit,
- UnusedInput,
- EquivalentInputs,
- UnconstrainedOutput,
- OptimisticGround,
- InequalitySplit,
- rules.Assert,
- DetupleInput,
- ADTSplit,
- InnerCaseSplit
- )
-
- def getChooses(ctx: LeonContext, content: String): (Program, SynthesisSettings, Seq[SourceInfo]) = {
- val opts = SynthesisSettings()
- val pipeline = leon.utils.TemporaryInputPhase andThen
- frontends.scalac.ExtractionPhase andThen
- new leon.utils.PreprocessingPhase
-
- val (ctx2, program) = pipeline.run(ctx, (List(content), Nil))
-
- (program, opts, SourceInfo.extractFromProgram(ctx2, program))
- }
-
- case class Job(content: String, choosesToProcess: Set[Int], rules: List[String]) {
- def info(task: String): String = {
- val r = if (rules.isEmpty) "<init>" else "after "+rules.head
-
- val indent = " "* rules.size +" "
-
- f"${indent+r}%-40s [$task%s]"
- }
- }
-
-
- test(cat+": "+f.getName+" - Synthesis <-> Print (depth="+depth+")") {
- val res = Source.fromFile(f).mkString
-
- val workList = Stack[Job](Job(res, Set(), Nil))
-
- while(workList.nonEmpty) {
- val reporter = new TestSilentReporter
- val ctx = createLeonContext("--synthesis", "--solvers=smt-z3", "--timeout=120").copy(reporter = reporter)
- val j = workList.pop()
-
- info(j.info("compilation"))
-
- val (pgm, opts, chooses) = try {
- getChooses(ctx, j.content)
- } catch {
- case e: Throwable =>
- val contentWithLines = j.content.split("\n").zipWithIndex.map{ case (l, i) => f"${i+1}%4d: $l"}.mkString("\n")
- info("Error while compiling:\n"+contentWithLines)
- for (e <- reporter.lastErrors) {
- info(e)
- }
- info(e.getMessage)
- e.printStackTrace()
- fail("Compilation failed")
- }
-
- if (j.rules.size < depth) {
- for ((ci, i) <- chooses.zipWithIndex if j.choosesToProcess(i) || j.choosesToProcess.isEmpty) {
- val synthesizer = new Synthesizer(ctx, pgm, ci, opts)
- val sctx = synthesizer.sctx
- try {
- val search = synthesizer.getSearch
- val hctx = new SearchContext(sctx, ci.source, search.g.root, search)
- val problem = ci.problem
- info(j.info("synthesis "+problem.asString(sctx)))
- val apps = decompRules flatMap { _.instantiateOn(hctx, problem)}
-
- for (a <- apps) {
- a.apply(hctx) match {
- case RuleClosed(sols) =>
- case RuleExpanded(sub) =>
- a.onSuccess(sub.map(Solution.choose)) match {
- case Some(sol) =>
- val result = sol.toSimplifiedExpr(ctx, pgm, ci.fd)
-
- val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.source, (indent: Int) => {
- val p = new ScalaPrinter(PrinterOptions(), Some(pgm))
- p.pp(result)(PrinterContext(result, List(ci.fd), indent, p))
- p.toString
- })
-
- workList push Job(newContent, (i to i+sub.size).toSet, a.asString(ctx) :: j.rules)
- case None =>
- }
- }
- }
- } finally {
- synthesizer.shutdown()
- }
- }
- }
- }
- }
- }
-
-
-
- forEachFileIn("regression/synthesis/Church/") { f =>
- testIterativeSynthesis("Church", f, 1)
- }
-
- forEachFileIn("regression/synthesis/List/") { f =>
- testIterativeSynthesis("List", f, 1)
- }
-}
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
deleted file mode 100644
index ed9be0442e637a9398e42741864b489a4414d4d1..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
+++ /dev/null
@@ -1,73 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.synthesis
-
-import leon.test._
-
-import leon._
-import leon.synthesis._
-
-import java.io.File
-
-class SynthesisRegressionSuite extends LeonRegressionSuite {
- private def forEachFileIn(path : String)(block : File => Unit) {
- val fs = filesInResourceDir(path, _.endsWith(".scala"))
-
- for(f <- fs) {
- block(f)
- }
- }
-
- private def testSynthesis(cat: String, f: File, bound: Int) {
- val ctx = createLeonContext("--synthesis", "--solvers=smt-z3")
-
- val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase
-
- val (ctx2, program) = try {
- pipeline.run(ctx, f.getAbsolutePath :: Nil)
- } catch {
- case LeonFatalError(msg) =>
- test(s"$cat: ${f.getName}") {
- fail(s"Compilation failed: ${msg.getOrElse("")}")
- }
- return
- }
-
- val chooses = SourceInfo.extractFromProgram(ctx2, program)
- val settings = SynthesisSettings(searchBound = Some(bound))
-
- for (ci <- chooses) {
- test(s"$cat: ${f.getName} - ${ci.fd.id.name}") {
- val synthesizer = new Synthesizer(ctx, program, ci, settings)
- try {
- val (_, sols) = synthesizer.synthesize()
- if (sols.isEmpty) {
- fail(s"Solution was not found. (Search bound: $bound)")
- }
- } finally {
- synthesizer.shutdown()
- }
- }
- }
- }
-
- forEachFileIn("regression/synthesis/Church/") { f =>
- testSynthesis("Church", f, 200)
- }
-
- forEachFileIn("regression/synthesis/Examples/") { f =>
- testSynthesis("IOExamples", f, 200)
- }
-
- forEachFileIn("regression/synthesis/List/") { f =>
- testSynthesis("List", f, 200)
- }
-
- forEachFileIn("regression/synthesis/Misc/") { f =>
- testSynthesis("Miscellaneous", f, 1000)
- }
-
- forEachFileIn("regression/synthesis/Holes/") { f =>
- testSynthesis("Holes", f, 1000)
- }
-}
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
deleted file mode 100644
index 16759a041978f903babcf430c90a5cc14c4a3db7..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ /dev/null
@@ -1,118 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.termination
-
-import leon._
-import leon.test._
-
-import leon.termination._
-
-import java.io.File
-
-class TerminationSuite extends LeonRegressionSuite {
- private var counter : Int = 0
- private def nextInt() : Int = {
- counter += 1
- counter
- }
- private case class Output(report : TerminationReport, reporter : Reporter)
-
- private def mkPipeline : Pipeline[List[String],TerminationReport] =
- leon.frontends.scalac.ExtractionPhase andThen
- new leon.utils.PreprocessingPhase andThen
- leon.termination.TerminationPhase
-
- private def mkTest(file : File, leonOptions: Seq[String], forError: Boolean)(block: Output=>Unit) = {
- val fullName = file.getPath
- val start = fullName.indexOf("regression")
-
- val displayName = if(start != -1) {
- fullName.substring(start, fullName.length)
- } else {
- fullName
- }
-
- val ignored = List(
- "termination/valid/NNF.scala",
- //"verification/purescala/valid/MergeSort.scala",
- "verification/purescala/valid/Nested14.scala",
- "verification/purescala/valid/MergeSort2.scala"
- )
-
- val t = if (ignored.exists(displayName.replaceAll("\\\\","/").endsWith)) {
- ignore _
- } else {
- test _
- }
-
- t(f"${nextInt()}%3d: $displayName ${leonOptions.mkString(" ")}", Seq()) {
- assert(file.exists && file.isFile && file.canRead,
- s"Benchmark $displayName is not a readable file")
-
- val ctx = createLeonContext((leonOptions ++ List(file.getAbsolutePath)): _* )
-
- val pipeline = mkPipeline
-
- if(forError) {
- intercept[LeonFatalError]{
- pipeline.run(ctx, file.getPath :: Nil)
- }
- } else {
-
- val (ctx2, report) = pipeline.run(ctx, file.getPath :: Nil)
-
- block(Output(report, ctx2.reporter))
- }
- }
- }
-
- private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) {
- for(f <- files) {
- mkTest(f, Seq("--solvers=smt-z3", "--timeout=150"), forError)(block)
- }
- }
-
- def validFiles = filesInResourceDir("regression/termination/valid", _.endsWith(".scala")) ++
- filesInResourceDir("regression/verification/purescala/valid", _.endsWith(".scala"))
-
- def loopingFiles = filesInResourceDir("regression/termination/looping", _.endsWith(".scala"))
-
- forEachFileIn(validFiles) { case Output(report, _) =>
- val failures = report.results.collect { case (fd, guarantee) if !guarantee.isGuaranteed => fd }
- assert(failures.isEmpty, "Functions " + failures.map(_.id) + " should terminate")
- // can't say anything about error counts because of postcondition strengthening that might fail (normal behavior)
- // assert(reporter.errorCount === 0)
- //assert(reporter.warningCount === 0)
- }
-
- forEachFileIn(loopingFiles) { case Output(report, _) =>
- val looping = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("looping") }
- val notLooping = looping.filterNot(p => p._2.isInstanceOf[NonTerminating] || p._2.isInstanceOf[CallsNonTerminating])
- assert(notLooping.isEmpty, "Functions " + notLooping.map(_._1.id) + " should loop")
-
- val calling = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("calling") }
- val notCalling = calling.filterNot(p => p._2.isInstanceOf[CallsNonTerminating])
- assert(notCalling.isEmpty, "Functions " + notCalling.map(_._1.id) + " should call non-terminating")
-
- val guar = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("ok") }
- val notGuaranteed = guar.filterNot(p => p._2.isGuaranteed)
- assert(notGuaranteed.isEmpty, "Functions " + notGuaranteed.map(_._1.id) + " should terminate")
-
-// assert(reporter.errorCount >= looping.size + calling.size)
- //assert(reporter.warningCount === 0)
- }
-
- /*
- forEachFileIn("unknown") { output =>
- val Output(report, reporter) = output
- val unknown = report.results.filter { case (fd, guarantee) => fd.id.name.startsWith("unknown") }
- assert(unknown.forall(_._2 == NoGuarantee), "Functions " + unknown.filter(_._2 != NoGuarantee).map(_._1.id) + " should be unknown")
- // can't say anything about error counts because of postcondition strengthening that might fail (normal behavior)
- // assert(reporter.errorCount === 0)
- assert(reporter.warningCount === 0)
- }
- */
-
- //forEachFileIn("error", true) { output => () }
-
-}
diff --git a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala b/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
deleted file mode 100644
index 3f0fee98aee4155aff3f76e3ea0b9693dc4da65c..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.testcases
-
-import leon._
-import leon.test._
-import java.io.File
-
-abstract class TestCasesCompile(testDir: String) extends LeonRegressionSuite {
-
- val pipeline = frontends.scalac.ExtractionPhase andThen new utils.PreprocessingPhase
-
- private def filesIn(path : String): Seq[File] = {
- val fs = filesInResourceDir(path, _.endsWith(".scala"), recursive=true)
-
- fs.toSeq
- }
-
- val baseDir = "regression/testcases/"
-
- val allTests = filesIn(baseDir + testDir)
-
- allTests.foreach { f =>
-
- val path = f.getAbsolutePath
-
- val index = path.indexOf(baseDir)
- val name = path.drop(index)
-
- test("Compiling "+name) {
-
- val ctx = createLeonContext()
-
- try {
- pipeline.run(ctx, List(f.getAbsolutePath))
- } catch {
- case fe: LeonFatalError =>
- fail(ctx, s"Failed to compile $name", fe)
- }
- }
- }
-}
-
-class TestcasesCompile1 extends TestCasesCompile("repair/")
-class TestcasesCompile2 extends TestCasesCompile("runtime/")
-class TestcasesCompile3 extends TestCasesCompile("synthesis/")
-class TestcasesCompile4 extends TestCasesCompile("verification/")
-class TestcasesCompile5 extends TestCasesCompile("web/")
diff --git a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
deleted file mode 100644
index 72cf6715d8ab5cfc88e1907aac26238c50980c42..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.verification
-
-import leon._
-import leon.test._
-import leon.frontends.scalac.ExtractionPhase
-import leon.utils.PreprocessingPhase
-import leon.verification.VerificationPhase
-
-class LibraryVerificationSuite extends LeonRegressionSuite {
- test("Verify the library") {
- val pipeline = ExtractionPhase andThen
- new PreprocessingPhase andThen
- VerificationPhase
-
- val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
-
- val (_, report) = pipeline.run(ctx, Nil)
-
- assert(report.totalConditions === report.totalValid, "Only "+report.totalValid+" valid out of "+report.totalConditions)
- }
-}
diff --git a/src/test/scala/leon/regression/verification/NewSolversSuite.scala b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
deleted file mode 100644
index d41ea95dceaaaa014b8d5dcb5eeed46244bb37cb..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/verification/NewSolversSuite.scala
+++ /dev/null
@@ -1,34 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.verification
-
-import _root_.smtlib.interpreters._
-import leon._
-import leon.verification.VerificationPhase
-import leon.solvers.SolverFactory
-
-/* @EK: Disabled for now as many tests fail
-class NewSolversSuite extends VerificationSuite {
-
- val testDir = "regression/verification/newsolvers/"
- val pipeFront = xlang.NoXLangFeaturesChecking
- val pipeBack = AnalysisPhase
- val optionVariants: List[List[String]] = {
-
- val isCVC4Available = SolverFactory.hasCVC4
-
- val isZ3Available = SolverFactory.hasZ3
-
- (
- if (isCVC4Available)
- List(List("--solvers=smt-cvc4-cex,smt-cvc4-proof,ground", "--timeout=5"))
- else Nil
- ) ++ (
- if (isZ3Available)
- List(List("--solvers=smt-z3-q,ground", "--timeout=10"))
- else Nil
- )
-
- }
-}
-*/
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
deleted file mode 100644
index 14165edf545a2924a63aa46c474fcc0e1298759d..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ /dev/null
@@ -1,134 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.verification
-
-import leon._
-import leon.test._
-
-import leon.utils.UniqueCounter
-import leon.verification.{VerificationPhase, VerificationReport}
-import leon.purescala.Definitions.Program
-import leon.frontends.scalac.ExtractionPhase
-import leon.utils.PreprocessingPhase
-import leon.solvers.isabelle.AdaptationPhase
-import leon.xlang.FixReportLabels
-
-import org.scalatest.{Reporter => _, _}
-
-// If you add another regression test, make sure it contains exactly one object, whose name matches the file name.
-// This is because we compile all tests from each folder together.
-trait VerificationSuite extends LeonRegressionSuite {
-
- val optionVariants: List[List[String]]
- val testDir: String
-
- val ignored: Seq[String] = Seq()
- val desugarXLang: Boolean = false
- val isabelle: Boolean = false
-
- private val counter = new UniqueCounter[Unit]
- counter.nextGlobal // Start with 1
-
- private case class Output(report: VerificationReport, reporter: Reporter)
-
- private def mkTest(files: List[String], cat: String)(block: Output => Unit) = {
- val extraction =
- ExtractionPhase andThen
- new PreprocessingPhase
-
- val analysis =
- AdaptationPhase.when(isabelle) andThen
- VerificationPhase andThen
- FixReportLabels.when(desugarXLang)
-
- val ctx = createLeonContext(files:_*).copy(reporter = new TestErrorReporter)
-
- try {
- val (_, ast) = extraction.run(ctx, files)
- val programs = {
- val (user, lib) = ast.units partition { _.isMainUnit }
- user map ( u => Program(u :: lib) )
- }
- for ( p <- programs; options <- optionVariants) {
-
- val displayName = s"$cat/${p.units.head.id.name}.scala"
-
- val index = counter.nextGlobal
- val ts = if (ignored exists (_.endsWith(displayName)))
- ignore _
- else
- test _
-
- ts(f"$index%3d: $displayName ${options.mkString(" ")}", Seq()) {
- val ctx = createLeonContext(options: _*)
- try {
- val (ctx2, report) = analysis.run(ctx, p)
- block(Output(report, ctx2.reporter))
- } catch {
- case fe: LeonFatalError =>
- fail(ctx, "Verification failed", fe)
- }
- }
- }
- } catch {
- case fe: LeonFatalError =>
- test("Compilation") {
- fail(ctx, "Unexpected fatal error while setting up tests", fe)
- }
- }
- }
-
- private[verification] def forEachFileIn(cat: String)(block: Output => Unit) {
- val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
-
- fs foreach { file =>
- assert(file.exists && file.isFile && file.canRead,
- s"Benchmark ${file.getName} is not a readable file")
- }
-
- val files = fs map { _.getPath }
-
- mkTest(files, cat)(block)
- }
-
- protected def testValid() = forEachFileIn("valid") { output =>
- val Output(report, reporter) = output
- for ((vc, vr) <- report.vrs if vr.isInvalid) {
- fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
- }
- for ((vc, vr) <- report.vrs if vr.isInconclusive) {
- fail(s"The following verification condition was inconclusive: $vc @${vc.getPos}")
- }
- reporter.terminateIfError()
- }
-
- protected def testInvalid() = forEachFileIn("invalid") { output =>
- val Output(report, _) = output
- assert(report.totalUnknown === 0,
- "There should not be unknown verification conditions.")
- assert(report.totalInvalid > 0,
- "There should be at least one invalid verification condition.")
- }
-
- protected def testUnknown() = forEachFileIn("unknown") { output =>
- val Output(report, reporter) = output
- for ((vc, vr) <- report.vrs if vr.isInvalid) {
- fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
- }
- assert(report.totalUnknown > 0,
- "There should be at least one unknown verification condition.")
-
- reporter.terminateIfError()
- }
-
- protected def testAll() = {
- testValid()
- testInvalid()
- testUnknown()
- }
-
- override def run(testName: Option[String], args: Args): Status = {
- testAll()
- super.run(testName, args)
- }
-}
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
deleted file mode 100644
index 180e6ff1548a726f289d44b2e89472ca24d57d61..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ /dev/null
@@ -1,27 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.regression.verification
-
-import leon.solvers.SolverFactory
-
-// If you add another regression test, make sure it contains exactly one object, whose name matches the file name.
-// This is because we compile all tests from each folder together.
-class XLangVerificationSuite extends VerificationSuite {
-
- val optionVariants: List[List[String]] = {
- val isZ3Available = SolverFactory.hasZ3
-
- (List(
- List(),
- List("--feelinglucky")
- ) ++ (
- if (isZ3Available)
- List(List("--solvers=smt-z3", "--feelinglucky"))
- else Nil
- )).map ("--timeout=300" :: _)
- }
-
- val testDir: String = "regression/verification/xlang/"
- override val desugarXLang = true
-}
-
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
deleted file mode 100644
index 744e6b2f6cf7a3a7cfcafb8905b0089791ae6e8b..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ /dev/null
@@ -1,72 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package regression.verification
-package purescala
-
-import leon.solvers.SolverFactory
-
-// If you add another regression test, make sure it contains one object whose name matches the file name
-// This is because we compile all tests from each folder together.
-abstract class PureScalaVerificationSuite extends VerificationSuite {
-
- val testDir = "regression/verification/purescala/"
-
- val isZ3Available = SolverFactory.hasZ3
-
- val isCVC4Available = SolverFactory.hasCVC4
-
- val opts: List[List[String]] = {
- (List(
- List("--feelinglucky"),
- List("--codegen", /*"--evalground",*/ "--feelinglucky"),
- List("--solvers=fairz3,enum", "--codegen", /*"--evalground",*/ "--feelinglucky")) ++
- isZ3Available.option(List("--solvers=smt-z3", "--feelinglucky")) ++
- isCVC4Available.option(List("--solvers=smt-cvc4", "--feelinglucky")))
- .map( _ :+ "--timeout=300")
- }
-
-}
-
-trait PureScalaValidSuite extends PureScalaVerificationSuite {
- override def testAll() = testValid()
-}
-
-class PureScalaValidSuiteLuckyNativeZ3 extends PureScalaValidSuite {
- val optionVariants = List(opts(0))
-}
-class PureScalaValidSuiteCodeGenNativeZ3 extends PureScalaValidSuite {
- val optionVariants = List(opts(1))
-}
-class PureScalaValidSuiteEnumNativeZ3 extends PureScalaValidSuite {
- val optionVariants = List(opts(2))
- //override val ignored = Seq("valid/Predicate.scala","valid/TraceInductTacticTest.scala")
-}
-class PureScalaValidSuiteZ3 extends PureScalaValidSuite {
- val optionVariants = isZ3Available.option(opts(3)).toList
-}
-class PureScalaValidSuiteCVC4 extends PureScalaValidSuite {
- val optionVariants = isCVC4Available.option(opts.last).toList
-}
-
-trait PureScalaInvalidSuite extends PureScalaVerificationSuite {
- override def testAll() = testInvalid()
-}
-
-class PureScalaInvalidSuiteNativeZ3 extends PureScalaInvalidSuite {
- val optionVariants = opts.take(3)
-}
-
-class PureScalaInvalidSuiteZ3 extends PureScalaInvalidSuite {
- val optionVariants = isZ3Available.option(opts(3)).toList
-}
-
-class PureScalaInvalidSuiteCVC4 extends PureScalaInvalidSuite {
- val optionVariants = isCVC4Available.option(opts.last).toList
- override val ignored = List(
- "invalid/AbstractRefinementMap2.scala",
- "invalid/BinarySearchTreeQuant.scala",
- "invalid/PropositionalLogic.scala"
- )
-}
-
diff --git a/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala b/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala
deleted file mode 100644
index 4781e6a88af5f227394bf2b539b3e7d52cd27d66..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/xlang/XLangDesugaringSuite.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.regression.xlang
-
-import leon._
-import leon.test._
-import purescala.Definitions.Program
-import java.io.File
-
-class XLangDesugaringSuite extends LeonRegressionSuite {
- // Hard-code output directory, for Eclipse purposes
-
- val pipeline = frontends.scalac.ExtractionPhase andThen new utils.PreprocessingPhase
-
- def testFrontend(f: File, forError: Boolean) = {
- test ("Testing " + f.getName) {
- val ctx = createLeonContext("--timeout=40")
- if (forError) {
- intercept[LeonFatalError]{
- pipeline.run(ctx, List(f.getAbsolutePath))
- }
- } else {
- pipeline.run(ctx, List(f.getAbsolutePath))
- }
- }
-
- }
-
- private def forEachFileIn(path : String)(block : File => Unit) {
- val fs = filesInResourceDir(path, _.endsWith(".scala"))
-
- for(f <- fs) {
- block(f)
- }
- }
-
- val baseDir = "regression/xlang/"
-
- forEachFileIn(baseDir+"passing/") { f =>
- testFrontend(f, false)
- }
- forEachFileIn(baseDir+"error/") { f =>
- testFrontend(f, true)
- }
-
-}
diff --git a/src/test/scala/leon/test/LeonRegressionSuite.scala b/src/test/scala/leon/test/LeonRegressionSuite.scala
deleted file mode 100644
index ba4b51a1b71f2619acc608da8106debced6b9341..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/LeonRegressionSuite.scala
+++ /dev/null
@@ -1,76 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.test
-
-import leon._
-import leon.utils._
-
-import org.scalatest._
-import org.scalatest.concurrent._
-import org.scalatest.exceptions.TestFailedException
-
-import java.io.File
-
-trait LeonRegressionSuite extends FunSuite with Timeouts {
-
- val regressionTestDirectory = "src/test/resources"
-
- def createLeonContext(opts: String*): LeonContext = {
- val reporter = new TestSilentReporter
-
- Main.processOptions(opts.toList).copy(reporter = reporter, interruptManager = new InterruptManager(reporter))
- }
-
- def testIdentifier(name: String): String = {
- def sanitize(s: String) = s.replaceAll("[^0-9a-zA-Z-]", "")
-
- sanitize(this.getClass.getName)+"/"+sanitize(name)
- }
-
- override def test(name: String, tags: Tag*)(body: => Unit) {
- super.test(name) {
- try {
- body
- } catch {
- case fe: LeonFatalError =>
- throw new TestFailedException("Uncaught LeonFatalError" + fe.msg.map(": " + _).getOrElse(""), fe, 5)
- }
- }
- }
-
- protected val all : String=>Boolean = (s : String) => true
-
- def scanFilesIn(f: File, filter: String=>Boolean = all, recursive: Boolean = false): Iterable[File] = {
- Option(f.listFiles()).getOrElse(Array()).flatMap{f =>
- if (f.isDirectory && recursive) {
- scanFilesIn(f, filter, recursive)
- } else {
- List(f)
- }
- }.filter(f => filter(f.getPath)).toSeq.sortBy(_.getPath)
- }
-
- def filesInResourceDir(dir : String, filter : String=>Boolean = all, recursive: Boolean = false) : Iterable[File] = {
-
- val baseDir = new File(s"${Build.baseDirectory}/$regressionTestDirectory/$dir")
-
- scanFilesIn(baseDir, filter, recursive)
- }
-
- protected def fail(ctx: LeonContext, reason: String, fe: LeonFatalError): Nothing = {
- val omsg = ctx.reporter match {
- case sr: TestSilentReporter =>
- sr.lastErrors ++= fe.msg
- Some((sr.lastErrors ++ fe.msg).mkString("\n"))
- case _ =>
- fe.msg
- }
-
- val fullError = omsg match {
- case Some(msg) => s"$reason:\n$msg"
- case None => s"$reason"
- }
-
- throw new TestFailedException(fullError, fe, 5)
- }
-}
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
deleted file mode 100644
index 2c9399f12106032138b6abbe2793e10b6f10ef92..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ /dev/null
@@ -1,27 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.test
-
-import leon._
-
-import org.scalatest._
-import org.scalatest.exceptions.TestFailedException
-
-trait LeonTestSuite extends fixture.FunSuite {
- type FixtureParam = LeonContext
-
- override def withFixture(test: OneArgTest): Outcome = {
- val reporter = new TestSilentReporter
- val opts = List[String]()
-
- val ctx = Main.processOptions(opts).copy(reporter = reporter)
-
- try {
- test(ctx)
- } catch {
- case fe: LeonFatalError =>
- reporter.lastErrors ++= fe.msg
- Failed(new TestFailedException(reporter.lastErrors.mkString("\n"), fe, 5))
- }
- }
-}
diff --git a/src/test/scala/leon/test/LeonTestSuiteWithProgram.scala b/src/test/scala/leon/test/LeonTestSuiteWithProgram.scala
deleted file mode 100644
index 9448147272939754b7e69e6b23e651836fe3b187..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/LeonTestSuiteWithProgram.scala
+++ /dev/null
@@ -1,71 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.test
-
-import leon._
-import leon.purescala.Definitions.Program
-import leon.utils._
-import leon.frontends.scalac.ExtractionPhase
-
-import org.scalatest._
-import org.scalatest.exceptions.TestFailedException
-
-import scala.language.implicitConversions
-
-trait LeonTestSuiteWithProgram extends fixture.FunSuite {
-
- implicit def fixtureToCtx(implicit f: FixtureParam): LeonContext = f._1
- implicit def fixtureToPgm(implicit f: FixtureParam): Program = f._2
-
- val leonOpts = List[String]()
-
- val pipeline =
- TemporaryInputPhase andThen
- ExtractionPhase andThen
- new PreprocessingPhase
-
- val sources: List[String]
-
- private[this] var fixtureCache: Option[(LeonContext, Program)] = None
-
- def getFixture(): (LeonContext, Program) = synchronized {
- if (fixtureCache.isEmpty) {
- val reporter = new TestSilentReporter
- val im = new InterruptManager(reporter)
-
- val ctx = Main.processOptions(leonOpts).copy(reporter = reporter, interruptManager = im)
-
- val (ctx2, pgm) = pipeline.run(ctx, (sources, Nil))
-
- fixtureCache = Some((ctx2, pgm))
- }
-
- fixtureCache.get
- }
-
- type FixtureParam = (LeonContext, Program)
-
- override def withFixture(test: OneArgTest): Outcome = {
- try {
- val (ctx, pgm) = getFixture()
- try {
- val freshReporter = new TestSilentReporter
-
- val f = (ctx.copy(reporter = freshReporter), pgm)
-
- test(f)
- } catch {
- case fe: LeonFatalError =>
- ctx.reporter match {
- case sr: TestSilentReporter =>
- sr.lastErrors ++= fe.msg
- Failed(new TestFailedException(sr.lastErrors.mkString("\n"), fe, 5))
- }
- }
- } catch {
- case t: Throwable =>
- Failed(t)
- }
- }
-}
-
diff --git a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala b/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
deleted file mode 100644
index 7a760143cfe733f989164bc4320960f129788de1..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/helpers/ExpressionsDSL.scala
+++ /dev/null
@@ -1,109 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.test.helpers
-
-import org.scalatest.Assertions
-
-import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.Types._
-import leon.purescala.Expressions._
-
-import scala.language.implicitConversions
-
-trait ExpressionsDSLVariables {
- val F = BooleanLiteral(false)
- val T = BooleanLiteral(true)
-
- def bi(x: Int) = InfiniteIntegerLiteral(x)
- def b(x: Boolean) = BooleanLiteral(x)
- def i(x: Int) = IntLiteral(x)
- def r(n: BigInt, d: BigInt) = FractionalLiteral(n, d)
-
- val a = FreshIdentifier("a", Int32Type).toVariable
- val b = FreshIdentifier("b", Int32Type).toVariable
- val c = FreshIdentifier("c", Int32Type).toVariable
-
- val x = FreshIdentifier("x", IntegerType).toVariable
- val y = FreshIdentifier("y", IntegerType).toVariable
- val z = FreshIdentifier("z", IntegerType).toVariable
-
- val m = FreshIdentifier("m", RealType).toVariable
- val n = FreshIdentifier("n", RealType).toVariable
- val o = FreshIdentifier("o", RealType).toVariable
-
- val p = FreshIdentifier("p", BooleanType).toVariable
- val q = FreshIdentifier("q", BooleanType).toVariable
- val r = FreshIdentifier("r", BooleanType).toVariable
-}
-
-trait ExpressionsDSLProgram {
-self: Assertions =>
-
-
- def id(name: String, tpe: TypeTree)(implicit pgm: Program): Identifier = {
- FreshIdentifier(name, tpe)
- }
-
- def id(name: String, tpeName: String, tps: Seq[TypeTree] = Nil)(implicit pgm: Program): Identifier = {
- id(name, classType(tpeName, tps))
- }
-
- def funDef(name: String)(implicit pgm: Program): FunDef = {
- pgm.lookupAll(name).collect {
- case fd: FunDef => fd
- }.headOption.getOrElse {
- fail(s"Failed to lookup function '$name' in program")
- }
- }
-
- def classDef(name: String)(implicit pgm: Program): ClassDef = {
- pgm.lookupAll(name).collect {
- case cd: ClassDef => cd
- }.headOption.getOrElse {
- fail(s"Failed to lookup class '$name' in program")
- }
- }
-
- def classType(name: String, tps: Seq[TypeTree] = Nil)(implicit pgm: Program): ClassType = {
- classDef(name) match {
- case acd: AbstractClassDef => AbstractClassType(acd, tps)
- case ccd: CaseClassDef => CaseClassType(ccd, tps)
- }
- }
-
- def caseClassDef(name: String)(implicit pgm: Program): CaseClassDef = {
- pgm.lookupAll(name).collect {
- case ccd: CaseClassDef => ccd
- }.headOption.getOrElse {
- fail(s"Failed to lookup case class '$name' in program")
- }
- }
-
- def moduleDef(name: String)(implicit pgm: Program): ModuleDef = {
- pgm.lookupAll(name).collect {
- case m: ModuleDef => m
- }.headOption.getOrElse {
- fail(s"Failed to lookup module '$name' in program")
- }
- }
-
- def cc(name: String)(args: Expr*)(implicit pgm: Program): Expr = {
- val cct = caseClassDef(name).typed(Seq())
- CaseClass(cct, args.toSeq)
- }
-
- def fcall(name: String)(args: Expr*)(implicit pgm: Program): Expr = {
- val tfd = funDef(name).typed(Seq())
- FunctionInvocation(tfd, args.toSeq)
- }
-}
-
-trait ExpressionsDSL extends ExpressionsDSLVariables with ExpressionsDSLProgram {
- self: Assertions =>
-
-
- implicit def int2IntLit(i: Int): IntLiteral = IntLiteral(i)
- implicit def bigInt2IntegerLit(i: BigInt): InfiniteIntegerLiteral = InfiniteIntegerLiteral(i)
-
-}
diff --git a/src/test/scala/leon/test/helpers/WithLikelyEq.scala b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
deleted file mode 100644
index f121f4553809fd7ae5b9e93d15bb1b5b7d3b2de0..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/test/helpers/WithLikelyEq.scala
+++ /dev/null
@@ -1,64 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.test.helpers
-
-import org.scalatest.Assertions
-
-import leon.test._
-import leon.evaluators._
-import leon.purescala.Common._
-import leon.LeonContext
-import leon.purescala.Types._
-import leon.purescala.Definitions._
-import leon.purescala.ExprOps._
-import leon.purescala.Expressions._
-import leon.utils.SeqUtils._
-
-/*
- * Determine if two expressions over arithmetic variables are likely to be equal.
- *
- * This is a probabilistic based approach, it does not rely on any external solver and can
- * only prove the non equality of two expressions.
- */
-trait WithLikelyEq {
- self: Assertions =>
-
- val typesValues = Map[TypeTree, Seq[Expr]](
- IntegerType -> Seq(-42, -1, 0, 1, 7, 42).map(InfiniteIntegerLiteral(_)),
- Int32Type -> Seq(-42, -1, 0, 1, 7, 42).map(IntLiteral(_)),
- BooleanType -> Seq(BooleanLiteral(false), BooleanLiteral(true))
- )
-
- def checkLikelyEq(ctx: LeonContext, pgm: Program = Program.empty)(e1: Expr, e2: Expr, pre: Option[Expr] = None, values: Map[Identifier, Expr] = Map()): Unit = {
- val evaluator = new DefaultEvaluator(ctx, pgm)
-
- val freeVars = (variablesOf(e1) ++ variablesOf(e2)).toSeq.sorted
-
- if (freeVars.isEmpty) {
- val r1 = evaluator.eval(e1)
- val r2 = evaluator.eval(e2)
-
- assert(r1 === r2, s"'$e1' != '$e2' ('$r1' != '$r2')")
- } else {
-
- val allValues = freeVars.map(id => values.get(id).map(Seq(_)).getOrElse(typesValues(id.getType)))
-
- cartesianProduct(allValues).foreach { vs =>
- val m = evaluator.evalEnv(freeVars zip vs)
- val doTest = pre.map { p =>
- evaluator.eval(p, m).result match {
- case Some(BooleanLiteral(b)) => b
- case _ => fail("Precondition is not a boolean expression")
- }
- }.getOrElse(true)
-
- if (doTest) {
- val r1 = evaluator.eval(e1, m)
- val r2 = evaluator.eval(e2, m)
-
- assert(r1 === r2, s"'$e1' != '$e2' with '$m' ('$r1' != '$r2')")
- }
- }
- }
- }
-}