From 035e8bb59d037442324e08b9a95cf5bb8c431379 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 4 Apr 2013 15:24:28 +0200
Subject: [PATCH] ADTDual and Unification become normalizing rules
---
src/main/scala/leon/synthesis/rules/ADTDual.scala | 7 ++++---
src/main/scala/leon/synthesis/rules/Unification.scala | 4 ++--
2 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 41202315d..57c31c998 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
-case object ADTDual extends Rule("ADTDual") {
+case object ADTDual extends NormalizingRule("ADTDual") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val xs = p.xs.toSet
val as = p.as.toSet
@@ -15,9 +15,10 @@ case object ADTDual extends Rule("ADTDual") {
val (toRemove, toAdd) = exprs.collect {
- case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+ case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && !(variablesOf(cc) & xs).isEmpty =>
(eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } )
- case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+
+ case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && !(variablesOf(cc) & xs).isEmpty =>
(eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } )
}.unzip
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 88b9c806e..005f13eed 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -8,7 +8,7 @@ import purescala.TreeOps._
import purescala.Extractors._
object Unification {
- case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.") {
+ case object DecompTrivialClash extends NormalizingRule("Unif Dec./Clash/Triv.") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
@@ -36,7 +36,7 @@ object Unification {
// This rule is probably useless; it never happens except in crafted
// examples, and will be found by OptimisticGround anyway.
- case object OccursCheck extends Rule("Unif OccursCheck") {
+ case object OccursCheck extends NormalizingRule("Unif OccursCheck") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
--
GitLab