diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index a4f365a2508f72646488aef29641035ddba0e2d1..cd66e57d665ba5e310cc3b832772eae6af4e2c8c 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -281,7 +281,27 @@ object Constructors {
if (a == b && isDeterministic(a)) {
BooleanLiteral(true)
} else {
- Equals(a, b)
+ (a, b) match {
+ case (a: Literal[_], b: Literal[_]) =>
+ if (a.value == b.value) {
+ BooleanLiteral(true)
+ } else {
+ BooleanLiteral(false)
+ }
+
+ case _ =>
+ Equals(a, b)
+ }
+ }
+ }
+
+ def assertion(c: Expr, err: Option[String], res: Expr) = {
+ if (c == BooleanLiteral(true)) {
+ res
+ } else if (c == BooleanLiteral(false)) {
+ Error(res.getType, err.getOrElse("Assertion failed"))
+ } else {
+ Assert(c, err, res)
}
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 464c91445906d075800412b5f1eb7343ac36a004..d9fd1d1d6696991909ffd5cd9b1f2e95590db7a4 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -205,8 +205,8 @@ object Definitions {
// If this class was a method. owner is the original owner of the method
case class IsMethod(owner: ClassDef) extends FunctionFlag
// If this function represents a loop that was there before XLangElimination
- // Contains a copy of the original looping function
- case class IsLoop(orig: FunDef) extends FunctionFlag
+ // Contains a link to the FunDef where the loop was defined
+ case class IsLoop(owner: FunDef) extends FunctionFlag
// If extraction fails of the function's body fais, it is marked as abstract
case object IsAbstract extends FunctionFlag
// Currently, the only synthetic functions are those that calculate default values of parameters
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 0c18b51e3b9e473556aaf5817b49ad0d8104ea40..07c6781a8389be1df4e16681cd518bb043cb608a 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -145,11 +145,11 @@ object FunctionClosure extends TransformationPhase {
)
newFd.fullBody = preMap {
- case FunctionInvocation(tfd, args) if tfd.fd == inner =>
+ case fi@FunctionInvocation(tfd, args) if tfd.fd == inner =>
Some(FunctionInvocation(
newFd.typed(tfd.tps ++ tpFresh.map{ _.tp }),
args ++ freshVals.drop(args.length).map(Variable)
- ))
+ ).setPos(fi))
case _ => None
}(instBody)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 4959ae799c8f34b25dbdf1cac812ef8d954b4717..6523a1104127c174edf5c1e9d994be27b797d421 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -2,9 +2,11 @@
package leon
package repair
-
+
+import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
+import purescala.Extractors._
import purescala.ExprOps._
import purescala.Types._
import purescala.DefOps._
@@ -98,6 +100,60 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
bh.write()
}
+ reporter.ifDebug { printer =>
+ import java.io.FileWriter
+ import java.text.SimpleDateFormat
+ import java.util.Date
+
+ val categoryName = fd.getPos.file.toString.split("/").dropRight(1).lastOption.getOrElse("?")
+ val benchName = categoryName+"."+fd.id.name
+
+ val defs = visibleFunDefsFromMain(program).collect {
+ case fd: FunDef => 1 + fd.params.size + formulaSize(fd.fullBody)
+ }
+
+ val pSize = defs.sum;
+ val fSize = formulaSize(fd.body.get)
+
+ def localizedExprs(n: graph.Node): List[Expr] = {
+ n match {
+ case on: graph.OrNode =>
+ on.selected.map(localizedExprs).flatten
+ case an: graph.AndNode if an.ri.rule == Focus =>
+ an.selected.map(localizedExprs).flatten
+ case an: graph.AndNode =>
+ val TopLevelAnds(clauses) = an.p.ws
+
+ val res = clauses.collect {
+ case Guide(expr) => expr
+ }
+
+ res.toList
+ }
+ }
+
+ val locSize = localizedExprs(search.g.root).map(formulaSize).sum;
+
+ val (solSize, proof) = solutions.headOption match {
+ case Some((sol, trusted)) =>
+ val solExpr = sol.toSimplifiedExpr(ctx, program)
+ val totalSolSize = formulaSize(solExpr)
+ (locSize+totalSolSize-fSize, if (trusted) "$\\chmark$" else "")
+ case _ =>
+ (0, "X")
+ }
+
+ val date = new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(new Date())
+
+ val fw = new java.io.FileWriter("repair-report.txt", true)
+
+ try {
+ fw.write(f"$date: $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%2.1f & ${timeSynth/1000.0}%2.1f & $proof%7s \\\\\n")
+ } finally {
+ fw.close
+ }
+ }(DebugSectionReport)
+
if (synth.settings.generateDerivationTrees) {
val dot = new DotGenerator(search.g)
dot.writeFile("derivation"+ dotGenIds.nextGlobal + ".dot")
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index b9c0dfd94e449ac5a7d130e1279da8ebb7c19b92..1235d69c6d16a2726971cac386732fdcea501b95 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -16,6 +16,7 @@ import utils._
import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks, optUnfoldFactor}
import templates._
import evaluators._
+import Template._
class UnrollingSolver(val context: LeonContext, val program: Program, underlying: Solver)
extends Solver
@@ -116,7 +117,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
val optEnabler = evaluator.eval(b, model).result
if (optEnabler == Some(BooleanLiteral(true))) {
- val optArgs = m.args.map(arg => evaluator.eval(Matcher.argValue(arg), model).result)
+ val optArgs = m.args.map(arg => evaluator.eval(arg.encoded, model).result)
if (optArgs.forall(_.isDefined)) {
Set(optArgs.map(_.get))
} else {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 4ab8fa908b666c09f2f6b65fa03fdd941c4c6e41..820d74662b44ca252418b58087deabbaabfc5025 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -543,10 +543,8 @@ trait SMTLIBTarget extends Interruptible {
* ===== Everything else =====
*/
case ap @ Application(caller, args) =>
- FunctionApplication(
- declareLambda(caller.getType.asInstanceOf[FunctionType]),
- (caller +: args).map(toSMT)
- )
+ val dyn = declareLambda(caller.getType.asInstanceOf[FunctionType])
+ FunctionApplication(dyn, (caller +: args).map(toSMT))
case Not(u) => Core.Not(toSMT(u))
case UMinus(u) => Ints.Neg(toSMT(u))
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 75d163815a17fbf31c56b684d58e3d26efe7feaa..036654c25ab64839efa5af4cb0d49a6566ffcf20 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -12,9 +12,10 @@ import purescala.Types._
import utils._
import Instantiation._
+import Template._
-case class App[T](caller: T, tpe: FunctionType, args: Seq[T]) {
- override def toString = "(" + caller + " : " + tpe + ")" + args.mkString("(", ",", ")")
+case class App[T](caller: T, tpe: FunctionType, args: Seq[Arg[T]]) {
+ override def toString = "(" + caller + " : " + tpe + ")" + args.map(_.encoded).mkString("(", ",", ")")
}
object LambdaTemplate {
@@ -72,6 +73,28 @@ object LambdaTemplate {
}
}
+trait KeyedTemplate[T, E <: Expr] {
+ val dependencies: Map[Identifier, T]
+ val structuralKey: E
+
+ lazy val key: (E, Seq[T]) = {
+ def rec(e: Expr): Seq[Identifier] = e match {
+ case Variable(id) =>
+ if (dependencies.isDefinedAt(id)) {
+ Seq(id)
+ } else {
+ Seq.empty
+ }
+
+ case Operator(es, _) => es.flatMap(rec)
+
+ case _ => Seq.empty
+ }
+
+ structuralKey -> rec(structuralKey).distinct.map(dependencies)
+ }
+}
+
class LambdaTemplate[T] private (
val ids: (Identifier, T),
val encoder: TemplateEncoder[T],
@@ -87,34 +110,39 @@ class LambdaTemplate[T] private (
val quantifications: Seq[QuantificationTemplate[T]],
val matchers: Map[T, Set[Matcher[T]]],
val lambdas: Seq[LambdaTemplate[T]],
- private[templates] val dependencies: Map[Identifier, T],
- private[templates] val structuralKey: Lambda,
- stringRepr: () => String) extends Template[T] {
+ val dependencies: Map[Identifier, T],
+ val structuralKey: Lambda,
+ stringRepr: () => String) extends Template[T] with KeyedTemplate[T, Lambda] {
val args = arguments.map(_._2)
val tpe = ids._1.getType.asInstanceOf[FunctionType]
- def substitute(substituter: T => T): LambdaTemplate[T] = {
+ def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): LambdaTemplate[T] = {
val newStart = substituter(start)
val newClauses = clauses.map(substituter)
val newBlockers = blockers.map { case (b, fis) =>
val bp = if (b == start) newStart else b
- bp -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+ bp -> fis.map(fi => fi.copy(
+ args = fi.args.map(_.substitute(substituter, matcherSubst))
+ ))
}
val newApplications = applications.map { case (b, fas) =>
val bp = if (b == start) newStart else b
- bp -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
+ bp -> fas.map(fa => fa.copy(
+ caller = substituter(fa.caller),
+ args = fa.args.map(_.substitute(substituter, matcherSubst))
+ ))
}
- val newQuantifications = quantifications.map(_.substitute(substituter))
+ val newQuantifications = quantifications.map(_.substitute(substituter, matcherSubst))
val newMatchers = matchers.map { case (b, ms) =>
val bp = if (b == start) newStart else b
- bp -> ms.map(_.substitute(substituter))
+ bp -> ms.map(_.substitute(substituter, matcherSubst))
}
- val newLambdas = lambdas.map(_.substitute(substituter))
+ val newLambdas = lambdas.map(_.substitute(substituter, matcherSubst))
val newDependencies = dependencies.map(p => p._1 -> substituter(p._2))
@@ -139,45 +167,20 @@ class LambdaTemplate[T] private (
)
}
- private lazy val str : String = stringRepr()
- override def toString : String = str
-
- lazy val key: (Expr, Seq[T]) = {
- def rec(e: Expr): Seq[Identifier] = e match {
- case Variable(id) =>
- if (dependencies.isDefinedAt(id)) {
- Seq(id)
- } else {
- Seq.empty
- }
-
- case Operator(es, _) => es.flatMap(rec)
-
- case _ => Seq.empty
- }
-
- structuralKey -> rec(structuralKey).distinct.map(dependencies)
- }
-
- override def equals(that: Any): Boolean = that match {
- case t: LambdaTemplate[T] =>
- val (lambda1, deps1) = key
- val (lambda2, deps2) = t.key
- (lambda1 == lambda2) && {
- (deps1 zip deps2).forall { case (id1, id2) =>
- (manager.byID.get(id1), manager.byID.get(id2)) match {
- case (Some(t1), Some(t2)) => t1 == t2
- case _ => id1 == id2
- }
- }
- }
-
- case _ => false
+ def withId(idT: T): LambdaTemplate[T] = {
+ val substituter = encoder.substitute(Map(ids._2 -> idT))
+ new LambdaTemplate[T](
+ ids._1 -> idT, encoder, manager, pathVar, arguments, condVars, exprVars, condTree,
+ clauses map substituter, // make sure the body-defining clause is inlined!
+ blockers, applications, quantifications, matchers, lambdas,
+ dependencies, structuralKey, stringRepr
+ )
}
- override def hashCode: Int = key.hashCode
+ private lazy val str : String = stringRepr()
+ override def toString : String = str
- override def instantiate(substMap: Map[T, T]): Instantiation[T] = {
+ override def instantiate(substMap: Map[T, Arg[T]]): Instantiation[T] = {
super.instantiate(substMap) ++ manager.instantiateAxiom(this, substMap)
}
}
@@ -186,7 +189,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
private[templates] lazy val trueT = encoder.encodeExpr(Map.empty)(BooleanLiteral(true))
protected[templates] val byID = new IncrementalMap[T, LambdaTemplate[T]]
- protected val byType = new IncrementalMap[FunctionType, Set[LambdaTemplate[T]]].withDefaultValue(Set.empty)
+ protected val byType = new IncrementalMap[FunctionType, Map[(Expr, Seq[T]), LambdaTemplate[T]]].withDefaultValue(Map.empty)
protected val applications = new IncrementalMap[FunctionType, Set[(T, App[T])]].withDefaultValue(Set.empty)
protected val freeLambdas = new IncrementalMap[FunctionType, Set[T]].withDefaultValue(Set.empty)
@@ -203,27 +206,30 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
}
}
- def instantiateLambda(template: LambdaTemplate[T]): Instantiation[T] = {
- val idT = template.ids._2
- var clauses : Clauses[T] = equalityClauses(template)
- var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
+ def instantiateLambda(template: LambdaTemplate[T]): (T, Instantiation[T]) = {
+ byType(template.tpe).get(template.key) match {
+ case Some(template) =>
+ (template.ids._2, Instantiation.empty)
- // make sure the new lambda isn't equal to any free lambda var
- clauses ++= freeLambdas(template.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(pIdT, idT)))
+ case None =>
+ val idT = encoder.encodeId(template.ids._1)
+ val newTemplate = template.withId(idT)
- byID += idT -> template
+ var clauses : Clauses[T] = equalityClauses(newTemplate)
+ var appBlockers : AppBlockers[T] = Map.empty.withDefaultValue(Set.empty)
- if (byType(template.tpe)(template)) {
- (clauses, Map.empty, Map.empty)
- } else {
- byType += template.tpe -> (byType(template.tpe) + template)
+ // make sure the new lambda isn't equal to any free lambda var
+ clauses ++= freeLambdas(newTemplate.tpe).map(pIdT => encoder.mkNot(encoder.mkEquals(idT, pIdT)))
- for (blockedApp @ (_, App(caller, tpe, args)) <- applications(template.tpe)) {
- val equals = encoder.mkEquals(idT, caller)
- appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(template, equals, args)))
- }
+ byID += idT -> newTemplate
+ byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.key -> newTemplate))
+
+ for (blockedApp @ (_, App(caller, tpe, args)) <- applications(newTemplate.tpe)) {
+ val equals = encoder.mkEquals(idT, caller)
+ appBlockers += (blockedApp -> (appBlockers(blockedApp) + TemplateAppInfo(newTemplate, equals, args)))
+ }
- (clauses, Map.empty, appBlockers)
+ (idT, (clauses, Map.empty, appBlockers))
}
}
@@ -244,7 +250,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
// make sure that even if byType(tpe) is empty, app is recorded in blockers
// so that UnrollingBank will generate the initial block!
val init = instantiation withApps Map(key -> Set.empty)
- val inst = byType(tpe).foldLeft(init) {
+ val inst = byType(tpe).values.foldLeft(init) {
case (instantiation, template) =>
val equals = encoder.mkEquals(template.ids._2, caller)
instantiation withApp (key -> TemplateAppInfo(template, equals, args))
@@ -260,7 +266,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(enco
private def equalityClauses(template: LambdaTemplate[T]): Seq[T] = {
val (s1, deps1) = template.key
- byType(template.tpe).map { that =>
+ byType(template.tpe).values.map { that =>
val (s2, deps2) = that.key
val equals = encoder.mkEquals(template.ids._2, that.ids._2)
if (s1 == s2) {
diff --git a/src/main/scala/leon/solvers/templates/QuantificationManager.scala b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
index c7f715b5eefe573d88eeb94b45293ba7cde646bf..bc31267c09d8023390ac541b0cb99ecece6691ea 100644
--- a/src/main/scala/leon/solvers/templates/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/templates/QuantificationManager.scala
@@ -14,23 +14,17 @@ import purescala.Types._
import purescala.Quantification.{QuantificationTypeMatcher => QTM}
import Instantiation._
+import Template._
import scala.collection.mutable.{Map => MutableMap, Set => MutableSet, Stack => MutableStack, Queue}
-object Matcher {
- def argValue[T](arg: Either[T, Matcher[T]]): T = arg match {
- case Left(value) => value
- case Right(matcher) => matcher.encoded
- }
-}
-
-case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[Either[T, Matcher[T]]], encoded: T) {
+case class Matcher[T](caller: T, tpe: TypeTree, args: Seq[Arg[T]], encoded: T) {
override def toString = caller + args.map {
case Right(m) => m.toString
case Left(v) => v.toString
}.mkString("(",",",")")
- def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]] = Map.empty): Matcher[T] = copy(
+ def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): Matcher[T] = copy(
caller = substituter(caller),
args = args.map {
case Left(v) => matcherSubst.get(v) match {
@@ -58,11 +52,13 @@ class QuantificationTemplate[T](
val blockers: Map[T, Set[TemplateCallInfo[T]]],
val applications: Map[T, Set[App[T]]],
val matchers: Map[T, Set[Matcher[T]]],
- val lambdas: Seq[LambdaTemplate[T]]) {
+ val lambdas: Seq[LambdaTemplate[T]],
+ val dependencies: Map[Identifier, T],
+ val structuralKey: Forall) extends KeyedTemplate[T, Forall] {
lazy val start = pathVar._2
- def substitute(substituter: T => T): QuantificationTemplate[T] = {
+ def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): QuantificationTemplate[T] = {
new QuantificationTemplate[T](
quantificationManager,
pathVar._1 -> substituter(start),
@@ -76,15 +72,22 @@ class QuantificationTemplate[T](
condTree,
clauses.map(substituter),
blockers.map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+ substituter(b) -> fis.map(fi => fi.copy(
+ args = fi.args.map(_.substitute(substituter, matcherSubst))
+ ))
},
applications.map { case (b, apps) =>
- substituter(b) -> apps.map(app => app.copy(caller = substituter(app.caller), args = app.args.map(substituter)))
+ substituter(b) -> apps.map(app => app.copy(
+ caller = substituter(app.caller),
+ args = app.args.map(_.substitute(substituter, matcherSubst))
+ ))
},
matchers.map { case (b, ms) =>
- substituter(b) -> ms.map(_.substitute(substituter))
+ substituter(b) -> ms.map(_.substitute(substituter, matcherSubst))
},
- lambdas.map(_.substitute(substituter))
+ lambdas.map(_.substitute(substituter, matcherSubst)),
+ dependencies.map { case (id, value) => id -> substituter(value) },
+ structuralKey
)
}
}
@@ -104,7 +107,9 @@ object QuantificationTemplate {
condTree: Map[Identifier, Set[Identifier]],
guardedExprs: Map[Identifier, Seq[Expr]],
lambdas: Seq[LambdaTemplate[T]],
- subst: Map[Identifier, T]
+ baseSubstMap: Map[Identifier, T],
+ dependencies: Map[Identifier, T],
+ proposition: Forall
): QuantificationTemplate[T] = {
val q2s: (Identifier, T) = q2 -> encoder.encodeId(q2)
@@ -113,11 +118,15 @@ object QuantificationTemplate {
val (clauses, blockers, applications, matchers, _) =
Template.encode(encoder, pathVar, quantifiers, condVars, exprVars, guardedExprs, lambdas,
- substMap = subst + q2s + insts + guards + qs)
+ substMap = baseSubstMap + q2s + insts + guards + qs)
+
+ val (structuralQuant, structSubst) = normalizeStructure(proposition)
+ val keyDeps = dependencies.map { case (id, idT) => structSubst(id) -> idT }
+ val key = structuralQuant.asInstanceOf[Forall]
new QuantificationTemplate[T](quantificationManager,
- pathVar, qs, q2s, insts, guards._2, quantifiers,
- condVars, exprVars, condTree, clauses, blockers, applications, matchers, lambdas)
+ pathVar, qs, q2s, insts, guards._2, quantifiers, condVars, exprVars, condTree,
+ clauses, blockers, applications, matchers, lambdas, keyDeps, key)
}
}
@@ -130,9 +139,10 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
private val known = new IncrementalSet[T]
private val lambdaAxioms = new IncrementalSet[(LambdaTemplate[T], Seq[(Identifier, T)])]
+ private val templates = new IncrementalMap[(Expr, Seq[T]), T]
override protected def incrementals: List[IncrementalState] =
- List(quantifications, instCtx, handled, ignored, known, lambdaAxioms) ++ super.incrementals
+ List(quantifications, instCtx, handled, ignored, known, lambdaAxioms, templates) ++ super.incrementals
private sealed abstract class MatcherKey(val tpe: TypeTree)
private case class CallerKey(caller: T, tt: TypeTree) extends MatcherKey(tt)
@@ -386,7 +396,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
* matchers in the argument and quorum positions
*/
allMappings.filter { s =>
- def expand(ms: Traversable[(Either[T,Matcher[T]], Either[T,Matcher[T]])]): Set[(Matcher[T], Matcher[T])] = ms.flatMap {
+ def expand(ms: Traversable[(Arg[T], Arg[T])]): Set[(Matcher[T], Matcher[T])] = ms.flatMap {
case (Right(qm), Right(m)) => Set(qm -> m) ++ expand(qm.args zip m.args)
case _ => Set.empty[(Matcher[T], Matcher[T])]
}.toSet
@@ -398,11 +408,11 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
}
}
- private def extractSubst(mapping: Set[(Set[T], Matcher[T], Matcher[T])]): (Set[T], Map[T,Either[T, Matcher[T]]], Boolean) = {
+ private def extractSubst(mapping: Set[(Set[T], Matcher[T], Matcher[T])]): (Set[T], Map[T,Arg[T]], Boolean) = {
var constraints: Set[T] = Set.empty
var eqConstraints: Set[(T, T)] = Set.empty
var matcherEqs: List[(T, T)] = Nil
- var subst: Map[T, Either[T, Matcher[T]]] = Map.empty
+ var subst: Map[T, Arg[T]] = Map.empty
for {
(bs, qm @ Matcher(qcaller, _, qargs, _), m @ Matcher(caller, _, args, _)) <- mapping
@@ -411,16 +421,16 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(qarg, arg) <- (qargs zip args)
} qarg match {
case Left(quant) if subst.isDefinedAt(quant) =>
- eqConstraints += (quant -> Matcher.argValue(arg))
+ eqConstraints += (quant -> arg.encoded)
case Left(quant) if quantified(quant) =>
subst += quant -> arg
case Right(qam) =>
- val argVal = Matcher.argValue(arg)
+ val argVal = arg.encoded
eqConstraints += (qam.encoded -> argVal)
matcherEqs :+= qam.encoded -> argVal
}
- val substituter = encoder.substitute(subst.mapValues(Matcher.argValue))
+ val substituter = encoder.substitute(subst.mapValues(_.encoded))
val substConstraints = constraints.filter(_ != trueT).map(substituter)
val substEqs = eqConstraints.map(p => substituter(p._1) -> p._2)
.filter(p => p._1 != p._2).map(p => encoder.mkEquals(p._1, p._2))
@@ -437,25 +447,25 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val (enablers, subst, isStrict) = extractSubst(mapping)
val (enabler, optEnabler) = freshBlocker(enablers)
- if (optEnabler.isDefined) {
- instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
- }
-
- val baseSubstMap = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
- freshConds(pathVar._1 -> enabler, condVars, condTree)
- val lambdaSubstMap = lambdas map (lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
- val substMap = subst.mapValues(Matcher.argValue) ++ baseSubstMap ++ lambdaSubstMap ++ instanceSubst(enablers)
+ val baseSubst = subst ++ instanceSubst(enablers).mapValues(Left(_))
+ val (substMap, inst) = Template.substitution(encoder, QuantificationManager.this,
+ condVars, exprVars, condTree, Seq.empty, lambdas, baseSubst, pathVar._1, enabler)
if (!skip(substMap)) {
+ if (optEnabler.isDefined) {
+ instantiation = instantiation withClause encoder.mkEquals(enabler, optEnabler.get)
+ }
+
+ instantiation ++= inst
instantiation ++= Template.instantiate(encoder, QuantificationManager.this,
clauses, blockers, applications, Seq.empty, Map.empty[T, Set[Matcher[T]]], lambdas, substMap)
- val msubst = subst.collect { case (c, Right(m)) => c -> m }
- val substituter = encoder.substitute(substMap)
+ val msubst = substMap.collect { case (c, Right(m)) => c -> m }
+ val substituter = encoder.substitute(substMap.mapValues(_.encoded))
for ((b,ms) <- allMatchers; m <- ms) {
val sb = enablers ++ (if (b == start) Set.empty else Set(substituter(b)))
- val sm = m.substitute(substituter, matcherSubst = msubst)
+ val sm = m.substitute(substituter, msubst)
if (matchers(m)) {
handled += sb -> sm
@@ -473,7 +483,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
protected def instanceSubst(enablers: Set[T]): Map[T, T]
- protected def skip(subst: Map[T, T]): Boolean = false
+ protected def skip(subst: Map[T, Arg[T]]): Boolean = false
}
private class Quantification (
@@ -545,10 +555,11 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
Map(guardVar -> guardT, blocker -> newBlocker)
}
- override protected def skip(subst: Map[T, T]): Boolean = {
- val substituter = encoder.substitute(subst)
+ override protected def skip(subst: Map[T, Arg[T]]): Boolean = {
+ val substituter = encoder.substitute(subst.mapValues(_.encoded))
+ val msubst = subst.collect { case (c, Right(m)) => c -> m }
allMatchers.forall { case (b, ms) =>
- ms.forall(m => matchers(m) || instCtx(Set(substituter(b)) -> m.substitute(substituter)))
+ ms.forall(m => matchers(m) || instCtx(Set(substituter(b)) -> m.substitute(substituter, msubst)))
}
}
}
@@ -577,9 +588,9 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(m: Matcher[T]) => m.args.collect { case Left(a) if quantified(a) => a }.toSet)
}
- def instantiateAxiom(template: LambdaTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
- val quantifiers = template.arguments map {
- case (id, idT) => id -> substMap(idT)
+ def instantiateAxiom(template: LambdaTemplate[T], substMap: Map[T, Arg[T]]): Instantiation[T] = {
+ val quantifiers = template.arguments flatMap {
+ case (id, idT) => substMap(idT).left.toOption.map(id -> _)
} filter (p => isQuantifier(p._2))
if (quantifiers.isEmpty || lambdaAxioms(template -> quantifiers)) {
@@ -591,19 +602,24 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val guard = FreshIdentifier("guard", BooleanType, true)
val guardT = encoder.encodeId(guard)
- val substituter = encoder.substitute(substMap + (template.start -> blockerT))
- val allMatchers = template.matchers map { case (b, ms) => substituter(b) -> ms.map(_.substitute(substituter)) }
+ val substituter = encoder.substitute(substMap.mapValues(_.encoded) + (template.start -> blockerT))
+ val msubst = substMap.collect { case (c, Right(m)) => c -> m }
+
+ val allMatchers = template.matchers map { case (b, ms) =>
+ substituter(b) -> ms.map(_.substitute(substituter, msubst))
+ }
+
val qMatchers = allMatchers.flatMap(_._2).toSet
- val encArgs = template.args map substituter
+ val encArgs = template.args map (arg => Left(arg).substitute(substituter, msubst))
val app = Application(Variable(template.ids._1), template.arguments.map(_._1.toVariable))
- val appT = encoder.encodeExpr((template.arguments.map(_._1) zip encArgs).toMap + template.ids)(app)
- val selfMatcher = Matcher(template.ids._2, template.tpe, encArgs.map(Left(_)), appT)
+ val appT = encoder.encodeExpr((template.arguments.map(_._1) zip encArgs.map(_.encoded)).toMap + template.ids)(app)
+ val selfMatcher = Matcher(template.ids._2, template.tpe, encArgs, appT)
val enablingClause = encoder.mkImplies(guardT, blockerT)
instantiateAxiom(
- template.pathVar._1 -> substMap(template.start),
+ template.pathVar._1 -> substituter(template.start),
blockerT,
guardT,
quantifiers,
@@ -614,12 +630,17 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
template.condTree,
(template.clauses map substituter) :+ enablingClause,
template.blockers map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+ substituter(b) -> fis.map(fi => fi.copy(
+ args = fi.args.map(_.substitute(substituter, msubst))
+ ))
},
template.applications map { case (b, apps) =>
- substituter(b) -> apps.map(app => app.copy(caller = substituter(app.caller), args = app.args.map(substituter)))
+ substituter(b) -> apps.map(app => app.copy(
+ caller = substituter(app.caller),
+ args = app.args.map(_.substitute(substituter, msubst))
+ ))
},
- template.lambdas map (_.substitute(substituter))
+ template.lambdas map (_.substitute(substituter, msubst))
)
}
}
@@ -664,73 +685,70 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
for {
m <- matchers
- sm = m.substitute(substituter)
+ sm = m.substitute(substituter, Map.empty)
if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
} instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
instantiation
}
- def instantiateQuantification(template: QuantificationTemplate[T], substMap: Map[T, T]): Instantiation[T] = {
- val quantified = template.quantifiers.map(_._2).toSet
- val matchQuorums = extractQuorums(quantified, template.matchers.flatMap(_._2).toSet, template.lambdas)
-
- var instantiation = Instantiation.empty[T]
+ def instantiateQuantification(template: QuantificationTemplate[T]): (T, Instantiation[T]) = {
+ templates.get(template.key) match {
+ case Some(idT) =>
+ (idT, Instantiation.empty)
- val qs = for (matchers <- matchQuorums) yield {
- val newQ = encoder.encodeId(template.qs._1)
- val subst = substMap + (template.qs._2 -> newQ)
-
- val substituter = encoder.substitute(subst)
- val quantification = new Quantification(
- template.pathVar._1 -> substituter(template.start),
- template.qs._1 -> newQ,
- template.q2s, template.insts, template.guardVar,
- quantified,
- matchers map (_.substitute(substituter)),
- template.matchers map { case (b, ms) => substituter(b) -> ms.map(_.substitute(substituter)) },
- template.condVars,
- template.exprVars,
- template.condTree,
- template.clauses map substituter,
- template.blockers map { case (b, fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
- },
- template.applications map { case (b, fas) =>
- substituter(b) -> fas.map(fa => fa.copy(caller = substituter(fa.caller), args = fa.args.map(substituter)))
- },
- template.lambdas map (_.substitute(substituter))
- )
+ case None =>
+ val qT = encoder.encodeId(template.qs._1)
+ val quantified = template.quantifiers.map(_._2).toSet
+ val matchQuorums = extractQuorums(quantified, template.matchers.flatMap(_._2).toSet, template.lambdas)
- quantifications += quantification
+ var instantiation = Instantiation.empty[T]
- val newCtx = new InstantiationContext()
- for ((b,m) <- instCtx.instantiated) {
- instantiation ++= newCtx.instantiate(b, m)(quantification)
- }
- instCtx.merge(newCtx)
+ val qs = for (matchers <- matchQuorums) yield {
+ val newQ = encoder.encodeId(template.qs._1)
+ val substituter = encoder.substitute(Map(template.qs._2 -> newQ))
+
+ val quantification = new Quantification(
+ template.pathVar,
+ template.qs._1 -> newQ,
+ template.q2s, template.insts, template.guardVar,
+ quantified, matchers, template.matchers,
+ template.condVars, template.exprVars, template.condTree,
+ template.clauses map substituter, // one clause depends on 'q' (and therefore 'newQ')
+ template.blockers, template.applications, template.lambdas
+ )
+
+ quantifications += quantification
+
+ val newCtx = new InstantiationContext()
+ for ((b,m) <- instCtx.instantiated) {
+ instantiation ++= newCtx.instantiate(b, m)(quantification)
+ }
+ instCtx.merge(newCtx)
- quantification.qs._2
- }
+ quantification.qs._2
+ }
- instantiation = instantiation withClause {
- val newQs =
- if (qs.isEmpty) trueT
- else if (qs.size == 1) qs.head
- else encoder.mkAnd(qs : _*)
- encoder.mkImplies(substMap(template.start), encoder.mkEquals(substMap(template.qs._2), newQs))
- }
+ instantiation = instantiation withClause {
+ val newQs =
+ if (qs.isEmpty) trueT
+ else if (qs.size == 1) qs.head
+ else encoder.mkAnd(qs : _*)
+ encoder.mkImplies(template.start, encoder.mkEquals(qT, newQs))
+ }
- val quantifierSubst = uniformSubst(template.quantifiers)
- val substituter = encoder.substitute(substMap ++ quantifierSubst)
+ val quantifierSubst = uniformSubst(template.quantifiers)
+ val substituter = encoder.substitute(quantifierSubst)
- for {
- (_, ms) <- template.matchers; m <- ms
- sm = m.substitute(substituter)
- if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
- } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
+ for {
+ (_, ms) <- template.matchers; m <- ms
+ sm = m.substitute(substituter, Map.empty)
+ if !instCtx.corresponding(sm).exists(_._2.args == sm.args)
+ } instantiation ++= instCtx.instantiate(Set.empty, sm)(quantifications.toSeq : _*)
- instantiation
+ templates += template.key -> qT
+ (qT, instantiation)
+ }
}
def instantiateMatcher(blocker: T, matcher: Matcher[T]): Instantiation[T] = {
@@ -779,7 +797,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
var prev = emptyT
for ((b, m) <- insts.toSeq) {
val next = encoder.encodeId(setNext)
- val argsMap = (elems zip m.args).map { case (idT, arg) => idT -> Matcher.argValue(arg) }
+ val argsMap = (elems zip m.args).map { case (idT, arg) => idT -> arg.encoded }
val substMap = Map(guardT -> b, setPrevT -> prev, setNextT -> next) ++ argsMap
prev = next
clauses += encoder.substitute(substMap)(setT)
@@ -787,7 +805,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
val setMap = Map(setPrevT -> prev)
for ((b, m) <- ctx.toSeq) {
- val substMap = setMap ++ (elems zip m.args).map(p => p._1 -> Matcher.argValue(p._2))
+ val substMap = setMap ++ (elems zip m.args).map(p => p._1 -> p._2.encoded)
clauses += encoder.substitute(substMap)(encoder.mkImplies(b, containsT))
}
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 4434eafd5ae0569640b1c4f7cc60c3946ef56d7b..aa0e5dad6506be945919cb22361cce649f40c077 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -65,7 +65,9 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val invocationEqualsBody : Option[Expr] = lambdaBody match {
case Some(body) if isRealFunDef =>
- val b : Expr = And(Equals(invocation, body), liftedEquals(invocation, body, lambdaArguments))
+ val b : Expr = And(
+ liftedEquals(invocation, body, lambdaArguments),
+ Equals(invocation, body))
Some(if(prec.isDefined) {
Implies(prec.get, b)
@@ -121,7 +123,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
}
private def lambdaArgs(expr: Expr): Seq[Identifier] = expr match {
- case Lambda(args, body) => args.map(_.id) ++ lambdaArgs(body)
+ case Lambda(args, body) => args.map(_.id.freshen) ++ lambdaArgs(body)
case IsTyped(_, _: FunctionType) => sys.error("Only applicable on lambda chains")
case _ => Seq.empty
}
@@ -133,7 +135,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val arguments = currArgs.map(_.toVariable)
val apply = if (inline) application _ else Application
val (appliedInv, appliedBody) = (apply(i, arguments), apply(b, arguments))
- Equals(appliedInv, appliedBody) +: rec(appliedInv, appliedBody, nextArgs, false)
+ rec(appliedInv, appliedBody, nextArgs, false) :+ Equals(appliedInv, appliedBody)
case _ =>
assert(args.isEmpty, "liftedEquals should consume all provided arguments")
Seq.empty
@@ -453,8 +455,10 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
Equals(Variable(q), And(Variable(q2), Variable(inst)))
) ++ qGuarded.getOrElse(pathVar, Seq.empty)))
+ val dependencies: Map[Identifier, T] = vars.filterNot(quantifiers).map(id => id -> localSubst(id)).toMap
val template = QuantificationTemplate[T](encoder, manager, pathVar -> encodedCond(pathVar),
- qs, q2, inst, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qTree, allGuarded, qTemplates, localSubst)
+ qs, q2, inst, guard, idQuantifiers zip trQuantifiers, qConds, qExprs, qTree, allGuarded, qTemplates, localSubst,
+ dependencies, Forall(quantifiers.toSeq.sortBy(_.uniqueName).map(ValDef(_)), flatConj))
registerQuantification(template)
Variable(q)
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateInfo.scala b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
index 033f15dd6f251026a260ed6344212239e1714a37..27df9b25d13412c106f2bf30d6c75b1266b19d93 100644
--- a/src/main/scala/leon/solvers/templates/TemplateInfo.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
@@ -5,15 +5,22 @@ package solvers
package templates
import purescala.Definitions.TypedFunDef
+import Template.Arg
-case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[T]) {
+case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[Arg[T]]) {
override def toString = {
- tfd.signature+args.mkString("(", ", ", ")")
+ tfd.signature + args.map {
+ case Right(m) => m.toString
+ case Left(v) => v.toString
+ }.mkString("(", ", ", ")")
}
}
-case class TemplateAppInfo[T](template: LambdaTemplate[T], equals: T, args: Seq[T]) {
+case class TemplateAppInfo[T](template: LambdaTemplate[T], equals: T, args: Seq[Arg[T]]) {
override def toString = {
- template.ids._2 + "|" + equals + args.mkString("(", ",", ")")
+ template.ids._2 + "|" + equals + args.map {
+ case Right(m) => m.toString
+ case Left(v) => v.toString
+ }.mkString("(", ",", ")")
}
}
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index bb6629ec16988a79eb686259aea4fa32c6111dbb..2b75f08f0480cf272515bb8d8393e01e29d4dbf1 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -57,6 +57,7 @@ object Instantiation {
}
import Instantiation.{empty => _, _}
+import Template.Arg
trait Template[T] { self =>
val encoder : TemplateEncoder[T]
@@ -76,27 +77,14 @@ trait Template[T] { self =>
lazy val start = pathVar._2
- private var substCache : Map[Seq[T],Map[T,T]] = Map.empty
-
- def instantiate(aVar: T, args: Seq[T]): Instantiation[T] = {
-
- val baseSubstMap : Map[T,T] = substCache.get(args) match {
- case Some(subst) => subst
- case None =>
- val subst = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
- manager.freshConds(pathVar._1 -> aVar, condVars, condTree) ++
- (this.args zip args)
- substCache += args -> subst
- subst
- }
-
- val lambdaSubstMap = lambdas.map(lambda => lambda.ids._2 -> encoder.encodeId(lambda.ids._1))
- val quantificationSubstMap = quantifications.map(q => q.qs._2 -> encoder.encodeId(q.qs._1))
- val substMap : Map[T,T] = baseSubstMap ++ lambdaSubstMap ++ quantificationSubstMap + (start -> aVar)
- instantiate(substMap)
+ def instantiate(aVar: T, args: Seq[Arg[T]]): Instantiation[T] = {
+ val (substMap, instantiation) = Template.substitution(encoder, manager,
+ condVars, exprVars, condTree, quantifications, lambdas,
+ (this.args zip args).toMap + (start -> Left(aVar)), pathVar._1, aVar)
+ instantiation ++ instantiate(substMap)
}
- protected def instantiate(substMap: Map[T, T]): Instantiation[T] = {
+ protected def instantiate(substMap: Map[T, Arg[T]]): Instantiation[T] = {
Template.instantiate(encoder, manager,
clauses, blockers, applications, quantifications, matchers, lambdas, substMap)
}
@@ -106,6 +94,23 @@ trait Template[T] { self =>
object Template {
+ type Arg[T] = Either[T, Matcher[T]]
+
+ implicit class ArgWrapper[T](arg: Arg[T]) {
+ def encoded: T = arg match {
+ case Left(value) => value
+ case Right(matcher) => matcher.encoded
+ }
+
+ def substitute(substituter: T => T, matcherSubst: Map[T, Matcher[T]]): Arg[T] = arg match {
+ case Left(v) => matcherSubst.get(v) match {
+ case Some(m) => Right(m)
+ case None => Left(substituter(v))
+ }
+ case Right(m) => Right(m.substitute(substituter, matcherSubst))
+ }
+ }
+
private def invocationMatcher[T](encodeExpr: Expr => T)(tfd: TypedFunDef, args: Seq[Expr]): Matcher[T] = {
assert(tfd.returnType.isInstanceOf[FunctionType], "invocationMatcher() is only defined on function-typed defs")
@@ -144,9 +149,9 @@ object Template {
encodeExpr(Implies(Variable(b), e))
}).toSeq
- val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(_._2)))
+ val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(p => Left(p._2))))
val optIdApp = optApp.map { case (idT, tpe) =>
- App(idT, bestRealType(tpe).asInstanceOf[FunctionType], arguments.map(_._2))
+ App(idT, bestRealType(tpe).asInstanceOf[FunctionType], arguments.map(p => Left(p._2)))
}
lazy val invocMatcher = optCall.filter(_.returnType.isInstanceOf[FunctionType])
@@ -163,12 +168,7 @@ object Template {
var matchInfos : Set[Matcher[T]] = Set.empty
for (e <- es) {
- funInfos ++= firstOrderCallsOf(e).map(p => TemplateCallInfo(p._1, p._2.map(encodeExpr)))
- appInfos ++= firstOrderAppsOf(e).map { case (c, args) =>
- App(encodeExpr(c), bestRealType(c.getType).asInstanceOf[FunctionType], args.map(encodeExpr))
- }
-
- matchInfos ++= fold[Map[Expr, Matcher[T]]] { (expr, res) =>
+ val exprToMatcher = fold[Map[Expr, Matcher[T]]] { (expr, res) =>
val result = res.flatten.toMap
result ++ (expr match {
@@ -183,7 +183,19 @@ object Template {
Some(expr -> Matcher(encodeExpr(c), bestRealType(c.getType), encodedArgs, encodeExpr(expr)))
case _ => None
})
- }(e).values
+ }(e)
+
+ def encodeArg(arg: Expr): Arg[T] = exprToMatcher.get(arg) match {
+ case Some(matcher) => Right(matcher)
+ case None => Left(encodeExpr(arg))
+ }
+
+ funInfos ++= firstOrderCallsOf(e).map(p => TemplateCallInfo(p._1, p._2.map(encodeArg)))
+ appInfos ++= firstOrderAppsOf(e).map { case (c, args) =>
+ App(encodeExpr(c), bestRealType(c.getType).asInstanceOf[FunctionType], args.map(encodeArg))
+ }
+
+ matchInfos ++= exprToMatcher.values
}
val calls = funInfos -- optIdCall
@@ -194,7 +206,7 @@ object Template {
val matchs = matchInfos.filter { case m @ Matcher(mc, mtpe, margs, _) =>
!optIdApp.exists { case App(ac, atpe, aargs) =>
- mc == ac && mtpe == atpe && margs.map(Matcher.argValue) == aargs
+ mc == ac && mtpe == atpe && margs == aargs
}
} ++ (if (funInfos.exists(info => Some(info) == optIdCall)) invocMatcher else None)
@@ -212,8 +224,9 @@ object Template {
" * Activating boolean : " + pathVar._1 + "\n" +
" * Control booleans : " + condVars.keys.mkString(", ") + "\n" +
" * Expression vars : " + exprVars.keys.mkString(", ") + "\n" +
- " * Clauses : " +
- (for ((b,es) <- guardedExprs; e <- es) yield (b + " ==> " + e)).mkString("\n ") + "\n" +
+ " * Clauses : " + (if (guardedExprs.isEmpty) "\n" else {
+ "\n " + (for ((b,es) <- guardedExprs; e <- es) yield (b + " ==> " + e)).mkString("\n ") + "\n"
+ }) +
" * Invocation-blocks :" + (if (blockers.isEmpty) "\n" else {
"\n " + blockers.map(p => p._1 + " ==> " + p._2).mkString("\n ") + "\n"
}) +
@@ -231,6 +244,60 @@ object Template {
(clauses, encodedBlockers, encodedApps, encodedMatchers, stringRepr)
}
+ def substitution[T](
+ encoder: TemplateEncoder[T],
+ manager: QuantificationManager[T],
+ condVars: Map[Identifier, T],
+ exprVars: Map[Identifier, T],
+ condTree: Map[Identifier, Set[Identifier]],
+ quantifications: Seq[QuantificationTemplate[T]],
+ lambdas: Seq[LambdaTemplate[T]],
+ baseSubst: Map[T, Arg[T]],
+ pathVar: Identifier,
+ aVar: T
+ ): (Map[T, Arg[T]], Instantiation[T]) = {
+ val freshSubst = exprVars.map { case (id, idT) => idT -> encoder.encodeId(id) } ++
+ manager.freshConds(pathVar -> aVar, condVars, condTree)
+ val matcherSubst = baseSubst.collect { case (c, Right(m)) => c -> m }
+ var subst = freshSubst.mapValues(Left(_)) ++ baseSubst
+
+ // /!\ CAREFUL /!\
+ // We have to be wary while computing the lambda subst map since lambdas can
+ // depend on each other. However, these dependencies cannot be cyclic so it
+ // suffices to make sure the traversal order is correct.
+ var instantiation : Instantiation[T] = Instantiation.empty
+ var seen : Set[LambdaTemplate[T]] = Set.empty
+
+ val lambdaKeys = lambdas.map(lambda => lambda.ids._1 -> lambda).toMap
+ def extractSubst(lambda: LambdaTemplate[T]): Unit = {
+ for {
+ dep <- lambda.dependencies.flatMap(p => lambdaKeys.get(p._1))
+ if !seen(dep)
+ } extractSubst(dep)
+
+ if (!seen(lambda)) {
+ val substMap = subst.mapValues(_.encoded)
+ val substLambda = lambda.substitute(encoder.substitute(substMap), matcherSubst)
+ val (idT, inst) = manager.instantiateLambda(substLambda)
+ instantiation ++= inst
+ subst += lambda.ids._2 -> Left(idT)
+ seen += lambda
+ }
+ }
+
+ for (l <- lambdas) extractSubst(l)
+
+ for (q <- quantifications) {
+ val substMap = subst.mapValues(_.encoded)
+ val substQuant = q.substitute(encoder.substitute(substMap), matcherSubst)
+ val (qT, inst) = manager.instantiateQuantification(substQuant)
+ instantiation ++= inst
+ subst += q.qs._2 -> Left(qT)
+ }
+
+ (subst, instantiation)
+ }
+
def instantiate[T](
encoder: TemplateEncoder[T],
manager: QuantificationManager[T],
@@ -240,33 +307,27 @@ object Template {
quantifications: Seq[QuantificationTemplate[T]],
matchers: Map[T, Set[Matcher[T]]],
lambdas: Seq[LambdaTemplate[T]],
- substMap: Map[T, T]
+ substMap: Map[T, Arg[T]]
): Instantiation[T] = {
- val substituter : T => T = encoder.substitute(substMap)
+ val substituter : T => T = encoder.substitute(substMap.mapValues(_.encoded))
+ val msubst = substMap.collect { case (c, Right(m)) => c -> m }
val newClauses = clauses.map(substituter)
val newBlockers = blockers.map { case (b,fis) =>
- substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(substituter)))
+ substituter(b) -> fis.map(fi => fi.copy(args = fi.args.map(_.substitute(substituter, msubst))))
}
var instantiation: Instantiation[T] = (newClauses, newBlockers, Map.empty)
- for (lambda <- lambdas) {
- instantiation ++= manager.instantiateLambda(lambda.substitute(substituter))
- }
-
for ((b,apps) <- applications; bp = substituter(b); app <- apps) {
- val newApp = app.copy(caller = substituter(app.caller), args = app.args.map(substituter))
+ val newApp = app.copy(caller = substituter(app.caller), args = app.args.map(_.substitute(substituter, msubst)))
instantiation ++= manager.instantiateApp(bp, newApp)
}
for ((b, matchs) <- matchers; bp = substituter(b); m <- matchs) {
- instantiation ++= manager.instantiateMatcher(bp, m.substitute(substituter))
- }
-
- for (q <- quantifications) {
- instantiation ++= manager.instantiateQuantification(q, substMap)
+ val newMatcher = m.substitute(substituter, msubst)
+ instantiation ++= manager.instantiateMatcher(bp, newMatcher)
}
instantiation
@@ -343,8 +404,8 @@ class FunctionTemplate[T] private(
private lazy val str : String = stringRepr()
override def toString : String = str
- override def instantiate(aVar: T, args: Seq[T]): (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
- if (!isRealFunDef) manager.registerFree(tfd.params.map(_.id) zip args)
+ override def instantiate(aVar: T, args: Seq[Arg[T]]): Instantiation[T] = {
+ if (!isRealFunDef) manager.registerFree(tfd.params.map(_.id) zip args.map(_.left.get))
super.instantiate(aVar, args)
}
}
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index d1c4432a3c69f1882c9b4a1787a12dc8cf64f520..4543262d74204dd9f77d3eeea8882bf543956a90 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -171,7 +171,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
// define an activating boolean...
val template = templateGenerator.mkTemplate(expr)
- val trArgs = template.tfd.params.map(vd => bindings(Variable(vd.id)))
+ val trArgs = template.tfd.params.map(vd => Left(bindings(Variable(vd.id))))
for (vd <- template.tfd.params if vd.getType.isInstanceOf[FunctionType]) {
functionVars += vd.getType -> (functionVars.getOrElse(vd.getType, Set()) + bindings(vd.toVariable))
@@ -240,16 +240,22 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
callInfos --= ids
val apps = ids.flatMap(id => blockerToApps.get(id))
- val thisAppInfos = apps.map(app => app -> appInfos(app))
+ val thisAppInfos = apps.map(app => app -> {
+ val (gen, _, _, _, infos) = appInfos(app)
+ (gen, infos)
+ })
+
blockerToApps --= ids
appInfos --= apps
- for ((app, (_, _, _, _, infos)) <- thisAppInfos if infos.nonEmpty) {
+ for ((app, (_, infos)) <- thisAppInfos if infos.nonEmpty) {
val extension = extendAppBlock(app, infos)
reporter.debug(" -> extending lambda blocker: " + extension)
newClauses :+= extension
}
+ var fastAppInfos : Map[(T, App[T]), (Int, Set[TemplateAppInfo[T]])] = Map.empty
+
for ((id, (gen, _, _, infos)) <- newCallInfos; info @ TemplateCallInfo(tfd, args) <- infos) {
var newCls = Seq[T]()
@@ -268,13 +274,23 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
//reporter.debug(template)
val (newExprs, callBlocks, appBlocks) = template.instantiate(defBlocker, args)
- val blockExprs = freshAppBlocks(appBlocks.keys)
+
+ // we handle obvious appBlocks in an immediate manner in order to increase
+ // performance for folds that just pass a lambda around to recursive calls
+ val (fastApps, nextApps) = appBlocks.partition(p => p._2.toSeq match {
+ case Seq(TemplateAppInfo(_, equals, _)) if equals == manager.trueT => true
+ case _ => false
+ })
+
+ fastAppInfos ++= fastApps.mapValues(gen -> _)
+
+ val blockExprs = freshAppBlocks(nextApps.keys)
for((b, newInfos) <- callBlocks) {
registerCallBlocker(nextGeneration(gen), b, newInfos)
}
- for ((app, newInfos) <- appBlocks) {
+ for ((app, newInfos) <- nextApps) {
registerAppBlocker(nextGeneration(gen), app, newInfos)
}
@@ -296,7 +312,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
newClauses ++= newCls
}
- for ((app @ (b, _), (gen, _, _, _, infos)) <- thisAppInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
+ for ((app @ (b, _), (gen, infos)) <- thisAppInfos ++ fastAppInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
var newCls = Seq.empty[T]
val lambdaBlocker = lambdaBlockers.get(info) match {
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 6a96848c5fb283ec1a6ae22817afff95f9300122..3d39ae7e7e99e45b344859d46496c31baa17ad8c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -17,6 +17,7 @@ import purescala.ExprOps._
import purescala.Types._
import solvers.templates._
+import Template._
import evaluators._
@@ -66,7 +67,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
if (optEnabler == Some(true)) {
val optArgs = (m.args zip fromTypes).map {
- p => softFromZ3Formula(model, model.eval(Matcher.argValue(p._1), true).get, p._2)
+ p => softFromZ3Formula(model, model.eval(p._1.encoded, true).get, p._2)
}
if (optArgs.forall(_.isDefined)) {
@@ -243,7 +244,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
solver.assertCnstr(clause)
}
- reporter.debug(" - Verifying model transitivity")
+ reporter.debug(" - Enforcing model transitivity")
val timer = context.timers.solvers.z3.check.start()
solver.push() // FIXME: remove when z3 bug is fixed
val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.satisfactionAssumptions) :_*)
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index d172c27204e8fac1219ad4041221ad874f4b9ba2..13f1788fffec11ca03139210d52815699d386324 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -189,6 +189,8 @@ object ConversionPhase extends UnitPhase[Program] {
// extract spec from chooses at the top-level
fullBody match {
+ case Require(_, Choose(spec)) =>
+ withPostcondition(fullBody, Some(spec))
case Choose(spec) =>
withPostcondition(fullBody, Some(spec))
case _ =>
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 5565aa4e54c970d08f8ba29bcb32c95f0c05e7bf..cd27e272d53e9669f4c2d1f2c8e07356819b4827 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -42,10 +42,12 @@ object Rules {
Unification.OccursCheck, // probably useless
Disunification.Decomp,
ADTDual,
- //OnePoint,
+ OnePoint,
Ground,
CaseSplit,
+ IndependentSplit,
IfSplit,
+ InputSplit,
UnusedInput,
EquivalentInputs,
UnconstrainedOutput,
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 72cfffec3f8ef3fd8a526d778fda1f26a9ec1a41..b9ba6df1f688e01edf631e995ba2f8623bcfc5fe 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -6,6 +6,7 @@ package synthesis
import purescala.ExprOps._
import purescala.ScalaPrinter
+import leon.utils._
import purescala.Definitions.{Program, FunDef}
import leon.utils.ASCIIHelpers
@@ -20,12 +21,11 @@ object SynthesisPhase extends TransformationPhase {
val optDerivTrees = LeonFlagOptionDef( "derivtrees", "Generate derivation trees", false)
// CEGIS options
- val optCEGISShrink = LeonFlagOptionDef( "cegis:shrink", "Shrink non-det programs when tests pruning works well", true)
val optCEGISOptTimeout = LeonFlagOptionDef( "cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true)
val optCEGISVanuatoo = LeonFlagOptionDef( "cegis:vanuatoo", "Generate inputs using new korat-style generator", false)
override val definedOptions : Set[LeonOptionDef[Any]] =
- Set(optManual, optCostModel, optDerivTrees, optCEGISShrink, optCEGISOptTimeout, optCEGISVanuatoo)
+ Set(optManual, optCostModel, optDerivTrees, optCEGISOptTimeout, optCEGISVanuatoo)
def processOptions(ctx: LeonContext): SynthesisSettings = {
val ms = ctx.findOption(optManual)
@@ -57,7 +57,6 @@ object SynthesisPhase extends TransformationPhase {
manualSearch = ms,
functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
cegisUseOptTimeout = ctx.findOption(optCEGISOptTimeout),
- cegisUseShrink = ctx.findOption(optCEGISShrink),
cegisUseVanuatoo = ctx.findOption(optCEGISVanuatoo)
)
}
@@ -74,21 +73,25 @@ object SynthesisPhase extends TransformationPhase {
val synthesizer = new Synthesizer(ctx, program, ci, options)
- val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+ val to = new TimeoutFor(ctx.interruptManager)
- try {
- if (options.generateDerivationTrees) {
- val dot = new DotGenerator(search.g)
- dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
- }
+ to.interruptAfter(options.timeoutMs) {
+ val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+
+ try {
+ if (options.generateDerivationTrees) {
+ val dot = new DotGenerator(search.g)
+ dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
+ }
- val (sol, _) = solutions.head
+ val (sol, _) = solutions.head
- val expr = sol.toSimplifiedExpr(ctx, program)
- fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
- functions += fd
- } finally {
- synthesizer.shutdown()
+ val expr = sol.toSimplifiedExpr(ctx, program)
+ fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
+ functions += fd
+ } finally {
+ synthesizer.shutdown()
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index 9d227bdb611f2ca44eb70a95ce52bc506712e160..5202818e18765ebf4086ef41d1685967a14940d0 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -17,7 +17,6 @@ case class SynthesisSettings(
// Cegis related options
cegisUseOptTimeout: Option[Boolean] = None,
- cegisUseShrink: Option[Boolean] = None,
cegisUseVanuatoo: Option[Boolean] = None
)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 35fdfb845ae0a5de611ab3a01a3111005aff7a05..bafed6ec2bab51539bfc0547563bbad2aeea873e 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -8,6 +8,7 @@ import purescala.ExprOps._
import purescala.DefOps._
import purescala.ScalaPrinter
import solvers._
+import leon.utils._
import scala.concurrent.duration._
@@ -34,9 +35,10 @@ class Synthesizer(val context : LeonContext,
}
}
- def synthesize(): (Search, Stream[Solution]) = {
+ private var lastTime: Long = 0
- reporter.ifDebug { printer =>
+ def synthesize(): (Search, Stream[Solution]) = {
+ reporter.ifDebug { printer =>
printer(problem.eb.asString("Tests available for synthesis")(context))
}
@@ -47,8 +49,12 @@ class Synthesizer(val context : LeonContext,
val sols = s.search(sctx)
val diff = t.stop()
+
+ lastTime = diff
+
reporter.info("Finished in "+diff+"ms")
+
(s, sols)
}
@@ -62,6 +68,43 @@ class Synthesizer(val context : LeonContext,
validateSolution(s, sol, 5.seconds)
}
+ // Print out report for synthesis, if necessary
+ reporter.ifDebug { printer =>
+ import java.io.FileWriter
+ import java.text.SimpleDateFormat
+ import java.util.Date
+
+ val categoryName = ci.fd.getPos.file.toString.split("/").dropRight(1).lastOption.getOrElse("?")
+ val benchName = categoryName+"."+ci.fd.id.name
+ var time = lastTime/1000.0;
+
+ val defs = visibleDefsFrom(ci.fd)(program).collect {
+ case cd: ClassDef => 1 + cd.fields.size
+ case fd: FunDef => 1 + fd.params.size + formulaSize(fd.fullBody)
+ }
+
+ val psize = defs.sum;
+
+
+ val (size, calls, proof) = result.headOption match {
+ case Some((sol, trusted)) =>
+ val expr = sol.toSimplifiedExpr(context, program)
+ (formulaSize(expr), functionCallsOf(expr).size, if (trusted) "$\\surd$" else "")
+ case _ =>
+ (0, 0, "X")
+ }
+
+ val date = new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(new Date())
+
+ val fw = new java.io.FileWriter("synthesis-report.txt", true)
+
+ try {
+ fw.write(f"$date: $benchName%-50s & $psize%4d & $size%4d & $calls%4d & $proof%7s & $time%2.1f \\\\\n")
+ } finally {
+ fw.close
+ }
+ }(DebugSectionReport)
+
(s, if (result.isEmpty && allowPartial) {
List((new PartialSolution(s.g, true).getSolution, false)).toStream
} else {
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 5d06aa76a3c1186e806edf605431643e6b2a9359..4f03c9bed6ca7c7ce5338d04283483ab9f348890 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -45,14 +45,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// CEGIS Flags to activate or deactivate features
val useOptTimeout = sctx.settings.cegisUseOptTimeout.getOrElse(true)
val useVanuatoo = sctx.settings.cegisUseVanuatoo.getOrElse(false)
- val useShrink = sctx.settings.cegisUseShrink.getOrElse(false)
// Limits the number of programs CEGIS will specifically validate individually
val validateUpTo = 3
- // Shrink the program when the ratio of passing cases is less than the threshold
- val shrinkThreshold = 1.0/2
-
val interruptManager = sctx.context.interruptManager
val params = getParams(sctx, p)
@@ -67,9 +63,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val grammar = SizeBoundedGrammar(params.grammar)
- def rootLabel(tpe: TypeTree) = SizedLabel(params.rootLabel(tpe), termSize)
-
- def xLabels = p.xs.map(x => rootLabel(x.getType))
+ def rootLabel = SizedLabel(params.rootLabel(tupleTypeWrap(p.xs.map(_.getType))), termSize)
var nAltsCache = Map[SizedLabel[T], Int]()
@@ -84,7 +78,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
def allProgramsCount(): Int = {
- xLabels.map(countAlternatives).product
+ countAlternatives(rootLabel)
}
/**
@@ -108,7 +102,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// C identifiers corresponding to p.xs
- private var rootCs: Seq[Identifier] = Seq()
+ private var rootC: Identifier = _
private var bs: Set[Identifier] = Set()
@@ -179,9 +173,9 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val cGen = new CGenerator()
- rootCs = for (l <- xLabels) yield {
- val c = cGen.getNext(l)
- defineCTreeFor(l, c)
+ rootC = {
+ val c = cGen.getNext(rootLabel)
+ defineCTreeFor(rootLabel, c)
c
}
@@ -244,7 +238,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
}
- allProgramsFor(rootCs)
+ allProgramsFor(Seq(rootC))
}
private def debugCTree(cTree: Map[Identifier, Seq[(Identifier, Seq[Expr] => Expr, Seq[Identifier])]],
@@ -299,11 +293,11 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
cToFd(c).fullBody = body
}
- // Top-level expression for rootCs
- val expr = tupleWrap(rootCs.map { c =>
- val fd = cToFd(c)
+ // Top-level expression for rootC
+ val expr = {
+ val fd = cToFd(rootC)
FunctionInvocation(fd.typed, fd.params.map(_.toVariable))
- })
+ }
(expr, cToFd.values.toSeq)
}
@@ -441,7 +435,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
}
- tupleWrap(rootCs.map(c => getCValue(c)))
+ getCValue(rootC)
}
/**
@@ -521,7 +515,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val bvs = if (isMinimal) {
bs
} else {
- rootCs.flatMap(filterBTree).toSet
+ filterBTree(rootC)
}
excludedPrograms += bvs
@@ -829,14 +823,13 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
if (nPassing <= validateUpTo) {
// All programs failed verification, we filter everything out and unfold
- //ndProgram.shrinkTo(Set(), unfolding == maxUnfoldings)
doFilter = false
skipCESearch = true
}
}
}
- if (doFilter && !(nPassing < nInitial * shrinkThreshold && useShrink)) {
+ if (doFilter) {
sctx.reporter.debug("Excluding "+wrongPrograms.size+" programs")
wrongPrograms.foreach {
ndProgram.excludeProgram(_, true)
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index ed68fbfac84543b1922b44cb91273043756b3cb1..2ae2b1d5d0292a6ed725055e61b1b4af4100a63c 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -30,20 +30,28 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
* into a list of fresh typed identifiers, the tuple of these new identifiers,
* and the mapping of those identifiers to their respective expressions.
*/
- def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr]) = id.getType match {
+ def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr], Expr => Seq[Expr]) = id.getType match {
case cct @ CaseClassType(ccd, _) if !ccd.isAbstract =>
val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
val map = (ccd.fields zip newIds).map{ case (vd, nid) => nid -> caseClassSelector(cct, Variable(id), vd.id) }.toMap
- (newIds.toList, CaseClass(cct, newIds.map(Variable)), map)
+ val tMap: (Expr => Seq[Expr]) = {
+ case CaseClass(ccd, fields) => fields
+ }
+
+ (newIds.toList, CaseClass(cct, newIds.map(Variable)), map, tMap)
case TupleType(ts) =>
val newIds = ts.zipWithIndex.map{ case (t, i) => FreshIdentifier(id.name+"_"+(i+1), t, true) }
val map = newIds.zipWithIndex.map{ case (nid, i) => nid -> TupleSelect(Variable(id), i+1) }.toMap
- (newIds.toList, tupleWrap(newIds.map(Variable)), map)
+ val tMap: (Expr => Seq[Expr]) = {
+ case Tuple(fields) => fields
+ }
+
+ (newIds.toList, tupleWrap(newIds.map(Variable)), map, tMap)
case _ => sys.error("woot")
}
@@ -55,9 +63,11 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
var reverseMap = Map[Identifier, Expr]()
+ var ebMapInfo = Map[Identifier, Expr => Seq[Expr]]()
+
val subAs = p.as.map { a =>
if (isDecomposable(a)) {
- val (newIds, expr, map) = decompose(a)
+ val (newIds, expr, map, tMap) = decompose(a)
subProblem = subst(a -> expr, subProblem)
subPc = subst(a -> expr, subPc)
@@ -65,12 +75,25 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
reverseMap ++= map
+ ebMapInfo += a -> tMap
+
newIds
} else {
List(a)
}
}
+ var eb = p.qeb.mapIns { info =>
+ List(info.flatMap { case (id, v) =>
+ ebMapInfo.get(id) match {
+ case Some(m) =>
+ m(v)
+ case None =>
+ List(v)
+ }
+ })
+ }
+
val newAs = subAs.flatten
// Recompose CaseClasses and Tuples.
@@ -101,7 +124,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
case other => other
}
- val sub = Problem(newAs, subWs, subPc, subProblem, p.xs)
+ val sub = Problem(newAs, subWs, subPc, subProblem, p.xs, eb)
val s = {substAll(reverseMap, _:Expr)} andThen { simplePostTransform(recompose) }
diff --git a/src/main/scala/leon/synthesis/rules/IndependentSplit.scala b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
new file mode 100644
index 0000000000000000000000000000000000000000..72be06b9cff76a63ced4506ef086a58622326bef
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/IndependentSplit.scala
@@ -0,0 +1,80 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.utils._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.Constructors._
+import purescala.Common._
+import purescala.Types.CaseClassType
+
+case object IndependentSplit extends NormalizingRule("IndependentSplit") {
+ def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ val TopLevelAnds(clauses) = and(p.pc, p.phi)
+
+ var independentClasses = Set[Set[Identifier]]()
+
+ // We group connect variables together
+ for(c <- clauses) {
+ val vs = variablesOf(c)
+
+ var newClasses = Set[Set[Identifier]]()
+
+ var thisClass = vs
+
+ for (cl <- independentClasses) {
+ if ((cl & vs).nonEmpty) {
+ thisClass ++= cl
+ } else {
+ newClasses += cl
+ }
+ }
+
+ independentClasses = newClasses + thisClass
+ }
+
+ val outClasses = independentClasses.map(cl => cl & p.xs.toSet).filter(_.nonEmpty)
+
+ if (outClasses.size > 1) {
+
+ val TopLevelAnds(phiClauses) = p.phi
+
+ val subs = (for (cl <- outClasses.toList) yield {
+ val xs = p.xs.filter(cl)
+
+ if (xs.nonEmpty) {
+ val phi = andJoin(phiClauses.filter(c => (variablesOf(c) & cl).nonEmpty))
+
+ val xsToRemove = p.xs.filterNot(cl).toSet
+
+ val eb = p.qeb.removeOuts(xsToRemove)
+
+ Some(p.copy(phi = phi, xs = xs, eb = eb))
+ } else {
+ None
+ }
+ }).flatten
+
+ val onSuccess: List[Solution] => Option[Solution] = { sols =>
+
+ val infos = subs.map(_.xs).zip(sols.map(_.term))
+
+ val term = infos.foldLeft(tupleWrap(p.xs.map(_.toVariable))) {
+ case (expr, (xs, term)) =>
+ letTuple(xs, term, expr)
+ }
+
+ Some(Solution(andJoin(sols.map(_.pre)), sols.map(_.defs).flatten.toSet, term, sols.forall(_.isTrusted)))
+ }
+
+
+ List(decomp(subs, onSuccess, "Independent Clusters"))
+ } else {
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/rules/InputSplit.scala b/src/main/scala/leon/synthesis/rules/InputSplit.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b9ffef53793528b628b41485c0a9156e171f188
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/InputSplit.scala
@@ -0,0 +1,49 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.purescala.Common.Identifier
+import purescala.Expressions._
+import purescala.Extractors._
+import purescala.ExprOps._
+import purescala.Constructors._
+import purescala.Types._
+
+import solvers._
+
+import scala.concurrent.duration._
+
+case object InputSplit extends Rule("In. Split") {
+ def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ p.as.filter(_.getType == BooleanType).flatMap { a =>
+ def getProblem(v: Boolean): Problem = {
+ def replaceA(e: Expr) = replaceFromIDs(Map(a -> BooleanLiteral(v)), e)
+
+ p.copy(
+ as = p.as.filterNot(_ == a),
+ ws = replaceA(p.ws),
+ pc = replaceA(p.pc),
+ phi = replaceA(p.phi),
+ eb = p.qeb.removeIns(Set(a))
+ )
+ }
+
+ val sub1 = getProblem(true)
+ val sub2 = getProblem(false)
+
+ val onSuccess: List[Solution] => Option[Solution] = {
+ case List(s1, s2) =>
+ Some(Solution(or(and(Equals(Variable(a), BooleanLiteral(true)), s1.pre),
+ and(Equals(Variable(a), BooleanLiteral(false)), s2.pre)),
+ s1.defs ++ s2.defs,
+ IfExpr(Variable(a), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
+ case _ =>
+ None
+ }
+
+ Some(decomp(List(sub1, sub2), onSuccess, s"Split on '$a'"))
+ }
+ }
+}
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index c18881e47f23fd9c5503320888158cc38f68b10d..a0b790243a6dc309953d07ba02d504e463185880 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -23,6 +23,7 @@ case object DebugSectionLeon extends DebugSection("leon", 1 << 1
case object DebugSectionXLang extends DebugSection("xlang", 1 << 12)
case object DebugSectionTypes extends DebugSection("types", 1 << 13)
case object DebugSectionIsabelle extends DebugSection("isabelle", 1 << 14)
+case object DebugSectionReport extends DebugSection("report", 1 << 15)
object DebugSections {
val all = Set[DebugSection](
@@ -40,6 +41,7 @@ object DebugSections {
DebugSectionLeon,
DebugSectionXLang,
DebugSectionTypes,
- DebugSectionIsabelle
+ DebugSectionIsabelle,
+ DebugSectionReport
)
}
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 418da12eb62e1fb1ead33bc0317da9ceb9662e28..a2ba463a6519a4c10e224c583263b805b4f660d7 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -42,34 +42,34 @@ object InjectAsserts extends SimpleLeonPhase[Program, Program] {
).setPos(e))
case e @ Division(_, d) =>
- Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
Some("Division by zero"),
e
).setPos(e))
case e @ Remainder(_, d) =>
- Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
Some("Remainder by zero"),
e
).setPos(e))
case e @ Modulo(_, d) =>
- Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+ Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
Some("Modulo by zero"),
e
).setPos(e))
case e @ BVDivision(_, d) =>
- Some(Assert(Not(Equals(d, IntLiteral(0))),
+ Some(assertion(not(equality(d, IntLiteral(0))),
Some("Division by zero"),
e
).setPos(e))
case e @ BVRemainder(_, d) =>
- Some(Assert(Not(Equals(d, IntLiteral(0))),
+ Some(assertion(not(equality(d, IntLiteral(0))),
Some("Remainder by zero"),
e
).setPos(e))
case e @ RealDivision(_, d) =>
- Some(Assert(Not(Equals(d, FractionalLiteral(0, 1))),
+ Some(assertion(not(equality(d, FractionalLiteral(0, 1))),
Some("Division by zero"),
e
).setPos(e))
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 600640c7b35229f3d1c02dbcd54765d7e665b0d0..b6c5f9036003725c2493f35cbdfa2a3a9960ec3d 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -131,68 +131,22 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
(resId.toVariable, scope, scrutFun ++ modifiedVars.zip(freshIds).toMap)
case wh@While(cond, body) =>
- //TODO: rewrite by re-using the nested function transformation code
- val (condRes, condScope, condFun) = toFunction(cond)
- val (_, bodyScope, bodyFun) = toFunction(body)
- val condBodyFun = condFun ++ bodyFun
-
- val modifiedVars: Seq[Identifier] = condBodyFun.keys.toSet.intersect(varsInScope).toSeq
-
- if(modifiedVars.isEmpty)
- (UnitLiteral(), (b: Expr) => b, Map())
- else {
- val whileFunVars = modifiedVars.map(id => FreshIdentifier(id.name, id.getType))
- val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
- val whileFunValDefs = whileFunVars.map(ValDef(_))
- val whileFunReturnType = tupleTypeWrap(whileFunVars.map(_.getType))
- val whileFunDef = new FunDef(parent.id.freshen, Nil, whileFunValDefs, whileFunReturnType).setPos(wh)
- whileFunDef.addFlag(IsLoop(parent))
-
- val whileFunCond = condScope(condRes)
- val whileFunRecursiveCall = replaceNames(condFun,
- bodyScope(FunctionInvocation(whileFunDef.typed, modifiedVars.map(id => condBodyFun(id).toVariable)).setPos(wh)))
- val whileFunBaseCase =
- tupleWrap(modifiedVars.map(id => condFun.getOrElse(id, modifiedVars2WhileFunVars(id)).toVariable))
- val whileFunBody = replaceNames(modifiedVars2WhileFunVars,
- condScope(IfExpr(whileFunCond, whileFunRecursiveCall, whileFunBaseCase)))
- whileFunDef.body = Some(whileFunBody)
-
- val resVar = Variable(FreshIdentifier("res", whileFunReturnType))
- val whileFunVars2ResultVars: Map[Expr, Expr] =
- whileFunVars.zipWithIndex.map{ case (v, i) =>
- (v.toVariable, tupleSelect(resVar, i+1, whileFunVars.size))
- }.toMap
- val modifiedVars2ResultVars: Map[Expr, Expr] = modifiedVars.map(id =>
- (id.toVariable, whileFunVars2ResultVars(modifiedVars2WhileFunVars(id).toVariable))).toMap
-
- //the mapping of the trivial post condition variables depends on whether the condition has had some side effect
- val trivialPostcondition: Option[Expr] = Some(Not(replace(
- modifiedVars.map(id => (condFun.getOrElse(id, id).toVariable, modifiedVars2ResultVars(id.toVariable))).toMap,
- whileFunCond)))
- val invariantPrecondition: Option[Expr] = wh.invariant.map(expr => replaceNames(modifiedVars2WhileFunVars, expr))
- val invariantPostcondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2ResultVars, expr))
- whileFunDef.precondition = invariantPrecondition
- whileFunDef.postcondition = trivialPostcondition.map( expr =>
- Lambda(
- Seq(ValDef(resVar.id)),
- and(expr, invariantPostcondition.getOrElse(BooleanLiteral(true))).setPos(wh)
- ).setPos(wh)
- )
-
- val finalVars = modifiedVars.map(_.freshen)
- val finalScope = (body: Expr) => {
- val tupleId = FreshIdentifier("t", whileFunReturnType)
- LetDef(Seq(whileFunDef), Let(
- tupleId,
- FunctionInvocation(whileFunDef.typed, modifiedVars.map(_.toVariable)).setPos(wh),
- finalVars.zipWithIndex.foldLeft(body) { (b, id) =>
- Let(id._1, tupleSelect(tupleId.toVariable, id._2 + 1, finalVars.size), b)
- }
- ))
- }
+ val whileFunDef = new FunDef(parent.id.freshen, Nil, Nil, UnitType).setPos(wh)
+ whileFunDef.addFlag(IsLoop(parent))
+ whileFunDef.body = Some(
+ IfExpr(cond,
+ Block(Seq(body), FunctionInvocation(whileFunDef.typed, Seq()).setPos(wh)),
+ UnitLiteral()))
+ whileFunDef.precondition = wh.invariant
+ whileFunDef.postcondition = Some(
+ Lambda(
+ Seq(ValDef(FreshIdentifier("bodyRes", UnitType))),
+ and(Not(getFunctionalResult(cond)), wh.invariant.getOrElse(BooleanLiteral(true))).setPos(wh)
+ ).setPos(wh)
+ )
- (UnitLiteral(), finalScope, modifiedVars.zip(finalVars).toMap)
- }
+ val newExpr = LetDef(List(whileFunDef), FunctionInvocation(whileFunDef.typed, Seq()).setPos(wh)).setPos(wh)
+ toFunction(newExpr)
case Block(Seq(), expr) =>
toFunction(expr)
@@ -281,6 +235,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val modifiedVars: List[Identifier] =
collect[Identifier]({
case Assignment(v, _) => Set(v)
+ case FunctionInvocation(tfd, _) => state.funDefsMapping.get(tfd.fd).map(p => p._2.toSet).getOrElse(Set())
case _ => Set()
})(bd).intersect(state.varsInScope).toList
(fd, modifiedVars)
@@ -318,7 +273,11 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
yield TupleType(fd.returnType :: modifiedVars.map(_.getType))
val newFds = for(((fd, newParams), newReturnType) <- newParams.zip(newReturnType))
- yield (fd, new FunDef(fd.id.freshen, fd.tparams, newParams, newReturnType).setPos(fd))
+ yield {
+ val newFd = new FunDef(fd.id.freshen, fd.tparams, newParams, newReturnType).setPos(fd)
+ newFd.addFlags(fd.flags)
+ (fd, newFd)
+ }
val mappingToAdd: Seq[(FunDef, (FunDef, List[Identifier]))] =
for(((fd, newFd), (_, freshVarDecls)) <- newFds.zip(freshVarDecls)) yield (fd -> ((newFd, freshVarDecls.toList)))
@@ -328,7 +287,9 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
wrappedBodyOpt.map(wrappedBody =>
toFunction(wrappedBody)(
State(state.parent, Set(),
- state.funDefsMapping ++ mappingToAdd)
+ state.funDefsMapping.map{
+ case (fd, (nfd, mvs)) =>
+ (fd, (nfd, mvs.map(v => rewritingMap.getOrElse(v, v))))} ++ mappingToAdd)
)
)
}
@@ -399,4 +360,13 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
def replaceNames(fun: Map[Identifier, Identifier], expr: Expr) = replaceFromIDs(fun mapValues Variable, expr)
+
+ /* Extract functional result value. Useful to remove side effect from conditions when moving it to post-condition */
+ private def getFunctionalResult(expr: Expr): Expr = {
+ preMap({
+ case Block(_, res) => Some(res)
+ case _ => None
+ })(expr)
+ }
+
}
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index a8927f360e817d10761723c8a4b7e9085bf0738d..aa00e12d446e1b11984f741500279a5647cfe426 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -10,14 +10,11 @@ object PropositionalLogic {
case class Or(lhs: Formula, rhs: Formula) extends Formula
case class Implies(lhs: Formula, rhs: Formula) extends Formula
case class Not(f: Formula) extends Formula
- case class Literal(id: Int) extends Formula
+ case class Literal(id: BigInt) extends Formula
def simplify(f: Formula): Formula = (f match {
- case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
- case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
- case Not(f) => Not(simplify(f))
- case Literal(_) => f
+ case _ => f
}) ensuring(isSimplified(_))
def isSimplified(f: Formula): Boolean = f match {
@@ -28,18 +25,6 @@ object PropositionalLogic {
case Literal(_) => true
}
- def nnf(formula: Formula): Formula = (formula match {
- case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
- case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
- case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
- case Not(Not(f)) => nnf(f)
- case Not(Literal(_)) => formula
- case Literal(_) => formula
- }) ensuring(isNNF(_))
-
def isNNF(f: Formula): Boolean = f match {
case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
@@ -49,39 +34,14 @@ object PropositionalLogic {
case Literal(_) => true
}
- def vars(f: Formula): Set[Int] = {
- require(isNNF(f))
- f match {
- case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Not(Literal(i)) => Set[Int](i)
- case Literal(i) => Set[Int](i)
- }
- }
-
- def fv(f : Formula) = { vars(nnf(f)) }
// @induct
// def wrongCommutative(f: Formula) : Boolean = {
// nnf(simplify(f)) == simplify(nnf(f))
// }.holds
- @induct
- def simplifyBreaksNNF(f: Formula) : Boolean = {
+ def simplifyBreaksNNF(f: Formula) : Boolean = {
require(isNNF(f))
isNNF(simplify(f))
}.holds
-
- @induct
- def nnfIsStable(f: Formula) : Boolean = {
- require(isNNF(f))
- nnf(f) == f
- }.holds
-
- @induct
- def simplifyIsStable(f: Formula) : Boolean = {
- require(isSimplified(f))
- simplify(f) == f
- }.holds
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Formulas.scala b/src/test/resources/regression/verification/purescala/valid/Formulas.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0fafe4158a2fcbd1b6654d21dbfa072ec42d614f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Formulas.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon._
+
+object Formulas {
+ abstract class Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class BoolLiteral(i: BigInt) extends Expr
+
+ def exists(e: Expr, f: Expr => Boolean): Boolean = {
+ f(e) || (e match {
+ case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Not(e) => exists(e, f)
+ case _ => false
+ })
+ }
+
+ def existsImplies(e: Expr): Boolean = {
+ e.isInstanceOf[Implies] || (e match {
+ case And(lhs, rhs) => existsImplies(lhs) || existsImplies(rhs)
+ case Or(lhs, rhs) => existsImplies(lhs) || existsImplies(rhs)
+ case Implies(lhs, rhs) => existsImplies(lhs) || existsImplies(rhs)
+ case Not(e) => existsImplies(e)
+ case _ => false
+ })
+ }
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def desugar(e: Expr): Expr = {
+ e match {
+ case And(lhs, rhs) => And(desugar(lhs), desugar(rhs))
+ case Or(lhs, rhs) => Or(desugar(lhs), desugar(rhs))
+ case Implies(lhs, rhs) =>
+ Or(Not(desugar(lhs)), desugar(rhs))
+ case Not(e) => Not(desugar(e))
+ case e => e
+ }
+ } ensuring { out =>
+ !existsImplies(out) &&
+ !exists(out, f => f.isInstanceOf[Implies])
+ }
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/WhileAsFun1.scala b/src/test/resources/regression/verification/xlang/valid/WhileAsFun1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b81ea38598aed9b208da96bc88cd9385260b2e5b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/WhileAsFun1.scala
@@ -0,0 +1,25 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.lang._
+
+object WhileAsFun1 {
+
+
+ def counterN(n: Int): Int = {
+ require(n > 0)
+
+ var i = 0
+ def rec(): Unit = {
+ require(i >= 0 && i <= n)
+ if(i < n) {
+ i += 1
+ rec()
+ } else {
+ ()
+ }
+ } ensuring(_ => i >= 0 && i <= n && i >= n)
+ rec()
+
+ i
+ } ensuring(_ == n)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/WhileAsFun2.scala b/src/test/resources/regression/verification/xlang/valid/WhileAsFun2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..968aadfdbf044fd057d3628a6adffd4e917fdf67
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/WhileAsFun2.scala
@@ -0,0 +1,33 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.lang._
+
+object WhileAsFun2 {
+
+
+ def counterN(n: Int): Int = {
+ require(n > 0)
+
+ var counter = 0
+
+ def inc(): Unit = {
+ counter += 1
+ }
+
+ var i = 0
+ def rec(): Unit = {
+ require(i >= 0 && counter == i && i <= n)
+ if(i < n) {
+ inc()
+ i += 1
+ rec()
+ } else {
+ ()
+ }
+ } ensuring(_ => i >= 0 && counter == i && i <= n && i >= n)
+ rec()
+
+
+ counter
+ } ensuring(_ == n)
+
+}
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
index f49670ddc31632343fea32f1b8d39ca288f214d4..6323496df930172e84b71bf5c55006eb33767c6a 100644
--- a/testcases/repair/Compiler/Compiler4.scala
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -150,7 +150,7 @@ object Desugar {
case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
- case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIMXE should be 0
+ case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIXME should be 0
case Trees.Eq(lhs, rhs) =>
Eq(desugar(lhs), desugar(rhs))
case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
diff --git a/testcases/repair/Compiler/Compiler6.scala b/testcases/repair/Compiler/Compiler6.scala
index 44bf523ec7aff63376ba24312594045296536dcf..dc633b1ae3d4d929e262ea44d6466a41ee4babf0 100644
--- a/testcases/repair/Compiler/Compiler6.scala
+++ b/testcases/repair/Compiler/Compiler6.scala
@@ -207,6 +207,8 @@ object Simplifier {
case e => e
}
} ensuring {
- res => eval(res) == eval(e)
+ res => eval(res) == eval(e) && ((e, res) passes {
+ case Plus(IntLiteral(BigInt(0)), IntLiteral(a)) => IntLiteral(a)
+ })
}
}
diff --git a/testcases/repair/Heap/Heap3.scala b/testcases/repair/Heap/Heap3.scala
index 3305b5d15a0731bd3aeaa1269c2404807f49a266..8e3013399534679c58221bd4d5547a14a76d9b57 100644
--- a/testcases/repair/Heap/Heap3.scala
+++ b/testcases/repair/Heap/Heap3.scala
@@ -51,7 +51,7 @@ object Heaps {
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
- private def merge(h1: Heap, h2: Heap) : Heap = {
+ def merge(h1: Heap, h2: Heap) : Heap = {
require(
hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
hasHeapProperty(h1) && hasHeapProperty(h2)
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
index 914f0caacd49b42448ec428df24af6ea155c53d2..1093efc3dc951ee8307c2257d8dcec2d154c9ecd 100644
--- a/testcases/repair/List/List13.scala
+++ b/testcases/repair/List/List13.scala
@@ -78,14 +78,22 @@ sealed abstract class List[T] {
}
}
- def drop(i: BigInt): List[T] = (this, i) match {
- case (Nil(), _) => Nil()
- case (Cons(h, t), i) =>
- if (i == 0) {
- Cons(h, t)
- } else {
- t.drop(i) // FIXME Should be -1
- }
+ def drop(i: BigInt): List[T] = {
+ require(i >= 0)
+ (this, i) match {
+ case (Nil(), _) => Nil[T]()
+ case (Cons(h, t), i) =>
+ if (i == 0) {
+ Cons[T](h, t)
+ } else {
+ t.drop(i) // FIXME Should be -1
+ }
+ }
+ } ensuring { (res: List[T]) =>
+ ((this, i), res) passes {
+ case (Cons(a, Cons(b, Nil())), BigInt(1)) => Cons(b, Nil())
+ case (Cons(a, Cons(b, Nil())), BigInt(2)) => Nil()
+ }
}
def slice(from: BigInt, to: BigInt): List[T] = {
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index b6cb5e276741be29d86da86b7c43cbe7e1639c62..1ee180b3331e9cc51df34207b8ab5b6fec9b710b 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -78,16 +78,18 @@ sealed abstract class List[T] {
}
}
- def drop(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil[T]()
- case (Cons(h, t), i) =>
- // FIXME
- //if (i == 0) {
- // Cons(h, t)
- //} else {
- t.drop(i-1)
- //}
- }} ensuring { ((this, i), _) passes {
+ def drop(i: BigInt): List[T] = {
+ (this, i) match {
+ case (Nil(), _) => Nil[T]()
+ case (Cons(h, t), i) =>
+ // FIXME
+ if (i != 0) {
+ Cons(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+ } ensuring { ((this, i), _) passes {
case (Cons(_, Nil()), BigInt(42)) => Nil()
case (l@Cons(_, _), BigInt(0)) => l
case (Cons(a, Cons(b, Nil())), BigInt(1)) => Cons(b, Nil())
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 743cced6533536eac8c03bbc3f2381378b8190b8..f13f91da3d55d7cdcf0eb0d3ef41027e1a8e94d8 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -97,11 +97,11 @@ sealed abstract class List[T] {
case Nil() => Nil[T]()
case Cons(h, t) =>
val r = t.replace(from, to)
- //if (h == from) { FIXME
- // Cons(to, r)
- //} else {
+ if (h != from) { // FIXME
+ Cons(to, r)
+ } else {
Cons(h, r)
- //}
+ }
}} ensuring { res =>
(((this.content -- Set(from)) ++ (if (this.content contains from) Set(to) else Set[T]())) == res.content) &&
res.size == this.size
diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala
index 7eef0585e9cb467f75da05fdb7957db4f9838afa..41972f4cefffa0bd63245856b2d31b0cfe241c10 100644
--- a/testcases/repair/List/List7.scala
+++ b/testcases/repair/List/List7.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
}
}} ensuring { res =>
if (this.content contains e) {
- res.isDefined && this.size > res.get && this.apply(res.get) == e
+ res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
} else {
res.isEmpty
}
diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala
index faf7571e9582f652e3ba494b11eb34c5923d4dac..02f5294c26e7f3b4f29e307db07186927bfff82c 100644
--- a/testcases/repair/List/List8.scala
+++ b/testcases/repair/List/List8.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
}
}} ensuring { res =>
if (this.content contains e) {
- res.isDefined && this.size > res.get && this.apply(res.get) == e
+ res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
} else {
res.isEmpty
}
diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala
index 12a8152b1701fe993f36c33392eebda724ec4aad..104e2ecabdfa0ac8bef8cc179ff68acc1a7c6ccc 100644
--- a/testcases/repair/List/List9.scala
+++ b/testcases/repair/List/List9.scala
@@ -191,7 +191,7 @@ sealed abstract class List[T] {
}
}} ensuring { res =>
if (this.content contains e) {
- res.isDefined && this.size > res.get && this.apply(res.get) == e
+ res.isDefined && this.size > res.get && this.apply(res.get) == e && res.get >= 0
} else {
res.isEmpty
}
diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala
index 88b0319086023675c766cf8f6c74ccd420d2a182..340dfbc46077306b64752e73cebeb725ef40a781 100644
--- a/testcases/repair/MergeSort/MergeSort1.scala
+++ b/testcases/repair/MergeSort/MergeSort1.scala
@@ -5,7 +5,7 @@ object MergeSort {
def split(l : List[BigInt]) : (List[BigInt],List[BigInt]) = { l match {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
- (rec1, rec2) // FIXME: Forgot a,b
+ (rec1, Cons(b, rec2)) // FIXME: Forgot a
case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
diff --git a/testcases/repair/runTests.sh b/testcases/repair/runTests.sh
index 55ca5cdf9f74828855e9ce85eb8aa18bf8ba3169..896054f51dc75131d690b14dfa00dd8a3a747c46 100755
--- a/testcases/repair/runTests.sh
+++ b/testcases/repair/runTests.sh
@@ -15,53 +15,56 @@ echo "################################" >> $summaryLog
echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $summaryLog
#All benchmarks:
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler7.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap5.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap6.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap7.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=insert testcases/repair/Heap/Heap8.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=makeN testcases/repair/Heap/Heap9.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap10.scala | tee -a $fullLog
+echo "=====================================================================" >> repair-report.txt
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=pad testcases/repair/List/List1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=++ testcases/repair/List/List2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=:+ testcases/repair/List/List3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --functions=drop testcases/repair/List/List4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --functions=replace testcases/repair/List/List5.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=count testcases/repair/List/List6.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List7.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List8.scala | tee -a $fullLog
-./leon --repair --timeout=30 --functions=find testcases/repair/List/List9.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=size testcases/repair/List/List10.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=sum testcases/repair/List/List11.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=- testcases/repair/List/List12.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=drop testcases/repair/List/List13.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=power testcases/repair/Numerical/Numerical1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=moddiv testcases/repair/Numerical/Numerical3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap6.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap7.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap10.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=insert testcases/repair/Heap/Heap8.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=makeN testcases/repair/Heap/Heap9.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=split testcases/repair/MergeSort/MergeSort1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort4.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala | tee -a $fullLog
+
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=pad testcases/repair/List/List1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=++ testcases/repair/List/List2.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=:+ testcases/repair/List/List3.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --functions=replace testcases/repair/List/List5.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=count testcases/repair/List/List6.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List7.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=find testcases/repair/List/List8.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --functions=find testcases/repair/List/List9.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=size testcases/repair/List/List10.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=sum testcases/repair/List/List11.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=- testcases/repair/List/List12.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --functions=drop testcases/repair/List/List4.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=drop testcases/repair/List/List13.scala | tee -a $fullLog
+
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=power testcases/repair/Numerical/Numerical1.scala | tee -a $fullLog
+#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=moddiv testcases/repair/Numerical/Numerical3.scala | tee -a $fullLog
+
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=split testcases/repair/MergeSort/MergeSort1.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort2.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort3.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort4.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/MergeSort/MergeSort5.scala | tee -a $fullLog
# Average results
-cat $log >> $summaryLog
-awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $summaryLog
+#cat $log >> $summaryLog
+#awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $summaryLog
diff --git a/testcases/synthesis/etienne-thesis/AddressBook/Make.scala b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1fd12466c2c6f932f776c893a66e1a290d2212ca
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/AddressBook/Make.scala
@@ -0,0 +1,53 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+ case class Address[A](info: A, priv: Boolean)
+
+ sealed abstract class AddressList[A] {
+ def size: BigInt = {
+ this match {
+ case Nil() => BigInt(0)
+ case Cons(head, tail) => BigInt(1) + tail.size
+ }
+ } ensuring { res => res >= 0 }
+
+ def content: Set[Address[A]] = this match {
+ case Nil() => Set[Address[A]]()
+ case Cons(addr, l1) => Set(addr) ++ l1.content
+ }
+ }
+
+ case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+ case class Nil[A]() extends AddressList[A]
+
+ def allPersonal[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) allPersonal(l1)
+ else false
+ }
+
+ def allBusiness[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+ def size: BigInt = business.size + personal.size
+
+ def content: Set[Address[A]] = business.content ++ personal.content
+
+ def invariant = {
+ allPersonal(personal) && allBusiness(business)
+ }
+ }
+
+ def makeAddressBook[A](as: AddressList[A]): AddressBook[A] = {
+ choose( (res: AddressBook[A]) => res.content == as.content && res.invariant )
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala b/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
new file mode 100644
index 0000000000000000000000000000000000000000..92a5b5bfef213e35c4f2a76bbbc9f295e406d1f4
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
@@ -0,0 +1,69 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+ case class Address[A](info: A, priv: Boolean)
+
+ sealed abstract class AddressList[A] {
+ def size: BigInt = {
+ this match {
+ case Nil() => BigInt(0)
+ case Cons(head, tail) => BigInt(1) + tail.size
+ }
+ } ensuring { res => res >= 0 }
+
+ def content: Set[Address[A]] = this match {
+ case Nil() => Set[Address[A]]()
+ case Cons(addr, l1) => Set(addr) ++ l1.content
+ }
+
+ def ++(that: AddressList[A]): AddressList[A] = {
+ this match {
+ case Cons(h, t) => Cons(h, t ++ that)
+ case Nil() => that
+ }
+ } ensuring {
+ res => res.content == this.content ++ that.content
+ }
+ }
+
+ case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+ case class Nil[A]() extends AddressList[A]
+
+ def allPersonal[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) allPersonal(l1)
+ else false
+ }
+
+ def allBusiness[A](l: AddressList[A]): Boolean = l match {
+ case Nil() => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+ def size: BigInt = business.size + personal.size
+
+ def content: Set[Address[A]] = business.content ++ personal.content
+
+ @inline
+ def invariant = {
+ allPersonal(personal) && allBusiness(business)
+ }
+ }
+
+ def merge[A](a1: AddressBook[A], a2: AddressBook[A]): AddressBook[A] = {
+ require(a1.invariant && a2.invariant)
+
+ choose( (res: AddressBook[A]) =>
+ res.personal.content == (a1.personal.content ++ a2.personal.content) &&
+ res.business.content == (a1.business.content ++ a2.business.content) &&
+ res.invariant
+ )
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c44fc062847b9af2264a9b3bba05186a313ab36b
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
@@ -0,0 +1,80 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+ sealed abstract class List[T] {
+ def content: Set[T] = {
+ this match {
+ case Cons(h, t) => Set(h) ++ t.content
+ case Nil() => Set()
+ }
+ }
+
+ def size: BigInt = {
+ this match {
+ case Cons(h, t) => BigInt(1) + t.size
+ case Nil() => BigInt(0)
+ }
+ } ensuring { _ >= 0 }
+
+ def reverse: List[T] = {
+ this match {
+ case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+ case Nil() => Nil[T]()
+ }
+ } ensuring { res =>
+ this.content == res.content
+ }
+
+ def append(r: List[T]): List[T] = {
+ this match {
+ case Cons(h, t) => Cons(h, t.append(r))
+ case Nil() => r
+ }
+ }
+
+ def isEmpty: Boolean = {
+ this == Nil[T]()
+ }
+
+ def tail: List[T] = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => t
+ }
+ }
+
+ def head: T = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => h
+ }
+ }
+ }
+
+ case class Cons[T](h: T, t: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ case class Queue[T](f: List[T], r: List[T]) {
+ def content: Set[T] = f.content ++ r.content
+ def size: BigInt = f.size + r.size
+
+ def isEmpty: Boolean = f.isEmpty && r.isEmpty
+
+ def invariant: Boolean = {
+ (f.isEmpty) ==> (r.isEmpty)
+ }
+
+ def toList: List[T] = f.append(r.reverse)
+
+ def dequeue: Queue[T] = {
+ require(invariant && !isEmpty)
+
+ choose { (res: Queue[T]) =>
+ res.size == size-1 && res.toList == this.toList.tail && res.invariant
+ }
+ }
+ }
+
+ val test = Queue[BigInt](Cons(42, Nil()), Nil()).dequeue
+}
diff --git a/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fe01946d158153d2dd9ae2a3be2234ee4cd18aa9
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
@@ -0,0 +1,88 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+ sealed abstract class List[T] {
+ def content: Set[T] = {
+ this match {
+ case Cons(h, t) => Set(h) ++ t.content
+ case Nil() => Set()
+ }
+ }
+
+ def size: BigInt = {
+ this match {
+ case Cons(h, t) => BigInt(1) + t.size
+ case Nil() => BigInt(0)
+ }
+ } ensuring { _ >= 0 }
+
+ def reverse: List[T] = {
+ this match {
+ case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+ case Nil() => Nil[T]()
+ }
+ } ensuring { res =>
+ this.content == res.content
+ }
+
+ def append(r: List[T]): List[T] = {
+ this match {
+ case Cons(h, t) => Cons(h, t.append(r))
+ case Nil() => r
+ }
+ }
+
+ def tail: List[T] = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => t
+ }
+ }
+
+ def head: T = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, t) => h
+ }
+ }
+
+ def last: T = {
+ require(this != Nil[T]())
+ this match {
+ case Cons(h, Nil()) => h
+ case Cons(h, t) => t.last
+ }
+ }
+ }
+
+ case class Cons[T](h: T, t: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ case class Queue[T](f: List[T], r: List[T]) {
+ def content: Set[T] = f.content ++ r.content
+ def size: BigInt = f.size + r.size
+
+ def invariant: Boolean = {
+ (f == Nil[T]()) ==> (r == Nil[T]())
+ }
+
+ def toList: List[T] = f.append(r.reverse)
+
+ def enqueue(v: T): Queue[T] = {
+ require(invariant)
+
+ f match {
+ case Cons(h, t) =>
+ Queue(f, Cons(v, r))
+ case Nil() =>
+ Queue(Cons(v, f), Nil())
+ }
+
+ } ensuring { (res: Queue[T]) =>
+ res.invariant &&
+ res.toList.last == v &&
+ res.content == this.content ++ Set(v)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/Desugar.scala b/testcases/synthesis/etienne-thesis/Compiler/Desugar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2684c71b2b8bbc9e5fe6cc307899ca7b92d366b4
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/Desugar.scala
@@ -0,0 +1,118 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+ def rewriteMinus(in: Minus): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+ }
+ }
+
+ def rewriteImplies(in: Implies): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+ }
+ }
+
+
+ def plop(x: Expr) = {
+ eval(x) == Error//eval(Not(IntLiteral(BigInt(2))))
+ }.holds
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/DesugarImplies.scala b/testcases/synthesis/etienne-thesis/Compiler/DesugarImplies.scala
new file mode 100644
index 0000000000000000000000000000000000000000..de5c544ff368043ca7847376af8cd9ae6b513f4d
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/DesugarImplies.scala
@@ -0,0 +1,144 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ def exists(e: Expr, f: Expr => Boolean): Boolean = {
+ f(e) || (e match {
+ case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+ case Not(e) => exists(e, f)
+ case UMinus(e) => exists(e, f)
+ case _ => false
+ })
+ }
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+
+ //def desugar(e: Expr): Expr = {
+ // choose{ (out: Expr) =>
+ // eval(e) == eval(out) && !exists(out, f => f.isInstanceOf[Implies])
+ // }
+ //}
+
+ def desugar(e: Expr): Expr = {
+ e match {
+ case Plus(lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Minus(lhs, rhs) => Minus(desugar(lhs), desugar(rhs))
+ case LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case And(lhs, rhs) => And(desugar(lhs), desugar(rhs))
+ case Or(lhs, rhs) => Or(desugar(lhs), desugar(rhs))
+ case Implies(lhs, rhs) => //Implies(desugar(lhs), desugar(rhs))
+ Or(Not(desugar(lhs)), desugar(rhs))
+ case Eq(lhs, rhs) => Eq(desugar(lhs), desugar(rhs))
+ case Ite(c, t, e) => Ite(desugar(c), desugar(t), desugar(e))
+ case Not(e) => Not(desugar(e))
+ case UMinus(e) => UMinus(desugar(e))
+ case e => e
+ }
+ } ensuring { out =>
+ //eval(e) == eval(out) &&
+ !exists(out, f => f.isInstanceOf[Implies])
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/RewriteImplies.scala b/testcases/synthesis/etienne-thesis/Compiler/RewriteImplies.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b50b9cbe34043f65d1a8feeaadac929822e6c70
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/RewriteImplies.scala
@@ -0,0 +1,124 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ def exists(e: Expr, f: Expr => Boolean): Boolean = {
+ f(e) || (e match {
+ case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+ case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+ case Not(e) => exists(e, f)
+ case UMinus(e) => exists(e, f)
+ case _ => false
+ })
+ }
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+
+ def desugar(in: Expr): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/Compiler/RewriteMinus.scala b/testcases/synthesis/etienne-thesis/Compiler/RewriteMinus.scala
new file mode 100644
index 0000000000000000000000000000000000000000..de2fa4360de5fa899110b43c171e592be5282803
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/Compiler/RewriteMinus.scala
@@ -0,0 +1,107 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(e: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Implies(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 BoolLiteral(b : Boolean) extends Expr
+ case class IntLiteral(i: BigInt) extends Expr
+
+ abstract class Value
+ case class BoolValue(b: Boolean) extends Value
+ case class IntValue(i: BigInt) extends Value
+ case object Error extends Value
+
+ def eval(e: Expr): Value = e match {
+ case Plus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+ case _ => Error
+ }
+
+ case Minus(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+ case _ => Error
+ }
+
+ case UMinus(l) =>
+ eval(l) match {
+ case IntValue(b) => IntValue(-b)
+ case _ => Error
+ }
+
+ case LessThan(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+ case _ => Error
+ }
+
+ case And(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(false) => b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Or(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ b
+ case b: BoolValue =>
+ eval(r)
+ case _ =>
+ Error
+ }
+
+ case Implies(l, r) =>
+ eval(l) match {
+ case b @ BoolValue(true) =>
+ eval(r)
+ case b @ BoolValue(false) =>
+ BoolValue(true)
+ case _ => Error
+ }
+
+ case Not(l) =>
+ eval(l) match {
+ case BoolValue(b) => BoolValue(!b)
+ case _ => Error
+ }
+
+ case Eq(l, r) =>
+ (eval(l), eval(r)) match {
+ case (IntValue(il), IntValue(ir)) => BoolValue(il == ir)
+ case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+ case _ => Error
+ }
+
+ case Ite(c, t, e) =>
+ eval(c) match {
+ case BoolValue(true) => eval(t)
+ case BoolValue(false) => eval(t)
+ case _ => Error
+ }
+
+ case IntLiteral(l) => IntValue(l)
+ case BoolLiteral(b) => BoolValue(b)
+ }
+
+ def rewriteMinus(in: Minus): Expr = {
+ choose{ (out: Expr) =>
+ eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Delete.scala b/testcases/synthesis/etienne-thesis/List/Delete.scala
index 46f0710878d25a30e679f034ff07f985078950d1..30716c5919256f052d0a0e741a147d30c5bc82fa 100644
--- a/testcases/synthesis/etienne-thesis/List/Delete.scala
+++ b/testcases/synthesis/etienne-thesis/List/Delete.scala
@@ -7,7 +7,7 @@ object Delete {
case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : BigInt = (l match {
+ def size(l: List): BigInt = (l match {
case Nil => BigInt(0)
case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
@@ -17,25 +17,10 @@ object Delete {
case Cons(i, t) => Set(i) ++ content(t)
}
- def insert(in1: List, v: BigInt): List = {
- Cons(v, in1)
- } ensuring { content(_) == content(in1) ++ Set(v) }
-
- //def delete(in1: List, v: BigInt): List = {
- // in1 match {
- // case Cons(h,t) =>
- // if (h == v) {
- // delete(t, v)
- // } else {
- // Cons(h, delete(t, v))
- // }
- // case Nil =>
- // Nil
- // }
- //} ensuring { content(_) == content(in1) -- Set(v) }
-
- def delete(in1: List, v: BigInt) = choose {
+ def delete(in: List, v: BigInt) = {
+ ???[List]
+ } ensuring {
(out : List) =>
- content(out) == content(in1) -- Set(v)
+ content(out) == content(in) -- Set(v)
}
}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Delete.scala b/testcases/synthesis/etienne-thesis/SortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..788f232d35449cff75ac27442ce7e9cb50f42391
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDelete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in: List, v: BigInt) = {
+ require(isSorted(in))
+
+ choose( (res : List) =>
+ (content(res) == content(in) -- Set(v)) && isSorted(res)
+ )
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Diff.scala b/testcases/synthesis/etienne-thesis/SortedList/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d391b85ba60e2b405530ddb45b40d94071263725
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Diff.scala
@@ -0,0 +1,53 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDiff {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Insert.scala b/testcases/synthesis/etienne-thesis/SortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0bf80d1e99cef290e602b0da905d6966713c77b7
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsert {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala b/testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
new file mode 100644
index 0000000000000000000000000000000000000000..73e0b240d776780fab6ac8091a8f0c925c56e695
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertAlways {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insertAlways(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+
+ choose{ (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala b/testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0752ad33fe2249de829d7180e6facaab8fb6e160
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
@@ -0,0 +1,49 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertionSort {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+ def insertionSort(in1: List): List = {
+ choose { (out: List) =>
+ content(out) == content(in1) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/SortedList/Union.scala b/testcases/synthesis/etienne-thesis/SortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d3f11adcccc07e44d1b82c1c6aed7144cb30523c
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/SortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..23999d96c3577b80b00b252e0c07509f4b4b2176
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListDelete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in: List, v: BigInt) = {
+ require(isSorted(in))
+
+ choose( (res : List) =>
+ (content(res) == content(in) -- Set(v)) && isSorted(res)
+ )
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..65f3c01f9d7b7d8d45136196a6289088df46fa22
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListInsert {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala b/testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c10ed419d3c2cc4fefc9690efb37bc723799ef1c
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListUnion {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list: List): Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a34d1834fbb5cc2418ca830c5576e64d74169b4f
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsAdd {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4287378d1f95225e4ff1ffae57b2d0579d72c3a5
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsDistinct {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ x match {
+ case S(p) => S(add(p, y))
+ case Z => y
+ }
+ } ensuring { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+
+ def distinct(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ r != x && r != y
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala b/testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bfa39365e8a8b35555ddc2265f40c775251b8d17
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsMult {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ x match {
+ case S(p) => S(add(p, y))
+ case Z => y
+ }
+ } ensuring { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+
+ def mult(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) * value(y)
+ }
+ }
+}
diff --git a/testcases/synthesis/etienne-thesis/run.sh b/testcases/synthesis/etienne-thesis/run.sh
new file mode 100755
index 0000000000000000000000000000000000000000..ee64d86702076bf5ff909c3437f321498a2afe68
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/run.sh
@@ -0,0 +1,43 @@
+#!/bin/bash
+
+function run {
+ cmd="./leon --debug=report --timeout=30 --synthesis $1"
+ echo "Running " $cmd
+ echo "------------------------------------------------------------------------------------------------------------------"
+ $cmd;
+}
+
+echo "==================================================================================================================" >> synthesis-report.txt
+# These are all the benchmarks included in my thesis
+# List
+run testcases/synthesis/etienne-thesis/List/Insert.scala
+run testcases/synthesis/etienne-thesis/List/Delete.scala
+run testcases/synthesis/etienne-thesis/List/Union.scala
+run testcases/synthesis/etienne-thesis/List/Diff.scala
+run testcases/synthesis/etienne-thesis/List/Split.scala
+
+# SortedList
+run testcases/synthesis/etienne-thesis/SortedList/Insert.scala
+run testcases/synthesis/etienne-thesis/SortedList/InsertAlways.scala
+run testcases/synthesis/etienne-thesis/SortedList/Delete.scala
+run testcases/synthesis/etienne-thesis/SortedList/Union.scala
+run testcases/synthesis/etienne-thesis/SortedList/Diff.scala
+run testcases/synthesis/etienne-thesis/SortedList/InsertionSort.scala
+
+# StrictSortedList
+run testcases/synthesis/etienne-thesis/StrictSortedList/Insert.scala
+run testcases/synthesis/etienne-thesis/StrictSortedList/Delete.scala
+run testcases/synthesis/etienne-thesis/StrictSortedList/Union.scala
+
+# UnaryNumerals
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Add.scala
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Distinct.scala
+run testcases/synthesis/etienne-thesis/UnaryNumerals/Mult.scala
+
+# BatchedQueue
+#run testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
+run testcases/synthesis/etienne-thesis/BatchedQueue/Dequeue.scala
+
+# AddressBook
+#run testcases/synthesis/etienne-thesis/AddressBook/Make.scala
+run testcases/synthesis/etienne-thesis/AddressBook/Merge.scala
diff --git a/testcases/verification/xlang/BankTransfer.scala b/testcases/verification/xlang/BankTransfer.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c533b4e08a6297446aad36d7a31fd04e148ccc37
--- /dev/null
+++ b/testcases/verification/xlang/BankTransfer.scala
@@ -0,0 +1,73 @@
+import leon.lang._
+
+object BankTransfer {
+
+ def okTransaction(): Unit = {
+ var balance: BigInt = 0
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ balance += x
+ } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= balance)
+ balance -= x
+ } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+ deposit(35)
+ withdrawal(30)
+ }
+
+ def invalidTransaction(): Unit = {
+ var balance: BigInt = 0
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ balance += x
+ } ensuring(_ => balance == old(balance) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= balance)
+ balance -= x
+ } ensuring(_ => balance == old(balance) - x && balanceInvariant)
+
+ deposit(35)
+ withdrawal(40)
+ }
+
+
+ def internalTransfer(): Unit = {
+ var checking: BigInt = 0
+ var saving: BigInt = 0
+
+ def balance = checking + saving
+
+ def balanceInvariant: Boolean = balance >= 0
+
+ def deposit(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0)
+ checking += x
+ } ensuring(_ => checking == old(checking) + x && balanceInvariant)
+
+ def withdrawal(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && x <= checking)
+ checking -= x
+ } ensuring(_ => checking == old(checking) - x && balanceInvariant)
+
+ def checkingToSaving(x: BigInt): Unit = {
+ require(balanceInvariant && x >= 0 && checking >= x)
+ checking -= x
+ saving += x
+ } ensuring(_ => checking + saving == old(checking) + old(saving) && balanceInvariant)
+
+ deposit(50)
+ withdrawal(30)
+ checkingToSaving(10)
+ }
+
+}