Skip to content
Snippets Groups Projects
Commit 61211735 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Only rely on decomposing rules so that we don't waste time testing

printing of cegis result
parent bec7c1af
No related branches found
No related tags found
No related merge requests found
...@@ -10,6 +10,7 @@ import leon.purescala.ScalaPrinter ...@@ -10,6 +10,7 @@ import leon.purescala.ScalaPrinter
import leon.purescala.PrinterContext import leon.purescala.PrinterContext
import leon.purescala.PrinterOptions import leon.purescala.PrinterOptions
import leon.synthesis._ import leon.synthesis._
import leon.synthesis.rules._
import scala.collection.mutable.Stack import scala.collection.mutable.Stack
import scala.io.Source import scala.io.Source
...@@ -28,6 +29,27 @@ class StablePrintingSuite extends LeonRegressionSuite { ...@@ -28,6 +29,27 @@ class StablePrintingSuite extends LeonRegressionSuite {
private def testIterativeSynthesis(cat: String, f: File, depth: Int) { 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]) = { def getChooses(ctx: LeonContext, content: String): (Program, SynthesisSettings, Seq[ChooseInfo]) = {
val opts = SynthesisSettings() val opts = SynthesisSettings()
val pipeline = leon.utils.TemporaryInputPhase andThen val pipeline = leon.utils.TemporaryInputPhase andThen
...@@ -85,7 +107,7 @@ class StablePrintingSuite extends LeonRegressionSuite { ...@@ -85,7 +107,7 @@ class StablePrintingSuite extends LeonRegressionSuite {
val hctx = SearchContext(sctx, ci, search.g.root, search) val hctx = SearchContext(sctx, ci, search.g.root, search)
val problem = ci.problem val problem = ci.problem
info(j.info("synthesis "+problem.asString(sctx.context))) 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) { for (a <- apps) {
a.apply(hctx) match { a.apply(hctx) match {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment