From 1a6a2be33d4bfa34727bc5134ac3a4614be8ef0b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 18:08:24 +0200
Subject: [PATCH] ADTDual
---
.../scala/leon/purescala/Definitions.scala | 2 ++
src/main/scala/leon/synthesis/Rules.scala | 36 +++++++++++++++++++
.../scala/leon/synthesis/Synthesizer.scala | 2 +-
testcases/synthesis/Unification.scala | 2 ++
4 files changed, 41 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 3c18e858f..d39d8abf5 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -246,6 +246,8 @@ object Definitions {
fields.map(f => f.id).toSet
}
+ def fieldsIds = fields.map(_.id)
+
def selectorID2Index(id: Identifier) : Int = {
var i : Int = 0
var found = false
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 5afcb0f5a..1c045aabb 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -9,6 +9,7 @@ object Rules {
def all(synth: Synthesizer) = List(
new Unification.DecompTrivialClash(synth),
new Unification.OccursCheck(synth),
+ new ADTDual(synth),
new OnePoint(synth),
new Ground(synth),
new CaseSplit(synth),
@@ -243,3 +244,38 @@ object Unification {
}
}
}
+
+
+class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth) {
+ def isApplicable(task: Task): List[DecomposedTask] = {
+ val p = task.problem
+
+ val xs = p.xs.toSet
+ val as = p.as.toSet
+
+ val TopLevelAnds(exprs) = p.phi
+
+
+ val (toRemove, toAdd, toPre) = exprs.collect {
+ case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+ (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) )
+ case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+ (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) )
+ }.unzip3
+
+ if (!toRemove.isEmpty) {
+ val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
+
+ val onSuccess: List[Solution] => Solution = {
+ case List(s) =>
+ Solution(And(s.pre +: toPre), s.term)
+ case _ =>
+ Solution.none
+ }
+
+ List(task.decompose(this, List(sub), onSuccess, 80))
+ } else {
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 44a049134..2b927cad0 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -64,11 +64,11 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
}
def onTaskSucceeded(task: Task, solution: Solution) {
+ info(" => Solved "+task.problem+" ⊢ "+solution)
if (task.parent eq null) {
info(" SUCCESS!")
this.solution = Some(solution)
} else {
- info(" => Solved "+task.problem+" ⊢ "+solution)
task.parent.subSucceeded(task.problem, solution)
}
}
diff --git a/testcases/synthesis/Unification.scala b/testcases/synthesis/Unification.scala
index b98f7acd3..c2b111352 100644
--- a/testcases/synthesis/Unification.scala
+++ b/testcases/synthesis/Unification.scala
@@ -12,6 +12,8 @@ object UnificationSynthesis {
def u5(a1: Int): List = choose { (xs: List) => Cons(a1, Nil()) == xs }
+ def u6(a1: List): Int = choose { (xs: Int) => Cons(xs, Nil()) == a1 }
+
sealed abstract class List
case class Nil() extends List
case class Cons(head : Int, tail : List) extends List
--
GitLab