diff --git a/cp-demo/LazyVars.scala b/cp-demo/LazyVars.scala
index bca91fc7494ae3787b7246ffba58f6e538a902c1..cc9714fa7412dadfac46b0052214828a07652dbf 100644
--- a/cp-demo/LazyVars.scala
+++ b/cp-demo/LazyVars.scala
@@ -3,47 +3,49 @@ 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 = {
- f4()
+ f1()
+ f2()
+ f3()
}
- // 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 b9d2991e895b0f53d81a6b2005fbc2b0b8243fd0..b21e675a6d51980e1421a2ff117bb027ef780738 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] {
- val converter: Converter
+ def convert(s: Seq[Expr]): T
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.converter.exprSeq2scala1[T](model)
+ val toRet = handler.convert(model)
handler.enqueueAsForced(ids, model)
cache = Some(toRet)
toRet
@@ -132,40 +132,8 @@ object LTrees {
}
/** END OF GENERATED CODE ***/
- 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]
+ /** A stream for symbolic variables */
+ class LIterator[T](val constraint: (L[T]) => Constraint[T]) extends Iterator[L[T]] {
import ConstraintSolving.GlobalContext
private var guards: Map[Seq[Identifier],Identifier] = Map.empty
@@ -174,7 +142,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
@@ -226,7 +194,7 @@ object LTrees {
}
private def handler(): LHandler[T] = new LHandler[T] {
- val converter: Converter = constraint.converter
+ def convert(s: Seq[Expr]): T = convertingFunction(s)
def enqueueAsForced(ids: Seq[Identifier], values: Seq[Expr]): Unit =
enqueueAsForcedInStream(ids, values)
}
@@ -238,18 +206,15 @@ object LTrees {
// set of tricks to overcome circular dependency between creation of L's
// and Constraints
- 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
+ val placeHolders = Seq(FreshIdentifier("placeholder", true).setType(BottomType))
+ val candidateL = new L[T](handler(), placeHolders)
+ val instantiatedCnstr = constraint(candidateL)
// now that we have a Constraint, we can perform some actions such as:
- GlobalContext.initializeIfNeeded(constraint.program)
- // convertingFunction = constraint.convertingFunction
+ GlobalContext.initializeIfNeeded(instantiatedCnstr.program)
+ convertingFunction = instantiatedCnstr.convertingFunction
- val (newConsts, newExpr) = combineConstraint(constraint)
+ val (newConsts, newExpr) = combineConstraint(instantiatedCnstr)
val typedPlaceHolders = newConsts map {
case cst => FreshIdentifier("fresh", true).setType(cst.getType)
}
@@ -266,16 +231,15 @@ object LTrees {
}
def hasNext: Boolean = !underlying.isEmpty
- def next: T = {
+ def next: L[T] = {
val toRet = underlying.head
underlying = underlying.tail
- // toRet
- throw new Exception()
+ toRet
}
- def withFilter2(p: (T) => Constraint[S]): LIterator[S,T] /*= {
+ def withFilter2(p: (L[T]) => Constraint[T]): LIterator[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 f101f2b44fc82efe37c95753bbf75bd0b0a5065d..4c907dc417fccdfd9765cb1c54de439d3d6c9c54 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] {
- val converter: Converter = constraint.converter
+ def convert(s: Seq[Expr]): T = constraint.converter.exprSeq2scala1[T](s)
def enqueueAsForced(ids: Seq[Identifier], values: Seq[Expr]): Unit = {
val haveValues = And((ids zip values) map {
case (i, v) => Equals(Variable(i), v)
@@ -185,10 +185,6 @@ 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)