diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index b1727fb71926e8e067d687a3bb62a42b78f5198f..d65e5ce1d7fb1312f3009b600eaae79dc82f0324 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -8,6 +8,7 @@ import purescala.Trees._
import purescala.TreeOps._
import purescala.TypeTrees._
import purescala.Definitions._
+import utils.StreamUtils._
import evaluators._
@@ -18,54 +19,15 @@ import scala.collection.mutable.{Map=>MutableMap}
* e.g. by passing trees representing variables for the "bounds". */
class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds : Option[Map[TypeTree,Seq[Expr]]] = None) extends DataGenerator {
- private val defaultBounds : Map[TypeTree,Seq[Expr]] = Map(
- Int32Type -> Seq(IntLiteral(0), IntLiteral(1), IntLiteral(-1))
- )
-
- val bounds = _bounds.getOrElse(defaultBounds)
-
- private val boolStream : Stream[Expr] =
- Stream.cons(BooleanLiteral(true), Stream.cons(BooleanLiteral(false), Stream.empty))
-
- class VectorizedStream[T](initial : Stream[T]) {
- private def mkException(i : Int) = new IndexOutOfBoundsException("Can't access VectorizedStream at : " + i)
- private def streamHeadIndex : Int = indexed.size
- private var stream : Stream[T] = initial
- private var indexed : Vector[T] = Vector.empty
-
- def apply(index : Int) : T = {
- if(index < streamHeadIndex) {
- indexed(index)
- } else {
- val diff = index - streamHeadIndex // diff >= 0
- var i = 0
- while(i < diff) {
- if(stream.isEmpty) throw mkException(index)
- indexed = indexed :+ stream.head
- stream = stream.tail
- i += 1
- }
- // The trick is *not* to read past the desired element. Leave it in the
- // stream, or it will force the *following* one...
- stream.headOption.getOrElse { throw mkException(index) }
- }
- }
- }
-
- private def intStream : Stream[Expr] = Stream.cons(IntLiteral(0), intStream0(1))
- private def intStream0(n : Int) : Stream[Expr] = Stream.cons(IntLiteral(n), intStream0(if(n > 0) -n else -(n-1)))
+ val bounds = _bounds.getOrElse(Map())
private def tpStream(tp: TypeParameter, i: Int = 1): Stream[Expr] = Stream.cons(GenericValue(tp, i), tpStream(tp, i+1))
- def natStream : Stream[Expr] = natStream0(0)
- private def natStream0(n : Int) : Stream[Expr] = Stream.cons(IntLiteral(n), natStream0(n+1))
-
private val streamCache : MutableMap[TypeTree,Stream[Expr]] = MutableMap.empty
-
- def generate(tpe : TypeTree, bounds : Map[TypeTree,Seq[Expr]] = defaultBounds) : Stream[Expr] = {
+ def generate(tpe : TypeTree) : Stream[Expr] = {
try {
streamCache.getOrElse(tpe, {
- val s = generate0(tpe, bounds)
+ val s = generate0(tpe)
streamCache(tpe) = s
s
})
@@ -75,20 +37,19 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
}
}
- // TODO We should make sure the cache depends on the bounds (i.e. is not reused for different bounds.)
- private def generate0(tpe : TypeTree, bounds : Map[TypeTree,Seq[Expr]]) : Stream[Expr] = bounds.get(tpe).map(_.toStream).getOrElse {
+ private def generate0(tpe: TypeTree): Stream[Expr] = bounds.get(tpe).map(_.toStream).getOrElse {
tpe match {
case BooleanType =>
- boolStream
+ BooleanLiteral(true) #:: BooleanLiteral(false) #:: Stream.empty
case Int32Type =>
- intStream
+ IntLiteral(0) #:: IntLiteral(1) #:: IntLiteral(-1) #:: Stream.empty
case tp: TypeParameter =>
tpStream(tp)
case TupleType(bses) =>
- naryProduct(bses.map(generate(_, bounds))).map(Tuple)
+ cartesianProduct(bses.map(generate(_))).map(Tuple)
case act : AbstractClassType =>
// We prioritize base cases among the children.
@@ -100,12 +61,12 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
// The stream for leafs...
val leafsStream = leafs.toStream.flatMap { cct =>
- generate(cct, bounds)
+ generate(cct)
}
// ...to which we append the streams for constructors.
leafsStream.append(interleave(conss.map { cct =>
- generate(cct, bounds)
+ generate(cct)
}))
case cct : CaseClassType =>
@@ -113,115 +74,31 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
Stream.cons(CaseClass(cct, Nil), Stream.empty)
} else {
val fieldTypes = cct.fieldsTypes
- val subStream = naryProduct(fieldTypes.map(generate(_, bounds)))
- subStream.map(prod => CaseClass(cct, prod))
+ cartesianProduct(fieldTypes.map(generate(_))).map(CaseClass(cct, _))
}
case _ => Stream.empty
}
}
- //def findModels(expr : Expr, maxModels : Int, maxTries : Int, bounds : Map[TypeTree,Seq[Expr]] = defaultBounds, forcedFreeVars: Option[Seq[Identifier]] = None) : Stream[Map[Identifier,Expr]] = {
def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid : Int, maxEnumerated : Int) : Iterator[Seq[Expr]] = {
- evaluator.compile(satisfying, ins).map { evalFun =>
- val sat = EvaluationResults.Successful(BooleanLiteral(true))
-
- naryProduct(ins.map(id => generate(id.getType, bounds)))
- .take(maxEnumerated)
- .takeWhile(s => !interrupted.get)
- .filter{s => evalFun(s) == sat }
- .take(maxValid)
- .iterator
-
- } getOrElse {
- Stream.empty.iterator
- }
- }
-
- // The following are stream utilities.
-
- // Takes a series of streams and merges them, round-robin style.
- private def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = int0(streams)
- private def int0[T](streams : Seq[Stream[T]]) : Stream[T] = {
- var ss = streams
- while(!ss.isEmpty && ss.head.isEmpty) {
- ss = ss.tail
- }
- if(ss.isEmpty) return Stream.empty
- if(ss.size == 1) return ss(0)
- // TODO: This circular-shifts the list. I'd be interested in a constant time
- // operation. Perhaps simply by choosing the right data-structure?
- Stream.cons(ss.head.head, interleave(ss.tail :+ ss.head.tail))
- }
-
- // Takes a series of streams and enumerates their cartesian product.
- private def naryProduct[T](streams : Seq[Stream[T]]) : Stream[List[T]] = {
- val dimensions = streams.size
- val vectorizedStreams = streams.map(new VectorizedStream(_))
-
- if(dimensions == 0)
- return Stream.cons(Nil, Stream.empty)
-
- if(streams.exists(_.isEmpty))
- return Stream.empty
-
- val indices = if(streams.forall(_.hasDefiniteSize)) {
- val max = streams.map(_.size).max
- diagCount(dimensions).take(max)
+ val filtering = if (satisfying == BooleanLiteral(true)) {
+ { (e: Seq[Expr]) => true }
} else {
- diagCount(dimensions)
- }
-
- var allReached : Boolean = false
- val bounds : Array[Int] = Array.fill(dimensions)(Int.MaxValue)
-
- indices.takeWhile(_ => !allReached).flatMap { indexList =>
- var d = 0
- var continue = true
- var is = indexList
- var ss = vectorizedStreams.toList
+ evaluator.compile(satisfying, ins).map { evalFun =>
+ val sat = EvaluationResults.Successful(BooleanLiteral(true))
- if(indexList.sum >= bounds.max) {
- allReached = true
+ { (e: Seq[Expr]) => evalFun(e) == sat }
+ } getOrElse {
+ { (e: Seq[Expr]) => false }
}
-
- var tuple : List[T] = Nil
-
- while(continue && d < dimensions) {
- var i = is.head
- if(i > bounds(d)) {
- continue = false
- } else try {
- // TODO can we speed up by caching the random access into
- // the stream in an indexedSeq? After all, `i` increases
- // slowly.
- tuple = (ss.head)(i) :: tuple
- is = is.tail
- ss = ss.tail
- d += 1
- } catch {
- case e : IndexOutOfBoundsException =>
- bounds(d) = i - 1
- continue = false
- }
- }
- if(continue) Some(tuple.reverse) else None
}
- }
- // Utility function for n-way cartesian product.
- // Counts over indices in `dim` dimensions in a fair, diagonal, way.
- private def diagCount(dim : Int) : Stream[List[Int]] = diag0(dim, 0)
- private def diag0(dim : Int, nextSum : Int) : Stream[List[Int]] = summingTo(nextSum, dim).append(diag0(dim, nextSum + 1))
- // All tuples of dimension `n` whose sum is `sum`.
- private def summingTo(sum : Int, n : Int) : Stream[List[Int]] = {
- // assert(sum >= 0)
- if(sum < 0) {
- Stream.empty
- } else if(n == 1) {
- Stream.cons(sum :: Nil, Stream.empty)
- } else {
- (0 to sum).toStream.flatMap(fst => summingTo(sum - fst, n - 1).map(fst :: _))
- }
+ cartesianProduct(ins.map(id => generate(id.getType)))
+ .take(maxEnumerated)
+ .takeWhile(s => !interrupted.get)
+ .filter{filtering}
+ .take(maxValid)
+ .iterator
}
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index bf5efce46c23be9074ac4c08c13ced0a7cc51e16..8803ae47dc84f96f169e800e0bd89e1d26fc7e24 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -8,6 +8,7 @@ import Trees._
object Extractors {
import Common._
import TypeTrees._
+ import TypeTreeOps._
import Definitions._
import Extractors._
import TreeOps._
@@ -108,7 +109,15 @@ object Extractors {
case ((keys, values, isKey), rExpr) => if(isKey) (rExpr::keys, values, false) else (keys, rExpr::values, true)
}
assert(isKey)
- FiniteMap(keys.zip(values))
+ val tpe = (keys, values) match {
+ case (Seq(), Seq()) => expr.getType
+ case _ =>
+ MapType(
+ leastUpperBound(keys.map(_.getType)).get,
+ leastUpperBound(values.map(_.getType)).get
+ )
+ }
+ FiniteMap(keys.zip(values)).setType(tpe)
}
Some((subArgs, builder))
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 6065fc172bd8bedf7b9f0c90d6476479f221b8e7..e0557a3d82e4ad239c9e995e333237ef53ff3c04 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -689,8 +689,8 @@ object TreeOps {
case TuplePattern(_, subps) =>
val TupleType(subts) = in.getType
- val subExprs = (subps zip subts) map {
- case (p, t) => p.binder.getOrElse(FreshIdentifier("b", true).setType(t)).toVariable
+ val subExprs = (subps zip subts).zipWithIndex map {
+ case ((p, t), index) => p.binder.map(_.toVariable).getOrElse(TupleSelect(in, index+1))
}
// Special case to get rid of (a,b) match { case (c,d) => .. }
@@ -706,8 +706,8 @@ object TreeOps {
})
case CaseClassPattern(_, cct, subps) =>
- val subExprs = (subps zip cct.fieldsTypes) map {
- case (p, t) => p.binder.getOrElse(FreshIdentifier("b", true).setType(t)).toVariable
+ val subExprs = (subps zip cct.fields) map {
+ case (p, f) => p.binder.map(_.toVariable).getOrElse(CaseClassSelector(cct, in, f.id))
}
// Special case to get rid of Cons(a,b) match { case Cons(c,d) => .. }
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
index 71b08a49cb422687fd34a1e04781ee1351be4252..8b4ea7c175b99a6a2c78e949509cd4f44cdbe462 100644
--- a/src/main/scala/leon/refactor/Repairman.scala
+++ b/src/main/scala/leon/refactor/Repairman.scala
@@ -23,6 +23,8 @@ import synthesis._
class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
val reporter = ctx.reporter
+ implicit val debugSection = DebugSectionRefactor
+
var testBank = List[Example]()
var solutions: List[(Solution, Expr, List[FunDef])] = Nil
@@ -45,7 +47,11 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
tupleWrap(ins) -> tupleWrap(outs)
}.toList).setType(MapType(argsWrapped.getType, out.getType))
- val passes = FunctionInvocation(tfd, Seq(argsWrapped, out.toVariable, testsExpr))
+ val passes = if (testsExpr.singletons.nonEmpty) {
+ FunctionInvocation(tfd, Seq(argsWrapped, out.toVariable, testsExpr))
+ } else {
+ BooleanLiteral(true)
+ }
// Compute guide implementation
val gexpr = fd.body.get
@@ -58,8 +64,8 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
val term = FunctionInvocation(termfd.typed(Seq(fd.returnType)), Seq(withinCall))
val spec = And(Seq(
- fd.postcondition.map(_._2).getOrElse(BooleanLiteral(true))
- // passes
+ fd.postcondition.map(_._2).getOrElse(BooleanLiteral(true)),
+ passes
))
val pc = And(Seq(
@@ -211,6 +217,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
val tests = new NaiveDataGen(ctx, program, evaluator)
val pre = fd.precondition.getOrElse(BooleanLiteral(true))
+
val inputs = tests.generateFor(fd.params.map(_.id), pre, 30, 10000).toList
testBank ++= inputs.map { i =>
@@ -232,4 +239,5 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
}
discoverTests()
+
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index fae464a790c904b5e14d50f98b12a466bebbf22d..9623624af94dc495cbe1edc335ba4cde5fca0197 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -38,18 +38,17 @@ object Rules {
//AngelicHoles // @EK: Disabled now as it is explicit with withOracle { .. }
)
- def getInstantiations(sctx: SynthesisContext, problem: Problem) = {
- val sub = sctx.rules.flatMap { r =>
- r.instantiateOn(sctx, problem)
- }
+ def getInstantiations(sctx: SynthesisContext, problem: Problem): List[RuleInstantiation] = {
- val res = sub.groupBy(_.priority).toSeq.sortBy(_._1)
+ val rulesPrio = sctx.rules.groupBy(_.priority).toSeq.sortBy(_._1)
- if (res.nonEmpty) {
- res.head._2.toList
- } else {
- Nil
+ for ((_, rs) <- rulesPrio) {
+ val results = rs.flatMap(_.instantiateOn(sctx, problem)).toList
+ if (results.nonEmpty) {
+ return results;
+ }
}
+ Nil
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index e00c5f5d77fd490035aa4d40afd15280b4c8ef22..160f3ec13e5a2c97783f5bed15f3179318600995 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -4,6 +4,7 @@ package leon
package synthesis
package rules
+import leon.utils.StreamUtils
import solvers._
import solvers.z3._
@@ -18,7 +19,7 @@ import purescala.Extractors._
import purescala.ScalaPrinter
import utils.Helpers._
-import scala.collection.mutable.{Map=>MutableMap}
+import scala.collection.mutable.{HashMap=>MutableMap, ArrayBuffer}
import evaluators._
import datagen._
@@ -34,11 +35,10 @@ case object CEGIS extends Rule("CEGIS") {
val useUninterpretedProbe = sctx.options.cegisUseUninterpretedProbe
val useUnsatCores = sctx.options.cegisUseUnsatCores
val useOptTimeout = sctx.options.cegisUseOptTimeout
- val useFunGenerators = sctx.options.cegisGenerateFunCalls
- val useBPaths = sctx.options.cegisUseBPaths
val useVanuatoo = sctx.options.cegisUseVanuatoo
val useCETests = sctx.options.cegisUseCETests
val useCEPruning = sctx.options.cegisUseCEPruning
+
// Limits the number of programs CEGIS will specifically test for instead of reasonning symbolically
val testUpTo = 5
val useBssFiltering = sctx.options.cegisUseBssFiltering
@@ -48,38 +48,56 @@ case object CEGIS extends Rule("CEGIS") {
val interruptManager = sctx.context.interruptManager
- val grammar = new ExpressionGrammar(sctx, p)
-
class NonDeterministicProgram(val p: Problem,
val initGuard: Identifier) {
- //var program: Expr = BooleanLiteral(true)
+ val grammar = new ExpressionGrammar(sctx, p)
// 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
+ // b -> Set(c1, c2) means c1 and c2 are uninterpreted behind 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)
+ /**
+ * Stores which b's guard which c's, which then are represented by which
+ * b's:
+ *
+ * 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)
+ /**
+ * Computes dependencies of c's
+ *
+ * Assuming encoding:
+ * b1 => c == F(c2, c3)
+ * b2 => c == F(c4, c5)
+ *
+ * will be represented here as c -> Set(c2, c3, c4, c5)
+ */
+ private var cChildren: Map[Identifier, Set[Identifier]] = Map().withDefaultValue(Set())
+
// Returns all possible assignments to Bs in order to enumerate all possible programs
- def allPrograms(): Set[Set[Identifier]] = {
+ def allPrograms(): Traversable[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 =>
+ val streams = cToBs.values.toSeq.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 } }
+ StreamUtils.cartesianProduct(streams).map { ls =>
+ ls.foldLeft(Set[Identifier]())(_ ++ _)
+ }
case None =>
Stream.cons(Set(b), Stream.empty)
}
@@ -93,10 +111,6 @@ case object CEGIS extends Rule("CEGIS") {
* 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())
-
-
type EvaluationResult = EvaluationResults.Result
private var triedCompilation = false
@@ -159,7 +173,7 @@ case object CEGIS extends Rule("CEGIS") {
// 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
+ val baseExpr = removeWitnesses(sctx.program)(p.phi)
bssOrdered = bss.toSeq.sortBy(_.id)
@@ -235,6 +249,10 @@ case object CEGIS extends Rule("CEGIS") {
}
+ /**
+ * Shrinks the non-deterministic program to the provided set of
+ * alternatives only
+ */
def filterFor(remainingBss: Set[Identifier]): Seq[Expr] = {
val filteredBss = remainingBss + initGuard
@@ -283,14 +301,18 @@ case object CEGIS extends Rule("CEGIS") {
(pathConstraints ++ impliess).toSeq
}
- def unroll: (List[Expr], Set[Identifier]) = {
+ def unroll(finalUnrolling: Boolean): (List[Expr], Set[Identifier]) = {
var newClauses = List[Expr]()
var newGuardedTerms = Map[Identifier, Set[Identifier]]()
var newMappings = Map[Identifier, (Identifier, Expr)]()
+
for ((parentGuard, recIds) <- guardedTerms; recId <- recIds) {
- val alts = grammar.getGenerators(recId.getType)
+ var alts = grammar.getGenerators(recId.getType)
+ if (finalUnrolling) {
+ alts = alts.filter(_.subTrees.isEmpty)
+ }
val altsWithBranches = alts.map(alt => FreshIdentifier("B", true).setType(BooleanType) -> alt)
@@ -305,8 +327,15 @@ case object CEGIS extends Rule("CEGIS") {
val pre = And(Seq(Or(failedPath +: bvs), Implies(failedPath, And(bvs.map(Not(_))))) ++ distinct)
+ var cBankCache = Map[TypeTree, Stream[Identifier]]()
+ def freshC(t: TypeTree): Stream[Identifier] = Stream.cons(FreshIdentifier("c", true).setType(t), freshC(t))
+ def getC(t: TypeTree, index: Int) = cBankCache.getOrElse(t, {
+ cBankCache += t -> freshC(t)
+ cBankCache(t)
+ })(index)
+
val cases = for((bid, gen) <- altsWithBranches.toList) yield { // b1 => E(gen1, gen2) [b1 -> {gen1, gen2}]
- val rec = gen.subTrees.map(FreshIdentifier("c", true).setType(_))
+ val rec = for ((t, i) <- gen.subTrees.zipWithIndex) yield { getC(t, i) }
val ex = gen.builder(rec.map(_.toVariable))
if (!rec.isEmpty) {
@@ -325,6 +354,11 @@ case object CEGIS extends Rule("CEGIS") {
newClauses = newClauses ::: pre :: cases
}
+ sctx.reporter.ifDebug { printer =>
+ printer("Grammar so far:");
+ grammar.printGrammar(printer)
+ }
+
//program = And(program :: newClauses)
mappings = mappings ++ newMappings
@@ -352,31 +386,33 @@ case object CEGIS extends Rule("CEGIS") {
val initGuard = FreshIdentifier("START", true).setType(BooleanType)
val ndProgram = new NonDeterministicProgram(p, initGuard)
- var unrolings = 0
+ var unrolings = 1
val maxUnrolings = 3
val exSolverTo = 2000L
val cexSolverTo = 2000L
- var baseExampleInputs: Seq[Seq[Expr]] = Seq()
+ 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")
baseExampleInputs ++= p.getTests(sctx).map(_.ins).toSet
- if (p.pc == BooleanLiteral(true)) {
- baseExampleInputs = p.as.map(a => simplestValue(a.getType)) +: baseExampleInputs
+ val safePc = removeWitnesses(sctx.program)(p.pc)
+
+ if (safePc == BooleanLiteral(true)) {
+ baseExampleInputs += p.as.map(a => simplestValue(a.getType))
} else {
val solver = sctx.newSolver.setTimeout(exSolverTo)
- solver.assertCnstr(p.pc)
+ solver.assertCnstr(safePc)
try {
solver.check match {
case Some(true) =>
val model = solver.getModel
- baseExampleInputs = p.as.map(a => model.getOrElse(a, simplestValue(a.getType))) +: baseExampleInputs
+ baseExampleInputs += p.as.map(a => model.getOrElse(a, simplestValue(a.getType)))
case Some(false) =>
return RuleFailed()
@@ -396,25 +432,37 @@ case object CEGIS extends Rule("CEGIS") {
}
}
+ /**
+ * We generate tests for discarding potential programs
+ */
val inputIterator: Iterator[Seq[Expr]] = if (useVanuatoo) {
- new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, 20, 3000)
+ new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, safePc, 20, 3000)
} else {
- new NaiveDataGen(sctx.context, sctx.program, evaluator).generateFor(p.as, p.pc, 20, 1000)
+ new NaiveDataGen(sctx.context, sctx.program, evaluator).generateFor(p.as, safePc, 20, 1000)
}
val cachedInputIterator = new Iterator[Seq[Expr]] {
def next() = {
val i = inputIterator.next()
- baseExampleInputs = i +: baseExampleInputs
+ baseExampleInputs += i
i
}
def hasNext() = inputIterator.hasNext
}
+ val failedTestsStats = new MutableMap[Seq[Expr], Int]().withDefaultValue(0)
+
def hasInputExamples() = baseExampleInputs.size > 0 || cachedInputIterator.hasNext
- def allInputExamples() = baseExampleInputs.iterator ++ cachedInputIterator
+ var n = 1;
+ def allInputExamples() = {
+ if (n % 1000 == 0) {
+ baseExampleInputs = baseExampleInputs.sortBy(e => -failedTestsStats(e))
+ }
+ n += 1
+ baseExampleInputs.iterator ++ cachedInputIterator
+ }
def checkForPrograms(programs: Set[Set[Identifier]]): RuleApplication = {
for (prog <- programs) {
@@ -422,7 +470,7 @@ case object CEGIS extends Rule("CEGIS") {
val res = Equals(Tuple(p.xs.map(Variable(_))), expr)
val solver3 = sctx.newSolver.setTimeout(cexSolverTo)
- solver3.assertCnstr(And(p.pc :: res :: Not(p.phi) :: Nil))
+ solver3.assertCnstr(And(safePc :: res :: Not(p.phi) :: Nil))
try {
solver3.check match {
@@ -444,8 +492,8 @@ case object CEGIS extends Rule("CEGIS") {
// Keep track of collected cores to filter programs to test
var collectedCores = Set[Set[Identifier]]()
- val initExClause = And(p.pc :: p.phi :: Variable(initGuard) :: Nil)
- val initCExClause = And(p.pc :: Not(p.phi) :: Variable(initGuard) :: Nil)
+ val initExClause = And(safePc :: p.phi :: Variable(initGuard) :: Nil)
+ val initCExClause = And(safePc :: Not(p.phi) :: Variable(initGuard) :: Nil)
// solver1 is used for the initial SAT queries
var solver1 = sctx.newSolver.setTimeout(exSolverTo)
@@ -466,7 +514,7 @@ case object CEGIS extends Rule("CEGIS") {
var bssAssumptions = Set[Identifier]()
if (!didFilterAlready) {
- val (clauses, closedBs) = ndProgram.unroll
+ val (clauses, closedBs) = ndProgram.unroll(unrolings == maxUnrolings)
bssAssumptions = closedBs
@@ -486,7 +534,7 @@ case object CEGIS extends Rule("CEGIS") {
// Compute all programs that have not been excluded yet
var prunedPrograms: Set[Set[Identifier]] = if (useCEPruning) {
- ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p)))
+ ndProgram.allPrograms.filterNot(p => collectedCores.exists(c => c.subsetOf(p))).toSet
} else {
Set()
}
@@ -495,26 +543,33 @@ case object CEGIS extends Rule("CEGIS") {
sctx.reporter.debug("#Programs: "+prunedPrograms.size)
+ var wrongPrograms = Set[Set[Identifier]]();
+
// We further filter the set of working programs to remove those that fail on known examples
if (useCEPruning && hasInputExamples() && ndProgram.canTest()) {
for (p <- prunedPrograms if !interruptManager.isInterrupted()) {
- if (!allInputExamples().forall(ndProgram.testForProgram(p))) {
- // This program failed on at least one example
- solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
- prunedPrograms -= p
+ var valid = true
+ val examples = allInputExamples()
+ while(valid && examples.hasNext) {
+ val e = examples.next()
+ println("Running on "+e)
+ if (!ndProgram.testForProgram(p)(e)) {
+ failedTestsStats(e) += 1
+ wrongPrograms += p
+ prunedPrograms -= p
+ valid = false;
+ }
+ println("Done")
}
- }
- if (prunedPrograms.isEmpty) {
- needMoreUnrolling = true
+ if (wrongPrograms.size % 1000 == 0) {
+ sctx.reporter.debug("..."+wrongPrograms.size)
+ }
}
-
- //println("Passing tests: "+prunedPrograms.size)
}
val nPassing = prunedPrograms.size
-
sctx.reporter.debug("#Programs passing tests: "+nPassing)
if (nPassing == 0) {
@@ -525,6 +580,9 @@ case object CEGIS extends Rule("CEGIS") {
case rs: RuleClosed =>
result = Some(rs)
case _ =>
+ wrongPrograms.foreach { p =>
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ }
}
} else if (((nPassing < allPrograms*filterThreshold) || didFilterAlready) && useBssFiltering) {
// We filter the Bss so that the formula we give to z3 is much smalled
@@ -548,6 +606,10 @@ case object CEGIS extends Rule("CEGIS") {
solver1.assertCnstr(clause)
solver2.assertCnstr(clause)
+ } else {
+ wrongPrograms.foreach { p =>
+ solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
+ }
}
val bss = ndProgram.bss
@@ -592,7 +654,7 @@ case object CEGIS extends Rule("CEGIS") {
val newCE = p.as.map(valuateWithModel(invalidModel))
- baseExampleInputs = newCE +: baseExampleInputs
+ baseExampleInputs += newCE
// Retest whether the newly found C-E invalidates all programs
if (useCEPruning && ndProgram.canTest) {
@@ -674,7 +736,7 @@ case object CEGIS extends Rule("CEGIS") {
}
unrolings += 1
- } while(unrolings < maxUnrolings && result.isEmpty && !interruptManager.isInterrupted())
+ } while(unrolings <= maxUnrolings && result.isEmpty && !interruptManager.isInterrupted())
result.getOrElse(RuleFailed())
diff --git a/src/main/scala/leon/synthesis/rules/GuidedCloser.scala b/src/main/scala/leon/synthesis/rules/GuidedCloser.scala
index d38be690679b53c59e0efa96d74f72a025659969..eb4843903ba4f9f06d8b8d26f679fddeacc1651e 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/synthesis/rules/GuidedCloser.scala
@@ -40,7 +40,6 @@ case object GuidedCloser extends NormalizingRule("Guided Closer") {
solver.assertCnstr(vc)
val osol = solver.check match {
case Some(false) =>
- println("==== UNSAT ===")
Some(Solution(BooleanLiteral(true), Set(), wrappedE, true))
case None =>
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index c2e5d2c0cb2b55984a8f8d528853226feb878047..fe63e4ce5b83032b2e13f2309b30df0fdb1f6e0f 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -151,7 +151,7 @@ class ExpressionGrammar(ctx: LeonContext, prog: Program, inputs: Seq[Expr], curr
}
}
- val funcs = visibleFunDefsFromMain(prog).toSeq.flatMap(getCandidates)
+ val funcs = functionsAvailable(prog).toSeq.flatMap(getCandidates)
funcs.map{ tfd =>
Generator[TypeTree, Expr](tfd.params.map(_.tpe), { sub => FunctionInvocation(tfd, sub) })
@@ -170,12 +170,12 @@ class ExpressionGrammar(ctx: LeonContext, prog: Program, inputs: Seq[Expr], curr
}
}
- def printGrammar() {
+ def printGrammar(printer: String => Unit) {
for ((t, gs) <- cache; g <- gs) {
val subs = g.subTrees.map { tpe => FreshIdentifier(tpe.toString).setType(tpe).toVariable }
val gen = g.builder(subs)
- println(f"$t%30s ::= "+gen)
+ printer(f"$t%30s ::= "+gen)
}
}
}
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index a0806f5c53968a900357e14688a3bbf2fefa27a7..cfc8d574546b76cdae92660be56063ffcaf58636 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -3,6 +3,19 @@
package leon.utils
object StreamUtils {
+ def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
+ var ss = streams
+ while(!ss.isEmpty && ss.head.isEmpty) {
+ ss = ss.tail
+ }
+ if(ss.isEmpty) return Stream.empty
+ if(ss.size == 1) return ss(0)
+
+ // TODO: This circular-shifts the list. I'd be interested in a constant time
+ // operation. Perhaps simply by choosing the right data-structure?
+ Stream.cons(ss.head.head, interleave(ss.tail :+ ss.head.tail))
+ }
+
def cartesianProduct[T](streams : Seq[Stream[T]]) : Stream[List[T]] = {
val dimensions = streams.size
val vectorizedStreams = streams.map(new VectorizedStream(_))
diff --git a/testcases/synthesis/repair/HeapSort/HeapSort2.scala b/testcases/synthesis/repair/HeapSort/HeapSort2.scala
index c33921bee19b368bd21a2308e63a8da6835c9e59..706d47074be2cfe83a651a0a7fce54e442a6b35e 100644
--- a/testcases/synthesis/repair/HeapSort/HeapSort2.scala
+++ b/testcases/synthesis/repair/HeapSort/HeapSort2.scala
@@ -50,7 +50,7 @@ object HeapSort {
hasLeftistProperty(res) &&
heapSize(h1) + heapSize(h2) == heapSize(res)
}
-/*
+
private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
require(hasLeftistProperty(left) && hasLeftistProperty(right))
if(left.rank >= right.rank)
@@ -58,7 +58,7 @@ object HeapSort {
else
Node(value, right, left)
} ensuring { hasLeftistProperty(_) }
-*/
+
def insert(element: Int, heap: Heap) : Heap = {
require(hasLeftistProperty(heap))
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic1.scala b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
index 9668ca1a1bbfd288d27ca65728077e196c2ce3ba..8ff0b9f158014010b928fb838a3e8e28a20c9a0f 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic1.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
@@ -5,11 +5,11 @@ import leon.collection._
object SemanticsPreservation {
sealed abstract class Formula
- case class And(lhs : Formula, rhs : Formula) extends Formula
- case class Or(lhs : Formula, rhs : Formula) extends Formula
- case class Not(f: Formula) extends Formula
case class Const(v: Boolean) extends Formula
case class Literal(id: Int) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class And(lhs : Formula, rhs : Formula) extends Formula
+ case class Or(lhs : Formula, rhs : Formula) extends Formula
def size(f : Formula) : Int = { f match {
case And(l,r) => 1 + size(l) + size(r)
@@ -33,7 +33,7 @@ object SemanticsPreservation {
case Not(Not(e)) => e // FIXME: should be nnf(e)
case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- case other => other
+ case other => other
}} ensuring { isNNF(_) }
def isNNF(f : Formula) : Boolean = f match {