From f37f0bd4df0dbdbc139844ae98ca0487313c064f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 12 Feb 2016 18:35:07 +0100
Subject: [PATCH] Rerwiting of integer/comparison rules. Cleaning up.
terminatingCalls now returns calls with integers too.
IntInduction and all integer comparison rules are phased out. Instead
there is a single InequalitySplit rules which splits into (up to) 3 branches,
taking pc into account.
No more EqualitySplit for any other type, except generic types.
Isolate unused rules. Clean up Rules.
Improve QualifiedExamplesBank API
---
src/main/scala/leon/repair/rules/Focus.scala | 2 +-
.../scala/leon/synthesis/ExamplesBank.scala | 36 +++--
src/main/scala/leon/synthesis/Rules.scala | 31 +----
.../leon/synthesis/rules/EqualitySplit.scala | 61 ---------
.../rules/GenericTypeEqualitySplit.scala | 72 ++++++++++
.../synthesis/rules/InequalitySplit.scala | 126 +++++++++++-------
.../rules/{ => unused}/ADTInduction.scala | 2 +-
.../rules/{ => unused}/ADTLongInduction.scala | 2 +-
.../rules/{ => unused}/AsChoose.scala | 6 +-
.../rules/{ => unused}/BottomUpTegis.scala | 2 +-
.../rules/{ => unused}/DetupleOutput.scala | 2 +-
.../rules/{ => unused}/IntInduction.scala | 12 +-
.../rules/{ => unused}/IntegerEquation.scala | 2 +-
.../{ => unused}/IntegerInequalities.scala | 2 +-
.../{ => unused}/OptimisticInjection.scala | 2 +-
.../{ => unused}/SelectiveInlining.scala | 6 +-
.../rules/{ => unused}/SygusCVC4.scala | 4 +-
.../synthesis/rules/{ => unused}/TEGIS.scala | 2 +-
.../rules/{ => unused}/TEGISLike.scala | 2 +-
.../rules/{ => unused}/TEGLESS.scala | 3 +-
.../scala/leon/synthesis/utils/Helpers.scala | 11 +-
.../synthesis/StablePrintingSuite.scala | 2 -
synthesis-collective.txt | 2 +-
.../current/RunLength/RunLength.scala | 8 --
24 files changed, 214 insertions(+), 186 deletions(-)
delete mode 100644 src/main/scala/leon/synthesis/rules/EqualitySplit.scala
create mode 100644 src/main/scala/leon/synthesis/rules/GenericTypeEqualitySplit.scala
rename src/main/scala/leon/synthesis/rules/{ => unused}/ADTInduction.scala (99%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/ADTLongInduction.scala (99%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/AsChoose.scala (79%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/BottomUpTegis.scala (99%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/DetupleOutput.scala (98%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/IntInduction.scala (95%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/IntegerEquation.scala (99%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/IntegerInequalities.scala (99%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/OptimisticInjection.scala (98%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/SelectiveInlining.scala (90%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/SygusCVC4.scala (90%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/TEGIS.scala (94%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/TEGISLike.scala (99%)
rename src/main/scala/leon/synthesis/rules/{ => unused}/TEGLESS.scala (96%)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 943a5a67f..7ce3fd261 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -164,7 +164,7 @@ case object Focus extends PreprocessingRule("Focus") {
val eb3 = if (vars.nonEmpty) {
eb2.mapIns(ebF)
} else {
- eb2
+ eb2.eb
}
val newPc = andJoin(cond +: vars.map { id => equality(id.toVariable, map(id)) })
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 1da37b350..35a698686 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -160,38 +160,44 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
object ExamplesBank {
def empty = ExamplesBank(Nil, Nil)
+
}
/** Same as an ExamplesBank, but with identifiers corresponding to values. This
* allows us to evaluate expressions. */
case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb: ExamplesBank)(implicit hctx: SearchContext) {
- def removeOuts(toRemove: Set[Identifier]) = {
+ def removeOuts(toRemove: Set[Identifier]): QualifiedExamplesBank = {
+ val nxs = xs.filterNot(toRemove)
val toKeep = xs.zipWithIndex.filterNot(x => toRemove(x._1)).map(_._2)
- eb mapOuts { out => List(toKeep.map(out)) }
+ QualifiedExamplesBank(as, nxs, eb mapOuts { out => List(toKeep.map(out)) })
}
def removeIns(toRemove: Set[Identifier]) = {
+ val nas = as.filterNot(toRemove)
val toKeep: List[Int] = as.zipWithIndex.filterNot(a => toRemove(a._1)).map(_._2)
- eb mapIns { (in: Seq[Expr]) => List(toKeep.map(in)) }
+
+ QualifiedExamplesBank(nas, xs, eb mapIns { (in: Seq[Expr]) => List(toKeep.map(in)) })
}
/** Filter inputs throught expr which is an expression evaluating to a boolean */
- def filterIns(expr: Expr): ExamplesBank = {
+ def filterIns(expr: Expr): QualifiedExamplesBank = {
filterIns(m => hctx.defaultEvaluator.eval(expr, m).result == Some(BooleanLiteral(true)))
}
/** Filters inputs through the predicate pred, with an assignment of input variables to expressions. */
- def filterIns(pred: Map[Identifier, Expr] => Boolean): ExamplesBank = {
- eb mapIns { in =>
- val m = (as zip in).toMap
- if(pred(m)) {
- List(in)
- } else {
- Nil
+ def filterIns(pred: Map[Identifier, Expr] => Boolean): QualifiedExamplesBank = {
+ QualifiedExamplesBank(as, xs,
+ eb mapIns { in =>
+ val m = (as zip in).toMap
+ if(pred(m)) {
+ List(in)
+ } else {
+ Nil
+ }
}
- }
+ )
}
/** Maps inputs through the function f
@@ -206,3 +212,9 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
}
}
}
+
+import scala.language.implicitConversions
+
+object QualifiedExamplesBank {
+ implicit def qebToEb(qeb: QualifiedExamplesBank): ExamplesBank = qeb.eb
+}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index f55c670f4..ff92b251e 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -51,26 +51,15 @@ object Rules {
UnusedInput,
EquivalentInputs,
UnconstrainedOutput,
+ if(naiveGrammar) NaiveCEGIS else CEGIS,
OptimisticGround,
- EqualitySplit,
+ GenericTypeEqualitySplit,
InequalitySplit,
IntroduceRecCalls,
- if(naiveGrammar) NaiveCEGIS else CEGIS,
- //TEGIS,
- //BottomUpTEGIS,
rules.Assert,
- //DetupleOutput, // Subsumed by IndependentSplit
DetupleInput,
ADTSplit,
- //IntegerEquation,
- //IntegerInequalities,
- IntInduction,
InnerCaseSplit
- //new OptimisticInjection(_),
- //new SelectiveInlining(_),
- //ADTLongInduction,
- //ADTInduction
- //AngelicHoles // @EK: Disabled now as it is explicit with withOracle { .. }
)
}
@@ -212,20 +201,4 @@ trait RuleDSL {
case _ => None
}
-
- /** Straightforward combination of solutions, where expression is reconstructed according to a combiner.
- * If combiner fails, no solution will be returned.
- *
- * @param combiner The combiner of synthesized subterms which reconstructs the term of the solution from the subterms.
- */
- def simpleCombine(combiner: PartialFunction[List[Expr], Expr]): List[Solution] => Option[Solution] = { ls =>
- combiner.lift(ls map (_.term)).map{ combined =>
- Solution(
- orJoin(ls map (_.pre)),
- ls.flatMap (_.defs).toSet,
- combined,
- ls.forall(_.isTrusted)
- )
- }
- }
}
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
deleted file mode 100644
index 6f6eea54f..000000000
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ /dev/null
@@ -1,61 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package synthesis
-package rules
-
-import purescala.Common.Identifier
-import purescala.Expressions._
-import purescala.Extractors._
-import purescala.Constructors._
-
-/** For every pair of input variables of the same type,
- * checks equality and output an If-Then-Else statement with the two new branches. */
-case object EqualitySplit extends Rule("Eq. Split") {
- def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- // We approximate knowledge of equality based on facts found at the top-level
- // we don't care if the variables are known to be equal or not, we just
- // don't want to split on two variables for which only one split
- // alternative is viable. This should be much less expensive than making
- // calls to a solver for each pair.
- var facts = Set[Set[Identifier]]()
-
- def addFacts(e: Expr): Unit = e match {
- case Not(e) => addFacts(e)
- case LessThan(Variable(a), Variable(b)) => facts += Set(a,b)
- case LessEquals(Variable(a), Variable(b)) => facts += Set(a,b)
- case GreaterThan(Variable(a), Variable(b)) => facts += Set(a,b)
- case GreaterEquals(Variable(a), Variable(b)) => facts += Set(a,b)
- case Equals(Variable(a), Variable(b)) => facts += Set(a,b)
- case _ =>
- }
-
- val TopLevelAnds(as) = and(p.pc, p.phi)
- for (e <- as) {
- addFacts(e)
- }
-
- val candidates = p.as.groupBy(_.getType).mapValues{ as =>
- as.combinations(2).filterNot(facts contains _.toSet)
- }.values.flatten
-
- candidates.flatMap {
- case List(a1, a2) =>
-
- val sub1 = p.copy(
- pc = and(Equals(Variable(a1), Variable(a2)), p.pc),
- eb = p.qeb.filterIns( (m: Map[Identifier, Expr]) => m(a1) == m(a2))
- )
- val sub2 = p.copy(
- pc = and(not(Equals(Variable(a1), Variable(a2))), p.pc),
- eb = p.qeb.filterIns( (m: Map[Identifier, Expr]) => m(a1) != m(a2))
- )
-
- val onSuccess = simpleCombine { case List(s1, s2) => IfExpr(Equals(Variable(a1), Variable(a2)), s1, s2) }
-
- Some(decomp(List(sub1, sub2), onSuccess, s"Eq. Split on '$a1' and '$a2'"))
- case _ =>
- None
- }
- }
-}
diff --git a/src/main/scala/leon/synthesis/rules/GenericTypeEqualitySplit.scala b/src/main/scala/leon/synthesis/rules/GenericTypeEqualitySplit.scala
new file mode 100644
index 000000000..8dce44d68
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/GenericTypeEqualitySplit.scala
@@ -0,0 +1,72 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import leon.purescala.Common.Identifier
+import purescala.Constructors._
+import purescala.Expressions._
+import leon.purescala.Extractors.{IsTyped, TopLevelAnds}
+import purescala.Types._
+
+/** For every pair of input variables of the same generic type,
+ * checks equality and output an If-Then-Else statement with the two new branches.
+ */
+case object GenericTypeEqualitySplit extends Rule("Eq. Split") {
+ def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ // We approximate knowledge of equality based on facts found at the top-level
+ // we don't care if the variables are known to be equal or not, we just
+ // don't want to split on two variables for which only one split
+ // alternative is viable. This should be much less expensive than making
+ // calls to a solver for each pair.
+ def getFacts(e: Expr): Set[Set[Identifier]] = e match {
+ case Not(e) => getFacts(e)
+ case Equals(Variable(a), Variable(b)) => Set(Set(a,b))
+ case _ => Set()
+ }
+
+ val TopLevelAnds(as) = and(p.pc, p.phi)
+
+ val facts = as.flatMap(getFacts).toSet
+
+ val candidates = p.as.combinations(2).collect {
+ case List(IsTyped(a1, TypeParameter(t1)), IsTyped(a2, TypeParameter(t2)))
+ if t1 == t2 && !facts(Set(a1, a2)) =>
+ (a1, a2)
+ }.toList
+
+ candidates.flatMap {
+ case (a1, a2) =>
+ val v1 = Variable(a1)
+ val v2 = Variable(a2)
+ val subProblems = List(
+ p.copy(as = p.as.diff(Seq(a1)),
+ pc = subst(a1 -> v2, p.pc),
+ ws = subst(a1 -> v2, p.ws),
+ phi = subst(a1 -> v2, p.phi),
+ eb = p.qeb.filterIns(Equals(v1, v2)).removeIns(Set(a1))),
+
+ p.copy(pc = and(p.pc, not(Equals(v1, v2))),
+ eb = p.qeb.filterIns(not(Equals(v1, v2))))
+ )
+
+ val onSuccess: List[Solution] => Option[Solution] = {
+ case sols @ List(sEQ, sNE) =>
+ val pre = or(
+ and(Equals(v1, v2), sEQ.pre),
+ and(not(Equals(v1, v2)), sNE.pre)
+ )
+
+ val term = IfExpr(Equals(v1, v2), sEQ.term, sNE.term)
+
+ Some(Solution(pre, sols.flatMap(_.defs).toSet, term, sols.forall(_.isTrusted)))
+ }
+
+ Some(decomp(subProblems, onSuccess, s"Eq. Split on '$v1' and '$v2'"))
+
+ case _ =>
+ None
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index db41c6c3b..54445a5d4 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -8,65 +8,99 @@ import purescala.Expressions._
import purescala.Types._
import purescala.Constructors._
import purescala.Extractors._
-import purescala.Common._
+/** For every pair of variables of an integer type plus 0 of that type,
+ * splits for inequality between these variables
+ * and reconstructs the subproblems with a (nested) if-then-else.
+ *
+ * Takes into account knowledge about equality/inequality in the path condition.
+ *
+ */
case object InequalitySplit extends Rule("Ineq. Split.") {
+
+ // Represents NEGATIVE knowledge
+ private abstract class Fact {
+ val l: Expr
+ val r: Expr
+ }
+ private case class LT(l: Expr, r: Expr) extends Fact
+ private case class EQ(l: Expr, r: Expr) extends Fact
+
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- // We approximate knowledge of equality based on facts found at the top-level
- // we don't care if the variables are known to be equal or not, we just
- // don't want to split on two variables for which only one split
- // alternative is viable. This should be much less expensive than making
- // calls to a solver for each pair.
val TopLevelAnds(as) = and(p.pc, p.phi)
- def addFacts(e: Expr): Set[Identifier] = e match {
- case Not(e) => addFacts(e)
- case LessThan(Variable(a), Variable(b)) => Set(a,b)
- case LessEquals(Variable(a), Variable(b)) => Set(a,b)
- case GreaterThan(Variable(a), Variable(b)) => Set(a,b)
- case GreaterEquals(Variable(a), Variable(b)) => Set(a,b)
- case Equals(Variable(a), Variable(b)) => Set(a,b)
+
+ def getFacts(e: Expr): Set[Fact] = e match {
+ case LessThan(a, b) => Set(LT(b,a), EQ(a,b))
+ case LessEquals(a, b) => Set(LT(b,a))
+ case GreaterThan(a, b) => Set(LT(a,b), EQ(a,b))
+ case GreaterEquals(a, b) => Set(LT(a,b))
+ case Equals(a, b) => Set(LT(a,b), LT(b,a))
+ case Not(LessThan(a, b)) => Set(LT(a,b))
+ case Not(LessEquals(a, b)) => Set(LT(a,b), EQ(a,b))
+ case Not(GreaterThan(a, b)) => Set(LT(b,a))
+ case Not(GreaterEquals(a, b)) => Set(LT(b,a), EQ(a,b))
+ case Not(Equals(a, b)) => Set(EQ(a,b))
case _ => Set()
}
- val facts = as map addFacts
-
- val argsPairs = p.as.filter(_.getType == IntegerType).combinations(2) ++
- p.as.filter(_.getType == Int32Type).combinations(2)
-
- val candidates = argsPairs.toList.filter { case List(a1, a2) => !(facts contains Set(a1, a2)) }
-
- candidates.collect {
- case List(a1, a2) =>
- val onSuccess = simpleCombine {
- case sols@List(sLT, sEQ, sGT) =>
- IfExpr(
- LessThan(Variable(a1), Variable(a2)),
- sLT,
- IfExpr(
- Equals(Variable(a1), Variable(a2)),
- sEQ,
- sGT
- )
- )
- }
- val subTypes = List(p.outType, p.outType, p.outType)
+ val facts = as flatMap getFacts
+
+ val candidates =
+ (p.as.map(_.toVariable).filter(_.getType == Int32Type) :+ IntLiteral(0)).combinations(2).toList ++
+ (p.as.map(_.toVariable).filter(_.getType == IntegerType) :+ InfiniteIntegerLiteral(0)).combinations(2).toList
- new RuleInstantiation(s"Ineq. Split on '$a1' and '$a2'",
- SolutionBuilderDecomp(subTypes, onSuccess)) {
+ candidates.flatMap {
+ case List(v1, v2) =>
- def apply(hctx: SearchContext) = {
- implicit val _ = hctx
+ val lt = if (!facts.contains(LT(v1, v2))) {
+ val pc = LessThan(v1, v2)
+ Some(pc, p.copy(pc = and(p.pc, pc), eb = p.qeb.filterIns(pc)))
+ } else None
- val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc),
- eb = p.qeb.filterIns(LessThan(Variable(a1), Variable(a2))))
- val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc),
- eb = p.qeb.filterIns(Equals(Variable(a1), Variable(a2))))
- val subGT = p.copy(pc = and(GreaterThan(Variable(a1), Variable(a2)), p.pc),
- eb = p.qeb.filterIns(GreaterThan(Variable(a1), Variable(a2))))
+ val gt = if (!facts.contains(LT(v2, v1))) {
+ val pc = GreaterThan(v1, v2)
+ Some(pc, p.copy(pc = and(p.pc, pc), eb = p.qeb.filterIns(pc)))
+ } else None
- RuleExpanded(List(subLT, subEQ, subGT))
+ val eq = if (!facts.contains(EQ(v1, v2)) && !facts.contains(EQ(v2,v1))) {
+ val pc = Equals(v1, v2)
+ // One of v1, v2 will be an input variable
+ val a1 = (v1, v2) match {
+ case (Variable(a), _) => a
+ case (_, Variable(a)) => a
}
+ val newP = p.copy(
+ as = p.as.diff(Seq(a1)),
+ pc = subst(a1 -> v2, p.pc),
+ ws = subst(a1 -> v2, p.ws),
+ phi = subst(a1 -> v2, p.phi),
+ eb = p.qeb.filterIns(Equals(v1, v2)).removeIns(Set(a1))
+ )
+ Some(pc, newP)
+ } else None
+
+ val (pcs, subProblems) = List(eq, lt, gt).flatten.unzip
+
+ if (pcs.size < 2) None
+ else {
+
+ val onSuccess: List[Solution] => Option[Solution] = { sols =>
+ val pre = orJoin(pcs.zip(sols).map { case (pc, sol) =>
+ and(pc, sol.pre)
+ })
+
+ val term = pcs.zip(sols) match {
+ case Seq((pc1, s1), (_, s2)) =>
+ IfExpr(pc1, s1.term, s2.term)
+ case Seq((pc1, s1), (pc2, s2), (_, s3)) =>
+ IfExpr(pc1, s1.term, IfExpr(pc2, s2.term, s3.term))
+ }
+
+ Some(Solution(pre, sols.flatMap(_.defs).toSet, term, sols.forall(_.isTrusted)))
+ }
+
+ Some(decomp(subProblems, onSuccess, s"Ineq. Split on '$v1' and '$v2'"))
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/unused/ADTInduction.scala
similarity index 99%
rename from src/main/scala/leon/synthesis/rules/ADTInduction.scala
rename to src/main/scala/leon/synthesis/rules/unused/ADTInduction.scala
index 90738c698..ab2720fb0 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/ADTInduction.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Common._
import purescala.Expressions._
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/unused/ADTLongInduction.scala
similarity index 99%
rename from src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
rename to src/main/scala/leon/synthesis/rules/unused/ADTLongInduction.scala
index d14c2b0f8..4ffd1a8c2 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/ADTLongInduction.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Common._
import purescala.Expressions._
diff --git a/src/main/scala/leon/synthesis/rules/AsChoose.scala b/src/main/scala/leon/synthesis/rules/unused/AsChoose.scala
similarity index 79%
rename from src/main/scala/leon/synthesis/rules/AsChoose.scala
rename to src/main/scala/leon/synthesis/rules/unused/AsChoose.scala
index 7f231b85d..06270b939 100644
--- a/src/main/scala/leon/synthesis/rules/AsChoose.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/AsChoose.scala
@@ -1,8 +1,8 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
-package synthesis
-package rules
+package leon.synthesis.rules.unused
+
+import leon.synthesis._
case object AsChoose extends Rule("As Choose") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
similarity index 99%
rename from src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
rename to src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
index 5dbcbb3a1..8f82395a5 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/BottomUpTegis.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Expressions._
import purescala.Common._
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/unused/DetupleOutput.scala
similarity index 98%
rename from src/main/scala/leon/synthesis/rules/DetupleOutput.scala
rename to src/main/scala/leon/synthesis/rules/unused/DetupleOutput.scala
index a1d219340..18067e952 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/DetupleOutput.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Expressions._
import purescala.Common._
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/unused/IntInduction.scala
similarity index 95%
rename from src/main/scala/leon/synthesis/rules/IntInduction.scala
rename to src/main/scala/leon/synthesis/rules/unused/IntInduction.scala
index bfebd3929..6ef209fcb 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/IntInduction.scala
@@ -2,14 +2,14 @@
package leon
package synthesis
-package rules
+package rules.unused
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Extractors._
+import purescala.Common.FreshIdentifier
import purescala.Constructors._
-import purescala.Types._
-import purescala.Definitions._
+import purescala.Definitions.{FunDef, ValDef}
+import purescala.Expressions._
+import purescala.Extractors.IsTyped
+import purescala.Types.IntegerType
case object IntInduction extends Rule("Int Induction") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/unused/IntegerEquation.scala
similarity index 99%
rename from src/main/scala/leon/synthesis/rules/IntegerEquation.scala
rename to src/main/scala/leon/synthesis/rules/unused/IntegerEquation.scala
index f51d90075..fdb59b00d 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/IntegerEquation.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Common._
import purescala.Expressions._
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala
similarity index 99%
rename from src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
rename to src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala
index dfb1fa8d6..602a7e61b 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Common._
import purescala.Expressions._
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala b/src/main/scala/leon/synthesis/rules/unused/OptimisticInjection.scala
similarity index 98%
rename from src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
rename to src/main/scala/leon/synthesis/rules/unused/OptimisticInjection.scala
index 599fbd5df..b3d35f8a0 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/OptimisticInjection.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Expressions._
import purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala b/src/main/scala/leon/synthesis/rules/unused/SelectiveInlining.scala
similarity index 90%
rename from src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
rename to src/main/scala/leon/synthesis/rules/unused/SelectiveInlining.scala
index 446938213..9dd4e68e0 100644
--- a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/SelectiveInlining.scala
@@ -2,11 +2,11 @@
package leon
package synthesis
-package rules
+package rules.unused
-import purescala.Expressions._
-import purescala.Extractors._
import purescala.Constructors._
+import purescala.Expressions.{Equals, Expr, FunctionInvocation}
+import purescala.Extractors.TopLevelAnds
case object SelectiveInlining extends Rule("Sel. Inlining") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala b/src/main/scala/leon/synthesis/rules/unused/SygusCVC4.scala
similarity index 90%
rename from src/main/scala/leon/synthesis/rules/SygusCVC4.scala
rename to src/main/scala/leon/synthesis/rules/unused/SygusCVC4.scala
index d458de88c..800d1e5f8 100644
--- a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/SygusCVC4.scala
@@ -2,9 +2,9 @@
package leon
package synthesis
-package rules
+package rules.unused
-import solvers.sygus._
+import leon.solvers.sygus.CVC4SygusSolver
case object SygusCVC4 extends Rule("SygusCVC4") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/rules/TEGIS.scala b/src/main/scala/leon/synthesis/rules/unused/TEGIS.scala
similarity index 94%
rename from src/main/scala/leon/synthesis/rules/TEGIS.scala
rename to src/main/scala/leon/synthesis/rules/unused/TEGIS.scala
index 242502a16..7b08304dc 100644
--- a/src/main/scala/leon/synthesis/rules/TEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/TEGIS.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Types._
import grammars._
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
similarity index 99%
rename from src/main/scala/leon/synthesis/rules/TEGISLike.scala
rename to src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
index a085ad436..cd6382864 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/TEGISLike.scala
@@ -2,7 +2,7 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Expressions._
import purescala.Types._
diff --git a/src/main/scala/leon/synthesis/rules/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/unused/TEGLESS.scala
similarity index 96%
rename from src/main/scala/leon/synthesis/rules/TEGLESS.scala
rename to src/main/scala/leon/synthesis/rules/unused/TEGLESS.scala
index f87968ea3..a58a0b138 100644
--- a/src/main/scala/leon/synthesis/rules/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/unused/TEGLESS.scala
@@ -2,11 +2,10 @@
package leon
package synthesis
-package rules
+package rules.unused
import purescala.Types._
import purescala.Extractors._
-import utils._
import Witnesses._
import grammars._
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 87d9c587c..a0b940958 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -61,9 +61,19 @@ object Helpers {
case _ => None
}
+ val z = InfiniteIntegerLiteral(0)
+ val one = InfiniteIntegerLiteral(1)
val knownSmallers = clauses.collect {
case Equals(v: Variable, s@CaseClassSelector(cct, r, _)) => subExprsOf(s, v)
case Equals(s@CaseClassSelector(cct, r, _), v: Variable) => subExprsOf(s, v)
+ case GreaterThan(v: Variable, `z`) =>
+ Some(v -> Minus(v, one))
+ case LessThan(`z`, v: Variable) =>
+ Some(v -> Minus(v, one))
+ case LessThan(v: Variable, `z`) =>
+ Some(v -> Plus(v, one))
+ case GreaterThan(`z`, v: Variable) =>
+ Some(v -> Plus(v, one))
}.flatten.groupBy(_._1).mapValues(v => v.map(_._2))
def argsSmaller(e: Expr, tpe: TypeTree): Seq[Expr] = e match {
@@ -74,7 +84,6 @@ object Helpers {
}.flatten
case v: Variable =>
knownSmallers.getOrElse(v, Seq())
-
case _ => Nil
}
diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
index da7f51f4f..6ab235dd5 100644
--- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala
@@ -42,10 +42,8 @@ class StablePrintingSuite extends LeonRegressionSuite {
OptimisticGround,
InequalitySplit,
rules.Assert,
- DetupleOutput,
DetupleInput,
ADTSplit,
- IntInduction,
InnerCaseSplit
)
diff --git a/synthesis-collective.txt b/synthesis-collective.txt
index 5085e1dcc..f2cbedc5d 100644
--- a/synthesis-collective.txt
+++ b/synthesis-collective.txt
@@ -6,7 +6,7 @@ F = Timeout/failed to synth.
============================================================================
-Name | FDefs| Size | O-O-5 | O-O-7 |<current> |
+Name | FDefs| Size | O-O-5 | O-O-7 | 0515ff9 |
============================================================================
List.insert | 59 | 3 | ✓ | 0.8 | ✓ | 1.0 | ✓ | 0.7 |
List.delete | 61 | 0 | ✓ | 4.5 | F | 30.1 | ✓ | 3.2 |
diff --git a/testcases/synthesis/current/RunLength/RunLength.scala b/testcases/synthesis/current/RunLength/RunLength.scala
index fd886180e..8813b97f7 100644
--- a/testcases/synthesis/current/RunLength/RunLength.scala
+++ b/testcases/synthesis/current/RunLength/RunLength.scala
@@ -5,7 +5,6 @@ import leon.collection._
object RunLength {
-
def decode[A](l: List[(BigInt, A)]): List[A] = {
def fill[A](i: BigInt, a: A): List[A] = {
if (i > 0) a :: fill(i - 1, a)
@@ -18,7 +17,6 @@ object RunLength {
}
}
-
def legal[A](l: List[(BigInt, A)]): Boolean = l match {
case Cons((i, x), tl) =>
i > 0 && (tl match {
@@ -28,12 +26,6 @@ object RunLength {
case _ => true
}
- /*def unique[A](l1: List[A], l2: List[A]) => {
- require(encode(l1) == encode(l2))
- l1 == l2
- }.holds*/
-
- // Solvable with --manual=2,0,0,1,0,0,3,0,1,1,0,0,1,0,0,0,1,1,1
def encode[A](l: List[A]): List[(BigInt, A)] = {
// Solution
/*l match {
--
GitLab