diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index babf6d728b383740202d0802c449d1549509265d..ad3dc998a2d023022250c0e6de4b8b4db00cbcbe 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -374,6 +374,11 @@ trait CodeExtraction extends Extractors {
varSubsts(b.symbol) = (() => Variable(newID))
WildcardPattern(Some(newID))
}
+ case b @ Bind(name, Typed(Ident(nme.WILDCARD), tpe)) => {
+ val newID = FreshIdentifier(name.toString).setType(scalaType2PureScala(unit,silent)(tpe.tpe))
+ varSubsts(b.symbol) = (() => Variable(newID))
+ WildcardPattern(Some(newID))
+ }
case a @ Apply(fn, args) if fn.isType && a.tpe.typeSymbol.isCase && classesToClasses.keySet.contains(a.tpe.typeSymbol) => {
val cd = classesToClasses(a.tpe.typeSymbol).asInstanceOf[CaseClassDef]
assert(args.size == cd.fields.size)
@@ -660,7 +665,7 @@ trait CodeExtraction extends Extractors {
case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
case ExUnitLiteral() => UnitLiteral
-
+ case ExLocally(body) => rec(body)
case ExTyped(e,tpt) => rec(e)
case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
case Some(fun) => fun()
@@ -1016,6 +1021,7 @@ trait CodeExtraction extends Extractors {
val fd = defsToDefs(sy)
FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
}
+
case pm @ ExPatternMatching(sel, cses) => {
val rs = rec(sel)
val rc = cses.map(rewriteCaseDef(_))
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index e301ab021fd893bdff68900c448c6415805496c0..b6b15a1628037bc385145f2699d5a0b3483cba40 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -304,6 +304,16 @@ trait Extractors {
}
}
+ object ExLocally {
+ def unapply(tree: Apply) : Option[Tree] = tree match {
+ case Apply(TypeApply(ExSelected("scala", "Predef", "locally"), _), List(body)) =>
+ Some(body)
+
+ case _ =>
+ None
+ }
+ }
+
object ExTupleExtract {
def unapply(tree: Select) : Option[(Tree,Int)] = tree match {
case Select(lhs, n) => {
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index fde8be1a91953db0af6efedcf58fcc50b189b055..16b8959f3930b30fc040ff1263588c3ad38cf9a1 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -57,6 +57,9 @@ object Common {
object FreshIdentifier {
def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = new Identifier(name, UniqueCounter.nextGlobal, UniqueCounter.next(name), alwaysShowUniqueID)
+
+ def apply(name: String, forceId: Int): Identifier = new Identifier(name, UniqueCounter.nextGlobal, forceId, true)
+
}
trait ScalacPositional {
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index f957848c9b9a16d0a91881524702c71cc4ec9898..d9a82aa8c9cfdad9636d827f9f3ad342fa14a61d 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -15,6 +15,12 @@ object ScalaPrinter {
retSB.toString
}
+ def apply(tree: Expr, lvl: Int): String = {
+ val retSB = new StringBuffer
+ pp(tree, retSB, lvl)
+ retSB.toString
+ }
+
def apply(tpe: TypeTree): String = {
val retSB = new StringBuffer
pp(tpe, retSB, 0)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2a0acb3f2c51362d6cee172beb6d624104ea8abc..b0516a56f56a777bf6ee78affa519751f701e51c 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -463,9 +463,9 @@ object TreeOps {
def simplifyLets(expr: Expr) : Expr = {
def simplerLet(t: Expr) : Option[Expr] = t match {
- case letExpr @ Let(i, t: Terminal, b) => Some(replace(Map((Variable(i) -> t)), b))
+ case letExpr @ Let(i, t: Terminal, b) if !containsChoose(b) => Some(replace(Map((Variable(i) -> t)), b))
- case letExpr @ Let(i,e,b) => {
+ case letExpr @ Let(i,e,b) if !containsChoose(b) => {
val occurences = treeCatamorphism[Int]((e:Expr) => e match {
case Variable(x) if x == i => 1
case _ => 0
@@ -479,7 +479,7 @@ object TreeOps {
}
}
- case letTuple @ LetTuple(ids, Tuple(exprs), body) =>
+ case letTuple @ LetTuple(ids, Tuple(exprs), body) if !containsChoose(body) =>
var newBody = body
@@ -513,7 +513,7 @@ object TreeOps {
Some(LetTuple(remIds, Tuple(remExprs), newBody))
}
- case l @ LetTuple(ids, tExpr, body) =>
+ case l @ LetTuple(ids, tExpr, body) if !containsChoose(body) =>
val TupleType(types) = tExpr.getType
val arity = ids.size
// A map containing vectors of the form (0, ..., 1, ..., 0) where the one corresponds to the index of the identifier in the
@@ -541,7 +541,7 @@ object TreeOps {
None
}
- case _ => None
+ case _ => None
}
searchAndReplaceDFS(simplerLet)(expr)
}
@@ -1171,8 +1171,117 @@ object TreeOps {
simplePreTransform(pre)(expr)
}
- // This function could be made ridiculously faster by using push/pop...
- def simplifyPaths(solver : Solver)(expr : Expr) : Expr = {
+ def simplifyPaths(solver : Solver): Expr => Expr = {
+ new SimplifierWithPaths(solver).transform _
+ }
+
+ trait Transformer {
+ def transform(e: Expr): Expr
+ }
+
+ trait Traverser[T] {
+ def traverse(e: Expr): T
+ }
+
+ abstract class TransformerWithPC extends Transformer {
+ type C
+
+ protected val initC: C
+
+ protected def register(cond: Expr, path: C): C
+
+ protected def rec(e: Expr, path: C): Expr = e match {
+ case Let(i, e @ FunctionInvocation(fd, callArgs), b) if fd.hasPostcondition =>
+ val argsMap = fd.args.map(vd => Variable(vd.id)) zip callArgs
+
+ val newPost = TreeOps.replace(Map(ResultVariable() -> Variable(i)) ++ argsMap, fd.postcondition.get)
+
+ val pred = newPost
+
+ val se = rec(e, path)
+ val sb = rec(b, register(pred, path))
+ Let(i, se, sb)
+
+ case Let(i, e, b) =>
+ val se = rec(e, path)
+ val sb = rec(b, register(Equals(Variable(i), se), path))
+ Let(i, se, sb)
+
+ case MatchExpr(scrut, cases) =>
+ val rs = rec(scrut, path)
+
+ var soFar = path
+
+ MatchExpr(rs, cases.map { c =>
+ val patternExpr = conditionForPattern(rs, c.pattern)
+
+ val subPath = register(patternExpr, soFar)
+ soFar = register(Not(patternExpr), soFar)
+
+ c match {
+ case SimpleCase(p, rhs) =>
+ SimpleCase(p, rec(rhs, subPath))
+ case GuardedCase(p, g, rhs) =>
+ GuardedCase(p, g, rec(rhs, subPath))
+ }
+ })
+
+ case LetTuple(is, e, b) =>
+ val se = rec(e, path)
+ val sb = rec(b, register(Equals(Tuple(is.map(Variable(_))), se), path))
+ LetTuple(is, se, sb)
+
+ case IfExpr(cond, then, elze) =>
+ val rc = rec(cond, path)
+
+ IfExpr(rc, rec(then, register(rc, path)), rec(elze, register(Not(rc), path)))
+
+ case And(es) => {
+ var soFar = path
+ And(for(e <- es) yield {
+ val se = rec(e, soFar)
+ soFar = register(se, soFar)
+ se
+ })
+ }
+
+ case Or(es) => {
+ var soFar = path
+ Or(for(e <- es) yield {
+ val se = rec(e, soFar)
+ soFar = register(Not(se), soFar)
+ se
+ })
+ }
+
+
+ case UnaryOperator(e, builder) =>
+ builder(rec(e, path))
+
+ case BinaryOperator(e1, e2, builder) =>
+ builder(rec(e1, path), rec(e2, path))
+
+ case NAryOperator(es, builder) =>
+ builder(es.map(rec(_, path)))
+
+ case t : Terminal => t
+
+ case _ =>
+ sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
+ }
+
+ def transform(e: Expr): Expr = {
+ rec(e, initC)
+ }
+ }
+
+ class SimplifierWithPaths(solver: Solver) extends TransformerWithPC {
+ type C = List[Expr]
+
+ val initC = Nil
+
+ protected def register(e: Expr, c: C) = e :: c
+
def impliedBy(e : Expr, path : Seq[Expr]) : Boolean = try {
solver.solve(Implies(And(path), e)) match {
case Some(true) => true
@@ -1191,11 +1300,30 @@ object TreeOps {
case _ : Exception => false
}
- def rec(e : Expr, path : Seq[Expr]): Expr = e match {
- case Let(i, e, b) =>
- // The path condition for the body of the Let is the same as outside, plus an equality to constrain the newly bound variable.
- val se = rec(e, path)
- Let(i, se, rec(b, Equals(Variable(i), se) +: path))
+ protected override def rec(e: Expr, path: C) = e match {
+ case IfExpr(cond, then, elze) =>
+ super.rec(e, path) match {
+ case IfExpr(BooleanLiteral(true) , t, _) => t
+ case IfExpr(BooleanLiteral(false), _, e) => e
+ case ite => ite
+ }
+
+ case And(es) => {
+ var soFar = path
+ var continue = true
+ var r = And(for(e <- es if continue) yield {
+ val se = rec(e, soFar)
+ if(se == BooleanLiteral(false)) continue = false
+ soFar = register(se, soFar)
+ se
+ })
+
+ if (continue) {
+ r
+ } else {
+ BooleanLiteral(false)
+ }
+ }
case MatchExpr(scrut, cases) =>
val rs = rec(scrut, path)
@@ -1206,7 +1334,7 @@ object TreeOps {
// unsupported for now
e
} else {
- MatchExpr(rs, cases.flatMap { c =>
+ MatchExpr(rs, cases.flatMap { c =>
val patternExpr = conditionForPattern(rs, c.pattern)
if (stillPossible && !contradictedBy(patternExpr, path)) {
@@ -1227,41 +1355,21 @@ object TreeOps {
})
}
- case LetTuple(is, e, b) =>
- // Similar to the Let case
- val se = rec(e, path)
- LetTuple(is, se, rec(b, Equals(Tuple(is.map(Variable(_))), se) +: path))
-
- case IfExpr(cond, then, elze) =>
- val rc = rec(cond, path)
- rc match {
- case BooleanLiteral(true) => rec(then, path)
- case BooleanLiteral(false) => rec(elze, path)
- case _ => IfExpr(rc, rec(then, rc +: path), rec(elze, Not(rc) +: path))
- }
-
- case And(es) => {
- var extPath = path
- var continue = true
- var r = And(for(e <- es if continue) yield {
- val se = rec(e, extPath)
- if(se == BooleanLiteral(false)) continue = false
- extPath = se +: extPath
- se
- })
- if (continue) r else BooleanLiteral(false)
- }
-
case Or(es) => {
- var extPath = path
+ var soFar = path
var continue = true
- val r = Or(for(e <- es if continue) yield {
- val se = rec(e, extPath)
+ var r = Or(for(e <- es if continue) yield {
+ val se = rec(e, soFar)
if(se == BooleanLiteral(true)) continue = false
- extPath = Not(se) +: extPath
+ soFar = register(Not(se), soFar)
se
})
- if (continue) r else BooleanLiteral(true)
+
+ if (continue) {
+ r
+ } else {
+ BooleanLiteral(true)
+ }
}
case b if b.getType == BooleanType && impliedBy(b, path) =>
@@ -1270,14 +1378,135 @@ object TreeOps {
case b if b.getType == BooleanType && contradictedBy(b, path) =>
BooleanLiteral(false)
+ case _ =>
+ super.rec(e, path)
+ }
+ }
+
+ class ChooseCollectorWithPaths extends TransformerWithPC with Traverser[Seq[(Choose, Expr)]] {
+ type C = Seq[Expr]
+ val initC = Nil
+ def register(e: Expr, path: C) = path :+ e
+
+ var results: Seq[(Choose, Expr)] = Nil
+
+ override def rec(e: Expr, path: C) = e match {
+ case c : Choose =>
+ results = results :+ (c, And(path))
+ c
+ case _ =>
+ super.rec(e, path)
+ }
+
+ def traverse(e: Expr) = {
+ results = Nil
+ rec(e, initC)
+ results
+ }
+ }
+
+ class ScopeSimplifier extends Transformer {
+
+ case class Scope(inScope: Set[Identifier] = Set(), oldToNew: Map[Identifier, Identifier] = Map(), funDefs: Map[FunDef, FunDef] = Map()) {
+
+ def register(oldNew: (Identifier, Identifier)): Scope = {
+ val (oldId, newId) = oldNew
+ copy(inScope = inScope + newId, oldToNew = oldToNew + oldNew)
+ }
+
+ def registerFunDef(oldNew: (FunDef, FunDef)): Scope = {
+ copy(funDefs = funDefs + oldNew)
+ }
+ }
+
+ protected def genId(id: Identifier, scope: Scope): Identifier = {
+ val existCount = scope.inScope.count(_.name == id.name)
+
+ FreshIdentifier(id.name, existCount).setType(id.getType)
+ }
+
+ protected def rec(e: Expr, scope: Scope): Expr = e match {
+ case Let(i, e, b) =>
+ val si = genId(i, scope)
+ val se = rec(e, scope)
+ val sb = rec(b, scope.register(i -> si))
+ Let(si, se, sb)
+
+ case LetTuple(is, e, b) =>
+ var newScope = scope
+ val sis = for (i <- is) yield {
+ val si = genId(i, newScope)
+ newScope = newScope.register(i -> si)
+ si
+ }
+
+ val se = rec(e, scope)
+ val sb = rec(b, newScope)
+ LetTuple(sis, se, sb)
+
+ case MatchExpr(scrut, cases) =>
+ val rs = rec(scrut, scope)
+
+ def trPattern(p: Pattern, scope: Scope): (Pattern, Scope) = {
+ val (newBinder, newScope) = p.binder match {
+ case Some(id) =>
+ val newId = genId(id, scope)
+ val newScope = scope.register(id -> newId)
+ (Some(newId), newScope)
+ case None =>
+ (None, scope)
+ }
+
+ var curScope = newScope
+ var newSubPatterns = for (sp <- p.subPatterns) yield {
+ val (subPattern, subScope) = trPattern(sp, curScope)
+ curScope = subScope
+ subPattern
+ }
+
+ val newPattern = p match {
+ case InstanceOfPattern(b, ctd) =>
+ InstanceOfPattern(newBinder, ctd)
+ case WildcardPattern(b) =>
+ WildcardPattern(newBinder)
+ case CaseClassPattern(b, ccd, sub) =>
+ CaseClassPattern(newBinder, ccd, newSubPatterns)
+ case TuplePattern(b, sub) =>
+ TuplePattern(newBinder, newSubPatterns)
+ }
+
+
+ (newPattern, curScope)
+ }
+
+ MatchExpr(rs, cases.map { c =>
+ val (newP, newScope) = trPattern(c.pattern, scope)
+
+ c match {
+ case SimpleCase(p, rhs) =>
+ SimpleCase(newP, rec(rhs, newScope))
+ case GuardedCase(p, g, rhs) =>
+ GuardedCase(newP, rec(g, newScope), rec(rhs, newScope))
+ }
+ })
+
+ case Variable(id) =>
+ Variable(scope.oldToNew.getOrElse(id, id))
+
+ case FunctionInvocation(fd, args) =>
+ val newFd = scope.funDefs.getOrElse(fd, fd)
+ val newArgs = args.map(rec(_, scope))
+
+ FunctionInvocation(newFd, newArgs)
+
case UnaryOperator(e, builder) =>
- builder(rec(e, path))
+ builder(rec(e, scope))
case BinaryOperator(e1, e2, builder) =>
- builder(rec(e1, path), rec(e2, path))
+ builder(rec(e1, scope), rec(e2, scope))
case NAryOperator(es, builder) =>
- builder(es.map(rec(_, path)))
+ builder(es.map(rec(_, scope)))
case t : Terminal => t
@@ -1285,7 +1514,9 @@ object TreeOps {
sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
}
- rec(expr, Nil)
+ def transform(e: Expr): Expr = {
+ rec(e, Scope())
+ }
}
// Eliminates tuples of arity 0 and 1. This function also affects types!
@@ -1415,7 +1646,15 @@ object TreeOps {
}
def collectChooses(e: Expr): List[Choose] = {
- collect({ case c: Choose => c })(e)
+ new ChooseCollectorWithPaths().traverse(e).map(_._1).toList
+ }
+
+ def containsChoose(e: Expr): Boolean = {
+ simplePreTransform{
+ case Choose(_, _) => return true
+ case e => e
+ }(e)
+ false
}
def valuateWithModel(model: Map[Identifier, Expr])(id: Identifier): Expr = {
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index f522f4f0dd1ebe88d9918d2ef338bb76b81498e2..f1bd339c5170ecbfc2443c74c0363f49313eccaa 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -23,8 +23,15 @@ object Trees {
* the expected type. */
case class Error(description: String) extends Expr with Terminal with ScalacPositional
- case class Choose(vars: List[Identifier], pred: Expr) extends Expr with ScalacPositional with UnaryExtractable {
- def extract = Some((pred, (e: Expr) => Choose(vars, e).setPosInfo(this).setType(TupleType(vars.map(_.getType)))))
+ case class Choose(vars: List[Identifier], pred: Expr) extends Expr with ScalacPositional with UnaryExtractable with FixedType {
+
+ assert(!vars.isEmpty)
+
+ val fixedType = if (vars.size > 1) TupleType(vars.map(_.getType)) else vars.head.getType
+
+ def extract = {
+ Some((pred, (e: Expr) => Choose(vars, e).setPosInfo(this)))
+ }
}
/* Like vals */
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
new file mode 100644
index 0000000000000000000000000000000000000000..adfec0f1750ffeda8498f1858932de1ee1c6a9eb
--- /dev/null
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -0,0 +1,34 @@
+package leon
+package synthesis
+
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps.ChooseCollectorWithPaths
+
+case class ChooseInfo(ctx: LeonContext,
+ prog: Program,
+ fd: FunDef,
+ pc: Expr,
+ ch: Choose,
+ options: SynthesisOptions) {
+
+ val synthesizer = new Synthesizer(ctx, Some(fd), prog, Problem.fromChoose(ch), options)
+ val problem = Problem.fromChoose(ch, pc)
+}
+
+object ChooseInfo {
+ def extractFromProgram(ctx: LeonContext, prog: Program, options: SynthesisOptions): List[ChooseInfo] = {
+ def noop(u:Expr, u2: Expr) = u
+
+ var results = List[ChooseInfo]()
+
+ // Look for choose()
+ for (f <- prog.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
+ for ((ch, path) <- new ChooseCollectorWithPaths().traverse(f.body.get)) {
+ results = ChooseInfo(ctx, prog, f, path, ch, options) :: results
+ }
+ }
+
+ results.reverse
+ }
+}
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index b761841826c82ef89f06bc5e184632dab46f5644..0fd787e733a911bcfb129e3151e5925b5ecdf602 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -5,9 +5,9 @@ import purescala.Trees._
import purescala.ScalaPrinter
import java.io.File
-class FileInterface(reporter: Reporter, origFile: File) {
+class FileInterface(reporter: Reporter) {
- def updateFile(solutions: Map[Choose, Expr], ignoreMissing: Boolean = false) {
+ def updateFile(origFile: File, solutions: Map[ChooseInfo, Expr], ignoreMissing: Boolean = false) {
import java.io.{File, BufferedWriter, FileWriter}
val FileExt = """^(.+)\.([^.]+)$""".r
@@ -35,7 +35,7 @@ class FileInterface(reporter: Reporter, origFile: File) {
}
}
- def substitueChooses(str: String, solutions: Map[Choose, Expr], ignoreMissing: Boolean = false): String = {
+ def substitueChooses(str: String, solutions: Map[ChooseInfo, Expr], ignoreMissing: Boolean = false): String = {
var lines = List[Int]()
// Compute line positions
@@ -58,6 +58,27 @@ class FileInterface(reporter: Reporter, origFile: File) {
}
}
+ def getLineIndentation(offset: Int): Int = {
+ var i = str.lastIndexOf('\n', offset)+1
+
+ var res = 0;
+
+ while (i < str.length) {
+ val c = str.charAt(i)
+ i += 1
+
+ if (c == ' ') {
+ res += 1
+ } else if (c == '\t') {
+ res += 4
+ } else {
+ i = str.length
+ }
+ }
+
+ res
+ }
+
lastFound = -1
var newStr = str
@@ -71,7 +92,9 @@ class FileInterface(reporter: Reporter, origFile: File) {
// compute scala equivalent of the position:
val scalaOffset = str.substring(lineoffset, lastFound).replaceAll("\t", " "*8).length
- solutions.find(_._1.posIntInfo == (lineno, scalaOffset)) match {
+ val indent = getLineIndentation(lastFound)
+
+ solutions.find(_._1.ch.posIntInfo == (lineno, scalaOffset)) match {
case Some((choose, solution)) =>
var lvl = 0;
var i = lastFound + 6;
@@ -89,7 +112,7 @@ class FileInterface(reporter: Reporter, origFile: File) {
i += 1
} while(continue)
- val newCode = ScalaPrinter(solution)
+ val newCode = ScalaPrinter(solution, indent/2)
newStr = (newStr.substring(0, lastFound+newStrOffset))+newCode+(newStr.substring(i+newStrOffset, newStr.length))
newStrOffset += -(i-lastFound)+newCode.length
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index cb18ef781aec214808b3d9275b03c992deef524b..858938a91af30dc690f6cc9689cc62c777674826 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -38,7 +38,7 @@ object HeuristicInstantiation {
Some(s)
}
- def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Option[Solution]): RuleInstantiation = {
+ def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Option[Solution], description: String): RuleInstantiation = {
val subTypes = subProblems.map(p => TupleType(p.xs.map(_.getType)))
val builder = new SolutionBuilder(subProblems.size, subTypes) {
@@ -47,7 +47,7 @@ object HeuristicInstantiation {
}
}
- new RuleInstantiation(problem, rule, builder) {
+ new RuleInstantiation(problem, rule, builder, description) {
def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems)
}
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index efe05182e1d329af67f7d744b7fa10348b941244..ca4346ade489ee110db92945452d891c822993df 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -12,6 +12,10 @@ class ParallelSearch(synth: Synthesizer,
costModel: CostModel,
nWorkers: Int) extends AndOrGraphParallelSearch[SynthesisContext, TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel)), nWorkers) {
+ def this(synth: Synthesizer, problem: Problem, nWorkers: Int) = {
+ this(synth, problem, synth.rules, synth.options.costModel, nWorkers)
+ }
+
import synth.reporter._
// This is HOT shared memory, used only in stop() for shutting down solvers!
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index e0ca64b78dff385aad774b86f44315b16dc7bb83..7810483affb6268979ba5f4d35f82b62db6905cf 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -12,11 +12,11 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
}
object Problem {
- def fromChoose(ch: Choose): Problem = {
+ def fromChoose(ch: Choose, pc: Expr = BooleanLiteral(true)): Problem = {
val xs = ch.vars
val phi = ch.pred
- val as = (variablesOf(phi)--xs).toList
+ val as = (variablesOf(And(pc, phi))--xs).toList
- Problem(as, BooleanLiteral(true), phi, xs)
+ Problem(as, pc, phi, xs)
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 7926efd69ac916f6678ec00b6a97fbddb7171864..ae46319400edf0efa255d31425f1e4df39b0da98 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -49,8 +49,10 @@ object SolutionBuilder {
}
}
-abstract class RuleInstantiation(val problem: Problem, val rule: Rule, val onSuccess: SolutionBuilder) {
+abstract class RuleInstantiation(val problem: Problem, val rule: Rule, val onSuccess: SolutionBuilder, val description: String) {
def apply(sctx: SynthesisContext): RuleApplicationResult
+
+ override def toString = description
}
sealed abstract class RuleApplicationResult
@@ -59,16 +61,16 @@ case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
case object RuleApplicationImpossible extends RuleApplicationResult
object RuleInstantiation {
- def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Option[Solution]) = {
+ def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Option[Solution], description: String) = {
val subTypes = sub.map(p => TupleType(p.xs.map(_.getType)))
- new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, subTypes, onSuccess)) {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, subTypes, onSuccess), description) {
def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
}
}
def immediateSuccess(problem: Problem, rule: Rule, solution: Solution) = {
- new RuleInstantiation(problem, rule, new SolutionCombiner(0, Seq(), ls => Some(solution))) {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(0, Seq(), ls => Some(solution)), "Solve with "+solution) {
def apply(sctx: SynthesisContext) = RuleSuccess(solution)
}
}
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 32258cedda16cbb3da45c077b89f68d8e0cd074c..06fa7da537e3ed2143ac88ea9c05c498c3d11916 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -35,6 +35,10 @@ class SimpleSearch(synth: Synthesizer,
rules: Seq[Rule],
costModel: CostModel) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel))) {
+ def this(synth: Synthesizer, problem: Problem) = {
+ this(synth, problem, synth.rules, synth.options.costModel)
+ }
+
import synth.reporter._
val sctx = SynthesisContext.fromSynthesizer(synth)
@@ -85,25 +89,29 @@ class SimpleSearch(synth: Synthesizer,
var shouldStop = false
+ def searchStep() {
+ nextLeaf() match {
+ case Some(l) =>
+ l match {
+ case al: g.AndLeaf =>
+ val sub = expandAndTask(al.task)
+ onExpansion(al, sub)
+ case ol: g.OrLeaf =>
+ val sub = expandOrTask(ol.task)
+ onExpansion(ol, sub)
+ }
+ case None =>
+ stop()
+ }
+ }
+
def search(): Option[Solution] = {
sctx.solver.init()
shouldStop = false
while (!g.tree.isSolved && !shouldStop) {
- nextLeaf() match {
- case Some(l) =>
- l match {
- case al: g.AndLeaf =>
- val sub = expandAndTask(al.task)
- onExpansion(al, sub)
- case ol: g.OrLeaf =>
- val sub = expandOrTask(ol.task)
- onExpansion(ol, sub)
- }
- case None =>
- stop()
- }
+ searchStep()
}
g.tree.solution
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 6dbfc3844b52a0eb873ea7304c6436ee9c67ca89..965b1f74a7bde5c2c7c8d2bb18dc2919be7274e6 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -1,11 +1,13 @@
package leon
package synthesis
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees.{TypeTree,TupleType}
-import leon.purescala.Definitions._
-import leon.purescala.TreeOps._
-import leon.xlang.Trees.LetDef
+import purescala.Trees._
+import purescala.TypeTrees.{TypeTree,TupleType}
+import purescala.Definitions._
+import purescala.TreeOps._
+import xlang.Trees.LetDef
+import xlang.TreeOps.{ScopeSimplifier => XLangScopeSimplifier}
+import solvers.z3.UninterpretedZ3Solver
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
@@ -26,6 +28,26 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
def fullTerm =
defs.foldLeft(term){ case (t, fd) => LetDef(fd, t) }
+
+ def toSimplifiedExpr(ctx: LeonContext, p: Program): Expr = {
+ val uninterpretedZ3 = new UninterpretedZ3Solver(ctx.copy(reporter = new SilentReporter))
+ uninterpretedZ3.setProgram(p)
+
+ val simplifiers = List[Expr => Expr](
+ simplifyTautologies(uninterpretedZ3)(_),
+ simplifyLets _,
+ decomposeIfs _,
+ matchToIfThenElse _,
+ simplifyPaths(uninterpretedZ3)(_),
+ patternMatchReconstruction _,
+ simplifyTautologies(uninterpretedZ3)(_),
+ simplifyLets _,
+ rewriteTuples _,
+ (new ScopeSimplifier with XLangScopeSimplifier).transform _
+ )
+
+ simplifiers.foldLeft(toExpr){ (x, sim) => sim(x) }
+ }
}
object Solution {
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 92ae31535579dfba4942f3ff6b55cc13ad5d774a..342e1766acc19e5e76def80d3e4161066b8e8210 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -10,10 +10,11 @@ import java.util.concurrent.atomic.AtomicBoolean
case class SynthesisContext(
context: LeonContext,
- options: SynthesizerOptions,
+ options: SynthesisOptions,
functionContext: Option[FunDef],
program: Program,
solver: Solver,
+ simpleSolver: Solver,
reporter: Reporter,
shouldStop: AtomicBoolean
)
@@ -26,6 +27,7 @@ object SynthesisContext {
synth.functionContext,
synth.program,
synth.solver,
+ synth.simpleSolver,
synth.reporter,
synth.shouldStop)
}
diff --git a/src/main/scala/leon/synthesis/SynthesizerOptions.scala b/src/main/scala/leon/synthesis/SynthesisOptions.scala
similarity index 78%
rename from src/main/scala/leon/synthesis/SynthesizerOptions.scala
rename to src/main/scala/leon/synthesis/SynthesisOptions.scala
index 647e4049da9e479d824621fc363426fbd6a4ae54..f221fb3aa82614874a0fc1a2da83467cf468a81c 100644
--- a/src/main/scala/leon/synthesis/SynthesizerOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesisOptions.scala
@@ -1,13 +1,15 @@
package leon
package synthesis
-case class SynthesizerOptions(
+case class SynthesisOptions(
+ inPlace: Boolean = false,
generateDerivationTrees: Boolean = false,
filterFuns: Option[Set[String]] = None,
searchWorkers: Int = 1,
firstOnly: Boolean = false,
timeoutMs: Option[Long] = None,
costModel: CostModel = CostModel.default,
+ rules: Seq[Rule] = Rules.all ++ Heuristics.all,
// Cegis related options
cegisGenerateFunCalls: Boolean = false,
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index ed7cf742958023fa68b7f99cc6dfce984a763d2f..dc15b0b2ad828903690abd6a12fe7d5d52c0aeff 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -24,21 +24,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
LeonFlagOptionDef( "cegis:gencalls", "--cegis:gencalls", "Include function calls in CEGIS generators")
)
- def run(ctx: LeonContext)(p: Program): Program = {
- val silentContext : LeonContext = ctx.copy(reporter = new SilentReporter)
-
- val mainSolver = new FairZ3Solver(silentContext)
- mainSolver.setProgram(p)
-
- val uninterpretedZ3 = new UninterpretedZ3Solver(silentContext)
- uninterpretedZ3.setProgram(p)
-
- var options = SynthesizerOptions()
- var inPlace = false
+ def processOptions(ctx: LeonContext): SynthesisOptions = {
+ var options = SynthesisOptions()
for(opt <- ctx.options) opt match {
case LeonFlagOption("inplace") =>
- inPlace = true
+ options = options.copy(inPlace = true)
case LeonValueOption("functions", ListValue(fs)) =>
options = options.copy(filterFuns = Some(fs.toSet))
@@ -84,74 +75,36 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
case _ =>
}
- def synthesizeAll(program: Program): Map[Choose, (FunDef, Solution)] = {
- def noop(u:Expr, u2: Expr) = u
-
- var solutions = Map[Choose, (FunDef, Solution)]()
-
- def actOnChoose(f: FunDef)(e: Expr, a: Expr): Expr = e match {
- case ch @ Choose(vars, pred) =>
- val problem = Problem.fromChoose(ch)
- val synth = new Synthesizer(ctx,
- Some(f),
- mainSolver,
- p,
- problem,
- Rules.all ++ Heuristics.all,
- options)
- val sol = synth.synthesize()
+ options
+ }
- solutions += ch -> (f, sol._1)
+ def run(ctx: LeonContext)(p: Program): Program = {
+ val options = processOptions(ctx)
- a
- case _ =>
- a
- }
+ def toProcess(ci: ChooseInfo) = {
+ options.filterFuns.isEmpty || options.filterFuns.get.contains(ci.fd.id.toString)
+ }
- // Look for choose()
- for (f <- program.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
- if (options.filterFuns.isEmpty || options.filterFuns.get.contains(f.id.toString)) {
- treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
- }
- }
+ var chooses = ChooseInfo.extractFromProgram(ctx, p, options).filter(toProcess)
- solutions
- }
+ val results = chooses.map { ci =>
+ val (sol, isComplete) = ci.synthesizer.synthesize()
- val solutions = synthesizeAll(p)
-
- // Simplify expressions
- val simplifiers = List[Expr => Expr](
- simplifyTautologies(uninterpretedZ3)(_),
- simplifyLets _,
- decomposeIfs _,
- matchToIfThenElse _,
- simplifyPaths(uninterpretedZ3)(_),
- patternMatchReconstruction _,
- simplifyTautologies(uninterpretedZ3)(_),
- simplifyLets _,
- rewriteTuples _
- )
-
- def simplify(e: Expr): Expr = simplifiers.foldLeft(e){ (x, sim) => sim(x) }
-
- val chooseToExprs = solutions.map {
- case (ch, (fd, sol)) =>
- (ch, (fd, simplify(sol.toExpr)))
- }
+ ci -> sol.toSimplifiedExpr(ctx, p)
+ }.toMap
- if (inPlace) {
+ if (options.inPlace) {
for (file <- ctx.files) {
- new FileInterface(ctx.reporter, file).updateFile(chooseToExprs.mapValues(_._2))
+ new FileInterface(ctx.reporter).updateFile(file, results)
}
} else {
- for ((chs, (fd, ex)) <- chooseToExprs) {
- val middle = " In "+fd.id.toString+", synthesis of: "
+ for ((ci, ex) <- results) {
+ val middle = " In "+ci.fd.id.toString+", synthesis of: "
val remSize = (80-middle.length)
ctx.reporter.info("-"*math.floor(remSize/2).toInt+middle+"-"*math.ceil(remSize/2).toInt)
- ctx.reporter.info(chs)
+ ctx.reporter.info(ci.ch)
ctx.reporter.info("-"*35+" Result: "+"-"*36)
ctx.reporter.info(ScalaPrinter(ex))
ctx.reporter.info("")
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 624b6a178e01c71090cb94823b56364900743676..6b792aea284d8765d46b7cee821ce78a624f5f07 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -6,6 +6,7 @@ import purescala.Definitions.{Program, FunDef}
import purescala.TreeOps._
import purescala.Trees.{Expr, Not}
import purescala.ScalaPrinter
+import solvers.z3._
import sun.misc.{Signal, SignalHandler}
import solvers.Solver
@@ -19,25 +20,31 @@ import java.util.concurrent.atomic.AtomicBoolean
class Synthesizer(val context : LeonContext,
val functionContext: Option[FunDef],
- val solver: Solver,
val program: Program,
val problem: Problem,
- val rules: Seq[Rule],
- val options: SynthesizerOptions) {
+ val options: SynthesisOptions) {
- protected[synthesis] val reporter = context.reporter
+ val silentContext = context.copy(reporter = new SilentReporter)
- import reporter.{error,warning,info,fatalError}
+ val rules: Seq[Rule] = options.rules
+
+ val solver: FairZ3Solver = new FairZ3Solver(silentContext)
+ solver.setProgram(program)
+
+ val simpleSolver: Solver = new UninterpretedZ3Solver(silentContext)
+ simpleSolver.setProgram(program)
+
+ val reporter = context.reporter
var shouldStop = new AtomicBoolean(false)
def synthesize(): (Solution, Boolean) = {
- val search = if (options.searchWorkers > 1) {
- new ParallelSearch(this, problem, rules, options.costModel, options.searchWorkers)
- } else {
- new SimpleSearch(this, problem, rules, options.costModel)
- }
+ val search = if (options.searchWorkers > 1) {
+ new ParallelSearch(this, problem, options.searchWorkers)
+ } else {
+ new SimpleSearch(this, problem)
+ }
val sigINT = new Signal("INT")
var oldHandler: SignalHandler = null
@@ -72,7 +79,4 @@ class Synthesizer(val context : LeonContext,
(new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem)).getSolution, false)
}
}
-
}
-
-
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index b1f95c72644a81f0fa39364c1cbcc52522ce582a..39ff4d4c25cdc6e67424afe5d01ba33af6f671eb 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -15,7 +15,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
}
- val steps = for (candidate <- candidates) yield {
+ val instances = for (candidate <- candidates) yield {
val (origId, cd) = candidate
val oas = p.as.filterNot(_ == origId)
@@ -35,10 +35,13 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
case _ => false
}
+ // Map for getting a formula in the context of within the recursive function
+ val substMap = residualMap + (origId -> Variable(inductOn))
+
if (isRecursive) {
- val innerPhi = substAll(residualMap + (origId -> Variable(inductOn)), p.phi)
- val innerPC = substAll(residualMap + (origId -> Variable(inductOn)), p.pc)
+ val innerPhi = substAll(substMap, p.phi)
+ val innerPC = substAll(substMap, p.pc)
val subProblemsInfo = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
case ccd : CaseClassDef =>
@@ -92,11 +95,12 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
// might only have to enforce it on solutions of base cases.
None
} else {
- val funPre = subst(origId -> Variable(inductOn), Or(globalPre))
+ val funPre = substAll(substMap, Or(globalPre))
+ val funPost = substAll(substMap, p.phi)
val outerPre = Or(globalPre)
newFun.precondition = Some(funPre)
- newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(resType), p.phi))
+ newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(resType), funPost))
newFun.body = Some(MatchExpr(Variable(inductOn), cases))
@@ -107,12 +111,12 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
}
}
- Some(HeuristicInstantiation(p, this, subProblemsInfo.map(_._1).toList, onSuccess))
+ Some(HeuristicInstantiation(p, this, subProblemsInfo.map(_._1).toList, onSuccess, "ADT Induction on '"+origId+"'"))
} else {
None
}
}
- steps.flatten
+ instances.flatten
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
index b2782c5dc3d7dbb1d3a3979a06bf9065df0a68f0..8a76cd9f0d7a40e6700fcbe0446328514f8f8346 100644
--- a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
@@ -26,13 +26,13 @@ case object InnerCaseSplit extends Rule("Inner-Case-Split") with Heuristic {
phi match {
case Or(os) =>
- List(rules.CaseSplit.split(os, p))
+ List(rules.CaseSplit.split(os, p, "Inner case-split"))
case And(as) =>
val optapp = for ((a, i) <- as.zipWithIndex) yield {
a match {
case Or(os) =>
- Some(rules.CaseSplit.split(os.map(o => And(as.updated(i, o))), p))
+ Some(rules.CaseSplit.split(os.map(o => And(as.updated(i, o))), p, "Inner case-split"))
case _ =>
None
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index e59150394e2146f0ce6badcd99f44248e2d5d8d0..b94ceffd967931c7db640f42976a68353385734d 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -60,7 +60,7 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
None
}
- Some(HeuristicInstantiation(p, this, List(subBase, subGT, subLT), onSuccess))
+ Some(HeuristicInstantiation(p, this, List(subBase, subGT, subLT), onSuccess, "Int Induction on '"+origId+"'"))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index 1a957e40250d7cab755d4657463d0a9f04aad9ed..a4308de79ec42d4ac50b24c0dcabae4291385698 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -36,7 +36,7 @@ case object OptimisticInjection extends Rule("Opt. Injection") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, this, List(sub), forward))
+ Some(HeuristicInstantiation(p, this, List(sub), forward, this.name))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 488df73556f61321eaf64ca21923b505087978b1..b906d37e9355e0a2ca4cb6572c3ca175c4f7ac51 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -36,7 +36,7 @@ case object SelectiveInlining extends Rule("Sel. Inlining") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, this, List(sub), forward))
+ Some(HeuristicInstantiation(p, this, List(sub), forward, this.name))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index f1811f073e66e3fc69a7546d9d52be91428dea08..41202315d13fa2b9dc9bf8f1573c9fbd9365ebf7 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -24,7 +24,7 @@ case object ADTDual extends Rule("ADTDual") {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward, "ADTDual"))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 04cd58c5a70b6a2bbbec25ce9807e00457a746a8..228923bb49b4a3d3a6dd6f0374f09cff569fdae0 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -2,8 +2,6 @@ package leon
package synthesis
package rules
-import solvers.TimeoutSolver
-
import purescala.Trees._
import purescala.Common._
import purescala.TypeTrees._
@@ -13,7 +11,7 @@ import purescala.Definitions._
case object ADTSplit extends Rule("ADT Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
- val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+ val solver = sctx.simpleSolver
val candidates = p.as.collect {
case IsTyped(id, AbstractClassType(cd)) =>
@@ -73,7 +71,7 @@ case object ADTSplit extends Rule("ADT Split.") {
Some(Solution(Or(globalPre), sols.flatMap(_.defs).toSet, MatchExpr(Variable(id), cases)))
}
- Some(RuleInstantiation.immediateDecomp(p, this, subInfo.map(_._2).toList, onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, subInfo.map(_._2).toList, onSuccess, "ADT Split on '"+id+"'"))
case _ =>
None
}}.flatten
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index cab8ea72c20094db0018dd2ad97f74c982a2c5a9..efafc204d318141d1cdef74a456269cd2cc56af0 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -23,7 +23,7 @@ case object Assert extends NormalizingRule("Assert") {
List(RuleInstantiation.immediateDecomp(p, this, List(sub), {
case Solution(pre, defs, term) :: Nil => Some(Solution(And(exprsA :+ pre), defs, term))
case _ => None
- }))
+ }, "Assert "+And(exprsA)))
}
} else {
Nil
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 1e1ac7940967c3791060f1bf9ab58afe947fc30d..f22f97be439f1d084c5b1751042ec07337916e54 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -10,13 +10,13 @@ case object CaseSplit extends Rule("Case-Split") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
p.phi match {
case Or(os) =>
- List(split(os, p))
+ List(split(os, p, "Split top-level Or"))
case _ =>
Nil
}
}
- def split(alts: Seq[Expr], p: Problem): RuleInstantiation = {
+ def split(alts: Seq[Expr], p: Problem, description: String): RuleInstantiation = {
val subs = alts.map(a => Problem(p.as, p.pc, a, p.xs)).toList
val onSuccess: List[Solution] => Option[Solution] = {
@@ -34,7 +34,7 @@ case object CaseSplit extends Rule("Case-Split") {
None
}
- RuleInstantiation.immediateDecomp(p, this, subs, onSuccess)
+ RuleInstantiation.immediateDecomp(p, this, subs, onSuccess, description)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 296d4ef401007d165f0f6e9d6b59790a3f6ba2e6..41527707f3150f6b2fb6bba0705b9deb37337a42 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -365,289 +365,278 @@ case object CEGIS extends Rule("CEGIS") {
def css : Set[Identifier] = mappings.values.map(_._1).toSet ++ guardedTerms.flatMap(_._2)
}
- val TopLevelAnds(ands) = p.phi
+ List(new RuleInstantiation(p, this, SolutionBuilder.none, "CEGIS") {
+ def apply(sctx: SynthesisContext): RuleApplicationResult = {
+ var result: Option[RuleApplicationResult] = None
- val xsSet = p.xs.toSet
+ var ass = p.as.toSet
+ var xss = p.xs.toSet
+ val initGuard = FreshIdentifier("START", true).setType(BooleanType)
- val (exprsA, others) = ands.partition(e => (variablesOf(e) & xsSet).isEmpty)
- if (exprsA.isEmpty) {
- val res = new RuleInstantiation(p, this, SolutionBuilder.none) {
- def apply(sctx: SynthesisContext): RuleApplicationResult = {
- var result: Option[RuleApplicationResult] = None
+ val ndProgram = new NonDeterministicProgram(p, initGuard)
+ var unrolings = 0
+ val maxUnrolings = 3
- var ass = p.as.toSet
- var xss = p.xs.toSet
+ val mainSolver = new TimeoutSolver(sctx.solver, 10000L) // 10sec
- val initGuard = FreshIdentifier("START", true).setType(BooleanType)
+ var exampleInputs = Set[Seq[Expr]]()
- val ndProgram = new NonDeterministicProgram(p, initGuard)
- var unrolings = 0
- val maxUnrolings = 3
-
- val mainSolver = new TimeoutSolver(sctx.solver, 2000L) // 2sec
-
- var exampleInputs = Set[Seq[Expr]]()
-
- // We populate the list of examples with a predefined one
- if (p.pc == BooleanLiteral(true)) {
- exampleInputs += p.as.map(a => simplestValue(a.getType))
- } else {
- val solver = mainSolver.getNewSolver
+ // We populate the list of examples with a predefined one
+ if (p.pc == BooleanLiteral(true)) {
+ exampleInputs += p.as.map(a => simplestValue(a.getType))
+ } else {
+ val solver = mainSolver.getNewSolver
- solver.assertCnstr(p.pc)
+ solver.assertCnstr(p.pc)
- solver.check match {
- case Some(true) =>
- val model = solver.getModel
- exampleInputs += p.as.map(a => model.getOrElse(a, simplestValue(a.getType)))
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
+ exampleInputs += p.as.map(a => model.getOrElse(a, simplestValue(a.getType)))
- case Some(false) =>
- return RuleApplicationImpossible
+ case Some(false) =>
+ return RuleApplicationImpossible
- case None =>
- sctx.reporter.warning("Solver could not solve path-condition")
- return RuleApplicationImpossible // This is not necessary though, but probably wanted
- }
+ case None =>
+ sctx.reporter.warning("Solver could not solve path-condition")
+ return RuleApplicationImpossible // This is not necessary though, but probably wanted
}
+ }
- // Keep track of collected cores to filter programs to test
- var collectedCores = Set[Set[Identifier]]()
-
- // solver1 is used for the initial SAT queries
- var solver1 = mainSolver.getNewSolver
- solver1.assertCnstr(And(p.pc :: p.phi :: Variable(initGuard) :: Nil))
+ // Keep track of collected cores to filter programs to test
+ var collectedCores = Set[Set[Identifier]]()
- // solver2 is used for validating a candidate program, or finding new inputs
- val solver2 = mainSolver.getNewSolver
- solver2.assertCnstr(And(p.pc :: Not(p.phi) :: Variable(initGuard) :: Nil))
+ // solver1 is used for the initial SAT queries
+ var solver1 = mainSolver.getNewSolver
+ solver1.assertCnstr(And(p.pc :: p.phi :: Variable(initGuard) :: Nil))
+ // solver2 is used for validating a candidate program, or finding new inputs
+ val solver2 = mainSolver.getNewSolver
+ solver2.assertCnstr(And(p.pc :: Not(p.phi) :: Variable(initGuard) :: Nil))
- var allClauses = List[Expr]()
- try {
- do {
- var needMoreUnrolling = false
+ var allClauses = List[Expr]()
- // Compute all programs that have not been excluded yet
- var allPrograms: Set[Set[Identifier]] = if (useCEPruning) {
- ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p)))
- } else {
- Set()
- }
+ try {
+ do {
+ var needMoreUnrolling = false
- //println("Programs: "+allPrograms.size)
- //println("CEs: "+exampleInputs.size)
+ // Compute all programs that have not been excluded yet
+ var allPrograms: Set[Set[Identifier]] = if (useCEPruning) {
+ ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p)))
+ } else {
+ Set()
+ }
- // We further filter the set of working programs to remove those that fail on known examples
- if (useCEPruning && !exampleInputs.isEmpty && ndProgram.canTest()) {
- //for (ce <- exampleInputs) {
- // println("CE: "+ce)
- //}
+ //println("Programs: "+allPrograms.size)
+ //println("CEs: "+exampleInputs.size)
- for (p <- allPrograms) {
- if (!exampleInputs.forall(ndProgram.testForProgram(p))) {
- // This program failed on at least one example
- solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
- allPrograms -= p
- }
- }
+ // We further filter the set of working programs to remove those that fail on known examples
+ if (useCEPruning && !exampleInputs.isEmpty && ndProgram.canTest()) {
+ //for (ce <- exampleInputs) {
+ // println("CE: "+ce)
+ //}
- if (allPrograms.isEmpty) {
- needMoreUnrolling = true
+ for (p <- allPrograms) {
+ if (!exampleInputs.forall(ndProgram.testForProgram(p))) {
+ // This program failed on at least one example
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ allPrograms -= p
}
+ }
- //println("Passing tests: "+allPrograms.size)
+ if (allPrograms.isEmpty) {
+ needMoreUnrolling = true
}
- //allPrograms.foreach { p =>
- // println("PATH: "+p)
- // println("CLAUSES: "+p.flatMap( b => ndProgram.mappings.get(b).map{ case (c, ex) => c+" = "+ex}).mkString(" && "))
- //}
+ //println("Passing tests: "+allPrograms.size)
+ }
- val (clauses, closedBs) = ndProgram.unroll
- //println("UNROLLING: ")
- //for (c <- clauses) {
- // println(" - " + c)
- //}
- //println("CLOSED Bs "+closedBs)
+ //allPrograms.foreach { p =>
+ // println("PATH: "+p)
+ // println("CLAUSES: "+p.flatMap( b => ndProgram.mappings.get(b).map{ case (c, ex) => c+" = "+ex}).mkString(" && "))
+ //}
- val clause = And(clauses)
- allClauses = clause :: allClauses
+ val (clauses, closedBs) = ndProgram.unroll
+ //println("UNROLLING: ")
+ //for (c <- clauses) {
+ // println(" - " + c)
+ //}
+ //println("CLOSED Bs "+closedBs)
- solver1.assertCnstr(clause)
- solver2.assertCnstr(clause)
+ val clause = And(clauses)
+ allClauses = clause :: allClauses
- val tpe = TupleType(p.xs.map(_.getType))
- val bss = ndProgram.bss
+ solver1.assertCnstr(clause)
+ solver2.assertCnstr(clause)
- if (clauses.isEmpty) {
- needMoreUnrolling = true
- }
+ val tpe = TupleType(p.xs.map(_.getType))
+ val bss = ndProgram.bss
- while (result.isEmpty && !needMoreUnrolling && !sctx.shouldStop.get) {
+ if (clauses.isEmpty) {
+ needMoreUnrolling = true
+ }
- solver1.checkAssumptions(closedBs.map(id => Not(Variable(id)))) match {
- case Some(true) =>
- val satModel = solver1.getModel
+ while (result.isEmpty && !needMoreUnrolling && !sctx.shouldStop.get) {
- val bssAssumptions: Set[Expr] = bss.map(b => satModel(b) match {
- case BooleanLiteral(true) => Variable(b)
- case BooleanLiteral(false) => Not(Variable(b))
- })
+ solver1.checkAssumptions(closedBs.map(id => Not(Variable(id)))) match {
+ case Some(true) =>
+ val satModel = solver1.getModel
- //println("CEGIS OUT!")
- //println("Found solution: "+bssAssumptions)
+ val bssAssumptions: Set[Expr] = bss.map(b => satModel(b) match {
+ case BooleanLiteral(true) => Variable(b)
+ case BooleanLiteral(false) => Not(Variable(b))
+ })
- //bssAssumptions.collect { case Variable(b) => ndProgram.mappings(b) }.foreach {
- // case (c, ex) =>
- // println(". "+c+" = "+ex)
- //}
+ //println("CEGIS OUT!")
+ //println("Found solution: "+bssAssumptions)
- val validateWithZ3 = if (useCETests && !exampleInputs.isEmpty && ndProgram.canTest()) {
+ //bssAssumptions.collect { case Variable(b) => ndProgram.mappings(b) }.foreach {
+ // case (c, ex) =>
+ // println(". "+c+" = "+ex)
+ //}
- val p = bssAssumptions.collect { case Variable(b) => b }
+ val validateWithZ3 = if (useCETests && !exampleInputs.isEmpty && ndProgram.canTest()) {
- if (exampleInputs.forall(ndProgram.testForProgram(p))) {
- // All valid inputs also work with this, we need to
- // make sure by validating this candidate with z3
- true
- } else {
- // One valid input failed with this candidate, we can skip
- solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
- false
- }
- } else {
- // No inputs or capability to test, we need to ask Z3
+ val p = bssAssumptions.collect { case Variable(b) => b }
+
+ if (exampleInputs.forall(ndProgram.testForProgram(p))) {
+ // All valid inputs also work with this, we need to
+ // make sure by validating this candidate with z3
true
+ } else {
+ // One valid input failed with this candidate, we can skip
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ false
}
+ } else {
+ // No inputs or capability to test, we need to ask Z3
+ true
+ }
- if (validateWithZ3) {
- solver2.checkAssumptions(bssAssumptions) match {
- case Some(true) =>
- //println("#"*80)
- val invalidModel = solver2.getModel
+ if (validateWithZ3) {
+ solver2.checkAssumptions(bssAssumptions) match {
+ case Some(true) =>
+ //println("#"*80)
+ val invalidModel = solver2.getModel
- val fixedAss = And(ass.collect {
- case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
- }.toSeq)
+ val fixedAss = And(ass.collect {
+ case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
+ }.toSeq)
- val newCE = p.as.map(valuateWithModel(invalidModel))
+ val newCE = p.as.map(valuateWithModel(invalidModel))
- exampleInputs += newCE
+ exampleInputs += newCE
- //println("Found counter example: "+fixedAss)
+ //println("Found counter example: "+fixedAss)
- // Retest whether the newly found C-E invalidates all programs
- if (useCEPruning && ndProgram.canTest) {
- if (allPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
- // println("I found a killer example!")
- needMoreUnrolling = true
- }
+ // Retest whether the newly found C-E invalidates all programs
+ if (useCEPruning && ndProgram.canTest) {
+ if (allPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
+ // println("I found a killer example!")
+ needMoreUnrolling = true
}
+ }
- val unsatCore = if (useUnsatCores) {
- solver1.push()
- solver1.assertCnstr(fixedAss)
+ val unsatCore = if (useUnsatCores) {
+ solver1.push()
+ solver1.assertCnstr(fixedAss)
- val core = solver1.checkAssumptions(bssAssumptions) match {
- case Some(false) =>
- // Core might be empty if unrolling level is
- // insufficient, it becomes unsat no matter what
- // the assumptions are.
- solver1.getUnsatCore
+ val core = solver1.checkAssumptions(bssAssumptions) match {
+ case Some(false) =>
+ // Core might be empty if unrolling level is
+ // insufficient, it becomes unsat no matter what
+ // the assumptions are.
+ solver1.getUnsatCore
- case Some(true) =>
- // Can't be!
- bssAssumptions
+ case Some(true) =>
+ // Can't be!
+ bssAssumptions
- case None =>
- return RuleApplicationImpossible
- }
+ case None =>
+ return RuleApplicationImpossible
+ }
- solver1.pop()
+ solver1.pop()
- collectedCores += core.collect{ case Variable(id) => id }
+ collectedCores += core.collect{ case Variable(id) => id }
- core
- } else {
- bssAssumptions
- }
+ core
+ } else {
+ bssAssumptions
+ }
- if (unsatCore.isEmpty) {
- needMoreUnrolling = true
- } else {
- //if (useCEAsserts) {
- // val freshCss = ndProgram.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
- // val ceIn = ass.collect {
- // case id if invalidModel contains id => id -> invalidModel(id)
- // }
+ if (unsatCore.isEmpty) {
+ needMoreUnrolling = true
+ } else {
+ //if (useCEAsserts) {
+ // val freshCss = ndProgram.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
+ // val ceIn = ass.collect {
+ // case id if invalidModel contains id => id -> invalidModel(id)
+ // }
- // val ceMap = (freshCss ++ ceIn)
+ // val ceMap = (freshCss ++ ceIn)
- // val counterexample = substAll(ceMap, And(Seq(ndProgram.program, p.phi)))
+ // val counterexample = substAll(ceMap, And(Seq(ndProgram.program, p.phi)))
- // //val And(ands) = counterexample
- // //println("CE:")
- // //for (a <- ands) {
- // // println(" - "+a)
- // //}
+ // //val And(ands) = counterexample
+ // //println("CE:")
+ // //for (a <- ands) {
+ // // println(" - "+a)
+ // //}
- // solver1.assertCnstr(counterexample)
- //}
+ // solver1.assertCnstr(counterexample)
+ //}
- solver1.assertCnstr(Not(And(unsatCore.toSeq)))
- }
+ solver1.assertCnstr(Not(And(unsatCore.toSeq)))
+ }
- case Some(false) =>
+ case Some(false) =>
- val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
+ val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
- case _ =>
- return RuleApplicationImpossible
- }
+ case _ =>
+ return RuleApplicationImpossible
}
+ }
- case Some(false) =>
- //println("%%%% UNSAT")
+ case Some(false) =>
+ //println("%%%% UNSAT")
- if (useUninterpretedProbe) {
- solver1.check match {
- case Some(false) =>
- // Unsat even without blockers (under which fcalls are then uninterpreted)
- return RuleApplicationImpossible
+ if (useUninterpretedProbe) {
+ solver1.check match {
+ case Some(false) =>
+ // Unsat even without blockers (under which fcalls are then uninterpreted)
+ return RuleApplicationImpossible
- case _ =>
- }
+ case _ =>
}
+ }
- needMoreUnrolling = true
+ needMoreUnrolling = true
- case _ =>
- //println("%%%% WOOPS")
- return RuleApplicationImpossible
- }
+ case _ =>
+ //println("%%%% WOOPS")
+ return RuleApplicationImpossible
}
+ }
- unrolings += 1
- } while(unrolings < maxUnrolings && result.isEmpty && !sctx.shouldStop.get)
+ unrolings += 1
+ } while(unrolings < maxUnrolings && result.isEmpty && !sctx.shouldStop.get)
- result.getOrElse(RuleApplicationImpossible)
+ result.getOrElse(RuleApplicationImpossible)
- } catch {
- case e: Throwable =>
- sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
- e.printStackTrace
- RuleApplicationImpossible
- }
+ } catch {
+ case e: Throwable =>
+ sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
+ e.printStackTrace
+ RuleApplicationImpossible
}
}
- List(res)
- } else {
- Nil
- }
+ })
}
}
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index b5746897e6cddd6900ceebc0cf09eafe4d61851c..3d475f336668bd80d6b4edbb0a89b3632ccba49a 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -49,7 +49,7 @@ case object DetupleOutput extends Rule("Detuple Out") {
}
- Some(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess, this.name))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 4925f60004acf4e1f604fc47cbfee5a72a3083dc..b496a4dd41b459ca195b76098ef09caa1c2e91ac 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -26,7 +26,7 @@ object Disunification {
if (!toRemove.isEmpty) {
val sub = p.copy(phi = Or((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward, this.name))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index c59d37aa014af86df043465d4db59194fe86ff0e..ae6d6da241d570469541574515eff6850af462aa 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -2,16 +2,15 @@ package leon
package synthesis
package rules
-import solvers.TimeoutSolver
import purescala.Trees._
import purescala.Common._
import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
-case object EqualitySplit extends Rule("Eq. Split.") {
+case object EqualitySplit extends Rule("Eq. Split") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+ val solver = sctx.simpleSolver
val candidates = p.as.groupBy(_.getType).mapValues(_.combinations(2).filter {
case List(a1, a2) =>
@@ -51,7 +50,7 @@ case object EqualitySplit extends Rule("Eq. Split.") {
None
}
- Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess, "Eq. Split on '"+a1+"' and '"+a2+"'"))
case _ =>
None
})
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index bb74de12aba2f3a80861261cc221e045edd3f11f..73b1a81a56441138f53f9f939919aa4fa8b86720 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -12,7 +12,7 @@ case object Ground extends Rule("Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
- val solver = new TimeoutSolver(sctx.solver, 1000L) // We give that 1s
+ val solver = new TimeoutSolver(sctx.solver, 5000L) // We give that 1s
val tpe = TupleType(p.xs.map(_.getType))
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 11040132becd8790fbfb93ebf84a5163d41e0a8a..6c9e07d73e95c07d259c0b34f274d8a06b0e844e 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -2,8 +2,6 @@ package leon
package synthesis
package rules
-import solvers.TimeoutSolver
-
import purescala.Trees._
import purescala.TypeTrees._
import purescala.Common._
@@ -13,7 +11,7 @@ import purescala.Extractors._
case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+ val solver = sctx.simpleSolver
val candidates = p.as.filter(_.getType == Int32Type).combinations(2).toList.filter {
case List(a1, a2) =>
@@ -74,7 +72,7 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
None
}
- Some(RuleInstantiation.immediateDecomp(p, this, List(subLT, subEQ, subGT), onSuccess))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(subLT, subEQ, subGT), onSuccess, "Ineq. Split on '"+a1+"' and '"+a2+"'"))
case _ =>
None
})
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 1d357990756e3d36c847e3bfe6ff3ac424cb790e..60101558d83417f88ab7e864ffad59ff3ca57abb 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -60,7 +60,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
None
}
- List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess, this.name))
} else {
val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
@@ -105,7 +105,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
None
}
- List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess, this.name))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 540dd6b947847be7477cb76b04458d5558d9b18d..3ed407bb9256732e025114bc2b240e7d009fb1a6 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -131,7 +131,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val constraints: List[Expr] = for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds)
yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc)))
val pre = And(exprNotUsed ++ constraints)
- List(RuleInstantiation.immediateSuccess(problem, this, Solution(pre, Set(), witness)))
+ List(RuleInstantiation.immediateSuccess(problem, this, Solution(pre, Set(), Tuple(Seq(witness)))))
} else {
val involvedVariables = (upperBounds++lowerBounds).foldLeft(Set[Identifier]())((acc, t) => {
@@ -201,7 +201,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
None
}
- List(RuleInstantiation.immediateDecomp(problem, this, List(subProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(problem, this, List(subProblem), onSuccess, this.name))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index d245e7bb2ee45030442ff0bf41beae33c066a28e..1b44bbd06369beabe1449b6eb58f4e6595141f4c 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -37,7 +37,7 @@ case object OnePoint extends NormalizingRule("One-point") {
None
}
- List(RuleInstantiation.immediateDecomp(p, this, List(newProblem), onSuccess))
+ List(RuleInstantiation.immediateDecomp(p, this, List(newProblem), onSuccess, this.name))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 7e65ed7970c6e9d5c67e25b997c8f9c8d3f48f16..aeefe055eeac384a596f3e87306557247b2e86bf 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -2,7 +2,6 @@ package leon
package synthesis
package rules
-import solvers.TimeoutSolver
import purescala.Trees._
import purescala.TypeTrees._
import purescala.TreeOps._
@@ -11,10 +10,10 @@ import purescala.Extractors._
case object OptimisticGround extends Rule("Optimistic Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (!p.as.isEmpty && !p.xs.isEmpty) {
- val res = new RuleInstantiation(p, this, SolutionBuilder.none) {
+ val res = new RuleInstantiation(p, this, SolutionBuilder.none, this.name) {
def apply(sctx: SynthesisContext) = {
- val solver = new TimeoutSolver(sctx.solver, 100L) // We give that 100ms
+ val solver = sctx.simpleSolver // Optimistic ground is given a simple solver (uninterpreted)
val xss = p.xs.toSet
val ass = p.as.toSet
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 2ae957da30dc98e0b5e5903c331a08a9ac089cd7..2572aebccb6712f17ddd6e867e306be6f3592a59 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -20,7 +20,7 @@ case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
None
}
- List(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess, this.name))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 9b7ea42304e2f6271a888984c5cdb6375a7ab8b3..88b9c806efe92699934f6e7b61c6d5830596c3aa 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -27,7 +27,7 @@ object Unification {
val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
- List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward, this.name))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index b97ff9033b44c7e926c86362ace2fb6497399e65..a3b21fc28a1128562276886e668c947a505e3f75 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -13,7 +13,7 @@ case object UnusedInput extends NormalizingRule("UnusedInput") {
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
- List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), forward, this.name))
} else {
Nil
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 8227a0e9faaca71b7952383d4a1800c027d22623..a289e40ca469a08d9205a36212b2041e7b6849e8 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -201,5 +201,30 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
parent.expandLeaf(this, succ)
}
}
+
+ def getStatus: (Int, Int) = {
+ var total: Int = 0
+ var closed: Int = 0
+
+ def tr(t: Tree, isParentClosed: Boolean) {
+ val isClosed = isParentClosed || t.isSolved || t.isUnsolvable
+ if (isClosed) {
+ closed += 1
+ }
+ total += 1
+
+ t match {
+ case an: AndNode =>
+ an.subProblems.values.foreach(tr(_, isClosed))
+ case on: OrNode =>
+ (on.alternatives.values ++ on.triedAlternatives.values).foreach(tr(_, isClosed))
+ case _ =>
+ }
+ }
+
+ tr(tree, false)
+
+ (closed, total)
+ }
}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index 79e70aecf1c6a9b58de398aaffa094c09bfc4632..d4f5e94168610634ff0b38e692b749502fe63e9c 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -103,4 +103,37 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
processing -= ol
}
+
+ def traversePathFrom(n: g.Tree, path: List[Int]): Option[g.Tree] = {
+ n match {
+ case l: g.Leaf =>
+ assert(path.isEmpty)
+ Some(l)
+ case an: g.AndNode =>
+ path match {
+ case x :: xs =>
+ traversePathFrom(an.subProblems(an.subTasks(x)), xs)
+ case Nil =>
+ Some(an)
+ }
+
+ case on: g.OrNode =>
+ path match {
+ case x :: xs =>
+ val t = on.altTasks(x)
+ if (on.triedAlternatives contains t) {
+ None
+ } else {
+ traversePathFrom(on.alternatives(t), xs)
+ }
+
+ case Nil =>
+ Some(on)
+ }
+ }
+ }
+
+ def traversePath(path: List[Int]): Option[g.Tree] = {
+ traversePathFrom(g.tree, path)
+ }
}
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 8cb4c5fa741aaccafe7834c96b37a38ecebeb225..04998922b5d4b16e8f4ec38613121515774aa809 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -76,7 +76,7 @@ object Benchmarks extends App {
for (file <- ctx.files) {
val innerCtx = ctx.copy(files = List(file))
- val opts = SynthesizerOptions()
+ val opts = SynthesisOptions()
val pipeline = leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
@@ -85,15 +85,19 @@ object Benchmarks extends App {
val solver = new FairZ3Solver(ctx.copy(reporter = new SilentReporter))
solver.setProgram(program)
+ val simpleSolver = new UninterpretedZ3Solver(ctx.copy(reporter = new SilentReporter))
+ simpleSolver.setProgram(program)
+
for ((f, ps) <- results.toSeq.sortBy(_._1.id.toString); p <- ps) {
val sctx = SynthesisContext(
- context = ctx,
- options = opts,
+ context = ctx,
+ options = opts,
functionContext = Some(f),
- program = program,
- solver = solver,
- reporter = new DefaultReporter,
- shouldStop = new java.util.concurrent.atomic.AtomicBoolean
+ program = program,
+ solver = solver,
+ simpleSolver = simpleSolver,
+ reporter = new DefaultReporter,
+ shouldStop = new java.util.concurrent.atomic.AtomicBoolean
)
val ts = System.currentTimeMillis
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 5ac64e8da43ca437c0fee36e1ad87f17fd10ad13..24b154cc1339a92683ad8def03b34231a12c6cc7 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -21,13 +21,116 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
)
+ def generateVerificationConditions(reporter: Reporter, program: Program, functionsToAnalyse: Set[String]) : List[VerificationCondition] = {
+ val defaultTactic = new DefaultTactic(reporter)
+ defaultTactic.setProgram(program)
+ val inductionTactic = new InductionTactic(reporter)
+ inductionTactic.setProgram(program)
+
+ var allVCs: Seq[VerificationCondition] = Seq.empty
+ val analysedFunctions: MutableSet[String] = MutableSet.empty
+
+ for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (functionsToAnalyse.isEmpty || functionsToAnalyse.contains(funDef.id.name))) {
+ analysedFunctions += funDef.id.name
+
+ val tactic: Tactic =
+ if(funDef.annotations.contains("induct")) {
+ inductionTactic
+ } else {
+ defaultTactic
+ }
+
+ if(funDef.body.isDefined) {
+ allVCs ++= tactic.generatePreconditions(funDef)
+ allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
+ allVCs ++= tactic.generatePostconditions(funDef)
+ allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+ allVCs ++= tactic.generateArrayAccessChecks(funDef)
+ }
+ allVCs = allVCs.sortWith((vc1, vc2) => {
+ val id1 = vc1.funDef.id.name
+ val id2 = vc2.funDef.id.name
+ if(id1 != id2) id1 < id2 else vc1 < vc2
+ })
+ }
+
+ val notFound = functionsToAnalyse -- analysedFunctions
+ notFound.foreach(fn => reporter.error("Did not find function \"" + fn + "\" though it was marked for analysis."))
+
+ allVCs.toList
+ }
+
+ def checkVerificationConditions(reporter: Reporter, solvers: Seq[Solver], vcs: Seq[VerificationCondition]) : VerificationReport = {
+ for(vcInfo <- vcs) {
+ val funDef = vcInfo.funDef
+ val vc = vcInfo.condition
+
+ reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
+ reporter.info("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
+ reporter.info(simplifyLets(vc))
+
+ // try all solvers until one returns a meaningful answer
+ var superseeded : Set[String] = Set.empty[String]
+ solvers.find(se => {
+ reporter.info("Trying with solver: " + se.name)
+ if(superseeded(se.name) || superseeded(se.description)) {
+ reporter.info("Solver was superseeded. Skipping.")
+ false
+ } else {
+ superseeded = superseeded ++ Set(se.superseeds: _*)
+
+ val t1 = System.nanoTime
+ se.init()
+ val (satResult, counterexample) = se.solveSAT(Not(vc))
+ val solverResult = satResult.map(!_)
+
+ val t2 = System.nanoTime
+ val dt = ((t2 - t1) / 1000000) / 1000.0
+
+ solverResult match {
+ case None => false
+ case Some(true) => {
+ reporter.info("==== VALID ====")
+
+ vcInfo.value = Some(true)
+ vcInfo.solvedWith = Some(se)
+ vcInfo.time = Some(dt)
+
+ true
+ }
+ case Some(false) => {
+ reporter.error("Found counter-example : ")
+ reporter.error(counterexample.toSeq.sortBy(_._1.name).map(p => p._1 + " -> " + p._2).mkString("\n"))
+ reporter.error("==== INVALID ====")
+ vcInfo.value = Some(false)
+ vcInfo.solvedWith = Some(se)
+ vcInfo.counterExample = Some(counterexample)
+ vcInfo.time = Some(dt)
+
+ true
+ }
+ }
+ }
+ }) match {
+ case None => {
+ reporter.warning("No solver could prove or disprove the verification condition.")
+ }
+ case _ =>
+ }
+
+ }
+
+ val report = new VerificationReport(vcs)
+ report
+ }
+
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
- val functionsToAnalyse : MutableSet[String] = MutableSet.empty
+ var functionsToAnalyse = Set[String]()
var timeout: Option[Int] = None
for(opt <- ctx.options) opt match {
case LeonValueOption("functions", ListValue(fs)) =>
- functionsToAnalyse ++= fs
+ functionsToAnalyse = Set() ++ fs
case v @ LeonValueOption("timeout", _) =>
timeout = v.asInt(ctx)
@@ -49,111 +152,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
solvers.foreach(_.setProgram(program))
- val defaultTactic = new DefaultTactic(reporter)
- defaultTactic.setProgram(program)
- val inductionTactic = new InductionTactic(reporter)
- inductionTactic.setProgram(program)
-
- def generateVerificationConditions : List[VerificationCondition] = {
- var allVCs: Seq[VerificationCondition] = Seq.empty
- val analysedFunctions: MutableSet[String] = MutableSet.empty
-
- for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (functionsToAnalyse.isEmpty || functionsToAnalyse.contains(funDef.id.name))) {
- analysedFunctions += funDef.id.name
-
- val tactic: Tactic =
- if(funDef.annotations.contains("induct")) {
- inductionTactic
- } else {
- defaultTactic
- }
-
- if(funDef.body.isDefined) {
- allVCs ++= tactic.generatePreconditions(funDef)
- allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
- allVCs ++= tactic.generatePostconditions(funDef)
- allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
- allVCs ++= tactic.generateArrayAccessChecks(funDef)
- }
- allVCs = allVCs.sortWith((vc1, vc2) => {
- val id1 = vc1.funDef.id.name
- val id2 = vc2.funDef.id.name
- if(id1 != id2) id1 < id2 else vc1 < vc2
- })
- }
-
- val notFound = functionsToAnalyse -- analysedFunctions
- notFound.foreach(fn => reporter.error("Did not find function \"" + fn + "\" though it was marked for analysis."))
-
- allVCs.toList
- }
-
- def checkVerificationConditions(vcs: Seq[VerificationCondition]) : VerificationReport = {
- for(vcInfo <- vcs) {
- val funDef = vcInfo.funDef
- val vc = vcInfo.condition
-
- reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
- reporter.info("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
- reporter.info(simplifyLets(vc))
-
- // try all solvers until one returns a meaningful answer
- var superseeded : Set[String] = Set.empty[String]
- solvers.find(se => {
- reporter.info("Trying with solver: " + se.name)
- if(superseeded(se.name) || superseeded(se.description)) {
- reporter.info("Solver was superseeded. Skipping.")
- false
- } else {
- superseeded = superseeded ++ Set(se.superseeds: _*)
-
- val t1 = System.nanoTime
- se.init()
- val (satResult, counterexample) = se.solveSAT(Not(vc))
- val solverResult = satResult.map(!_)
-
- val t2 = System.nanoTime
- val dt = ((t2 - t1) / 1000000) / 1000.0
-
- solverResult match {
- case None => false
- case Some(true) => {
- reporter.info("==== VALID ====")
-
- vcInfo.value = Some(true)
- vcInfo.solvedWith = Some(se)
- vcInfo.time = Some(dt)
-
- true
- }
- case Some(false) => {
- reporter.error("Found counter-example : ")
- reporter.error(counterexample.toSeq.sortBy(_._1.name).map(p => p._1 + " -> " + p._2).mkString("\n"))
- reporter.error("==== INVALID ====")
- vcInfo.value = Some(false)
- vcInfo.solvedWith = Some(se)
- vcInfo.time = Some(dt)
-
- true
- }
- }
- }
- }) match {
- case None => {
- reporter.warning("No solver could prove or disprove the verification condition.")
- }
- case _ =>
- }
-
- }
-
- val report = new VerificationReport(vcs)
- report
- }
-
val report = if(solvers.size > 1) {
reporter.info("Running verification condition generation...")
- checkVerificationConditions(generateVerificationConditions)
+ val vcs = generateVerificationConditions(reporter, program, functionsToAnalyse)
+ checkVerificationConditions(reporter, solvers, vcs)
} else {
reporter.warning("No solver specified. Cannot test verification conditions.")
VerificationReport.emptyReport
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 893fb39b3a0cbd22485f1fb0d10230d8cb8fd2b9..a8cbfb51b041a367b2b63c27eba653a34b9f84a1 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -14,6 +14,7 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
var value : Option[Boolean] = None
var solvedWith : Option[Solver] = None
var time : Option[Double] = None
+ var counterExample : Option[Map[Identifier, Expr]] = None
def status : String = value match {
case None => "unknown"
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index c567a85dcc98959c00c4821de45dbcf3ac8ffc85..5eb20b284178ad8009b1caad89c4b86e6240c23e 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -88,4 +88,32 @@ object TreeOps {
treeCatamorphism(convert, combine, compute, expr)
}
+ trait ScopeSimplifier extends purescala.TreeOps.ScopeSimplifier {
+ override def rec(e: Expr, scope: Scope) = e match {
+ case LetDef(fd: FunDef, body: Expr) =>
+ val newId = genId(fd.id, scope)
+ var newScope = scope.register(fd.id -> newId)
+
+ val newArgs = for(VarDecl(id, tpe) <- fd.args) yield {
+ val newArg = genId(id, newScope)
+ newScope = newScope.register(id -> newArg)
+ VarDecl(newArg, tpe)
+ }
+
+ val newFd = new FunDef(newId, fd.returnType, newArgs)
+
+ newScope = newScope.registerFunDef(fd -> newFd)
+
+ newFd.body = fd.body.map(b => rec(b, newScope))
+ newFd.precondition = fd.precondition.map(pre => rec(pre, newScope))
+ newFd.postcondition = fd.postcondition.map(post => rec(post, newScope))
+
+
+ LetDef(newFd, rec(body, newScope))
+
+ case _ =>
+ super.rec(e, scope)
+ }
+ }
+
}
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 13fded9dc87ac2b3635b1c045acda927ab01227e..0517d7ee3ae04aab8c889f4877410f87ae365b92 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -357,12 +357,13 @@ object Trees {
tp: (TypeTree, StringBuffer, Int) => Unit,
dp: (Definition, StringBuffer, Int) => Unit
): StringBuffer = {
- sb.append("\n")
+ sb.append("{\n")
dp(fd, sb, lvl+1)
sb.append("\n")
sb.append("\n")
ind(sb, lvl)
ep(body, sb, lvl)
+ sb.append("}\n")
sb
}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 567d30abb14c99eaf01340fd38fd809d2d0c8f4b..686a968c450e2e2b0899634e571a416da0696f46 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -33,7 +33,7 @@ class SynthesisSuite extends FunSuite {
reporter = new SilentReporter
)
- val opts = SynthesizerOptions()
+ val opts = SynthesisOptions()
val pipeline = leon.plugin.TemporaryInputPhase andThen leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
@@ -42,9 +42,19 @@ class SynthesisSuite extends FunSuite {
val solver = new FairZ3Solver(ctx)
solver.setProgram(program)
+ val simpleSolver = new FairZ3Solver(ctx)
+ simpleSolver.setProgram(program)
+
for ((f, ps) <- results; p <- ps) {
test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, title)) {
- val sctx = SynthesisContext(ctx, opts, Some(f), program, solver, new DefaultReporter, new java.util.concurrent.atomic.AtomicBoolean)
+ val sctx = SynthesisContext(ctx,
+ opts,
+ Some(f),
+ program,
+ solver,
+ simpleSolver,
+ new DefaultReporter,
+ new java.util.concurrent.atomic.AtomicBoolean)
block(sctx, f, p)
}
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/ADTInduction.scala
index bf7d8b16da99ee33830617c4e4bd6a4a71c0a67d..7487247cda198b0a6f51cf7a39f2f922f6736eda 100644
--- a/testcases/synthesis/ADTInduction.scala
+++ b/testcases/synthesis/ADTInduction.scala
@@ -25,12 +25,21 @@ object SortedList {
// content(out) == (content(Nil()) -- Set(v))
//}
- def deleteSynth(in: List, v: Int) = choose {
- (out: List) =>
- // This spec is too weak. Maybe use later as bad example?
- //!(content(out) contains v) && size(out)+1 >= size(in)
- (content(out) == (content(in) -- Set(v)))
- }
+ def deleteSynth(in: List, v: Int) = (in match {
+ case Cons(head22, tail21) =>
+ (tail21 match {
+ case Cons(head23, tail23) =>
+ (choose { (out: List) =>
+ (content(out) == (content(Cons(head22, Cons(head23, tail23))) -- Set(v)))
+ })
+ case _ =>
+ (choose { (out: List) =>
+ (content(out) == (content(Cons(head22, Nil())) -- Set(v)))
+ })
+ })
+ case _ =>
+ Nil()
+ })
def concatSynth(in1: List, in2: List) = choose {
(out : List) =>
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index ad729b296b42ae5b301b8a70fe5273dbed9d945e..6fbac66487957764fbc9ab103ec80624618f1f8a 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -3,22 +3,54 @@ import leon.Utils._
// Examples taken from http://lara.epfl.ch/~psuter/spt/
object SynthesisProceduresToolkit {
- def e1(a: Nat, b: Nat, c: Nat): Nat = choose( (x: Nat) => x != a && x != b && x != c)
+ def e1(a: Nat, b: Nat, c: Nat): Nat = if ((b == c)) {
+ if ((a == c)) {
+ (choose { (x: Nat) =>
+ (x != a)
+ })
+ } else {
+ (choose { (x: Nat) =>
+ ((x != a) && (x != b))
+ })
+ }
+} else {
+ if ((a == b)) {
+ (choose { (x: Nat) =>
+ ((x != a) && (x != c))
+ })
+ } else {
+ (choose { (x: Nat) =>
+ ((x != a) && (x != b) && (x != c))
+ })
+ }
+}
- def e2(): (Nat, Nat, Nat) = choose( (x: Nat, y: Nat, z: Nat) => x != y && y != z && x != z)
+ def e2(): (Nat, Nat, Nat) = (Z(), Succ(Z()), Succ(Succ(Succ(Z()))))
- def e3(a1 : Nat, a2 : Nat, a3 : Nat, a4 : Nat): (Nat, Nat) = choose( (x1 : Nat, x2 : Nat) => Cons(x1, Cons(x2, Nil())) == Cons(a3, Cons(a4, Nil())) && Cons(a1, Cons(a2, Nil())) != Cons(x1, Cons(x2, Nil())))
+ def e3(a1 : Nat, a2 : Nat, a3 : Nat, a4 : Nat): (Nat, Nat) = (a3, a4)
- def e4(a1 : Nat, a2 : Nat, a3 : Nat, a4 : Nat): (Nat, Nat, NatList) = choose( (x1 : Nat, x2 : Nat, x3 : NatList) => Cons(x1, Cons(x2, Nil())) != Cons(a1, Cons(a2, Nil())))
+ def e4(a1 : Nat, a2 : Nat, a3 : Nat, a4 : Nat): (Nat, Nat, NatList) = (Succ(a2), a1, Nil())
- def e5(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) => Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4)))
+ def e5(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = (choose { (x1: Nat, x2: NatList, x3: Nat, x4: NatList) =>
+ ((Cons(Succ(x1), x2) == a1) && (Succ(x1) != a2) && (a3 == Cons(x3, Cons(x3, x4))))
+})
- def e6(a: Nat, b: Nat): (Nat, NatList) = choose( (x: Nat, y: NatList) => a == Succ(b))
+ def e6(a: Nat, b: Nat): (Nat, NatList) = if ((a == Succ(b))) {
+ (Z(), Nil())
+} else {
+ leon.Utils.error[(Nat, NatList)]("Precondition failed")
+}
- def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) =>
- Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4)) || (a1 == a3 && x1 == x3))
+ def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = (choose { (x1: Nat, x2: NatList, x3: Nat, x4: NatList) =>
+ ((Cons(Succ(x1), x2) == a1) && (Succ(x1) != a2) && (a3 == Cons(x3, Cons(x3, x4))))
+})
- def e8(a : Nat) = choose { (x : Nat) => Succ(x) == a }
+ def e8(a : Nat) = (a match {
+ case Succ(n150) =>
+ n150
+ case _ =>
+ leon.Utils.error[(Nat)]("Precondition failed")
+})
abstract class Nat
case class Z() extends Nat