From b55e4e0549546972a608116afef3bf70468917ca Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 14 Apr 2015 19:30:59 +0200
Subject: [PATCH] Introduce GrammarDataGen for using faster evaluators
- Refactor CEGIS options for clearer defaults
---
.../scala/leon/codegen/CodeGenParams.scala | 10 +++-
.../scala/leon/codegen/CompilationUnit.scala | 2 +-
.../codegen/runtime/ChooseEntryPoint.scala | 2 +-
.../scala/leon/datagen/GrammarDataGen.scala | 55 +++++++++++++++++++
.../scala/leon/datagen/NaiveDataGen.scala | 2 +-
.../leon/evaluators/CodeGenEvaluator.scala | 2 +-
.../scala/leon/purescala/Constructors.scala | 42 ++++++++++++++
src/main/scala/leon/purescala/ExprOps.scala | 2 +
src/main/scala/leon/repair/Repairman.scala | 2 +-
.../scala/leon/synthesis/ExamplesFinder.scala | 6 +-
.../scala/leon/synthesis/SynthesisPhase.scala | 21 ++-----
.../leon/synthesis/SynthesisSettings.scala | 11 +---
.../leon/synthesis/rules/BottomUpTegis.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 42 +++++++++-----
.../leon/synthesis/rules/TEGISLike.scala | 2 +-
.../synthesis/utils/ExpressionGrammar.scala | 25 +++++----
16 files changed, 167 insertions(+), 61 deletions(-)
create mode 100644 src/main/scala/leon/datagen/GrammarDataGen.scala
diff --git a/src/main/scala/leon/codegen/CodeGenParams.scala b/src/main/scala/leon/codegen/CodeGenParams.scala
index 97a21a78b..dd0d191b7 100644
--- a/src/main/scala/leon/codegen/CodeGenParams.scala
+++ b/src/main/scala/leon/codegen/CodeGenParams.scala
@@ -4,11 +4,15 @@ package leon
package codegen
case class CodeGenParams (
- maxFunctionInvocations: Int = -1, // Monitor calls and abort execution if more than X calls
- checkContracts: Boolean = false, // Generate calls that checks pre/postconditions
- doInstrument: Boolean = true // Instrument reads to case classes (mainly for vanuatoo)
+ maxFunctionInvocations: Int, // Monitor calls and abort execution if more than X calls
+ checkContracts: Boolean, // Generate calls that checks pre/postconditions
+ doInstrument: Boolean // Instrument reads to case classes (mainly for vanuatoo)
) {
val recordInvocations = maxFunctionInvocations > -1
val requireMonitor = recordInvocations
}
+
+object CodeGenParams {
+ def default = CodeGenParams(maxFunctionInvocations = -1, checkContracts = true, doInstrument = false)
+}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index b166be16b..34fc9097a 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -24,7 +24,7 @@ import java.lang.reflect.Constructor
class CompilationUnit(val ctx: LeonContext,
val program: Program,
- val params: CodeGenParams = CodeGenParams()) extends CodeGeneration {
+ val params: CodeGenParams = CodeGenParams.default) extends CodeGeneration {
val loader = new CafebabeClassLoader(classOf[CompilationUnit].getClassLoader)
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index d91b6e18d..2b31225ff 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -40,7 +40,7 @@ object ChooseEntryPoint {
val program = unit.program
val ctx = unit.ctx
- ctx.reporter.debug("Executing choose!")
+ ctx.reporter.debug("Executing choose (codegen)!")
val is = inputs.toSeq
if (cache contains (i, is)) {
diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
new file mode 100644
index 000000000..da2e54a48
--- /dev/null
+++ b/src/main/scala/leon/datagen/GrammarDataGen.scala
@@ -0,0 +1,55 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package datagen
+
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Definitions._
+import utils.StreamUtils._
+
+import purescala.Definitions._
+import purescala.ExprOps._
+import purescala.Types.TypeTree
+import purescala.Common._
+import purescala.Constructors._
+import purescala.Extractors._
+import evaluators._
+import synthesis.utils._
+import bonsai.enumerators._
+
+import scala.collection.mutable.{Map=>MutableMap}
+
+import synthesis.utils._
+
+/** Utility functions to generate values of a given type.
+ * In fact, it could be used to generate *terms* of a given type,
+ * e.g. by passing trees representing variables for the "bounds". */
+class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar[TypeTree] = ExpressionGrammars.ValueGrammar) extends DataGenerator {
+
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
+ val enum = new MemoizedEnumerator[TypeTree, Expr](grammar.getProductions)
+ val values = enum.iterator(tupleTypeWrap(ins.map{ _.getType }))
+
+ val detupled = values.map {
+ v => unwrapTuple(v, ins.size)
+ }
+
+ def filterCond(vs: Seq[Expr]): Boolean = satisfying match {
+ case BooleanLiteral(true) =>
+ true
+ case e =>
+ // in -> e should be enough. We shouldn't find any subexpressions of in.
+ evaluator.eval(e, (ins zip vs).toMap) match {
+ case EvaluationResults.Successful(BooleanLiteral(true)) => true
+ case _ => false
+ }
+ }
+
+ detupled.take(maxEnumerated)
+ .filter(filterCond)
+ .take(maxValid)
+ }
+
+}
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 70caf95cb..e7034d752 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -42,7 +42,7 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
BooleanLiteral(true) #:: BooleanLiteral(false) #:: Stream.empty
case Int32Type =>
- IntLiteral(0) #:: IntLiteral(1) #:: IntLiteral(-1) #:: Stream.empty
+ IntLiteral(0) #:: IntLiteral(1) #:: IntLiteral(2) #:: IntLiteral(-1) #:: Stream.empty
case tp: TypeParameter =>
tpStream(tp)
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index e097e75c1..52383bec6 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -15,7 +15,7 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
val description = "Evaluator for PureScala expressions based on compilation to JVM"
/** Another constructor to make it look more like other `Evaluator`s. */
- def this(ctx : LeonContext, prog : Program, params: CodeGenParams = CodeGenParams()) {
+ def this(ctx : LeonContext, prog : Program, params: CodeGenParams = CodeGenParams.default) {
this(ctx, new CompilationUnit(ctx, prog, params))
}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 3d3bd42ee..dbb7f361b 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -4,6 +4,7 @@ package leon
package purescala
import Expressions._
+import Extractors._
import ExprOps._
import Definitions._
import TypeOps._
@@ -253,4 +254,45 @@ object Constructors {
case _ => Application(fn, realArgs)
}
+ def equality(a: Expr, b: Expr) = {
+ if (a == b && isDeterministic(a)) {
+ BooleanLiteral(true)
+ } else {
+ Equals(a, b)
+ }
+ }
+
+ def plus(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
+ case (InfiniteIntegerLiteral(bi), _) if bi == 0 => rhs
+ case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => lhs
+ case (IntLiteral(0), _) => rhs
+ case (_, IntLiteral(0)) => lhs
+ case (IsTyped(_, IntegerType), IsTyped(_, IntegerType)) => Plus(lhs, rhs)
+ case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVPlus(lhs, rhs)
+ }
+
+ def minus(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match {
+ case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => lhs
+ case (_, IntLiteral(0)) => lhs
+ case (IsTyped(_, IntegerType), IsTyped(_, IntegerType)) => Minus(lhs, rhs)
+ case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVMinus(lhs, rhs)
+ }
+
+ def times(lhs: Expr, rhs: Expr): Expr = {
+ val r = (lhs, rhs) match {
+ case (InfiniteIntegerLiteral(bi), _) if bi == 1 => rhs
+ case (_, InfiniteIntegerLiteral(bi)) if bi == 1 => lhs
+ case (InfiniteIntegerLiteral(bi), _) if bi == 0 => InfiniteIntegerLiteral(0)
+ case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => InfiniteIntegerLiteral(0)
+ case (IntLiteral(1), _) => rhs
+ case (_, IntLiteral(1)) => lhs
+ case (IntLiteral(0), _) => IntLiteral(0)
+ case (_, IntLiteral(0)) => IntLiteral(0)
+ case (IsTyped(_, IntegerType), IsTyped(_, IntegerType)) => Times(lhs, rhs)
+ case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVTimes(lhs, rhs)
+ }
+ println("!@#!@# "+lhs+" * "+rhs+" == "+r)
+ r
+ }
+
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 32f2c2225..901a6810d 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1286,6 +1286,8 @@ object ExprOps {
preTraversal{
case Choose(_, None) => return false
case Hole(_, _) => return false
+ //@EK FIXME: do we need it?
+ //case Error(_, _) => return false
case Gives(_,_) => return false
case _ =>
}(e)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 23648ee3f..221e8ddce 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -402,7 +402,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val maxEnumerated = 1000
val maxValid = 400
- val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams(checkContracts = true))
+ val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
val inputs = enum.iterator(tupleTypeWrap(fd.params map { _.getType})).map(unwrapTuple(_, fd.params.size))
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 05fcc551a..a6c19d26d 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -58,8 +58,12 @@ class ExamplesFinder(ctx: LeonContext, program: Program) {
(Nil, Nil)
}
- def extractTests(p: Problem): Seq[Example] = {
+ def generateTests(p: Problem): Seq[Example] = {
+ Nil
+ }
+ // Extract examples from the passes found in expression
+ def extractTests(p: Problem): Seq[Example] = {
val testClusters = extractTestsOf(and(p.pc, p.phi))
// Finally, we keep complete tests covering all as++xs
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index f450c63c5..acbd06e27 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -25,10 +25,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
LeonValueOptionDef("costmodel", "--costmodel=cm", "Use a specific cost model for this search"),
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,.."),
// CEGIS options
- LeonFlagOptionDef( "cegis:gencalls", "--cegis:gencalls", "Include function calls in CEGIS generators", true),
- LeonFlagOptionDef( "cegis:unintprobe", "--cegis:unintprobe", "Check for UNSAT without bloecks and with uninterpreted functions", false),
- LeonFlagOptionDef( "cegis:bssfilter", "--cegis:bssfilter", "Filter non-det programs when tests pruning works well", true),
- LeonFlagOptionDef( "cegis:unsatcores", "--cegis:unsatcores", "Use UNSAT-cores in pruning", true),
+ LeonFlagOptionDef( "cegis:shrink", "--cegis:shrink", "Shrink non-det programs when tests pruning works well", true),
LeonFlagOptionDef( "cegis:opttimeout", "--cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true),
LeonFlagOptionDef( "cegis:vanuatoo", "--cegis:vanuatoo", "Generate inputs using new korat-style generator", false),
LeonFlagOptionDef( "holes:discrete", "--holes:discrete", "Oracles get split", false)
@@ -82,23 +79,17 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
case LeonFlagOption("derivtrees", v) =>
options = options.copy(generateDerivationTrees = v)
- case LeonFlagOption("cegis:unsatcores", v) =>
- options = options.copy(cegisUseUnsatCores = v)
-
case LeonFlagOption("cegis:bssfilter", v) =>
- options = options.copy(cegisUseBssFiltering = v)
+ options = options.copy(cegisUseShrink = Some(v))
case LeonFlagOption("cegis:opttimeout", v) =>
- options = options.copy(cegisUseOptTimeout = v)
-
- case LeonFlagOption("cegis:gencalls", v) =>
- options = options.copy(cegisGenerateFunCalls = v)
+ options = options.copy(cegisUseOptTimeout = Some(v))
case LeonFlagOption("cegis:vanuatoo", v) =>
- options = options.copy(cegisUseVanuatoo = v)
+ options = options.copy(cegisUseVanuatoo = Some(v))
- case LeonFlagOption("holes:discrete", v) =>
- options = options.copy(distreteHoles = v)
+// case LeonFlagOption("holes:discrete", v) =>
+// options = options.copy(distreteHoles = v)
case _ =>
}
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index 5f279ee5d..28e59b1e6 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -22,14 +22,9 @@ case class SynthesisSettings(
functionsToIgnore: Set[FunDef] = Set(),
// Cegis related options
- cegisUseUnsatCores: Boolean = true,
- cegisUseOptTimeout: Boolean = true,
- cegisUseBssFiltering: Boolean = true,
- cegisGenerateFunCalls: Boolean = true,
- cegisUseCETests: Boolean = true,
- cegisUseCEPruning: Boolean = true,
- cegisUseBPaths: Boolean = true,
- cegisUseVanuatoo: Boolean = false,
+ cegisUseOptTimeout: Option[Boolean] = None,
+ cegisUseShrink: Option[Boolean] = None,
+ cegisUseVanuatoo: Option[Boolean] = None,
// Oracles and holes
distreteHoles: Boolean = false
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 2190e473c..36f1fc8f8 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -41,7 +41,7 @@ abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) {
def apply(hctx: SearchContext): RuleApplication = {
val sctx = hctx.sctx
- val evalParams = CodeGenParams(maxFunctionInvocations = 2000, checkContracts = true)
+ val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
//val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
//val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index d6dd87720..53303b4a4 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -45,16 +45,15 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val ctx = sctx.context
// CEGIS Flags to activate or deactivate features
- //val useUnsatCores = sctx.settings.cegisUseUnsatCores
- val useOptTimeout = sctx.settings.cegisUseOptTimeout
- val useVanuatoo = sctx.settings.cegisUseVanuatoo
- val useCETests = sctx.settings.cegisUseCETests
+ val useOptTimeout = sctx.settings.cegisUseOptTimeout.getOrElse(true)
+ val useVanuatoo = sctx.settings.cegisUseVanuatoo.getOrElse(false)
+ val useShrink = sctx.settings.cegisUseShrink.getOrElse(true)
// Limits the number of programs CEGIS will specifically validate individually
val validateUpTo = 5
- val useBssFiltering = sctx.settings.cegisUseBssFiltering
- val filterThreshold = 1.0/2
+ // Shrink the program when the ratio of passing cases is less than the threshold
+ val shrinkThreshold = 1.0/2
val interruptManager = sctx.context.interruptManager
@@ -317,7 +316,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
None
}(cTree))
- val evalParams = CodeGenParams(maxFunctionInvocations = -1, doInstrument = false)
+ val evalParams = CodeGenParams.default
//println("-- "*30)
//println(programCTree)
@@ -791,7 +790,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
var baseExampleInputs: ArrayBuffer[Seq[Expr]] = new ArrayBuffer[Seq[Expr]]()
// We populate the list of examples with a predefined one
- sctx.reporter.debug("Acquiring list of examples")
+ sctx.reporter.debug("Acquiring initial list of examples")
val ef = new ExamplesFinder(sctx.context, sctx.program)
baseExampleInputs ++= ef.extractTests(p).map(_.ins).toSet
@@ -836,19 +835,22 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val inputIterator: Iterator[Seq[Expr]] = if (useVanuatoo) {
new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, pc, 20, 3000)
} else {
- val evalParams = CodeGenParams(maxFunctionInvocations = -1, doInstrument = false)
- val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
- new NaiveDataGen(sctx.context, sctx.program, evaluator).generateFor(p.as, pc, 20, 1000)
+ val evaluator = new DualEvaluator(sctx.context, sctx.program, CodeGenParams.default)
+ new GrammarDataGen(evaluator, ExpressionGrammars.ValueGrammar).generateFor(p.as, pc, 20, 1000)
}
val cachedInputIterator = new Iterator[Seq[Expr]] {
def next() = {
val i = inputIterator.next()
+ println("Found "+i)
baseExampleInputs += i
i
}
- def hasNext = inputIterator.hasNext
+ def hasNext = {
+ println("Has next? "+ inputIterator.hasNext)
+ inputIterator.hasNext
+ }
}
val failedTestsStats = new MutableMap[Seq[Expr], Int]().withDefaultValue(0)
@@ -903,7 +905,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val e = examples.next()
if (!ndProgram.testForProgram(bs)(e)) {
failedTestsStats(e) += 1
- sctx.reporter.debug(" Program: "+ndProgram.getExpr(bs)+" failed on "+e.mkString(" ; "))
+ sctx.reporter.debug(f" Program: ${ndProgram.getExpr(bs)}%-80s failed on: ${e.mkString(", ")}")
wrongPrograms += bs
prunedPrograms -= bs
@@ -927,6 +929,16 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
printer(" - ...")
}
}
+ sctx.reporter.debug("#Tests: "+baseExampleInputs.size)
+ sctx.reporter.ifDebug{ printer =>
+ for (i <- baseExampleInputs.take(10)) {
+ printer(" - "+i.mkString(", "))
+ }
+ if(baseExampleInputs.size > 10) {
+ printer(" - ...")
+ }
+ }
+
if (nPassing == 0 || interruptManager.isInterrupted) {
// No test passed, we can skip solver and unfold again, if possible
@@ -953,7 +965,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
if (doFilter) {
- if (nPassing < nInitial * filterThreshold && useBssFiltering) {
+ if (nPassing < nInitial * shrinkThreshold && useShrink) {
// We shrink the program to only use the bs mentionned
val bssToKeep = prunedPrograms.foldLeft(Set[Identifier]())(_ ++ _)
ndProgram.shrinkTo(bssToKeep, unfolding == maxUnfoldings)
@@ -972,7 +984,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
case Some(Some(bs)) =>
// Should we validate this program with Z3?
- val validateWithZ3 = if (useCETests && hasInputExamples) {
+ val validateWithZ3 = if (hasInputExamples) {
if (allInputExamples().forall(ndProgram.testForProgram(bs))) {
// All valid inputs also work with this, we need to
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index c33886a03..5ea9fb787 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -38,7 +38,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
var tests = ef.extractTests(p).map(_.ins).distinct
if (tests.nonEmpty) {
- val evalParams = CodeGenParams(maxFunctionInvocations = 2000, checkContracts = true)
+ val evalParams = CodeGenParams.default.copy(maxFunctionInvocations = 2000)
val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams)
val enum = new MemoizedEnumerator[T, Expr](grammar.getProductions)
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index af474fb7e..5839f5bf5 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -14,6 +14,7 @@ import purescala.ExprOps._
import purescala.DefOps._
import purescala.TypeOps._
import purescala.Extractors._
+import purescala.Constructors._
import purescala.ScalaPrinter
import purescala.Constructors.finiteSet
@@ -80,33 +81,33 @@ object ExpressionGrammars {
List(
Generator(Nil, { _ => BooleanLiteral(true) }),
Generator(Nil, { _ => BooleanLiteral(false) }),
- Generator(List(BooleanType), { case Seq(a) => Not(a) }),
- Generator(List(BooleanType, BooleanType), { case Seq(a, b) => And(a, b) }),
- Generator(List(BooleanType, BooleanType), { case Seq(a, b) => LeonOr(a, b) }),
+ Generator(List(BooleanType), { case Seq(a) => not(a) }),
+ Generator(List(BooleanType, BooleanType), { case Seq(a, b) => and(a, b) }),
+ Generator(List(BooleanType, BooleanType), { case Seq(a, b) => or(a, b) }),
Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessThan(a, b) }),
Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessEquals(a, b) }),
- Generator(List(Int32Type, Int32Type ), { case Seq(a, b) => Equals(a, b) }),
+ Generator(List(Int32Type, Int32Type ), { case Seq(a, b) => equality(a, b) }),
Generator(List(IntegerType, IntegerType), { case Seq(a, b) => LessThan(a, b) }),
Generator(List(IntegerType, IntegerType), { case Seq(a, b) => LessEquals(a, b) }),
- Generator(List(IntegerType, IntegerType), { case Seq(a, b) => Equals(a, b) }),
- Generator(List(BooleanType, BooleanType), { case Seq(a, b) => Equals(a, b) })
+ Generator(List(IntegerType, IntegerType), { case Seq(a, b) => equality(a, b) }),
+ Generator(List(BooleanType, BooleanType), { case Seq(a, b) => equality(a, b) })
)
case Int32Type =>
List(
Generator(Nil, { _ => IntLiteral(0) }),
Generator(Nil, { _ => IntLiteral(1) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a,b) => BVPlus(a, b) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a,b) => BVMinus(a, b) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a,b) => BVTimes(a, b) })
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => plus(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => minus(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => times(a, b) })
)
case IntegerType =>
List(
Generator(Nil, { _ => InfiniteIntegerLiteral(0) }),
Generator(Nil, { _ => InfiniteIntegerLiteral(1) }),
- Generator(List(IntegerType, IntegerType), { case Seq(a,b) => Plus(a, b) }),
- Generator(List(IntegerType, IntegerType), { case Seq(a,b) => Minus(a, b) }),
- Generator(List(IntegerType, IntegerType), { case Seq(a,b) => Times(a, b) })
+ Generator(List(IntegerType, IntegerType), { case Seq(a,b) => plus(a, b) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a,b) => minus(a, b) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a,b) => times(a, b) })
)
case TupleType(stps) =>
--
GitLab