diff --git a/src/cp/ConstraintSolving.scala b/src/cp/ConstraintSolving.scala index 14adb2e049dbf9015a82b41b36db6289ca35592c..152e758135e5716cc23f954e217e19821909b6d5 100644 --- a/src/cp/ConstraintSolving.scala +++ b/src/cp/ConstraintSolving.scala @@ -21,7 +21,8 @@ object ConstraintSolving { s } - private val DEBUG = false + private val DEBUG = true + private def printDebug(msg: String): Unit = if (DEBUG) println(msg) object GlobalContext { private var solver: FairZ3Solver = null @@ -31,6 +32,7 @@ object ConstraintSolving { private var toAssertQueue: Seq[Expr] = Seq.empty def kill(id: Identifier): Unit = { + printDebug(" - Removing from live set: " + id) liveSet = liveSet - id } @@ -39,6 +41,7 @@ object ConstraintSolving { } def addLive(id: Identifier): Unit = { + printDebug(" - Adding to live set: " + id) liveSet = liveSet + id } @@ -49,21 +52,22 @@ object ConstraintSolving { def checkAssumptions(expr: Expr) : Boolean = checkAssumptions(expr, liveSet map (Variable(_))) private def checkAssumptions(expr: Expr, assumptions: Set[Expr]): Boolean = { - if (DEBUG) { - println(" - Checking assumptions: " + expr) - println(" - live set: " + liveSet) - if (! toAssertQueue.isEmpty) - println(" - Will also assert enqueued expressions: " + toAssertQueue) - } + printDebug(" - Checking assumptions: " + expr) + printDebug(" - live set: " + liveSet) + if (! toAssertQueue.isEmpty) + printDebug(" - Will also assert enqueued expressions: " + toAssertQueue) val toCheck = And(expr +: toAssertQueue) toAssertQueue = Seq.empty + printDebug(" - To check: " + toCheck) solver.decideWithModel(toCheck, false, assumptions = Some(assumptions)) match { case (Some(false), model) => + printDebug(" - SAT: " + model) lastModel = model true case _ => + printDebug(" - UNSAT") false } } @@ -78,11 +82,9 @@ object ConstraintSolving { // } def assertConstraint(expr: Expr): Boolean = { - if (DEBUG) { - println(" - Asserting constraint: " +expr) - if (! toAssertQueue.isEmpty) - println(" - Will also assert enqueued expressions: " + toAssertQueue) - } + printDebug(" - Asserting constraint: " +expr) + if (! toAssertQueue.isEmpty) + printDebug(" - Will also assert enqueued expressions: " + toAssertQueue) val toAssert = And(expr +: toAssertQueue) toAssertQueue = Seq.empty diff --git a/src/cp/LTrees.scala b/src/cp/LTrees.scala index b21e675a6d51980e1421a2ff117bb027ef780738..43c16faeb850b026332009d56a7cfb615e66ba10 100644 --- a/src/cp/LTrees.scala +++ b/src/cp/LTrees.scala @@ -199,7 +199,7 @@ object LTrees { enqueueAsForcedInStream(ids, values) } - private var underlying = underlyingStream() + private var underlying: Stream[L[T]] = null private def underlyingStream(): Stream[L[T]] = { @@ -230,11 +230,15 @@ object LTrees { } } - def hasNext: Boolean = !underlying.isEmpty + def hasNext: Boolean = { + if (underlying == null) + underlying = underlyingStream() + else + underlying = underlying.tail + !underlying.isEmpty + } def next: L[T] = { - val toRet = underlying.head - underlying = underlying.tail - toRet + underlying.head } def withFilter2(p: (L[T]) => Constraint[T]): LIterator[T] = {