From fc86cbcefd40a4b3f0d9410871dfa92b8f0995b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com> Date: Tue, 5 Jul 2011 18:48:08 +0000 Subject: [PATCH] unfinished implementation moved to branch --- cp-demo/LazyVars.scala | 72 ++++++++++++++++++++---------------------- src/cp/LTrees.scala | 68 +++++++++++++++++++++++++++++---------- src/cp/Terms.scala | 12 ++++--- 3 files changed, 95 insertions(+), 57 deletions(-) diff --git a/cp-demo/LazyVars.scala b/cp-demo/LazyVars.scala index cc9714fa7..bca91fc74 100644 --- a/cp-demo/LazyVars.scala +++ b/cp-demo/LazyVars.scala @@ -3,49 +3,47 @@ import cp.Definitions._ import cp.LTrees._ object LazyVars { - def NonnegativeInt = ((x: Int) => x >= 0).lazyFindAll - def chooseInt(lower: Int, upper: Int) = ((x: Int) => x >= lower && x <= upper).lazyFindAll + // def NonnegativeInt = ((x: Int) => x >= 0).lazyFindAll + // def chooseInt(lower: Int, upper: Int) = ((x: Int) => x >= lower && x <= upper).lazyFindAll def main(args: Array[String]): Unit = { - f1() - f2() - f3() + f4() } - def f1() { - for { - x <- chooseInt(0, 5) - y <- chooseInt(1, 3) - if x > y - } { - val a: Int = x - val b: Int = y - println(a, b) - } - } + // def f1() { + // for { + // x <- chooseInt(0, 5) + // y <- chooseInt(1, 3) + // if x > y + // } { + // val a: Int = x + // val b: Int = y + // println(a, b) + // } + // } - def f2() { - // will loop forever if Scala Stream.from(0) is used instead. - for { - x <- NonnegativeInt - if x < 3 - y <- NonnegativeInt - if x > y - } { - val i: Int = x - val j: Int = y - println(i, j) - } - } + // def f2() { + // // will loop forever if Scala Stream.from(0) is used instead. + // for { + // x <- NonnegativeInt + // if x < 3 + // y <- NonnegativeInt + // if x > y + // } { + // val i: Int = x + // val j: Int = y + // println(i, j) + // } + // } - def f3() { - for { - i <- chooseInt(0, 3) - pair <- ((x: Int, y: Int) => x > 0 && y == 2 * x && x <= i).lazyFindAll - } { - println("i, (a, b):" + i.value + ", " + pair.value) - } - } + // def f3() { + // for { + // i <- chooseInt(0, 3) + // pair <- ((x: Int, y: Int) => x > 0 && y == 2 * x && x <= i).lazyFindAll + // } { + // println("i, (a, b):" + i.value + ", " + pair.value) + // } + // } def f4() { val (x, y) = ((x: Int, y: Int) => x > 0 && y == 2 * x && x <= 5).lazySolve diff --git a/src/cp/LTrees.scala b/src/cp/LTrees.scala index b21e675a6..b9d2991e8 100644 --- a/src/cp/LTrees.scala +++ b/src/cp/LTrees.scala @@ -16,7 +16,7 @@ object LTrees { /** Handler for converting values from Expr to Scala and reporting forced * values */ trait LHandler[T] { - def convert(s: Seq[Expr]): T + val converter: Converter def enqueueAsForced(ids: Seq[Identifier], values: Seq[Expr]): Unit } @@ -36,7 +36,7 @@ object LTrees { case Some(value) => value case None => val model = GlobalContext.findValues(ids) - val toRet = handler.convert(model) + val toRet = handler.converter.exprSeq2scala1[T](model) handler.enqueueAsForced(ids, model) cache = Some(toRet) toRet @@ -132,8 +132,40 @@ object LTrees { } /** END OF GENERATED CODE ***/ - /** A stream for symbolic variables */ - class LIterator[T](val constraint: (L[T]) => Constraint[T]) extends Iterator[L[T]] { + def dummyL[T]: L[T] = new L[T](null, Seq(FreshIdentifier("dummy", true).setType(BottomType))) + def dummyTuple1[T1]: Tuple1[L[T1]] = Tuple1(dummyL[T1]) + def dummyTuple2[T1,T2]: (L[T1],L[T2]) = (dummyL[T1],dummyL[T2]) + def dummyTuple3[T1,T2,T3]: (L[T1],L[T2],L[T3]) = (dummyL[T1],dummyL[T2],dummyL[T3]) + def dummyTuple4[T1,T2,T3,T4]: (L[T1],L[T2],L[T3],L[T4]) = (dummyL[T1],dummyL[T2],dummyL[T3],dummyL[T4]) + def dummyTuple5[T1,T2,T3,T4,T5]: (L[T1],L[T2],L[T3],L[T4],L[T5]) = (dummyL[T1],dummyL[T2],dummyL[T3],dummyL[T4],dummyL[T5]) + def dummyTuple6[T1,T2,T3,T4,T5,T6]: (L[T1],L[T2],L[T3],L[T4],L[T5],L[T6]) = (dummyL[T1],dummyL[T2],dummyL[T3],dummyL[T4],dummyL[T5],dummyL[T6]) + def dummyTuple7[T1,T2,T3,T4,T5,T6,T7]: (L[T1],L[T2],L[T3],L[T4],L[T5],L[T6],L[T7]) = (dummyL[T1],dummyL[T2],dummyL[T3],dummyL[T4],dummyL[T5],dummyL[T6],dummyL[T7]) + def dummyTuple8[T1,T2,T3,T4,T5,T6,T7,T8]: (L[T1],L[T2],L[T3],L[T4],L[T5],L[T6],L[T7],L[T8]) = (dummyL[T1],dummyL[T2],dummyL[T3],dummyL[T4],dummyL[T5],dummyL[T6],dummyL[T7],dummyL[T8]) + def dummyTuple9[T1,T2,T3,T4,T5,T6,T7,T8,T9]: (L[T1],L[T2],L[T3],L[T4],L[T5],L[T6],L[T7],L[T8],L[T9]) = (dummyL[T1],dummyL[T2],dummyL[T3],dummyL[T4],dummyL[T5],dummyL[T6],dummyL[T7],dummyL[T8],dummyL[T9]) + + class LIterator1[T1](val constraintGivenTuple: (L[T1]) => Constraint1[T1]) extends LIterator[T1,(L[T1])] { + val dummyTuple: Tuple1[L[T1]] = dummyTuple1[T1] + val constraint: Constraint[T1] = constraintGivenTuple(dummyTuple._1) + + def withFilter2(p: (L[T1]) => Constraint[T1]): LIterator1[T1] = { + new LIterator1[T1]((l: L[T1]) => this.constraintGivenTuple(l).asInstanceOf[Constraint1[T1]] && p(l).asInstanceOf[Constraint1[T1]]) + } + } + + class LIterator2[T1,T2](val constraintGivenTuple: ((L[T1], L[T2])) => Constraint2[T1,T2]) extends LIterator[(T1,T2),(L[T1],L[T2])] { + val dummyTuple: (L[T1],L[T2]) = dummyTuple2[T1,T2] + val constraint: Constraint[(T1,T2)] = constraintGivenTuple(dummyTuple) + + def withFilter2(p: ((L[T1],L[T2])) => Constraint[(T1,T2)]): LIterator2[T1,T2] = { + new LIterator2[T1,T2]((t: (L[T1],L[T2])) => this.constraintGivenTuple(t).asInstanceOf[Constraint2[T1,T2]] && p(t).asInstanceOf[Constraint2[T1,T2]]) + } + } + + /** A lazy iterator for symbolic variables. S denotes the Scala value type + * (which can be a tuple) and T denotes the corresponding L tuple type. */ + abstract class LIterator[S,T] extends Iterator[T] { + val dummyTuple: Product + val constraint: Constraint[S] import ConstraintSolving.GlobalContext private var guards: Map[Seq[Identifier],Identifier] = Map.empty @@ -142,7 +174,7 @@ object LTrees { private var forcedQueue: Seq[Seq[Identifier]] = Seq.empty // we don't have this until we first instantiate a constraint - private var convertingFunction: (Seq[Expr]) => T = null + // private var convertingFunction: (Seq[Expr]) => T = null def enqueueAsForcedInStream(ids: Seq[Identifier], values: Seq[Expr]): Unit = { // assert value @@ -194,7 +226,7 @@ object LTrees { } private def handler(): LHandler[T] = new LHandler[T] { - def convert(s: Seq[Expr]): T = convertingFunction(s) + val converter: Converter = constraint.converter def enqueueAsForced(ids: Seq[Identifier], values: Seq[Expr]): Unit = enqueueAsForcedInStream(ids, values) } @@ -206,15 +238,18 @@ object LTrees { // set of tricks to overcome circular dependency between creation of L's // and Constraints - val placeHolders = Seq(FreshIdentifier("placeholder", true).setType(BottomType)) - val candidateL = new L[T](handler(), placeHolders) - val instantiatedCnstr = constraint(candidateL) + val placeHolders: Seq[Identifier] = (for (l <- dummyTuple.productIterator) yield { + assert(l.isInstanceOf[L[_]]) + val castedL = l.asInstanceOf[L[_]] + assert(castedL.ids.size == 1) + castedL.ids.head + }).toSeq // now that we have a Constraint, we can perform some actions such as: - GlobalContext.initializeIfNeeded(instantiatedCnstr.program) - convertingFunction = instantiatedCnstr.convertingFunction + GlobalContext.initializeIfNeeded(constraint.program) + // convertingFunction = constraint.convertingFunction - val (newConsts, newExpr) = combineConstraint(instantiatedCnstr) + val (newConsts, newExpr) = combineConstraint(constraint) val typedPlaceHolders = newConsts map { case cst => FreshIdentifier("fresh", true).setType(cst.getType) } @@ -231,15 +266,16 @@ object LTrees { } def hasNext: Boolean = !underlying.isEmpty - def next: L[T] = { + def next: T = { val toRet = underlying.head underlying = underlying.tail - toRet + // toRet + throw new Exception() } - def withFilter2(p: (L[T]) => Constraint[T]): LIterator[T] = { + def withFilter2(p: (T) => Constraint[S]): LIterator[S,T] /*= { new LIterator[T]((l: L[T]) => this.constraint(l).asInstanceOf[Constraint1[T]] && p(l).asInstanceOf[Constraint1[T]]) - } + }*/ } } diff --git a/src/cp/Terms.scala b/src/cp/Terms.scala index 4c907dc41..f101f2b44 100644 --- a/src/cp/Terms.scala +++ b/src/cp/Terms.scala @@ -35,9 +35,9 @@ object Terms { findAllExprSeq(asConstraint(this)).map(convertingFunction(_)) } - def lazyFindAll(implicit asConstraint: (Term[T,R]) => Constraint[T]): LIterator[T] = { - new LIterator((l: L[T]) => asConstraint(this)) - } + // def lazyFindAll(implicit asConstraint: (Term[T,R]) => Constraint[T]): LIterator[T] = { + // new LIterator((l: L[T]) => asConstraint(this)) + // } } def removeGuard(g: Identifier): Unit = { @@ -48,7 +48,7 @@ object Terms { def createL[T](constraint: Constraint[_], constant: Identifier, guard: Identifier): L[T] = { val handler = new LHandler[T] { - def convert(s: Seq[Expr]): T = constraint.converter.exprSeq2scala1[T](s) + val converter: Converter = constraint.converter def enqueueAsForced(ids: Seq[Identifier], values: Seq[Expr]): Unit = { val haveValues = And((ids zip values) map { case (i, v) => Equals(Variable(i), v) @@ -185,6 +185,10 @@ object Terms { val (constants, guards) = constantsAndGuards(constraint) (createL[T1](constraint, constants(0), guards(0))) } + + def lazyFindAll(implicit asConstraint: (Term1[T1,R]) => Constraint1[T1]): LIterator1[T1] = { + new LIterator1((l: L[T1]) => asConstraint(this)) + } def compose0[A1](other : Term1[A1, T1]) : Term1[A1, R] = { val (newExpr, newTypes) = Terms.compose(other, this, 0, 1, 1) -- GitLab