diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index c495ccb5d54e19e65494b36387a467a6f6a9536a..0afef05bfd3f0918825d337578f87bc098c68649 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -45,6 +45,9 @@ object CodeGeneration {
case _ : MapType =>
"L" + MapClass + ";"
+ case ArrayType(base) =>
+ "[" + typeToJVM(base)
+
case _ => throw CompilationException("Unsupported type : " + tpe)
}
@@ -61,7 +64,7 @@ object CodeGeneration {
case Int32Type | BooleanType | UnitType =>
ch << IRETURN
- case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType =>
+ case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType =>
ch << ARETURN
case other =>
@@ -282,6 +285,34 @@ object CodeGeneration {
mkExpr(e, ch)
ch << INEG
+ case ArrayLength(a) =>
+ mkExpr(a, ch)
+ ch << ARRAYLENGTH
+
+ case as @ ArraySelect(a,i) =>
+ mkExpr(a, ch)
+ mkExpr(i, ch)
+ ch << (as.getType match {
+ case Untyped => throw CompilationException("Cannot compile untyped array access.")
+ case Int32Type => IALOAD
+ case BooleanType => BALOAD
+ case _ => AALOAD
+ })
+
+ case a @ FiniteArray(es) =>
+ ch << Ldc(es.size)
+ val storeInstr = a.getType match {
+ case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
+ case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
+ case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
+ case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
+ }
+ for((e,i) <- es.zipWithIndex) {
+ ch << DUP << Ldc(i)
+ mkExpr(e, ch)
+ ch << storeInstr
+ }
+
// Misc and boolean tests
case Error(desc) =>
ch << New(ErrorClass) << DUP
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 799241c5ccefa76c8e0a4fa7e47d033a90d8d313..0d547d27a72b44f07d7a7105645d5b7bfc50a828 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -67,7 +67,12 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
val cons = caseClassConstructors(ccd)
cons.newInstance(args.map(valueToJVM).toArray : _*).asInstanceOf[AnyRef]
- // just slightly overkill...
+ // For now, we only treat boolean arrays separately.
+ // We have a use for these, mind you.
+ case f @ FiniteArray(exprs) if f.getType == ArrayType(BooleanType) =>
+ exprs.map(e => valueToJVM(e).asInstanceOf[java.lang.Boolean].booleanValue).toArray
+
+ // Just slightly overkill...
case _ =>
compileExpression(e, Seq()).evalToJVM(Seq())
}
@@ -112,6 +117,9 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
}
def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
+ if(e.getType == Untyped) {
+ throw new IllegalArgumentException("Cannot compile untyped expression [%s].".format(e))
+ }
val id = nextExprId
@@ -149,7 +157,7 @@ class CompilationUnit(val program: Program, val classes: Map[Definition, ClassFi
case Int32Type | BooleanType =>
ch << IRETURN
- case UnitType | TupleType(_) | SetType(_) | MapType(_, _) | AbstractClassType(_) | CaseClassType(_) =>
+ case UnitType | TupleType(_) | SetType(_) | MapType(_, _) | AbstractClassType(_) | CaseClassType(_) | ArrayType(_) =>
ch << ARETURN
case other =>
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 7202c4ff1575abafceb642d651bbd0afdccc19f8..f4537232707462e9dd8b0c313abac19d1c64724a 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -30,21 +30,30 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
import leon.codegen.runtime.LeonCodeGenRuntimeException
import leon.codegen.runtime.LeonCodeGenEvaluationException
- val ce = unit.compileExpression(expression, argorder)
-
- Some((args : Seq[Expr]) => {
- try {
- EvaluationSuccessful(ce.eval(args))
- } catch {
- case e : ArithmeticException =>
- EvaluationFailure(e.getMessage)
-
- case e : LeonCodeGenRuntimeException =>
- EvaluationFailure(e.getMessage)
-
- case e : LeonCodeGenEvaluationException =>
- EvaluationError(e.getMessage)
- }
- })
+ try {
+ val ce = unit.compileExpression(expression, argorder)
+
+ Some((args : Seq[Expr]) => {
+ try {
+ EvaluationSuccessful(ce.eval(args))
+ } catch {
+ case e : ArithmeticException =>
+ EvaluationFailure(e.getMessage)
+
+ case e : ArrayIndexOutOfBoundsException =>
+ EvaluationFailure(e.getMessage)
+
+ case e : LeonCodeGenRuntimeException =>
+ EvaluationFailure(e.getMessage)
+
+ case e : LeonCodeGenEvaluationException =>
+ EvaluationError(e.getMessage)
+ }
+ })
+ } catch {
+ case t: Throwable =>
+ ctx.reporter.warning("Error while compiling expression: "+t.getMessage)
+ None
+ }
}
}
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index 9b0bbdc2e0f47c5f5b454b9c8d4580113e89afca..47d86be95e018c115f226d36334df54e9f5ce982 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -253,7 +253,11 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
case ArraySelect(a, i) => {
val IntLiteral(index) = rec(ctx, i)
val FiniteArray(exprs) = rec(ctx, a)
- exprs(index)
+ try {
+ exprs(index)
+ } catch {
+ case e : IndexOutOfBoundsException => throw RuntimeError(e.getMessage)
+ }
}
case FiniteArray(exprs) => {
FiniteArray(exprs.map(e => rec(ctx, e)))
@@ -297,6 +301,7 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
try {
EvaluationSuccessful(rec(mapping, expression))
} catch {
+ case so: StackOverflowError => EvaluationError("Stack overflow")
case EvalError(msg) => EvaluationError(msg)
case RuntimeError(msg) => EvaluationFailure(msg)
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 641b86c81bfc49aae5fb9baccf67102a1187fc9d..0b79871badfdabcd82cb5ca1e2be465f1b0521d8 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -36,11 +36,13 @@ class FairZ3Solver(context : LeonContext)
)
// What wouldn't we do to avoid defining vars?
- val (feelingLucky, checkModels, useCodeGen, evalGroundApps) = locally {
- var lucky = false
- var check = false
- var codegen = false
- var evalground = false
+ val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores, pruneUnsatCores) = locally {
+ var lucky = true
+ var check = false
+ var codegen = false
+ var evalground = false
+ var unrollUnsatCores = true
+ var pruneUnsatCores = true
for(opt <- context.options) opt match {
case LeonFlagOption("checkmodels") => check = true
@@ -50,7 +52,7 @@ class FairZ3Solver(context : LeonContext)
case _ =>
}
- (lucky,check,codegen,evalground)
+ (lucky, check, codegen, evalground, unrollUnsatCores, pruneUnsatCores)
}
private var evaluator : Evaluator = null
@@ -175,7 +177,7 @@ class FairZ3Solver(context : LeonContext)
(false, asMap)
case EvaluationError(msg) =>
- reporter.error("Something went wrong. While evaluating the model, we got this : " + msg)
+ reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
(false, asMap)
}
@@ -210,7 +212,7 @@ class FairZ3Solver(context : LeonContext)
// Keep which function invocation is guarded by which guard with polarity,
// also specify the generation of the blocker
- private var blockersInfoStack : List[MutableMap[(Z3AST,Boolean), (Int, Z3AST, Set[Z3FunctionInvocation])]] = List(MutableMap())
+ private var blockersInfoStack : List[MutableMap[(Z3AST,Boolean), (Int, Int, Z3AST, Set[Z3FunctionInvocation])]] = List(MutableMap())
def blockersInfo = blockersInfoStack.head
@@ -222,14 +224,28 @@ class FairZ3Solver(context : LeonContext)
blockersInfoStack = blockersInfoStack.drop(lvl)
}
- def z3CurrentZ3Blockers = blockersInfo.map(_._2._2)
+ def z3CurrentZ3Blockers = blockersInfo.map(_._2._3)
+
+ def dumpBlockers = {
+ blockersInfo.groupBy(_._2._1).toSeq.sortBy(_._1).foreach { case (gen, entries) =>
+ reporter.info("--- "+gen)
+
+ for (((bast, bpol), (gen, origGen, ast, fis)) <- entries) {
+ reporter.info(". "+(if(!bpol) "¬" else "")+bast +" ~> "+fis.map(_.funDef.id))
+ }
+ }
+ }
def canUnroll = !blockersInfo.isEmpty
def getZ3BlockersToUnlock: Seq[(Z3AST, Boolean)] = {
- val minGeneration = blockersInfo.values.map(_._1).min
+ if (!blockersInfo.isEmpty) {
+ val minGeneration = blockersInfo.values.map(_._1).min
- blockersInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1)
+ blockersInfo.filter(_._2._1 == minGeneration).toSeq.map(_._1)
+ } else {
+ Seq()
+ }
}
private def registerBlocker(gen: Int, id: Z3AST, pol: Boolean, fis: Set[Z3FunctionInvocation]) {
@@ -238,12 +254,12 @@ class FairZ3Solver(context : LeonContext)
val z3ast = if (pol) z3.mkNot(id) else id
blockersInfo.get(pair) match {
- case Some((exGen, _, exFis)) =>
+ case Some((exGen, origGen, _, exFis)) =>
assert(exGen == gen, "Mixing the same pair "+pair+" with various generations "+ exGen+" and "+gen)
- blockersInfo(pair) = ((gen, z3ast, fis++exFis))
+ blockersInfo(pair) = ((gen, origGen, z3ast, fis++exFis))
case None =>
- blockersInfo(pair) = ((gen, z3ast, fis))
+ blockersInfo(pair) = ((gen, gen, z3ast, fis))
}
}
@@ -264,18 +280,42 @@ class FairZ3Solver(context : LeonContext)
val (newClauses, newBlocks) = template.instantiate(template.z3ActivatingBool, true, z3args)
- for(((i, p), fis) <- newBlocks) {
- registerBlocker(1, i, p, fis)
+ val extraClauses = for(((i, p), fis) <- newBlocks) yield {
+ registerBlocker(nextGeneration(0), i, p, fis)
+ //unlock(i, p)
+ Nil
+ }
+
+ newClauses ++ extraClauses.flatten
+ }
+
+ def nextGeneration(gen: Int) = gen + 3
+
+ def decreaseAllGenerations() = {
+ for ((block, (gen, origGen, ast, finvs)) <- blockersInfo) {
+ // We also decrease the original generation here
+ blockersInfo(block) = (math.max(1,gen-1), math.max(1,origGen-1), ast, finvs)
+ }
+ }
+
+ def prune(ast: Z3AST, pol: Boolean) = {
+ val b = (ast, pol)
+ blockersInfo -= b
+ }
+
+ def promoteBlocker(bast: Z3AST, pol: Boolean) = {
+ val b = (bast, pol)
+ if (blockersInfo contains b) {
+ val (gen, origGen, ast, finvs) = blockersInfo(b)
+ blockersInfo(b) = (1, origGen, ast, finvs)
}
-
- newClauses
}
def unlock(id: Z3AST, pol: Boolean) : Seq[Z3AST] = {
val pair = (id, pol)
assert(blockersInfo contains pair)
- val (gen, _, fis) = blockersInfo(pair)
+ val (gen, origGen, _, fis) = blockersInfo(pair)
blockersInfo -= pair
var newClauses : Seq[Z3AST] = Seq.empty
@@ -285,7 +325,8 @@ class FairZ3Solver(context : LeonContext)
val (newExprs, newBlocks) = template.instantiate(id, pol, fi.args)
for(((i, p), fis) <- newBlocks) {
- registerBlocker(gen+1, i, p, fis)
+ // We use origGen here
+ registerBlocker(nextGeneration(origGen), i, p, fis)
}
newClauses ++= newExprs
@@ -405,9 +446,9 @@ class FairZ3Solver(context : LeonContext)
reporter.info(" - Running Z3 search...")
- //reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
- //reporter.info("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
- //reporter.info("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
+ reporter.info("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
+ reporter.info("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
+ reporter.info("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
z3Time.start
solver.push() // FIXME: remove when z3 bug is fixed
@@ -459,9 +500,47 @@ class FairZ3Solver(context : LeonContext)
// distinction is made inside.
case Some(false) =>
- //val core = z3CoreToCore(solver.getUnsatCore)
+ val z3Core = solver.getUnsatCore
- //reporter.info("UNSAT BECAUSE: "+solver.getUnsatCore.mkString(" AND "))
+ def coreElemToBlocker(c: Z3AST): (Z3AST, Boolean) = {
+ z3.getASTKind(c) match {
+ case Z3AppAST(decl, args) =>
+ z3.getDeclKind(decl) match {
+ case Z3DeclKind.OpNot =>
+ (args(0), true)
+ case Z3DeclKind.OpUninterpreted =>
+ (c, false)
+ }
+
+ case ast =>
+ (c, false)
+ }
+ }
+
+ if (unrollUnsatCores) {
+ unrollingBank.decreaseAllGenerations()
+
+ for (c <- solver.getUnsatCore) {
+ val (z3ast, pol) = coreElemToBlocker(c)
+
+ unrollingBank.promoteBlocker(z3ast, pol)
+ }
+
+ }
+
+ if (pruneUnsatCores) {
+ z3Core.toSeq match {
+ case Seq(c) =>
+ // If there is only one element in the Seq, we can prune
+ val (z3ast, pol) = coreElemToBlocker(c)
+
+ unrollingBank.prune(z3ast, !pol)
+ solver.assertCnstr(if (pol) z3ast else z3.mkNot(z3ast))
+ case _ =>
+ }
+ }
+
+ reporter.info("UNSAT BECAUSE: "+solver.getUnsatCore.mkString("\n AND \n"))
//reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
if (!forceStop) {
@@ -480,10 +559,10 @@ class FairZ3Solver(context : LeonContext)
res2 match {
case Some(false) =>
- //reporter.info("UNSAT WITHOUT Blockers")
+ reporter.info("UNSAT WITHOUT Blockers")
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) =>
- //reporter.info("SAT WITHOUT Blockers")
+ reporter.info("SAT WITHOUT Blockers")
if (this.feelingLucky && !forceStop) {
// we might have been lucky :D
luckyTime.start
@@ -507,15 +586,18 @@ class FairZ3Solver(context : LeonContext)
reporter.info("- We need to keep going.")
//val toReleaseAsPairs = unrollingBank.getBlockersToUnlock
+ // unrollingBank.dumpBlockers
val toReleaseAsPairs = unrollingBank.getZ3BlockersToUnlock
reporter.info(" - more unrollings")
+ unrollingBank.dumpBlockers
+
for((id, polarity) <- toReleaseAsPairs) {
unlockingTime.start
val newClauses = unrollingBank.unlock(id, polarity)
unlockingTime.stop
- //reporter.info(" - - Unrolling behind "+(if(!polarity) "¬" else "")+id)
+ reporter.info(" - - Unrolling behind "+(if(!polarity) "¬" else "")+id)
//for (cl <- newClauses) {
// reporter.info(" - - - "+cl)
//}
@@ -540,6 +622,8 @@ class FairZ3Solver(context : LeonContext)
StopwatchCollections.get("FairZ3 Unlocking") += unlockingTime
StopwatchCollections.get("FairZ3 ScalaTime") += scalaTime
+ reporter.info(" !! DONE !! ")
+
if(forceStop) {
None
} else {
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 66cb6af25f3008dc2427a41453f8c150fd23ab87..da4de64711a03fc1a8c068263b673ba81232c37a 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -142,6 +142,29 @@ object FunctionTemplate {
}
}
+ // Group elements that satisfy p toghether
+ // List(a, a, a, b, c, a, a), with p = _ == a will produce:
+ // List(List(a,a,a), List(b), List(c), List(a, a))
+ def groupWhile[T](p: T => Boolean, l: Seq[T]): Seq[Seq[T]] = {
+ var res: Seq[Seq[T]] = Nil
+
+ var c = l
+
+ while(!c.isEmpty) {
+ val (span, rest) = c.span(p)
+
+ if (span.isEmpty) {
+ res = res :+ Seq(rest.head)
+ c = rest.tail
+ } else {
+ res = res :+ span
+ c = rest
+ }
+ }
+
+ res
+ }
+
def rec(pathVar : Identifier, pathPol : Boolean, expr : Expr) : Expr = {
expr match {
case l @ Let(i, e, b) =>
@@ -154,6 +177,35 @@ object FunctionTemplate {
case m : MatchExpr => sys.error("MatchExpr's should have been eliminated.")
+ case i @ Implies(lhs, rhs) =>
+ if (containsFunctionCalls(i)) {
+ rec(pathVar, pathPol, IfExpr(lhs, rhs, BooleanLiteral(true)))
+ } else {
+ i
+ }
+
+ case a @ And(parts) =>
+ if (containsFunctionCalls(a)) {
+ val partitions = groupWhile((e: Expr) => !containsFunctionCalls(e), parts)
+
+ val ifExpr = partitions.map(And(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, b, BooleanLiteral(false)) }
+
+ rec(pathVar, pathPol, ifExpr)
+ } else {
+ a
+ }
+
+ case o @ Or(parts) =>
+ if (containsFunctionCalls(o)) {
+ val partitions = groupWhile((e: Expr) => !containsFunctionCalls(e), parts)
+
+ val ifExpr = partitions.map(Or(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, BooleanLiteral(true), b) }
+
+ rec(pathVar, pathPol, ifExpr)
+ } else {
+ o
+ }
+
case i @ IfExpr(cond, then, elze) => {
if(!containsFunctionCalls(cond) && !containsFunctionCalls(then) && !containsFunctionCalls(elze)) {
i
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 1245490fda7a6561547d9e8e06e04e6f1996ee88..92ae31535579dfba4942f3ff6b55cc13ad5d774a 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -9,6 +9,7 @@ import purescala.Common.Identifier
import java.util.concurrent.atomic.AtomicBoolean
case class SynthesisContext(
+ context: LeonContext,
options: SynthesizerOptions,
functionContext: Option[FunDef],
program: Program,
@@ -20,6 +21,7 @@ case class SynthesisContext(
object SynthesisContext {
def fromSynthesizer(synth: Synthesizer) = {
SynthesisContext(
+ synth.context,
synth.options,
synth.functionContext,
synth.program,
diff --git a/src/main/scala/leon/synthesis/SynthesizerOptions.scala b/src/main/scala/leon/synthesis/SynthesizerOptions.scala
index e9d2f4c94b89e78c473850bc8e0eda343e487f3f..647e4049da9e479d824621fc363426fbd6a4ae54 100644
--- a/src/main/scala/leon/synthesis/SynthesizerOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesizerOptions.scala
@@ -2,11 +2,16 @@ package leon
package synthesis
case class SynthesizerOptions(
- generateDerivationTrees: Boolean = false,
- filterFuns: Option[Set[String]] = None,
- searchWorkers: Int = 1,
- firstOnly: Boolean = false,
- timeoutMs: Option[Long] = None,
- costModel: CostModel = CostModel.default,
- cegisGenerateFunCalls: Boolean = false
+ generateDerivationTrees: Boolean = false,
+ filterFuns: Option[Set[String]] = None,
+ searchWorkers: Int = 1,
+ firstOnly: Boolean = false,
+ timeoutMs: Option[Long] = None,
+ costModel: CostModel = CostModel.default,
+
+ // Cegis related options
+ cegisGenerateFunCalls: Boolean = false,
+ cegisUseCETests: Boolean = true,
+ cegisUseCEPruning: Boolean = true,
+ cegisUseBPaths: Boolean = true
)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 0be34792948c462135e7fe1a982c8bc08442d4b9..2cb41ef38293fc445c65a3b45f8191ae8f5d4e6e 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -8,6 +8,9 @@ import purescala.Definitions._
import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
+import purescala.ScalaPrinter
+
+import evaluators._
import solvers.z3.FairZ3Solver
@@ -15,10 +18,14 @@ case object CEGIS extends Rule("CEGIS") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
// CEGIS Flags to actiave or de-activate features
- val useCounterExamples = false
+ val useCEAsserts = false
val useUninterpretedProbe = false
val useUnsatCores = true
val useFunGenerators = sctx.options.cegisGenerateFunCalls
+ val useBPaths = sctx.options.cegisUseBPaths
+ val useCETests = sctx.options.cegisUseCETests
+ val useCEPruning = sctx.options.cegisUseCEPruning
+ val evaluator = new CodeGenEvaluator(sctx.context, sctx.program)
case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
@@ -83,7 +90,17 @@ case object CEGIS extends Rule("CEGIS") {
false
}
- isSubtypeOf(fd.returnType, t) && !isRecursiveCall
+ val isNotSynthesizable = fd.body match {
+ case Some(b) =>
+ collectChooses(b).isEmpty
+
+ case None =>
+ false
+ }
+
+
+
+ isSubtypeOf(fd.returnType, t) && !isRecursiveCall && isNotSynthesizable
}
sctx.program.definedFunctions.filter(isCandidate).map{ fd =>
@@ -96,58 +113,255 @@ case object CEGIS extends Rule("CEGIS") {
}
}
- class TentativeFormula(val pathcond: Expr,
- val phi: Expr,
- var program: Expr,
- var mappings: Map[Identifier, (Identifier, Expr)],
- var recTerms: Map[Identifier, Set[Identifier]]) {
+ class NonDeterministicProgram(val p: Problem,
+ val initGuard: Identifier) {
+
+ //var program: Expr = BooleanLiteral(true)
+
+ // b -> (c, ex) means the clause b => c == ex
+ var mappings: Map[Identifier, (Identifier, Expr)] = Map()
+
+ // b -> Set(c1, c2) means c1 and c2 are uninterpreted behing b, requires b to be closed
+ private var guardedTerms: Map[Identifier, Set[Identifier]] = Map(initGuard -> p.xs.toSet)
+
+
+ def isBClosed(b: Identifier) = guardedTerms.contains(b)
+
+ // b -> Map(c1 -> Set(b2, b3), c2 -> Set(b4, b5)) means b protects c1 (with sub alternatives b2/b3), and c2 (with sub b4/b5)
+ private var bTree = Map[Identifier, Map[Identifier, Set[Identifier]]]( initGuard -> p.xs.map(_ -> Set[Identifier]()).toMap)
+
+ // Returns all possible assignments to Bs in order to enumerate all possible programs
+ def allPrograms(): Set[Set[Identifier]] = {
+ def allChildPaths(b: Identifier): Stream[Set[Identifier]] = {
+ if (isBClosed(b)) {
+ Stream.empty
+ } else {
+ bTree.get(b) match {
+ case Some(cToBs) =>
+ val streams = cToBs.values.map { children =>
+ children.toStream.flatMap(c => allChildPaths(c).map(l => l + b))
+ }
+
+ streams.reduceLeft{ (s1: Stream[Set[Identifier]], s2: Stream[Set[Identifier]]) => for(p1 <- s1; p2 <- s2) yield { p1 ++ p2 } }
+ case None =>
+ Stream.cons(Set(b), Stream.empty)
+ }
+ }
+ }
+
+ allChildPaths(initGuard).toSet
+ }
+
+ /*
+ * Compilation/Execution of programs
+ */
+
+ // b1 => c == F(c2, c3) OR b2 => c == F(c4, c5) is represented here as c -> Set(c2, c3, c4, c5)
+ private var cChildren: Map[Identifier, Set[Identifier]] = Map().withDefaultValue(Set())
+
+
+ private var triedCompilation = false
+ private var progEvaluator: Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = None
+
+ def canTest() = {
+ if (!triedCompilation) {
+ progEvaluator = compile()
+ }
+
+ progEvaluator.isDefined
+ }
+
+ private var bssOrdered: Seq[Identifier] = Seq()
+
+ def testForProgram(bss: Set[Identifier])(ins: Seq[Expr]): Boolean = {
+ if (canTest()) {
+ val bssValues : Seq[Expr] = bssOrdered.map(i => BooleanLiteral(bss(i)))
+
+ val evalResult = progEvaluator.get.apply(bssValues, ins)
+
+ evalResult match {
+ case EvaluationSuccessful(res) =>
+ res == BooleanLiteral(true)
+
+ case EvaluationError(err) =>
+ sctx.reporter.error("Error testing CE: "+err)
+ true
+
+ case EvaluationFailure(err) =>
+ sctx.reporter.error("Error testing CE: "+err)
+ true
+ }
+ } else {
+ true
+ }
+ }
+
+ def compile(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
+ var unreachableCs: Set[Identifier] = guardedTerms.flatMap(_._2).toSet
+
+ val cToExprs = mappings.groupBy(_._2._1).map {
+ case (c, maps) =>
+ // We only keep cases within the current unrolling closedBs
+ val cases = maps.flatMap{ case (b, (_, ex)) => if (isBClosed(b)) None else Some(b -> ex) }
+
+ // We compute the IF expression corresponding to each c
+ val ifExpr = if (cases.isEmpty) {
+ // This can happen with ADTs with only cases with arguments
+ Error("No valid clause available").setType(c.getType)
+ } else {
+ cases.tail.foldLeft(cases.head._2) {
+ case (elze, (b, then)) => IfExpr(Variable(b), then, elze)
+ }
+ }
+
+ c -> ifExpr
+ } toMap
+
+ // Map each x generated by the program to fresh xs passed as argument
+ val newXs = p.xs.map(x => x -> FreshIdentifier(x.name, true).setType(x.getType))
+
+ val baseExpr = p.phi
+
+ bssOrdered = bss.toSeq.sortBy(_.id)
+
+ var res = baseExpr
+
+ def composeWith(c: Identifier) {
+ cToExprs.get(c) match {
+ case Some(value) =>
+ res = Let(c, cToExprs(c), res)
+ case None =>
+ res = Let(c, Error("No value available").setType(c.getType), res)
+ }
+
+ for (dep <- cChildren(c) if !unreachableCs(dep)) {
+ composeWith(dep)
+ }
+
+ }
+
+ for (c <- p.xs) {
+ composeWith(c)
+ }
+
+ val simplerRes = simplifyLets(res)
+
+ // println("COMPILATION RESULT: ")
+ // println(ScalaPrinter(simplerRes))
+ // println("BSS: "+bssOrdered)
+ // println("FREE: "+variablesOf(simplerRes))
+
+ def compileWithArray(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
+ val ba = FreshIdentifier("bssArray").setType(ArrayType(BooleanType))
+ val bav = Variable(ba)
+ val substMap : Map[Expr,Expr] = (bssOrdered.zipWithIndex.map {
+ case (b,i) => Variable(b) -> ArraySelect(bav, IntLiteral(i)).setType(BooleanType)
+ }).toMap
+ val forArray = replace(substMap, simplerRes)
+
+ // println("FORARRAY RESULT: ")
+ // println(ScalaPrinter(forArray))
+ // println("FREE: "+variablesOf(simplerRes))
+
+ // We trust arrays to be fast...
+ // val simple = evaluator.compile(simplerRes, bssOrdered ++ p.as)
+ val eval = evaluator.compile(forArray, ba +: p.as)
+
+ eval.map{e => { case (bss, ins) =>
+ e(FiniteArray(bss).setType(ArrayType(BooleanType)) +: ins)
+ }}
+ }
+
+ def compileWithArgs(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
+ val eval = evaluator.compile(simplerRes, bssOrdered ++ p.as)
+
+ eval.map{e => { case (bss, ins) =>
+ e(bss ++ ins)
+ }}
+ }
+
+ triedCompilation = true
+
+ val localVariables = bss.size + cToExprs.size + p.as.size
+
+ if (localVariables < 128) {
+ compileWithArgs().orElse(compileWithArray())
+ } else {
+ compileWithArray()
+ }
+ }
+
+ def determinize(bss: Set[Identifier]): Expr = {
+ val cClauses = mappings.filterKeys(bss).map(_._2).toMap
+
+ def getCValue(c: Identifier): Expr = {
+ val map = for (dep <- cChildren(c) if cClauses contains dep) yield {
+ dep -> getCValue(dep)
+ }
+
+ substAll(map.toMap, cClauses(c))
+ }
+
+ Tuple(p.xs.map(c => getCValue(c))).setType(TupleType(p.xs.map(_.getType)))
+
+ }
def unroll: (List[Expr], Set[Identifier]) = {
- var newClauses = List[Expr]()
- var newRecTerms = Map[Identifier, Set[Identifier]]()
- var newMappings = Map[Identifier, (Identifier, Expr)]()
+ var newClauses = List[Expr]()
+ var newGuardedTerms = Map[Identifier, Set[Identifier]]()
+ var newMappings = Map[Identifier, (Identifier, Expr)]()
+
+ for ((parentGuard, recIds) <- guardedTerms; recId <- recIds) {
- for ((_, recIds) <- recTerms; recId <- recIds) {
val gen = getGenerator(recId.getType)
+
val alts = gen.altBuilder() ::: inputAlternatives(recId.getType) ::: funcAlternatives(recId.getType)
- val altsWithBranches = alts.map(alt => FreshIdentifier("b", true).setType(BooleanType) -> alt)
+ val altsWithBranches = alts.map(alt => FreshIdentifier("B", true).setType(BooleanType) -> alt)
- val bvs = altsWithBranches.map(alt => Variable(alt._1))
- val distinct = if (bvs.size > 1) {
- (for (i <- (1 to bvs.size-1); j <- 0 to i-1) yield {
- Or(Not(bvs(i)), Not(bvs(j)))
- }).toList
- } else {
- List(BooleanLiteral(true))
+ val bvs = altsWithBranches.map(alt => Variable(alt._1))
+
+ val failedPath = Not(Variable(parentGuard))
+
+ val distinct = bvs.combinations(2).collect {
+ case List(a, b) =>
+ Or(Not(a) :: Not(b) :: Nil)
}
- val pre = And(Or(bvs) :: distinct) // (b1 OR b2) AND (Not(b1) OR Not(b2))
+
+ val pre = And(Seq(Or(failedPath :: bvs), Implies(failedPath, And(bvs.map(Not(_))))) ++ distinct)
+
val cases = for((bid, (ex, rec)) <- altsWithBranches.toList) yield { // b1 => E(gen1, gen2) [b1 -> {gen1, gen2}]
if (!rec.isEmpty) {
- newRecTerms += bid -> rec
+ newGuardedTerms += bid -> rec
+ cChildren += recId -> (cChildren(recId) ++ rec)
}
- newMappings += bid -> (recId -> ex)
+
+ newMappings += bid -> (recId -> ex)
Implies(Variable(bid), Equals(Variable(recId), ex))
}
+ val newBIds = altsWithBranches.map(_._1).toSet
+ bTree += parentGuard -> (bTree.getOrElse(parentGuard, Map()) + (recId -> newBIds))
+
newClauses = newClauses ::: pre :: cases
}
- program = And(program :: newClauses)
+ //program = And(program :: newClauses)
mappings = mappings ++ newMappings
- recTerms = newRecTerms
+ guardedTerms = newGuardedTerms
+
+ // Finally, we reset the state of the evalautor
+ triedCompilation = false
+ progEvaluator = None
- (newClauses, newRecTerms.keySet)
+ (newClauses, newGuardedTerms.keySet)
}
- def bounds = recTerms.keySet.map(id => Not(Variable(id))).toList
def bss = mappings.keySet
- def css : Set[Identifier] = mappings.values.map(_._1).toSet ++ recTerms.flatMap(_._2)
-
- def entireFormula = And(pathcond :: phi :: program :: bounds)
+ def css : Set[Identifier] = mappings.values.map(_._1).toSet ++ guardedTerms.flatMap(_._2)
}
val TopLevelAnds(ands) = p.phi
@@ -158,51 +372,121 @@ case object CEGIS extends Rule("CEGIS") {
val (exprsA, others) = ands.partition(e => (variablesOf(e) & xsSet).isEmpty)
if (exprsA.isEmpty) {
val res = new RuleInstantiation(p, this, SolutionBuilder.none) {
- def apply(sctx: SynthesisContext) = {
+ def apply(sctx: SynthesisContext): RuleApplicationResult = {
var result: Option[RuleApplicationResult] = None
var ass = p.as.toSet
var xss = p.xs.toSet
- val unrolling = new TentativeFormula(p.pc, p.phi, BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
+ val initGuard = FreshIdentifier("START", true).setType(BooleanType)
+
+ val ndProgram = new NonDeterministicProgram(p, initGuard)
var unrolings = 0
val maxUnrolings = 3
- var predicates: Seq[Expr] = Seq()
-
val mainSolver: FairZ3Solver = sctx.solver.asInstanceOf[FairZ3Solver]
+ var exampleInputs = Set[Seq[Expr]]()
+
+ // We populate the list of examples with a predefined one
+ if (p.pc == BooleanLiteral(true)) {
+ exampleInputs += p.as.map(a => simplestValue(a.getType))
+ } else {
+ val solver = mainSolver.getNewSolver
+
+ solver.assertCnstr(p.pc)
+
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
+ exampleInputs += p.as.map(a => model.getOrElse(a, simplestValue(a.getType)))
+
+ case Some(false) =>
+ return RuleApplicationImpossible
+
+ case None =>
+ sctx.reporter.warning("Solver could not solve path-condition")
+ return RuleApplicationImpossible // This is not necessary though, but probably wanted
+ }
+ }
+
+ // Keep track of collected cores to filter programs to test
+ var collectedCores = Set[Set[Identifier]]()
+
// solver1 is used for the initial SAT queries
- val solver1 = mainSolver.getNewSolver
- solver1.assertCnstr(And(p.pc, p.phi))
+ var solver1 = mainSolver.getNewSolver
+ solver1.assertCnstr(And(p.pc :: p.phi :: Variable(initGuard) :: Nil))
- // solver2 is used for the CE search
+ // solver2 is used for validating a candidate program, or finding new inputs
val solver2 = mainSolver.getNewSolver
- solver2.assertCnstr(And(p.pc :: Not(p.phi) :: Nil))
+ solver2.assertCnstr(And(p.pc :: Not(p.phi) :: Variable(initGuard) :: Nil))
+
+
+ var allClauses = List[Expr]()
try {
do {
- val (clauses, bounds) = unrolling.unroll
+ var needMoreUnrolling = false
+
+ // Compute all programs that have not been excluded yet
+ var allPrograms: Set[Set[Identifier]] = if (useCEPruning) {
+ ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p)))
+ } else {
+ Set()
+ }
+
+ //println("Programs: "+allPrograms.size)
+ //println("CEs: "+exampleInputs.size)
+
+ // We further filter the set of working programs to remove those that fail on known examples
+ if (useCEPruning && !exampleInputs.isEmpty && ndProgram.canTest()) {
+ //for (ce <- exampleInputs) {
+ // println("CE: "+ce)
+ //}
+
+ for (p <- allPrograms) {
+ if (!exampleInputs.forall(ndProgram.testForProgram(p))) {
+ // This program failed on at least one example
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ allPrograms -= p
+ }
+ }
+
+ if (allPrograms.isEmpty) {
+ needMoreUnrolling = true
+ }
+
+ //println("Passing tests: "+allPrograms.size)
+ }
+
+ //allPrograms.foreach { p =>
+ // println("PATH: "+p)
+ // println("CLAUSES: "+p.flatMap( b => ndProgram.mappings.get(b).map{ case (c, ex) => c+" = "+ex}).mkString(" && "))
+ //}
+
+ val (clauses, closedBs) = ndProgram.unroll
//println("UNROLLING: ")
//for (c <- clauses) {
// println(" - " + c)
//}
- //println("BOUNDS "+bounds)
+ //println("CLOSED Bs "+closedBs)
val clause = And(clauses)
+ allClauses = clause :: allClauses
+
solver1.assertCnstr(clause)
solver2.assertCnstr(clause)
val tpe = TupleType(p.xs.map(_.getType))
- val bss = unrolling.bss
+ val bss = ndProgram.bss
- var continue = !clauses.isEmpty
+ if (clauses.isEmpty) {
+ needMoreUnrolling = true
+ }
- while (result.isEmpty && continue && !sctx.shouldStop.get) {
- //println("Looking for CE...")
- //println("-"*80)
+ while (result.isEmpty && !needMoreUnrolling && !sctx.shouldStop.get) {
- solver1.checkAssumptions(bounds.map(id => Not(Variable(id)))) match {
+ solver1.checkAssumptions(closedBs.map(id => Not(Variable(id)))) match {
case Some(true) =>
val satModel = solver1.getModel
@@ -211,80 +495,120 @@ case object CEGIS extends Rule("CEGIS") {
case BooleanLiteral(false) => Not(Variable(b))
})
+ //println("CEGIS OUT!")
//println("Found solution: "+bssAssumptions)
- //println("#"*80)
- solver2.checkAssumptions(bssAssumptions) match {
- case Some(true) =>
- //println("#"*80)
- val invalidModel = solver2.getModel
-
- val fixedAss = And(ass.collect {
- case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
- }.toSeq)
-
- solver1.push()
- solver1.assertCnstr(fixedAss)
- //println("Found counter example: "+fixedAss)
-
- val unsatCore = if (useUnsatCores) {
- solver1.checkAssumptions(bssAssumptions) match {
- case Some(false) =>
- // Core might be empty if unrolling level is
- // insufficient, it becomes unsat no matter what
- // the assumptions are.
- solver1.getUnsatCore
- case _ =>
- bssAssumptions
+ //bssAssumptions.collect { case Variable(b) => ndProgram.mappings(b) }.foreach {
+ // case (c, ex) =>
+ // println(". "+c+" = "+ex)
+ //}
+
+ val validateWithZ3 = if (useCETests && !exampleInputs.isEmpty && ndProgram.canTest()) {
+
+ val p = bssAssumptions.collect { case Variable(b) => b }
+
+ if (exampleInputs.forall(ndProgram.testForProgram(p))) {
+ // All valid inputs also work with this, we need to
+ // make sure by validating this candidate with z3
+ true
+ } else {
+ // One valid input failed with this candidate, we can skip
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ false
+ }
+ } else {
+ // No inputs or capability to test, we need to ask Z3
+ true
+ }
+
+ if (validateWithZ3) {
+ solver2.checkAssumptions(bssAssumptions) match {
+ case Some(true) =>
+ //println("#"*80)
+ val invalidModel = solver2.getModel
+
+ val fixedAss = And(ass.collect {
+ case a if invalidModel contains a => Equals(Variable(a), invalidModel(a))
+ }.toSeq)
+
+ val newCE = p.as.map(valuateWithModel(invalidModel))
+
+ exampleInputs += newCE
+
+ //println("Found counter example: "+fixedAss)
+
+ // Retest whether the newly found C-E invalidates all programs
+ if (useCEPruning && ndProgram.canTest) {
+ if (allPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
+ // println("I found a killer example!")
+ needMoreUnrolling = true
+ }
}
- } else {
- bssAssumptions
- }
-
- solver1.pop()
-
- if (unsatCore.isEmpty) {
- continue = false
- } else {
- if (useCounterExamples) {
- val freshCss = unrolling.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
- val ceIn = ass.collect {
- case id if invalidModel contains id => id -> invalidModel(id)
+
+ val unsatCore = if (useUnsatCores) {
+ solver1.push()
+ solver1.assertCnstr(fixedAss)
+
+ val core = solver1.checkAssumptions(bssAssumptions) match {
+ case Some(false) =>
+ // Core might be empty if unrolling level is
+ // insufficient, it becomes unsat no matter what
+ // the assumptions are.
+ solver1.getUnsatCore
+
+ case _ =>
+ bssAssumptions
}
- val ceMap = (freshCss ++ ceIn)
+ solver1.pop()
+
+ collectedCores += core.collect{ case Variable(id) => id }
+
+ core
+ } else {
+ bssAssumptions
+ }
+
+ if (unsatCore.isEmpty) {
+ needMoreUnrolling = true
+ } else {
+ //if (useCEAsserts) {
+ // val freshCss = ndProgram.css.map(c => c -> Variable(FreshIdentifier(c.name, true).setType(c.getType))).toMap
+ // val ceIn = ass.collect {
+ // case id if invalidModel contains id => id -> invalidModel(id)
+ // }
- val counterexample = substAll(ceMap, And(Seq(unrolling.program, unrolling.phi)))
+ // val ceMap = (freshCss ++ ceIn)
- //val And(ands) = counterexample
- //println("CE:")
- //for (a <- ands) {
- // println(" - "+a)
+ // val counterexample = substAll(ceMap, And(Seq(ndProgram.program, p.phi)))
+
+ // //val And(ands) = counterexample
+ // //println("CE:")
+ // //for (a <- ands) {
+ // // println(" - "+a)
+ // //}
+
+ // solver1.assertCnstr(counterexample)
//}
- solver1.assertCnstr(counterexample)
+ solver1.assertCnstr(Not(And(unsatCore.toSeq)))
}
- solver1.assertCnstr(Not(And(unsatCore.toSeq)))
- }
-
- case Some(false) =>
- var mapping = unrolling.mappings.filterKeys(satModel.mapValues(_ == BooleanLiteral(true))).values.toMap
+ case Some(false) =>
- // Resolve mapping
- for ((c, e) <- mapping) {
- mapping += c -> substAll(mapping, e)
- }
+ val expr = ndProgram.determinize(satModel.filter(_._2 == BooleanLiteral(true)).keySet)
- result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
- case _ =>
- if (!sctx.shouldStop.get) {
- sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
- }
- continue = false
+ case _ =>
+ if (!sctx.shouldStop.get) {
+ sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ }
+ needMoreUnrolling = true
+ }
}
+
case Some(false) =>
//println("%%%% UNSAT")
@@ -298,11 +622,14 @@ case object CEGIS extends Rule("CEGIS") {
}
}
- continue = false
+ needMoreUnrolling = true
case _ =>
+ if (!sctx.shouldStop.get) {
+ sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ }
//println("%%%% WOOPS")
- continue = false
+ needMoreUnrolling = true
}
}
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 15ebc81e64b028aa1190ccf1761ac643ecf68e88..8cb4c5fa741aaccafe7834c96b37a38ecebeb225 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -87,6 +87,7 @@ object Benchmarks extends App {
for ((f, ps) <- results.toSeq.sortBy(_._1.id.toString); p <- ps) {
val sctx = SynthesisContext(
+ context = ctx,
options = opts,
functionContext = Some(f),
program = program,
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 36edcf9f0bc4b221e6c696adb46b5d47ba2fed63..4fe7228d15a3ad68d671507d8735eb94b3c7b1d1 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -175,7 +175,6 @@ class EvaluatorsTests extends FunSuite {
|""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
for(e <- evaluators) {
@@ -211,7 +210,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
for(e <- evaluators) {
@@ -274,7 +272,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
val nil = mkCaseClass("Nil")
@@ -316,7 +313,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
val nil = mkCaseClass("Nil")
@@ -362,7 +358,6 @@ class EvaluatorsTests extends FunSuite {
|}""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
val cons1223 = mkCaseClass("PCons", IL(1), IL(2), mkCaseClass("PCons", IL(2), IL(3), mkCaseClass("PNil")))
@@ -379,6 +374,31 @@ class EvaluatorsTests extends FunSuite {
}
}
+ test("Arrays") {
+ val p = """|object Program {
+ | def boolArrayRead(bools : Array[Boolean], index : Int) : Boolean = bools(index)
+ |
+ | def intArrayRead(bools : Array[Int], index : Int) : Int = bools(index)
+ |}
+ |""".stripMargin
+
+ implicit val progs = parseString(p)
+ val evaluators = prepareEvaluators
+
+ val ba = FiniteArray(Seq(T, F)).setType(ArrayType(BooleanType))
+ val ia = FiniteArray(Seq(IL(41), IL(42), IL(43))).setType(ArrayType(Int32Type))
+
+ for(e <- evaluators) {
+ checkComp(e, mkCall("boolArrayRead", ba, IL(0)), T)
+ checkComp(e, mkCall("boolArrayRead", ba, IL(1)), F)
+ checkComp(e, mkCall("intArrayRead", ia, IL(0)), IL(41))
+ checkComp(e, mkCall("intArrayRead", ia, IL(1)), IL(42))
+ checkComp(e, ArrayLength(ia), IL(3))
+
+ checkError(e, mkCall("boolArrayRead", ba, IL(2)))
+ }
+ }
+
test("Misc") {
val p = """|object Program {
| import leon.Utils._
@@ -388,7 +408,6 @@ class EvaluatorsTests extends FunSuite {
|""".stripMargin
implicit val prog = parseString(p)
-
val evaluators = prepareEvaluators
for(e <- evaluators) {
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 96d7104d7521bd9b95ba27bc8d91f515e2479b33..567d30abb14c99eaf01340fd38fd809d2d0c8f4b 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -44,7 +44,7 @@ class SynthesisSuite extends FunSuite {
for ((f, ps) <- results; p <- ps) {
test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, title)) {
- val sctx = SynthesisContext(opts, Some(f), program, solver, new DefaultReporter, new java.util.concurrent.atomic.AtomicBoolean)
+ val sctx = SynthesisContext(ctx, opts, Some(f), program, solver, new DefaultReporter, new java.util.concurrent.atomic.AtomicBoolean)
block(sctx, f, p)
}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index f5b33c3e21d256f995a135cf9c56880a3c4f31ac..e590093cc3df6b9bfd1346ac2440ee5e512bd0de 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -79,7 +79,6 @@ class XLangVerificationRegression extends FunSuite {
assert(report.totalConditions === report.totalValid,
"All verification conditions ("+report.totalConditions+") should be valid.")
assert(reporter.errorCount === 0)
- assert(reporter.warningCount === 0)
}
forEachFileIn("invalid") { output =>
@@ -89,7 +88,6 @@ class XLangVerificationRegression extends FunSuite {
assert(report.totalUnknown === 0,
"There should not be unknown verification conditions.")
assert(reporter.errorCount >= report.totalInvalid)
- assert(reporter.warningCount === 0)
}
forEachFileIn("error", true) { output => () }