From a541166ce051c16ce3a208166218179894cd5b29 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 3 Mar 2014 12:36:55 +0100
Subject: [PATCH] Stabilize datagen, fix interrupts & parallel, fix array
boxing
---
build.sbt | 4 +
.../java/leon/codegen/runtime/ArrayBox.java | 85 +++++++++++++++++++
.../scala/leon/codegen/CodeGeneration.scala | 17 +++-
.../scala/leon/codegen/CompilationUnit.scala | 2 +-
.../scala/leon/datagen/NaiveDataGen.scala | 5 ++
.../scala/leon/datagen/VanuatooDataGen.scala | 68 +++++++++++----
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../frontends/scalac/CodeExtraction.scala | 8 +-
.../scala/leon/purescala/PrettyPrinter.scala | 2 +-
.../scala/leon/purescala/ScalaPrinter.scala | 2 +-
src/main/scala/leon/purescala/TreeOps.scala | 8 +-
src/main/scala/leon/purescala/Trees.scala | 2 +-
.../scala/leon/purescala/TypeTreeOps.scala | 16 ++--
src/main/scala/leon/purescala/TypeTrees.scala | 28 +-----
.../leon/solvers/EnumerationSolver.scala | 42 +++++----
.../solvers/combinators/PortfolioSolver.scala | 4 +
.../leon/solvers/z3/AbstractZ3Solver.scala | 46 +++++-----
.../condabd/SynthesizerExamples.scala | 2 +-
.../insynth/leon/loader/PreLoader.scala | 4 +-
.../leon/verification/AnalysisPhase.scala | 2 +-
.../xlang/ImperativeCodeElimination.scala | 6 +-
src/main/scala/leon/xlang/TreeOps.scala | 4 +-
.../insynth/testutil/CommonDeclarations.scala | 2 +-
.../test/condabd/refinement/FilterTest.scala | 10 +--
.../PureScalaVerificationRegression.scala | 1 +
25 files changed, 260 insertions(+), 112 deletions(-)
create mode 100644 src/main/java/leon/codegen/runtime/ArrayBox.java
diff --git a/build.sbt b/build.sbt
index 3e3014e82..ba228dd81 100644
--- a/build.sbt
+++ b/build.sbt
@@ -37,6 +37,10 @@ logBuffered in Test := false
testOptions in Test += Tests.Argument("-oD")
+javaOptions in test += "-Xss32M"
+
+parallelExecution in Test := false
+
sourcesInBase in Compile := false
// do not skip parent Eclipse project definition
diff --git a/src/main/java/leon/codegen/runtime/ArrayBox.java b/src/main/java/leon/codegen/runtime/ArrayBox.java
new file mode 100644
index 000000000..07f4bec8e
--- /dev/null
+++ b/src/main/java/leon/codegen/runtime/ArrayBox.java
@@ -0,0 +1,85 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon.codegen.runtime;
+
+import java.util.Arrays;
+
+/** If someone wants to make it an efficient implementation of immutable
+ * sets, go ahead. */
+public final class ArrayBox {
+ private final Object[] obj1;
+ private final int[] obj2;
+ private final boolean[] obj3;
+ private final int mode;
+
+ protected final Object[] arrayValue() {
+ return obj1;
+ }
+
+ protected final int[] arrayValueI() {
+ return obj2;
+ }
+
+ protected final boolean[] arrayValueZ() {
+ return obj3;
+ }
+
+ public ArrayBox(Object[] array) {
+ obj1 = array;
+ obj2 = null;
+ obj3 = null;
+ mode = 1;
+ }
+
+ public ArrayBox(int[] array) {
+ obj1 = null;
+ obj2 = array;
+ obj3 = null;
+ mode = 2;
+ }
+
+ public ArrayBox(boolean[] array) {
+ obj1 = null;
+ obj2 = null;
+ obj3 = array;
+ mode = 3;
+ }
+
+ @Override
+ public boolean equals(Object that) {
+ if(that == this) return true;
+ if(!(that instanceof ArrayBox)) return false;
+
+ ArrayBox other = (ArrayBox)that;
+
+ if (mode == 1) {
+ return (other.mode == 1) && Arrays.equals(this.obj1, other.obj1);
+ } else if (mode == 2) {
+ return (other.mode == 2) && Arrays.equals(this.obj2, other.obj2);
+ } else {
+ return (other.mode == 3) && Arrays.equals(this.obj3, other.obj3);
+ }
+ }
+
+ @Override
+ public String toString() {
+ if (mode == 1) {
+ return Arrays.toString(obj1);
+ } else if (mode == 2) {
+ return Arrays.toString(obj2);
+ } else {
+ return Arrays.toString(obj3);
+ }
+ }
+
+ @Override
+ public int hashCode() {
+ if (mode == 1) {
+ return Arrays.hashCode(obj1);
+ } else if (mode == 2) {
+ return Arrays.hashCode(obj2);
+ } else {
+ return Arrays.hashCode(obj3);
+ }
+ }
+}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index d815a0549..0702fb7da 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -34,6 +34,8 @@ trait CodeGeneration {
private[codegen] val BoxedIntClass = "java/lang/Integer"
private[codegen] val BoxedBoolClass = "java/lang/Boolean"
+ private[codegen] val BoxedArrayClass = "leon/codegen/runtime/ArrayBox"
+
private[codegen] val TupleClass = "leon/codegen/runtime/Tuple"
private[codegen] val SetClass = "leon/codegen/runtime/Set"
private[codegen] val MapClass = "leon/codegen/runtime/Map"
@@ -166,7 +168,7 @@ trait CodeGeneration {
case BooleanLiteral(v) =>
ch << Ldc(if(v) 1 else 0)
- case UnitLiteral =>
+ case UnitLiteral() =>
ch << Ldc(1)
// Case classes
@@ -458,6 +460,11 @@ trait CodeGeneration {
mkExpr(e, ch)
ch << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")
+ case at @ ArrayType(et) =>
+ ch << New(BoxedArrayClass) << DUP
+ mkExpr(e, ch)
+ ch << InvokeSpecial(BoxedArrayClass, constructorName, "(%s)V".format(typeToJVM(at)))
+
case _ =>
mkExpr(e, ch)
}
@@ -473,7 +480,9 @@ trait CodeGeneration {
case BooleanType | UnitType =>
ch << New(BoxedBoolClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")
- case _ =>
+ case at @ ArrayType(et) =>
+ ch << New(BoxedArrayClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedArrayClass, constructorName, "(%s)V".format(typeToJVM(at)))
+ case _ =>
}
}
@@ -503,6 +512,10 @@ trait CodeGeneration {
case tp : TypeParameter =>
+ case tp : ArrayType =>
+ ch << CheckCast(BoxedArrayClass) << InvokeVirtual(BoxedArrayClass, "arrayValue", "()%s".format(typeToJVM(tp)))
+ ch << CheckCast(typeToJVM(tp))
+
case _ =>
throw new CompilationException("Unsupported type in unboxing : " + tpe)
}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 8993fdc48..0af4052a6 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -348,7 +348,7 @@ class CompilationUnit(val ctx: LeonContext,
object CompilationUnit {
private var _nextExprId = 0
- private def nextExprId = {
+ private def nextExprId = synchronized {
_nextExprId += 1
_nextExprId
}
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 5bd33cb85..7be5b1075 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -55,6 +55,8 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
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)))
+ 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))
@@ -77,6 +79,9 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
case Int32Type =>
intStream
+ case tp: TypeParameter =>
+ tpStream(tp)
+
case TupleType(bses) =>
naryProduct(bses.map(generate(_, bounds))).map(Tuple)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index e94415131..12f76a2a8 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -34,9 +34,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
ConstructorPattern[Expr, TypeTree](c, args)
}
- private var ccConstructors = Map[CaseClassType, Constructor[Expr, TypeTree]]()
- private var acConstructors = Map[AbstractClassType, List[Constructor[Expr, TypeTree]]]()
- private var tConstructors = Map[TupleType, Constructor[Expr, TypeTree]]()
+ private var constructors = Map[TypeTree, List[Constructor[Expr, TypeTree]]]()
private def getConstructorFor(t: CaseClassType, act: AbstractClassType): Constructor[Expr, TypeTree] = {
// We "up-cast" the returnType of the specific caseclass generator to match its superclass
@@ -45,30 +43,66 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
private def getConstructors(t: TypeTree): List[Constructor[Expr, TypeTree]] = t match {
+ case UnitType =>
+ constructors.getOrElse(t, {
+ val cs = List(Constructor[Expr, TypeTree](List(), t, s => UnitLiteral(), "()"))
+ constructors += t -> cs
+ cs
+ })
+
+ case at @ ArrayType(sub) =>
+ constructors.getOrElse(at, {
+ val cs = for (size <- List(0, 1, 2, 5)) yield {
+ Constructor[Expr, TypeTree]((1 to size).map(i => sub).toList, at, s => FiniteArray(s).setType(at), at.toString+"@"+size)
+ }
+ constructors += at -> cs
+ cs
+ })
+
case tt @ TupleType(parts) =>
- List(tConstructors.getOrElse(tt, {
- val c = Constructor[Expr, TypeTree](parts, tt, s => Tuple(s).setType(tt), tt.toString)
- tConstructors += tt -> c
- c
- }))
+ constructors.getOrElse(tt, {
+ val cs = List(Constructor[Expr, TypeTree](parts, tt, s => Tuple(s).setType(tt), tt.toString))
+ constructors += tt -> cs
+ cs
+ })
+
+ case mt @ MapType(from, to) =>
+ constructors.getOrElse(mt, {
+ val cs = for (size <- List(0, 1, 2, 5)) yield {
+ val subs = (1 to size).flatMap(i => List(from, to)).toList
+
+ Constructor[Expr, TypeTree](subs, mt, s => FiniteMap(s.grouped(2).map(t => (t(0), t(1))).toSeq).setType(mt), mt.toString+"@"+size)
+ }
+ constructors += mt -> cs
+ cs
+ })
+
+ case tp: TypeParameter =>
+ constructors.getOrElse(tp, {
+ val cs = for (i <- List(1, 2)) yield {
+ Constructor[Expr, TypeTree](List(), tp, s => GenericValue(tp, i), tp.id+"#"+i)
+ }
+ constructors += tp -> cs
+ cs
+ })
case act: AbstractClassType =>
- acConstructors.getOrElse(act, {
+ constructors.getOrElse(act, {
val cs = act.knownCCDescendents.map {
cct => getConstructorFor(cct, act)
}.toList
- acConstructors += act -> cs
+ constructors += act -> cs
cs
})
case cct: CaseClassType =>
- List(ccConstructors.getOrElse(cct, {
- val c = Constructor[Expr, TypeTree](cct.fieldsTypes, cct, s => CaseClass(cct, s), cct.id.name)
- ccConstructors += cct -> c
+ constructors.getOrElse(cct, {
+ val c = List(Constructor[Expr, TypeTree](cct.fieldsTypes, cct, s => CaseClass(cct, s), cct.id.name))
+ constructors += cct -> c
c
- }))
+ })
case _ =>
ctx.reporter.error("Unknown type to generate constructor for: "+t)
@@ -128,8 +162,10 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
(ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2))
- case _ =>
- sys.error("Unsupported value, can't paternify : "+v+" : "+expType)
+ case (gv: GenericValue, t: TypeParameter) =>
+ (cPattern(getConstructors(t)(gv.id-1), List()), true)
+ case (v, t) =>
+ sys.error("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t)
}
type InstrumentedResult = (EvaluationResults.Result, Option[vanuatoo.Pattern[Expr, TypeTree]])
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 748056d58..7432e33b3 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -299,7 +299,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evalu
case f @ FiniteSet(els) => FiniteSet(els.map(se(_)).distinct).setType(f.getType)
case i @ IntLiteral(_) => i
case b @ BooleanLiteral(_) => b
- case u @ UnitLiteral => u
+ case u @ UnitLiteral() => u
case f @ ArrayFill(length, default) => {
val rDefault = se(default)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 523a487f3..7dad7128b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -740,7 +740,7 @@ trait CodeExtraction extends ASTExtractors {
val nctx = dctx.withNewVar(vs -> (() => Variable(newID)))
extractTree(rst)(nctx)
}
- case None => UnitLiteral
+ case None => UnitLiteral()
}
rest = None
@@ -764,7 +764,7 @@ trait CodeExtraction extends ASTExtractors {
val restTree = rest match {
case Some(rst) => extractTree(rst)
- case None => UnitLiteral
+ case None => UnitLiteral()
}
rest = None
LetDef(funDefWithBody, restTree)
@@ -793,7 +793,7 @@ trait CodeExtraction extends ASTExtractors {
val nctx = dctx.withNewVar(nv).withNewMutableVar(nv)
extractTree(rst)(nctx)
}
- case None => UnitLiteral
+ case None => UnitLiteral()
}
rest = None
@@ -873,7 +873,7 @@ trait CodeExtraction extends ASTExtractors {
BooleanLiteral(v)
case ExUnitLiteral() =>
- UnitLiteral
+ UnitLiteral()
case ExLocally(body) =>
extractTree(body)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index d57b1c58a..9e07420a2 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -116,7 +116,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case IntLiteral(v) => sb.append(v)
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
- case UnitLiteral => sb.append("()")
+ case UnitLiteral() => sb.append("()")
case GenericValue(tp, id) =>
pp(tp, p)
sb.append("#"+id)
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index bbab14678..660c60c12 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -100,7 +100,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case IntLiteral(v) => sb.append(v)
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
- case UnitLiteral => sb.append("()")
+ case UnitLiteral() => sb.append("()")
/* These two aren't really supported in Scala, but we know how to encode them. */
case Implies(l,r) => pp(Or(Not(l), r), p)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 54a634bb1..86f33d7b2 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -628,7 +628,7 @@ object TreeOps {
(realCond, newRhs)
}
- val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)).setPos(m))((p1, ex) => {
+ val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").copiedFrom(m))((p1, ex) => {
if(p1._1 == BooleanLiteral(true)) {
p1._2
} else {
@@ -1153,6 +1153,8 @@ object TreeOps {
} else {
None
}
+ case ft : FunctionType => None // FIXME
+
case a : AbstractClassType => None
case c : CaseClassType =>
// This is really just one big assertion. We don't rewrite class defs.
@@ -1166,7 +1168,7 @@ object TreeOps {
} else {
None
}
- case Untyped | AnyType | BottomType | BooleanType | Int32Type | UnitType => None
+ case Untyped | AnyType | BottomType | BooleanType | Int32Type | UnitType | TypeParameter(_) => None
}
var idMap = Map[Identifier, Identifier]()
@@ -1200,7 +1202,7 @@ object TreeOps {
}
def pre(e : Expr) : Expr = e match {
- case Tuple(Seq()) => UnitLiteral
+ case Tuple(Seq()) => UnitLiteral()
case Variable(id) if idMap contains id => Variable(idMap(id))
case Tuple(Seq(s)) => pre(s)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 76f573553..6cdb61b81 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -416,7 +416,7 @@ object Trees {
}
case class StringLiteral(value: String) extends Literal[String]
- case object UnitLiteral extends Literal[Unit] with FixedType {
+ case class UnitLiteral() extends Literal[Unit] with FixedType {
val fixedType = UnitType
val value = ()
}
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 75d9e9d8f..cb0dd2044 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -23,13 +23,16 @@ object TypeTreeOps {
}
def bestRealType(t: TypeTree) : TypeTree = t match {
- case c: ClassType if c.classDef.isInstanceOf[CaseClassDef] => {
+ case c: CaseClassType =>
c.classDef.parent match {
- case None => CaseClassType(c.classDef.asInstanceOf[CaseClassDef], c.tps)
- case Some(p) => instantiateType(p, (c.classDef.tparams zip c.tps).toMap)
+ case None =>
+ c
+
+ case Some(p) =>
+ instantiateType(p, (c.classDef.tparams zip c.tps).toMap)
}
- }
- case other => other
+
+ case NAryType(tps, builder) => builder(tps.map(bestRealType))
}
def leastUpperBound(t1: TypeTree, t2: TypeTree): Option[TypeTree] = (t1,t2) match {
@@ -181,6 +184,9 @@ object TypeTreeOps {
val newOb = ob.map(id => freshId(id, expTpe))
(WildcardPattern(newOb), (ob zip newOb).toMap)
+
+ case _ =>
+ sys.error("woot!?")
}
MatchExpr(srec(e), cases.map(trCase)).copiedFrom(m)
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 58c90f882..fbf266b0c 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -65,6 +65,7 @@ object TypeTrees {
case Int32Type => InfiniteSize
case ListType(_) => InfiniteSize
case ArrayType(_) => InfiniteSize
+ case TypeParameter(_) => InfiniteSize
case TupleType(bases) => {
val baseSizes = bases.map(domainSize(_))
baseSizes.find(_ == InfiniteSize) match {
@@ -104,32 +105,10 @@ object TypeTrees {
case class TypeParameter(id: Identifier) extends TypeTree
- class TupleType private (val bases: Seq[TypeTree]) extends TypeTree {
+ case class TupleType(val bases: Seq[TypeTree]) extends TypeTree {
lazy val dimension: Int = bases.length
-
- override def equals(other: Any): Boolean = {
- other match {
- case (t: TupleType) => t.bases == bases
- case _ => false
- }
- }
-
- override def hashCode: Int = {
- bases.foldLeft(42)((acc, t) => acc + t.hashCode)
- }
-
- }
- object TupleType {
- def apply(bases: Seq[TypeTree]): TupleType = {
- new TupleType(bases.map(bestRealType(_)))
- }
- //TODO: figure out which of the two unapply is better
- //def unapply(t: TypeTree): Option[Seq[TypeTree]] = t match {
- // case (tt: TupleType) => Some(tt.bases)
- // case _ => None
- //}
- def unapply(tt: TupleType): Option[Seq[TypeTree]] = if(tt == null) None else Some(tt.bases)
}
+
object TupleOneType {
def unapply(tt : TupleType) : Option[TypeTree] = if(tt == null) None else {
if(tt.bases.size == 1) {
@@ -204,7 +183,6 @@ object TypeTrees {
case TupleType(ts) => Some((ts, TupleType(_)))
case ListType(t) => Some((Seq(t), ts => ListType(ts.head)))
case ArrayType(t) => Some((Seq(t), ts => ArrayType(ts.head)))
- case TupleType(ts) => Some((ts, TupleType(_)))
case SetType(t) => Some((Seq(t), ts => SetType(ts.head)))
case MultisetType(t) => Some((Seq(t), ts => MultisetType(ts.head)))
case MapType(from,to) => Some((Seq(from, to), t => MapType(t(0), t(1))))
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 4f5d71659..3730fb45a 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -19,13 +19,15 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
val maxTried = 10000;
- var datagen: DataGenerator = _
+ var datagen: Option[DataGenerator] = None
+
+ private var interrupted = false;
var freeVars = List[Identifier]()
var constraints = List[Expr]()
def assertCnstr(expression: Expr): Unit = {
- constraints ::= expression
+ constraints = constraints :+ expression
val newFreeVars = (variablesOf(expression) -- freeVars).toList
freeVars = freeVars ::: newFreeVars
@@ -34,25 +36,29 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
private var modelMap = Map[Identifier, Expr]()
def check: Option[Boolean] = {
- try {
- val muteContext = context.copy(reporter = new DefaultReporter(context.settings))
- datagen = new VanuatooDataGen(muteContext, program)
-
- modelMap = Map()
+ val res = try {
+ datagen = Some(new VanuatooDataGen(context, program))
+ if (interrupted) {
+ None
+ } else {
+ modelMap = Map()
- val it = datagen.generateFor(freeVars, And(constraints.reverse), 1, maxTried)
+ val it = datagen.get.generateFor(freeVars, And(constraints), 1, maxTried)
- if (it.hasNext) {
- val model = it.next
- modelMap = (freeVars zip model).toMap
- Some(true)
- } else {
- None
+ if (it.hasNext) {
+ val model = it.next
+ modelMap = (freeVars zip model).toMap
+ Some(true)
+ } else {
+ None
+ }
}
} catch {
case e: codegen.CompilationException =>
None
}
+ datagen = None
+ res
}
def getModel: Map[Identifier, Expr] = {
@@ -64,10 +70,14 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
}
def interrupt(): Unit = {
- Option(datagen).foreach(_.interrupt)
+ interrupted = true;
+
+ datagen.foreach{ s =>
+ s.interrupt
+ }
}
def recoverInterrupt(): Unit = {
- Option(datagen).foreach(_.recoverInterrupt)
+ datagen.foreach(_.recoverInterrupt)
}
}
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 1c75bf3b8..246ea430c 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -55,12 +55,16 @@ class PortfolioSolver(val context: LeonContext, solvers: Seq[SolverFactory[Solve
val res = Await.result(result, 10.days) match {
case Some((s, r, m)) =>
modelMap = m
+ context.reporter.debug("Solved with "+s.name)
solversInsts.foreach(_.interrupt)
r
case None =>
None
}
+ // Block until all solvers finished
+ Await.result(Future.fold(fs)(0){ (i, r) => i+1 }, 10.days);
+
solversInsts.foreach(_.free)
res
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 20d447ed5..d0b52e283 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -381,22 +381,26 @@ trait AbstractZ3Solver
reverseADTFieldSelectors = Map.empty
}
+ def normalizeType(t: TypeTree): TypeTree = {
+ bestRealType(t)
+ }
+
// assumes prepareSorts has been called....
- protected[leon] def typeToSort(tt: TypeTree): Z3Sort = tt match {
+ protected[leon] def typeToSort(oldtt: TypeTree): Z3Sort = normalizeType(oldtt) match {
case Int32Type | BooleanType | UnitType =>
- sorts.toZ3(tt)
+ sorts.toZ3(oldtt)
case act: AbstractClassType =>
- sorts.toZ3OrCompute(rootType(act)) {
- declareADTSort(rootType(act))
+ sorts.toZ3OrCompute(act) {
+ declareADTSort(act)
}
case cct: CaseClassType =>
- sorts.toZ3OrCompute(rootType(cct)) {
- declareADTSort(rootType(cct))
+ sorts.toZ3OrCompute(cct) {
+ declareADTSort(cct)
}
- case SetType(base) =>
+ case tt @ SetType(base) =>
sorts.toZ3OrCompute(tt) {
val newSetSort = z3.mkSetSort(typeToSort(base))
@@ -406,7 +410,7 @@ trait AbstractZ3Solver
newSetSort
}
- case MapType(fromType, toType) =>
+ case tt @ MapType(fromType, toType) =>
sorts.toZ3OrCompute(tt) {
val fromSort = typeToSort(fromType)
val toSort = mapRangeSort(toType)
@@ -414,7 +418,7 @@ trait AbstractZ3Solver
z3.mkArraySort(fromSort, toSort)
}
- case ArrayType(base) =>
+ case tt @ ArrayType(base) =>
sorts.toZ3OrCompute(tt) {
val intSort = typeToSort(Int32Type)
val toSort = typeToSort(base)
@@ -426,7 +430,7 @@ trait AbstractZ3Solver
ats
}
- case TupleType(tpes) =>
+ case tt @ TupleType(tpes) =>
sorts.toZ3OrCompute(tt) {
val tpesSorts = tpes.map(typeToSort)
val sortSymbol = z3.mkFreshStringSymbol("Tuple")
@@ -437,7 +441,7 @@ trait AbstractZ3Solver
tupleSort
}
- case TypeParameter(id) =>
+ case tt @ TypeParameter(id) =>
sorts.toZ3OrCompute(tt) {
val symbol = z3.mkFreshStringSymbol(id.name)
val newTPSort = z3.mkUninterpretedSort(symbol)
@@ -470,13 +474,13 @@ trait AbstractZ3Solver
def rec(ex: Expr): Z3AST = ex match {
case tu @ Tuple(args) =>
typeToSort(tu.getType) // Make sure we generate sort & meta info
- val meta = tupleMetaDecls(tu.getType)
+ val meta = tupleMetaDecls(normalizeType(tu.getType))
meta.cons(args.map(rec(_)): _*)
case ts @ TupleSelect(tu, i) =>
typeToSort(tu.getType) // Make sure we generate sort & meta info
- val meta = tupleMetaDecls(tu.getType)
+ val meta = tupleMetaDecls(normalizeType(tu.getType))
meta.selects(i-1)(rec(tu))
@@ -519,7 +523,7 @@ trait AbstractZ3Solver
case Not(e) => z3.mkNot(rec(e))
case IntLiteral(v) => z3.mkInt(v, typeToSort(Int32Type))
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
- case UnitLiteral => unitValue
+ case UnitLiteral() => unitValue
case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) )
case Plus(l, r) => z3.mkAdd(rec(l), rec(r))
case Minus(l, r) => z3.mkSub(rec(l), rec(r))
@@ -593,7 +597,7 @@ trait AbstractZ3Solver
case fill @ ArrayFill(length, default) =>
val at @ ArrayType(base) = fill.getType
typeToSort(at)
- val meta = arrayMetaDecls(at)
+ val meta = arrayMetaDecls(normalizeType(at))
val ar = z3.mkConstArray(typeToSort(base), rec(default))
val res = meta.cons(ar, rec(length))
@@ -602,14 +606,14 @@ trait AbstractZ3Solver
case ArraySelect(a, index) =>
typeToSort(a.getType)
val ar = rec(a)
- val getArray = arrayMetaDecls(a.getType).select
+ val getArray = arrayMetaDecls(normalizeType(a.getType)).select
val res = z3.mkSelect(getArray(ar), rec(index))
res
case ArrayUpdated(a, index, newVal) =>
typeToSort(a.getType)
val ar = rec(a)
- val meta = arrayMetaDecls(a.getType)
+ val meta = arrayMetaDecls(normalizeType(a.getType))
val store = z3.mkStore(meta.select(ar), rec(index), rec(newVal))
val res = meta.cons(store, meta.length(ar))
@@ -618,7 +622,7 @@ trait AbstractZ3Solver
case ArrayLength(a) =>
typeToSort(a.getType)
val ar = rec(a)
- val meta = arrayMetaDecls(a.getType)
+ val meta = arrayMetaDecls(normalizeType(a.getType))
val res = meta.length(ar)
res
@@ -685,7 +689,7 @@ trait AbstractZ3Solver
val rargs = args.map(rec)
Tuple(rargs)
- case LeonType(ArrayType(dt)) =>
+ case LeonType(at @ ArrayType(dt)) =>
assert(args.size == 2)
val IntLiteral(length) = rec(args(1))
model.getArrayValue(args(0)) match {
@@ -699,7 +703,7 @@ trait AbstractZ3Solver
FiniteArray(for (i <- 1 to length) yield {
valuesMap.getOrElse(i, elseValue)
- })
+ }).setType(at)
}
case LeonType(tpe @ MapType(kt, vt)) =>
@@ -723,7 +727,7 @@ trait AbstractZ3Solver
}
case LeonType(UnitType) =>
- UnitLiteral
+ UnitLiteral()
case _ =>
import Z3DeclKind._
diff --git a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
index 7b8ecc0b8..0aec55e20 100755
--- a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
+++ b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
@@ -167,7 +167,7 @@ class SynthesizerForRuleExamples(
info("####################################")
info("# precondition is: " + tfd.precondition.getOrElse(BooleanLiteral(true)))
info("# accumulatingCondition is: " + accumulatingCondition)
- info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral))
+ info("# accumulatingExpression(Unit) is: " + accumulatingExpression(UnitLiteral()))
info("####################################")
interactivePause
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
index 47223b5a9..7b92e5f7b 100644
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
@@ -250,7 +250,7 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
)
// case u @ UnitLiteral => u
list += makeLiteral(
- IE( "UnitLit", UnitLiteral ),
+ IE( "UnitLit", UnitLiteral() ),
UnitType
)
@@ -269,4 +269,4 @@ object PreLoader extends ( (Boolean) => List[Declaration] ) {
def makeNAE( name: String, fun: List[Expr]=>Expr ): NAE = NAE( name, fun )
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 25ec22efc..aa24c61b0 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -103,7 +103,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val s = solverFactory.getNewSolver
try {
- reporter.debug("Trying with solver: " + s.name)
+ reporter.debug("Solving with: " + s.name)
val t1 = System.nanoTime
s.assertCnstr(Not(vc))
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 397744e10..96b66dbe6 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -57,7 +57,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val newId = FreshIdentifier(id.name).copiedFrom(id)
val (rhsVal, rhsScope, rhsFun) = toFunction(e)
val scope = (body: Expr) => rhsScope(Let(newId, rhsVal, body).copiedFrom(expr))
- (UnitLiteral, scope, rhsFun + (id -> newId))
+ (UnitLiteral(), scope, rhsFun + (id -> newId))
}
case ite@IfExpr(cond, tExpr, eExpr) => {
@@ -150,7 +150,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val modifiedVars: Seq[Identifier] = condBodyFun.keys.toSet.intersect(varInScope).toSeq
if(modifiedVars.isEmpty)
- (UnitLiteral, (b: Expr) => b, Map())
+ (UnitLiteral(), (b: Expr) => b, Map())
else {
val whileFunVars = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
@@ -210,7 +210,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
b))))
})
- (UnitLiteral, finalScope, modifiedVars.zip(finalVars).toMap)
+ (UnitLiteral(), finalScope, modifiedVars.zip(finalVars).toMap)
}
}
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index 8da89fc6d..fef1d95e3 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -40,11 +40,11 @@ object TreeOps {
case Block(exprs, last) =>
val nexprs = (exprs :+ last).flatMap{
case Block(es2, el) => es2 :+ el
- case UnitLiteral => Seq()
+ case UnitLiteral() => Seq()
case e2 => Seq(e2)
}
Some(nexprs match {
- case Seq() => UnitLiteral
+ case Seq() => UnitLiteral()
case Seq(e) => e
case es => Block(es.init, es.last).setType(es.last.getType)
})
diff --git a/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
index befa9a141..2d721e38b 100644
--- a/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
@@ -30,7 +30,7 @@ object CommonDeclarations {
Int32Type
)
- val unit = UnitLiteral
+ val unit = UnitLiteral()
val unitDeclaration = makeDeclaration(
ImmediateExpression("unit", unit),
diff --git a/src/test/scala/leon/test/condabd/refinement/FilterTest.scala b/src/test/scala/leon/test/condabd/refinement/FilterTest.scala
index baf08e6c6..2c1467ec5 100644
--- a/src/test/scala/leon/test/condabd/refinement/FilterTest.scala
+++ b/src/test/scala/leon/test/condabd/refinement/FilterTest.scala
@@ -60,7 +60,7 @@ class FilterTest extends JUnitSuite {
tail =
loader.extractFields.find {
_.expression match {
- case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".tail")
+ case ure: UnaryReconstructionExpression => ure(UnitLiteral()).toString.contains(".tail")
case _ => false
}
} match {
@@ -71,7 +71,7 @@ class FilterTest extends JUnitSuite {
head =
loader.extractFields.find {
_.expression match {
- case ure: UnaryReconstructionExpression => ure(UnitLiteral).toString.contains(".head")
+ case ure: UnaryReconstructionExpression => ure(UnitLiteral()).toString.contains(".head")
case _ => false
}
} match {
@@ -82,7 +82,7 @@ class FilterTest extends JUnitSuite {
cons =
loader.extractCaseClasses.find {
_.expression match {
- case nre: NaryReconstructionExpression => nre(List(UnitLiteral, UnitLiteral)).toString.contains("Cons")
+ case nre: NaryReconstructionExpression => nre(List(UnitLiteral(), UnitLiteral())).toString.contains("Cons")
case _ => false
}
} match {
@@ -114,8 +114,8 @@ class FilterTest extends JUnitSuite {
val variable1 = tfunDef.params.head
val variable2 = tfunDef.params(1)
- assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable1.id))
- assertEquals(+1, isLess(cons(List(UnitLiteral, variable1.toVariable)), variable2.id))
+ assertEquals(+1, isLess(cons(List(UnitLiteral(), variable1.toVariable)), variable1.id))
+ assertEquals(+1, isLess(cons(List(UnitLiteral(), variable1.toVariable)), variable2.id))
assertEquals(-1, isLess(tail(variable1.toVariable), variable1.id))
assertEquals(+1, isLess(head(variable1.toVariable), variable1.id))
assertEquals(0, isLess(variable1.toVariable, variable1.id))
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index de6acd0f1..d65e875fb 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -61,6 +61,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
for(f <- fs) {
mkTest(f, List(LeonFlagOption("feelinglucky", true)), forError)(block)
mkTest(f, List(LeonFlagOption("codegen", true), LeonFlagOption("evalground", true), LeonFlagOption("feelinglucky", true)), forError)(block)
+ mkTest(f, List(LeonValueOption("solvers", "fairz3,enum"), LeonFlagOption("codegen", true), LeonFlagOption("evalground", true), LeonFlagOption("feelinglucky", true)), forError)(block)
}
}
--
GitLab