diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala index 3bd58a01d575928a5663ff5bf5446d9c161dce64..e5216e63a49c6ae3a9776f6d0458e94d7402e811 100644 --- a/src/main/scala/leon/datagen/VanuatooDataGen.scala +++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala @@ -33,12 +33,24 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { b -> Constructor[Expr, TypeTree](List(), BooleanType, s => BooleanLiteral(b), ""+b) }).toMap + val chars = (for (c <- Set('a', 'b', 'c', 'd')) yield { + c -> Constructor[Expr, TypeTree](List(), CharType, s => CharLiteral(c), ""+c) + }).toMap + + val rationals = (for (n <- Set(0, 1, 2, 3); d <- Set(1,2,3,4)) yield { + (n, d) -> Constructor[Expr, TypeTree](List(), RealType, s => FractionalLiteral(n, d), "" + n + "/" + d) + }).toMap + def intConstructor(i: Int) = ints(i) def bigIntConstructor(i: Int) = bigInts(i) def boolConstructor(b: Boolean) = booleans(b) + def charConstructor(c: Char) = chars(c) + + def rationalConstructor(n: Int, d: Int) = rationals(n -> d) + def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = { ConstructorPattern[Expr, TypeTree](c, args) } @@ -50,7 +62,6 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { getConstructors(t).head.copy(retType = act) } - private def getConstructors(t: TypeTree): List[Constructor[Expr, TypeTree]] = t match { case UnitType => constructors.getOrElse(t, { @@ -97,8 +108,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { 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 - + 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))).toMap, from, to), mt.asString(ctx)+"@"+size) } constructors += mt -> cs @@ -162,6 +172,9 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { case (b: java.lang.Boolean, BooleanType) => (cPattern(boolConstructor(b), List()), true) + case (c: java.lang.Character, CharType) => + (cPattern(charConstructor(c), List()), true) + case (cc: codegen.runtime.CaseClass, ct: ClassType) => val r = cc.__getRead() @@ -189,7 +202,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { (ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2)) case _ => - ctx.reporter.error("Could not retreive type for :"+cc.getClass.getName) + ctx.reporter.error("Could not retrieve type for :"+cc.getClass.getName) (AnyPattern[Expr, TypeTree](), false) } @@ -213,6 +226,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { case (gv: GenericValue, t: TypeParameter) => (cPattern(getConstructors(t)(gv.id-1), List()), true) + case (v, t) => ctx.reporter.debug("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t) (AnyPattern[Expr, TypeTree](), false) @@ -283,8 +297,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { None }) - - val gen = new StubGenerator[Expr, TypeTree]((ints.values ++ bigInts.values ++ booleans.values).toSeq, + val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values + val gen = new StubGenerator[Expr, TypeTree](stubValues.toSeq, Some(getConstructors _), treatEmptyStubsAsChildless = true) diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala index 40fd073574cc9cb4f58d97ef22ca3b70ad87ce69..f88db3500cbb9ff4a53260c0d7ce045115aa3bd3 100644 --- a/src/test/scala/leon/integration/solvers/SolversSuite.scala +++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala @@ -32,61 +32,73 @@ class SolversSuite extends LeonTestSuiteWithProgram { ) else Nil) } - // Check that we correctly extract several types from solver models - for ((sname, sf) <- getFactories) { - test(s"Model Extraction in $sname") { implicit fix => - val ctx = fix._1 - val pgm = fix._2 + val types = Seq( + BooleanType, + UnitType, + CharType, + RealType, + IntegerType, + Int32Type, + TypeParameter.fresh("T"), + SetType(IntegerType), + MapType(IntegerType, IntegerType), + FunctionType(Seq(IntegerType), IntegerType), + TupleType(Seq(IntegerType, BooleanType, Int32Type)) + ) - val solver = sf(ctx, pgm) + val vs = types.map(FreshIdentifier("v", _).toVariable) - val types = Seq( - BooleanType, - UnitType, - CharType, - IntegerType, - Int32Type, - TypeParameter.fresh("T"), - SetType(IntegerType), - MapType(IntegerType, IntegerType), - TupleType(Seq(IntegerType, BooleanType, Int32Type)) - ) + // We need to make sure models are not co-finite + val cnstrs = vs.map(v => v.getType match { + case UnitType => + Equals(v, simplestValue(v.getType)) + case SetType(base) => + Not(ElementOfSet(simplestValue(base), v)) + case MapType(from, to) => + Not(Equals(MapApply(v, simplestValue(from)), simplestValue(to))) + case FunctionType(froms, to) => + Not(Equals(Application(v, froms.map(simplestValue)), simplestValue(to))) + case _ => + not(Equals(v, simplestValue(v.getType))) + }) - val vs = types.map(FreshIdentifier("v", _).toVariable) + def checkSolver(solver: Solver, vs: Set[Variable], cnstr: Expr)(implicit fix: (LeonContext, Program)): Unit = { + try { + solver.assertCnstr(cnstr) - - // We need to make sure models are not co-finite - val cnstr = andJoin(vs.map(v => v.getType match { - case UnitType => - Equals(v, simplestValue(v.getType)) - case SetType(base) => - Not(ElementOfSet(simplestValue(base), v)) - case MapType(from, to) => - Not(Equals(MapApply(v, simplestValue(from)), simplestValue(to))) + solver.check match { + case Some(true) => + val model = solver.getModel + for (v <- vs) { + if (model.isDefinedAt(v.id)) { + assert(model(v.id).getType === v.getType, "Extracting value of type "+v.getType) + } else { + fail("Model does not contain "+v.id+" of type "+v.getType) + } + } case _ => - not(Equals(v, simplestValue(v.getType))) - })) + fail("Constraint "+cnstr.asString+" is unsat!?") + } + } finally { + solver.free + } + } - try { - solver.assertCnstr(cnstr) + // Check that we correctly extract several types from solver models + for ((sname, sf) <- getFactories) { + test(s"Model Extraction in $sname") { implicit fix => + val ctx = fix._1 + val pgm = fix._2 - solver.check match { - case Some(true) => - val model = solver.getModel - for (v <- vs) { - if (model.isDefinedAt(v.id)) { - assert(model(v.id).getType === v.getType, "Extracting value of type "+v.getType) - } else { - fail("Model does not contain "+v.id+" of type "+v.getType) - } - } - case _ => - fail("Constraint "+cnstr.asString+" is unsat!?") - } - } finally { - solver.free - } + val solver = sf(ctx, pgm) + checkSolver(solver, vs.toSet, andJoin(cnstrs)) + } + } + test(s"Data generation in enum solver") { implicit fix => + for ((v,cnstr) <- vs zip cnstrs) { + val solver = new EnumerationSolver(fix._1, fix._2) + checkSolver(solver, Set(v), cnstr) } } }