diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index dc2352d4adeda982c03b73592265e51970435f0b..91999a0143ca394f3047a48201fda2c0eb9498bb 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1078,18 +1078,22 @@ object TreeOps {
case IfExpr(cond, then, elze) =>
val TopLevelOrs(orcases) = toDNF(cond)
- if (!orcases.tail.isEmpty) {
- pre(IfExpr(orcases.head, then, IfExpr(Or(orcases.tail), then, elze)))
- } else {
- val TopLevelAnds(andcases) = orcases.head
+ if (orcases.exists{ case TopLevelAnds(ands) => ands.exists(_.isInstanceOf[CaseClassInstanceOf]) } ) {
+ if (!orcases.tail.isEmpty) {
+ pre(IfExpr(orcases.head, then, IfExpr(Or(orcases.tail), then, elze)))
+ } else {
+ val TopLevelAnds(andcases) = orcases.head
- val (andis, andnotis) = andcases.partition(_.isInstanceOf[CaseClassInstanceOf])
+ val (andis, andnotis) = andcases.partition(_.isInstanceOf[CaseClassInstanceOf])
- if (andis.isEmpty || andnotis.isEmpty) {
- e
- } else {
- IfExpr(And(andis), IfExpr(And(andnotis), then, elze), elze)
+ if (andis.isEmpty || andnotis.isEmpty) {
+ e
+ } else {
+ IfExpr(And(andis), IfExpr(And(andnotis), then, elze), elze)
+ }
}
+ } else {
+ e
}
case _ =>
e
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 01aea89f986c7263cb312763864006714581057c..03e29dfcdaf39353d9458daed39a130e0b348c86 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -87,6 +87,10 @@ object TypeTrees {
case _ => None
}
+ def isSubtypeOf(t1: TypeTree, t2: TypeTree): Boolean = {
+ leastUpperBound(t1, t2) == Some(t2)
+ }
+
// returns the number of distinct values that inhabit a type
sealed abstract class TypeSize extends Serializable
case class FiniteSize(size: Int) extends TypeSize
diff --git a/src/main/scala/leon/synthesis/Complexity.scala b/src/main/scala/leon/synthesis/Complexity.scala
index c12f3c3f9b94403a7a739f02c1d6b29e68f921eb..2f09637d4738ad3b6eea8bc632487e96b561cec1 100644
--- a/src/main/scala/leon/synthesis/Complexity.scala
+++ b/src/main/scala/leon/synthesis/Complexity.scala
@@ -16,10 +16,10 @@ abstract class AbsSolComplexity extends Complexity[AbsSolComplexity] {
case class SolComplexity(s: Solution) extends AbsSolComplexity {
lazy val value = {
- val chooses = collectChooses(s.term)
+ val chooses = collectChooses(s.toExpr)
val chooseCost = chooses.foldLeft(0)((i, c) => i + (1000 * math.pow(2, c.vars.size).toInt + formulaSize(c.pred)))
- formulaSize(s.pre) + formulaSize(s.term) + chooseCost
+ formulaSize(s.toExpr) + chooseCost
}
}
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index ad716afe102a94e38eec7eb23c58886e3f8517d6..21c0a408c40d78b575f70483a84ed325275c4674 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -10,7 +10,6 @@ import purescala.Definitions._
object Heuristics {
def all = Set[Synthesizer => Rule](
- new OptimisticGround(_),
new IntInduction(_),
new OptimisticInjection(_)
)
@@ -22,62 +21,6 @@ trait Heuristic {
override def toString = "H: "+name
}
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) with Heuristic {
- def applyOn(task: Task): RuleResult = {
- val p = task.problem
-
- if (!p.as.isEmpty && !p.xs.isEmpty) {
- val xss = p.xs.toSet
- val ass = p.as.toSet
-
- val tpe = TupleType(p.xs.map(_.getType))
-
- var i = 0;
- var maxTries = 3;
-
- var result: Option[RuleResult] = None
- var predicates: Seq[Expr] = Seq()
-
- while (result.isEmpty && i < maxTries) {
- val phi = And(p.phi +: predicates)
- synth.solver.solveSAT(phi) match {
- case (Some(true), satModel) =>
- val satXsModel = satModel.filterKeys(xss)
-
- val newPhi = valuateWithModelIn(phi, xss, satModel)
-
- synth.solver.solveSAT(Not(newPhi)) match {
- case (Some(true), invalidModel) =>
- // Found as such as the xs break, refine predicates
- predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
-
- case (Some(false), _) =>
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
-
- case _ =>
- result = Some(RuleInapplicable)
- }
-
- case (Some(false), _) =>
- if (predicates.isEmpty) {
- result = Some(RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe))))
- } else {
- result = Some(RuleInapplicable)
- }
- case _ =>
- result = Some(RuleInapplicable)
- }
-
- i += 1
- }
-
- result.getOrElse(RuleInapplicable)
- } else {
- RuleInapplicable
- }
- }
-}
-
class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) with Heuristic {
def applyOn(task: Task): RuleResult = {
@@ -103,8 +46,16 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
val onSuccess: List[Solution] => Solution = {
case List(base, gt, lt) =>
+ val preIn = Or(Seq(And(Equals(Variable(inductOn), IntLiteral(0)), base.pre),
+ And(GreaterThan(Variable(inductOn), IntLiteral(0)), gt.pre),
+ And(LessThan(Variable(inductOn), IntLiteral(0)), lt.pre)))
+ val preOut = subst(inductOn -> Variable(origId), preIn)
+
val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
- newFun.body = Some(
+
+ newFun.precondition = Some(preIn)
+
+ newFun.body = Some(
IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
base.toExpr,
IfExpr(GreaterThan(Variable(inductOn), IntLiteral(0)),
@@ -112,7 +63,8 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80)
, LetTuple(postXs, FunctionInvocation(newFun, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
)
- Solution(BooleanLiteral(true), LetDef(newFun, FunctionInvocation(newFun, Seq(Variable(origId)))))
+
+ Solution(preOut, base.defs++gt.defs++lt.defs+newFun, FunctionInvocation(newFun, Seq(Variable(origId))))
case _ =>
Solution.none
}
@@ -195,3 +147,4 @@ class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth,
}
}
}
+
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index fc711b1e717eb570da1e25023e9db4cac55deb03..af3e7b8053f8c2f47b52a17f517f31dfe3be341c 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -7,6 +7,7 @@ import purescala.Trees._
import purescala.Extractors._
import purescala.TreeOps._
import purescala.TypeTrees._
+import purescala.Definitions._
object Rules {
def all = Set[Synthesizer => Rule](
@@ -18,6 +19,8 @@ object Rules {
new CaseSplit(_),
new UnusedInput(_),
new UnconstrainedOutput(_),
+ new OptimisticGround(_),
+ new CEGIS(_),
new Assert(_)
)
}
@@ -42,7 +45,7 @@ abstract class Rule(val name: String, val synth: Synthesizer, val priority: Prio
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
val forward: List[Solution] => Solution = {
- case List(s) => Solution(s.pre, s.term)
+ case List(s) => Solution(s.pre, s.defs, s.term)
case _ => Solution.none
}
@@ -72,11 +75,11 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 300) {
val newProblem = Problem(p.as, p.c, subst(x -> e, And(others)), oxs)
val onSuccess: List[Solution] => Solution = {
- case List(Solution(pre, term)) =>
+ case List(Solution(pre, defs, term)) =>
if (oxs.isEmpty) {
- Solution(pre, Tuple(e :: Nil))
+ Solution(pre, defs, Tuple(e :: Nil))
} else {
- Solution(pre, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))))
+ Solution(pre, defs, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))))
}
case _ => Solution.none
}
@@ -98,9 +101,9 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 500) {
synth.solver.solveSAT(p.phi) match {
case (Some(true), model) =>
- RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
+ RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
case (Some(false), model) =>
- RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe)))
+ RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
case _ =>
RuleInapplicable
}
@@ -119,7 +122,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 200) {
val sub2 = Problem(p.as, p.c, o2, p.xs)
val onSuccess: List[Solution] => Solution = {
- case List(Solution(p1, t1), Solution(p2, t2)) => Solution(Or(p1, p2), IfExpr(p1, t1, t2))
+ case List(Solution(p1, d1, t1), Solution(p2, d2, t2)) => Solution(Or(p1, p2), d1++d2, IfExpr(p1, t1, t2))
case _ => Solution.none
}
@@ -142,7 +145,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
if (!exprsA.isEmpty) {
if (others.isEmpty) {
- RuleSuccess(Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
+ RuleSuccess(Solution(And(exprsA), Set(), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
} else {
val sub = p.copy(c = And(p.c +: exprsA), phi = And(others))
@@ -160,7 +163,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 100) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
- val unused = p.as.toSet -- variablesOf(p.phi)
+ val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.c)
if (!unused.isEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
@@ -182,7 +185,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
val onSuccess: List[Solution] => Solution = {
case List(s) =>
- Solution(s.pre, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(Variable(id)) else Variable(id)))))
+ Solution(s.pre, s.defs, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(Variable(id)) else Variable(id)))))
case _ =>
Solution.none
}
@@ -242,7 +245,7 @@ object Unification {
if (isImpossible) {
val tpe = TupleType(p.xs.map(_.getType))
- RuleSuccess(Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe)))
+ RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe)))
} else {
RuleInapplicable
}
@@ -278,3 +281,234 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
}
}
+class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 50) {
+ def applyOn(task: Task): RuleResult = {
+ val p = task.problem
+
+ case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
+
+ var generators = Map[TypeTree, Generator]()
+ def getGenerator(t: TypeTree): Generator = generators.get(t) match {
+ case Some(g) => g
+ case None =>
+ val alternatives: () => List[(Expr, Set[Identifier])] = t match {
+ case BooleanType =>
+ { () => List((BooleanLiteral(true), Set()), (BooleanLiteral(false), Set())) }
+
+ case Int32Type =>
+ { () => List((IntLiteral(0), Set()), (IntLiteral(1), Set())) }
+
+ case TupleType(tps) =>
+ { () =>
+ val ids = tps.map(t => FreshIdentifier("t", true).setType(t))
+ List((Tuple(ids.map(Variable(_))), ids.toSet))
+ }
+
+ case CaseClassType(cd) =>
+ { () =>
+ val ids = cd.fieldsIds.map(i => FreshIdentifier("c", true).setType(i.getType))
+ List((CaseClass(cd, ids.map(Variable(_))), ids.toSet))
+ }
+
+ case AbstractClassType(cd) =>
+ { () =>
+ val alts: Seq[(Expr, Set[Identifier])] = cd.knownDescendents.flatMap(i => i match {
+ case acd: AbstractClassDef =>
+ synth.reporter.error("Unnexpected abstract class in descendants!")
+ None
+ case cd: CaseClassDef =>
+ val ids = cd.fieldsIds.map(i => FreshIdentifier("c", true).setType(i.getType))
+ Some((CaseClass(cd, ids.map(Variable(_))), ids.toSet))
+ })
+ alts.toList
+ }
+
+ case _ =>
+ synth.reporter.error("Can't construct generator. Unsupported type: "+t+"["+t.getClass+"]");
+ { () => Nil }
+ }
+ val g = Generator(t, alternatives)
+ generators += t -> g
+ g
+ }
+
+ def inputAlternatives(t: TypeTree): List[(Expr, Set[Identifier])] = {
+ p.as.filter(a => isSubtypeOf(a.getType, t)).map(id => (Variable(id) : Expr, Set[Identifier]()))
+ }
+
+ case class TentativeFormula(phi: Expr,
+ program: Expr,
+ mappings: Map[Identifier, (Identifier, Expr)],
+ recTerms: Map[Identifier, Set[Identifier]]) {
+ def unroll: TentativeFormula = {
+ var newProgram = List[Expr]()
+ var newRecTerms = Map[Identifier, Set[Identifier]]()
+ var newMappings = Map[Identifier, (Identifier, Expr)]()
+
+ for ((_, recIds) <- recTerms; recId <- recIds) {
+ val gen = getGenerator(recId.getType)
+ val alts = gen.altBuilder() ::: inputAlternatives(recId.getType)
+
+ val altsWithBranches = alts.map(alt => FreshIdentifier("b", true).setType(BooleanType) -> alt)
+
+ val bvs = altsWithBranches.map(alt => Variable(alt._1))
+ val distinct = if (bvs.size > 1) {
+ (for (i <- (1 to bvs.size-1); j <- 0 to i-1) yield {
+ Or(Not(bvs(i)), Not(bvs(j)))
+ }).toList
+ } else {
+ List(BooleanLiteral(true))
+ }
+ val pre = And(Or(bvs) :: distinct) // (b1 OR b2) AND (Not(b1) OR Not(b2))
+ val cases = for((bid, (ex, rec)) <- altsWithBranches.toList) yield { // b1 => E(gen1, gen2) [b1 -> {gen1, gen2}]
+ if (!rec.isEmpty) {
+ newRecTerms += bid -> rec
+ }
+ newMappings += bid -> (recId -> ex)
+
+ Implies(Variable(bid), Equals(Variable(recId), ex))
+ }
+
+ newProgram = newProgram ::: pre :: cases
+ }
+
+ TentativeFormula(phi, And(program :: newProgram), mappings ++ newMappings, newRecTerms)
+ }
+
+ def bounds = recTerms.keySet.map(id => Not(Variable(id))).toList
+ def bss = mappings.keySet
+
+ def entireFormula = And(phi :: program :: bounds)
+ }
+
+ var result: Option[RuleResult] = None
+
+ var ass = p.as.toSet
+ var xss = p.xs.toSet
+
+ var lastF = TentativeFormula(Implies(p.c, p.phi), BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
+ var currentF = lastF.unroll
+ var unrolings = 0
+ val maxUnrolings = 2
+ do {
+ //println("Was: "+lastF.entireFormula)
+ //println("Now Trying : "+currentF.entireFormula)
+
+ val tpe = TupleType(p.xs.map(_.getType))
+ val bss = currentF.bss
+
+ var predicates: Seq[Expr] = Seq()
+ var continue = true
+
+ while (result.isEmpty && continue) {
+ val basePhi = currentF.entireFormula
+ val constrainedPhi = And(basePhi +: predicates)
+ //println("-"*80)
+ //println("To satisfy: "+constrainedPhi)
+ synth.solver.solveSAT(constrainedPhi) match {
+ case (Some(true), satModel) =>
+ //println("Found candidate!: "+satModel.filterKeys(bss))
+
+ //println("Corresponding program: "+simplifyTautologies(synth.solver)(valuateWithModelIn(currentF.program, bss, satModel)))
+ val fixedBss = And(bss.map(b => Equals(Variable(b), satModel(b))).toSeq)
+ //println("Phi with fixed sat bss: "+fixedBss)
+
+ val counterPhi = Implies(And(fixedBss, currentF.program), currentF.phi)
+ //println("Formula to validate: "+counterPhi)
+
+ synth.solver.solveSAT(Not(counterPhi)) match {
+ case (Some(true), invalidModel) =>
+ // Found as such as the xs break, refine predicates
+ //println("Found counter EX: "+invalidModel)
+ predicates = Not(And(bss.map(b => Equals(Variable(b), satModel(b))).toSeq)) +: predicates
+ //println("Let's avoid this case: "+bss.map(b => Equals(Variable(b), satModel(b))).mkString(" "))
+
+ case (Some(false), _) =>
+ //println("Sat model: "+satModel.toSeq.sortBy(_._1.toString).map{ case (id, v) => id+" -> "+v }.mkString(", "))
+ var mapping = currentF.mappings.filterKeys(satModel.mapValues(_ == BooleanLiteral(true))).values.toMap
+
+ //println("Mapping: "+mapping)
+
+ // Resolve mapping
+ for ((c, e) <- mapping) {
+ mapping += c -> substAll(mapping, e)
+ }
+
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
+
+ case _ =>
+ }
+
+ case (Some(false), _) =>
+ //println("%%%% UNSAT")
+ continue = false
+ case _ =>
+ //println("%%%% WOOPS")
+ continue = false
+ }
+ }
+
+ lastF = currentF
+ currentF = currentF.unroll
+ unrolings += 1
+ } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty)
+
+ result.getOrElse(RuleInapplicable)
+ }
+}
+
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) {
+ def applyOn(task: Task): RuleResult = {
+ val p = task.problem
+
+ if (!p.as.isEmpty && !p.xs.isEmpty) {
+ val xss = p.xs.toSet
+ val ass = p.as.toSet
+
+ val tpe = TupleType(p.xs.map(_.getType))
+
+ var i = 0;
+ var maxTries = 3;
+
+ var result: Option[RuleResult] = None
+ var predicates: Seq[Expr] = Seq()
+
+ while (result.isEmpty && i < maxTries) {
+ val phi = And(p.phi +: predicates)
+ synth.solver.solveSAT(phi) match {
+ case (Some(true), satModel) =>
+ val satXsModel = satModel.filterKeys(xss)
+
+ val newPhi = valuateWithModelIn(phi, xss, satModel)
+
+ synth.solver.solveSAT(Not(newPhi)) match {
+ case (Some(true), invalidModel) =>
+ // Found as such as the xs break, refine predicates
+ predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
+
+ case (Some(false), _) =>
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
+
+ case _ =>
+ result = Some(RuleInapplicable)
+ }
+
+ case (Some(false), _) =>
+ if (predicates.isEmpty) {
+ result = Some(RuleSuccess(Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))))
+ } else {
+ result = Some(RuleInapplicable)
+ }
+ case _ =>
+ result = Some(RuleInapplicable)
+ }
+
+ i += 1
+ }
+
+ result.getOrElse(RuleInapplicable)
+ } else {
+ RuleInapplicable
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index a1ecacaa28368eb211db8e0a1edd50095c659bd4..cf2561de50e05f13613afedbf89a193b03092e34 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -2,23 +2,26 @@ package leon
package synthesis
import leon.purescala.Trees._
+import leon.purescala.Definitions._
import leon.purescala.TreeOps._
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
-class Solution(val pre: Expr, val term: Expr) {
- override def toString = "⟨ "+pre+" | "+term+" ⟩"
+class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
+ override def toString = "⟨ "+pre+" | "+defs.mkString(" ")+" "+term+" ⟩"
lazy val complexity: AbsSolComplexity = new SolComplexity(this)
def toExpr = {
- if (pre == BooleanLiteral(true)) {
+ val result = if (pre == BooleanLiteral(true)) {
term
} else if (pre == BooleanLiteral(false)) {
Error("Impossible program").setType(term.getType)
} else {
IfExpr(pre, term, Error("Precondition failed").setType(term.getType))
}
+
+ defs.foldLeft(result){ case (t, fd) => LetDef(fd, t) }
}
}
@@ -26,19 +29,19 @@ object Solution {
def simplify(e: Expr) = simplifyLets(e)
- def apply(pre: Expr, term: Expr) = {
- new Solution(simplify(pre), simplify(term))
+ def apply(pre: Expr, defs: Set[FunDef], term: Expr) = {
+ new Solution(simplify(pre), defs, simplify(term))
}
- def unapply(s: Solution): Option[(Expr, Expr)] = if (s eq null) None else Some((s.pre, s.term))
+ def unapply(s: Solution): Option[(Expr, Set[FunDef], Expr)] = if (s eq null) None else Some((s.pre, s.defs, s.term))
def choose(p: Problem): Solution = {
- new Solution(BooleanLiteral(true), Choose(p.xs, p.phi))
+ new Solution(BooleanLiteral(true), Set(), Choose(p.xs, p.phi))
}
// Generate the simplest, wrongest solution, used for complexity lowerbound
def basic(p: Problem): Solution = {
- new Solution(BooleanLiteral(true), Tuple(p.xs.map(id => simplestValue(id.getType))))
+ new Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(id => simplestValue(id.getType))))
}
def none: Solution = {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index ba8ec79c42f157b67381e56eb16611bad3af23e8..a811fe6b72c00cd89e068b086d76cb645632d336 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -42,9 +42,11 @@ class Synthesizer(val reporter: Reporter,
val ts = System.currentTimeMillis
+ def currentDurationMs = System.currentTimeMillis-ts
+
def timeoutExpired(): Boolean = {
timeoutMs match {
- case Some(t) if (System.currentTimeMillis-ts)/1000 > t => true
+ case Some(t) if currentDurationMs/1000 > t => true
case _ => false
}
}
@@ -64,6 +66,8 @@ class Synthesizer(val reporter: Reporter,
}
}
+ info("Finished in "+currentDurationMs+"ms")
+
if (generateDerivationTrees) {
val deriv = new DerivationTree(rootTask)
deriv.toDotFile("derivation"+derivationCounter+".dot")
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index ed3bd980d09ba83c4bb668bf61bfbdf2a3b41622..1176c19a7ebe56facba15555817f6804e719d3c2 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -56,6 +56,7 @@ class Task(synth: Synthesizer,
steps = new TaskStep(newProblems) :: steps
} else {
solution = Some(onSuccess(solutions))
+
parent.partlySolvedBy(this, solution.get)
}
}
@@ -80,8 +81,8 @@ class Task(synth: Synthesizer,
parent.partlySolvedBy(this, solution)
val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
- println(prefix+"Got: "+problem)
- println(prefix+"Solved with: "+solution)
+ synth.reporter.info(prefix+"Got: "+problem)
+ synth.reporter.info(prefix+"Solved with: "+solution)
Nil
case RuleMultiSteps(subProblems, interSteps, onSuccess) =>
@@ -96,10 +97,10 @@ class Task(synth: Synthesizer,
val simplestSolution = onSuccess(simplestSubSolutions)
minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
- println(prefix+"Got: "+problem)
- println(prefix+"Decomposed into:")
+ synth.reporter.info(prefix+"Got: "+problem)
+ synth.reporter.info(prefix+"Decomposed into:")
for(p <- subProblems) {
- println(prefix+" - "+p)
+ synth.reporter.info(prefix+" - "+p)
}
subProblems
@@ -121,8 +122,10 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
}
override def partlySolvedBy(t: Task, s: Solution) {
- solution = Some(s)
- solver = Some(t)
+ if (isBetterSolutionThan(s, solution)) {
+ solution = Some(s)
+ solver = Some(t)
+ }
}
override def unsolvedBy(t: Task) {
diff --git a/testcases/synthesis/Injection.scala b/testcases/synthesis/Injection.scala
new file mode 100644
index 0000000000000000000000000000000000000000..32c91ccad03674a50cd5cfb38f745fb091a046e1
--- /dev/null
+++ b/testcases/synthesis/Injection.scala
@@ -0,0 +1,24 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Injection {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ // proved with unrolling=0
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+
+ def listOfSizeSynth(in: List, i: Int) = choose{out: List => (size(out) == i) && (size(in) == i) }
+ def listOfSizeSynth2(i: Int) = choose{out: List => size(out) == i }
+
+ def subProblem(in: List, i: Int) = choose{out: List => (size(out) == i) && (size(in)+1 == i) }
+ def simple(in: List) = choose{out: List => size(out) == size(in) }
+
+ def invalidInjection(in: List, i: Int) = choose{out: List => (size(out) == i) && (size(in) == i) && in != out }
+}
diff --git a/testcases/synthesis/SimplestCegis.scala b/testcases/synthesis/SimplestCegis.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d0c5c44d8555c4e50c463df5f921762fe9242b8f
--- /dev/null
+++ b/testcases/synthesis/SimplestCegis.scala
@@ -0,0 +1,17 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Injection {
+ sealed abstract class List
+ case class Cons(tail: List) extends List
+ case class Nil() extends List
+
+ // proved with unrolling=0
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def simple(in: List) = choose{out: List => size(out) == size(in) }
+}