diff --git a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala index 5a33b0d8b0b35e3dd44c2fbf6ebf45eb3f8a962e..8ed9ed14e43e81cf7bcdfe10143b8627bf40e182 100644 --- a/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala +++ b/src/test/scala/leon/regression/synthesis/StablePrintingSuite.scala @@ -10,6 +10,7 @@ import leon.purescala.ScalaPrinter import leon.purescala.PrinterContext import leon.purescala.PrinterOptions import leon.synthesis._ +import leon.synthesis.rules._ import scala.collection.mutable.Stack import scala.io.Source @@ -28,6 +29,27 @@ class StablePrintingSuite extends LeonRegressionSuite { private def testIterativeSynthesis(cat: String, f: File, depth: Int) { + val decompRules = List[Rule]( + Unification.DecompTrivialClash, + Unification.OccursCheck, // probably useless + Disunification.Decomp, + ADTDual, + CaseSplit, + IfSplit, + UnusedInput, + EquivalentInputs, + UnconstrainedOutput, + OptimisticGround, + EqualitySplit, + InequalitySplit, + rules.Assert, + DetupleOutput, + DetupleInput, + ADTSplit, + IntInduction, + InnerCaseSplit + ) + def getChooses(ctx: LeonContext, content: String): (Program, SynthesisSettings, Seq[ChooseInfo]) = { val opts = SynthesisSettings() val pipeline = leon.utils.TemporaryInputPhase andThen @@ -85,7 +107,7 @@ class StablePrintingSuite extends LeonRegressionSuite { val hctx = SearchContext(sctx, ci, search.g.root, search) val problem = ci.problem info(j.info("synthesis "+problem.asString(sctx.context))) - val apps = sctx.rules flatMap { _.instantiateOn(hctx, problem)} + val apps = decompRules flatMap { _.instantiateOn(hctx, problem)} for (a <- apps) { a.apply(hctx) match {