Skip to content
Snippets Groups Projects
Commit 2191f9e3 authored by Ali Sinan Köksal's avatar Ali Sinan Köksal
Browse files

fix to lazy enumeration

parent e75243d6
No related branches found
No related tags found
No related merge requests found
...@@ -21,7 +21,8 @@ object ConstraintSolving { ...@@ -21,7 +21,8 @@ object ConstraintSolving {
s s
} }
private val DEBUG = false private val DEBUG = true
private def printDebug(msg: String): Unit = if (DEBUG) println(msg)
object GlobalContext { object GlobalContext {
private var solver: FairZ3Solver = null private var solver: FairZ3Solver = null
...@@ -31,6 +32,7 @@ object ConstraintSolving { ...@@ -31,6 +32,7 @@ object ConstraintSolving {
private var toAssertQueue: Seq[Expr] = Seq.empty private var toAssertQueue: Seq[Expr] = Seq.empty
def kill(id: Identifier): Unit = { def kill(id: Identifier): Unit = {
printDebug(" - Removing from live set: " + id)
liveSet = liveSet - id liveSet = liveSet - id
} }
...@@ -39,6 +41,7 @@ object ConstraintSolving { ...@@ -39,6 +41,7 @@ object ConstraintSolving {
} }
def addLive(id: Identifier): Unit = { def addLive(id: Identifier): Unit = {
printDebug(" - Adding to live set: " + id)
liveSet = liveSet + id liveSet = liveSet + id
} }
...@@ -49,21 +52,22 @@ object ConstraintSolving { ...@@ -49,21 +52,22 @@ object ConstraintSolving {
def checkAssumptions(expr: Expr) : Boolean = checkAssumptions(expr, liveSet map (Variable(_))) def checkAssumptions(expr: Expr) : Boolean = checkAssumptions(expr, liveSet map (Variable(_)))
private def checkAssumptions(expr: Expr, assumptions: Set[Expr]): Boolean = { private def checkAssumptions(expr: Expr, assumptions: Set[Expr]): Boolean = {
if (DEBUG) { printDebug(" - Checking assumptions: " + expr)
println(" - Checking assumptions: " + expr) printDebug(" - live set: " + liveSet)
println(" - live set: " + liveSet) if (! toAssertQueue.isEmpty)
if (! toAssertQueue.isEmpty) printDebug(" - Will also assert enqueued expressions: " + toAssertQueue)
println(" - Will also assert enqueued expressions: " + toAssertQueue)
}
val toCheck = And(expr +: toAssertQueue) val toCheck = And(expr +: toAssertQueue)
toAssertQueue = Seq.empty toAssertQueue = Seq.empty
printDebug(" - To check: " + toCheck)
solver.decideWithModel(toCheck, false, assumptions = Some(assumptions)) match { solver.decideWithModel(toCheck, false, assumptions = Some(assumptions)) match {
case (Some(false), model) => case (Some(false), model) =>
printDebug(" - SAT: " + model)
lastModel = model lastModel = model
true true
case _ => case _ =>
printDebug(" - UNSAT")
false false
} }
} }
...@@ -78,11 +82,9 @@ object ConstraintSolving { ...@@ -78,11 +82,9 @@ object ConstraintSolving {
// } // }
def assertConstraint(expr: Expr): Boolean = { def assertConstraint(expr: Expr): Boolean = {
if (DEBUG) { printDebug(" - Asserting constraint: " +expr)
println(" - Asserting constraint: " +expr) if (! toAssertQueue.isEmpty)
if (! toAssertQueue.isEmpty) printDebug(" - Will also assert enqueued expressions: " + toAssertQueue)
println(" - Will also assert enqueued expressions: " + toAssertQueue)
}
val toAssert = And(expr +: toAssertQueue) val toAssert = And(expr +: toAssertQueue)
toAssertQueue = Seq.empty toAssertQueue = Seq.empty
......
...@@ -199,7 +199,7 @@ object LTrees { ...@@ -199,7 +199,7 @@ object LTrees {
enqueueAsForcedInStream(ids, values) enqueueAsForcedInStream(ids, values)
} }
private var underlying = underlyingStream() private var underlying: Stream[L[T]] = null
private def underlyingStream(): Stream[L[T]] = { private def underlyingStream(): Stream[L[T]] = {
...@@ -230,11 +230,15 @@ object LTrees { ...@@ -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] = { def next: L[T] = {
val toRet = underlying.head underlying.head
underlying = underlying.tail
toRet
} }
def withFilter2(p: (L[T]) => Constraint[T]): LIterator[T] = { def withFilter2(p: (L[T]) => Constraint[T]): LIterator[T] = {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment