From 7d7d96fc7ddfb0dc6fe9ee7701c39a431c84cd08 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 12 Nov 2012 18:28:34 +0100
Subject: [PATCH] Work on the new CEGIS
---
.../scala/leon/synthesis/Heuristics.scala | 88 ++++++++++++++++++-
1 file changed, 87 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index ad716afe1..ce34ab79c 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -11,7 +11,8 @@ import purescala.Definitions._
object Heuristics {
def all = Set[Synthesizer => Rule](
new OptimisticGround(_),
- new IntInduction(_),
+ //new IntInduction(_),
+ new CEGISOnSteroids(_),
new OptimisticInjection(_)
)
}
@@ -195,3 +196,88 @@ class SelectiveInlining(synth: Synthesizer) extends Rule("Sel. Inlining", synth,
}
}
}
+
+class CEGISOnSteroids(synth: Synthesizer) extends Rule("cegis w. gen.", synth, 50) with Heuristic {
+ 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
+ }
+
+ case class TentativeFormula(f: Expr, recTerms: Map[Identifier, Set[Identifier]]) {
+ def unroll: TentativeFormula = {
+ var newF = this.f
+ var newRecTerms = Map[Identifier, Set[Identifier]]()
+ for ((_, recIds) <- recTerms; recId <- recIds) {
+ val gen = getGenerator(recId.getType)
+ val alts = gen.altBuilder().map(alt => FreshIdentifier("b", true) -> alt)
+
+ val pre = Or(alts.map{ case (id, _) => Variable(id) }) // b1 OR b2
+ val cases = for((bid, (ex, rec)) <- alts.toList) yield { // b1 => E(gen1, gen2) [b1 -> {gen1, gen2}]
+ if (!rec.isEmpty) {
+ newRecTerms += bid -> rec
+ }
+ Implies(Variable(bid), Equals(Variable(recId), ex))
+ }
+
+ newF = And(newF, And(pre :: cases))
+ }
+
+ TentativeFormula(newF, newRecTerms)
+ }
+
+ def closedFormula = And(f :: recTerms.keySet.map(id => Not(Variable(id))).toList)
+ }
+
+ println("Formula is: "+p.phi)
+ val initF = TentativeFormula(p.phi, Map() ++ p.xs.map(x => x -> Set(x))) // Set to expand on xs
+ println("unroll 1: "+initF.unroll.closedFormula)
+ println("unroll 2: "+initF.unroll.unroll.closedFormula)
+
+ RuleInapplicable
+ }
+}
--
GitLab