Commit b66eda0b authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

Merge branch 'lazy-dag'

parents 6e6ccb78 0039266a
......@@ -29,7 +29,7 @@ object GraphColoring extends Family("graph-coloring") {
val B = color("B")
// val C = color("C")
val sat = A =!= B// && B =!= C// && C =!= A
val sat = A =!= B // && B =!= C// && C =!= A
Seq(
SatProblem.fromSat(sat, 6),
// SatProblem.fromSat(sat && A === Green, 2),
......
......@@ -33,7 +33,6 @@ lazy val commonSettings = Seq(
"-feature",
"-language:higherKinds",
"-language:existentials",
// experimental option to speed up the build
//"-Ycache-plugin-class-loader",
//"-Ycache-macro-class-loader"
......@@ -124,10 +123,11 @@ lazy val planner = project
mainClass in assembly := Some("dahu.planner.Main"),
assemblyJarName in assembly := "dahu-planner.jar"
)
.settings(libraryDependencies ++= Seq(
"com.github.scopt" %% "scopt" % "3.7.0",
"io.monix" %% "monix" % "3.0.0-RC1"
))
.settings(
libraryDependencies ++= Seq(
"com.github.scopt" %% "scopt" % "3.7.0",
"io.monix" %% "monix" % "3.0.0-RC1"
))
resolvers += Resolver.sonatypeRepo("releases")
......
package dahu.model.ir
import cats.Functor
import cats.kernel.Hash
import dahu.model.functions.Fun
import dahu.model.input.Ident
import dahu.model.types.{ProductTag, Tag, Type, Value}
import scala.collection.mutable.ArraySeq
import scala.language.implicitConversions
import scala.runtime.ScalaRunTime
sealed abstract class ExprF[F] {
sealed trait ExprF[@specialized(Int) F] {
def typ: Type
override final val hashCode: Int = ExprF.hash(this)
}
sealed trait TotalOrOptionalF[F] { self: ExprF[F] =>
sealed trait TotalOrOptionalF[@specialized(Int) F] { self: ExprF[F] =>
def typ: Type
}
sealed trait TotalOrPartialF[F] { self: ExprF[F] =>
sealed trait TotalOrPartialF[@specialized(Int) F] { self: ExprF[F] =>
def typ: Type
}
object TotalOrOptionalF {
......@@ -39,28 +44,44 @@ object ExprF {
case ValidF(v) => ValidF(f(v))
}
}
def hash[A](exprF: ExprF[A]): Int = exprF match {
case x: ComputationF[A] => ScalaRunTime._hashCode(x)
case x: InputF[A] => ScalaRunTime._hashCode(x)
case x: CstF[A] => ScalaRunTime._hashCode(x)
case x: Partial[A] => ScalaRunTime._hashCode(x)
case x: OptionalF[A] => ScalaRunTime._hashCode(x)
case x: PresentF[A] => ScalaRunTime._hashCode(x)
case x: ValidF[A] => ScalaRunTime._hashCode(x)
case x: ITEF[A] => ScalaRunTime._hashCode(x)
case x: ProductF[A] => ScalaRunTime._hashCode(x)
}
}
/** Pure expressions that always yield value if they are fed with pure expressions.
*
* A Fix[Pure] can always be evaluated to its value.
* */
sealed trait Total[F] extends ExprF[F] with TotalOrOptionalF[F] with TotalOrPartialF[F]
sealed trait Total[@specialized(Int) F]
extends ExprF[F]
with TotalOrOptionalF[F]
with TotalOrPartialF[F]
object Total {
implicit val functor: Functor[Total] = new Functor[Total] {
override def map[A, B](fa: Total[A])(f: A => B): Total[B] = fa match {
case x @ InputF(_, _) => x
case x @ CstF(_, _) => x
case ComputationF(fun, args, typ) => ComputationF(fun, args.map(f), typ)
case ProductF(members, typ) => ProductF(members.map(f), typ)
case ITEF(cond, onTrue, onFalse, typ) => ITEF(f(cond), f(onTrue), f(onFalse), typ)
}
override def map[@specialized(Int) A, @specialized(Int) B](fa: Total[A])(f: A => B): Total[B] =
fa match {
case x @ InputF(_, _) => x
case x @ CstF(_, _) => x
case ComputationF(fun, args, typ) => ComputationF(fun, args.map(f), typ)
case ProductF(members, typ) => ProductF(members.map(f), typ)
case ITEF(cond, onTrue, onFalse, typ) => ITEF(f(cond), f(onTrue), f(onFalse), typ)
}
}
}
/** An (unset) input to the problem.
* Essentially a decision variable in CSP jargon. */
case class InputF[F](id: Ident, typ: Type) extends Total[F] {
case class InputF[@specialized(Int) F](id: Ident, typ: Type) extends Total[F] {
override def toString: String = s"$id"
}
object InputF {
......@@ -70,7 +91,7 @@ object InputF {
implicit def typeParamConversion[F, G](fa: InputF[F]): InputF[G] = fa.asInstanceOf[InputF[G]]
}
case class CstF[F](value: Value, typ: Type) extends Total[F] {
case class CstF[@specialized(Int) F](value: Value, typ: Type) extends Total[F] {
override def toString: String = value.toString
}
object CstF {
......@@ -79,15 +100,26 @@ object CstF {
implicit def typeParamConversion[F, G](fa: CstF[F]): CstF[G] = fa.asInstanceOf[CstF[G]]
}
final case class ComputationF[F](fun: Fun[_], args: Seq[F], typ: Type) extends Total[F] {
final case class ComputationF[@specialized(Int) F](fun: Fun[_], args: ArraySeq[F], typ: Type)
extends Total[F] {
override def toString: String = s"$fun(${args.mkString(", ")})"
}
object ComputationF {
def apply[F](fun: Fun[_], args: Seq[F], tpe: Type): ComputationF[F] =
new ComputationF(fun, ArraySeq(args: _*), tpe)
}
final case class ProductF[F](members: Seq[F], typ: ProductTag[Any]) extends Total[F] {
final case class ProductF[@specialized(Int) F](members: ArraySeq[F], typ: ProductTag[Any])
extends Total[F] {
override def toString: String = members.mkString("(", ", ", ")")
}
object ProductF {
def apply[F](args: Seq[F], tpe: ProductTag[Any]): ProductF[F] =
new ProductF[F](ArraySeq(args: _*), tpe)
}
final case class ITEF[F](cond: F, onTrue: F, onFalse: F, typ: Type) extends Total[F] {
final case class ITEF[@specialized(Int) F](cond: F, onTrue: F, onFalse: F, typ: Type)
extends Total[F] {
override def toString: String = s"ite($cond, $onTrue, $onFalse)"
}
......
......@@ -49,42 +49,19 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
def unsupported[K](): CellOpt[K] = Unsupported.asInstanceOf[CellOpt[K]]
private val supportedFunctions = Set[Fun[_]](int.Add,
int.LEQ,
int.EQ,
int.Times,
int.Negate,
int.Min,
bool.And,
bool.Or,
bool.XOr,
bool.Not)
// implicit val dag: DAG[Total, ast.ID] = new DAG[Total, ast.ID] {
// override def algebra: ast.ID => Total[ast.ID] = ast.tree.asFunction
//
// override def children(graph: Total[ast.ID]): Set[ast.ID] = graph match {
// case ProductF(members, _) => members.toSet
// case ComputationF(_, args, _) => args.toSet
// case _ => Set()
// }
// }
// translate all nodes of the AST to cells.
// we need to take since we want to maintain the same IDs and a node typically refers to its subnodes.
// private val leavesToRoot = dag.topologicalOrder(ast.tree.domain.toScalaSet()).reverse
// private val originalCells = mutable.Map[ID, CellOpt]()
// for(i <- leavesToRoot) {
// originalCells += ((i, TRANS(ast.tree(i))))
// }
// AST:
// X => Total[AST.ID]
// AST.ID => Total[AST.ID]
// target:
// X => CellOpt
abstract class LazyTree[K, F[_] : TreeNode : Functor, G[_], Opt[_] : Functor](orig: ILazyTree[K, F, Opt])
extends ILazyTree[K, G, Opt] {
int.LEQ,
int.EQ,
int.Times,
int.Negate,
int.Min,
bool.And,
bool.Or,
bool.XOr,
bool.Not)
abstract class LazyTree[K, F[_]: TreeNode: Functor, G[_], Opt[_]: Functor](
orig: ILazyTree[K, F, Opt])
extends ILazyTree[K, G, Opt] {
def g(rec: G[ID] => ID)(prev: ID => G[ID])(node: F[ID]): G[ID]
......@@ -122,11 +99,11 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
}
}
push(origID)
while (queue.nonEmpty) {
while(queue.nonEmpty) {
val cur = queue.pop()
if(!processed(cur)) {
val fk = orig.getInt(cur)
if (treeNode.children(fk).forall(processed)) {
if(treeNode.children(fk).forall(processed)) {
val fg: F[ID] = functor.map(fk)(id => idsMap(id))
val g: G[ID] = g2(fg)
val id = rec(g)
......@@ -149,11 +126,11 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
private def sup[X](e: CellOpt[X]) = e match {
case Unsupported => false
case _ => true
case _ => true
}
private def TRANS[K](rec: CellOpt[K] => K)(prev: K => CellOpt[K])(
node: Total[K]): CellOpt[K] = {
node: Total[K]): CellOpt[K] = {
def and(conjuncts: CellOpt[K]*): CellOpt[K] = {
IntermediateExpression(
ComputationF(bool.And, conjuncts.toSeq.map(x => rec(x)), Tag.ofBoolean)
......@@ -169,19 +146,19 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
def cst(n: Int): CellOpt[K] = CompatibleConstant(CstF(Value(n), Tag.ofInt), Tag.ofInt)
node match {
case x@CstF(v, Tag.ofBoolean) => SupportedConstant(x)
case x@CstF(v, t: TagIsoInt[_]) =>
case x @ CstF(v, Tag.ofBoolean) => SupportedConstant(x)
case x @ CstF(v, t: TagIsoInt[_]) =>
CompatibleConstant(CstF(Value(t.toIntUnsafe(v)), Tag.ofInt), t)
case x@InputF(name, Tag.ofBoolean) => SupportedInput(x)
case x@InputF(name, t: TagIsoInt[_]) => CompatibleInput(InputF(name, Tag.ofInt), t)
case x@ComputationF(f, args, t: TagIsoInt[_])
if supportedFunctions.contains(f) && args.forall(x => sup(prev(x))) =>
case x @ InputF(name, Tag.ofBoolean) => SupportedInput(x)
case x @ InputF(name, t: TagIsoInt[_]) => CompatibleInput(InputF(name, Tag.ofInt), t)
case x @ ComputationF(f, args, t: TagIsoInt[_])
if supportedFunctions.contains(f) && args.forall(x => sup(prev(x))) =>
IntermediateExpression(ComputationF(f, args, t))
case x@ComputationF(wf: WrappedFunction, args, t: TagIsoInt[_])
if supportedFunctions.contains(wf.f) && args.forall(x => sup(prev(x))) =>
case x @ ComputationF(wf: WrappedFunction, args, t: TagIsoInt[_])
if supportedFunctions.contains(wf.f) && args.forall(x => sup(prev(x))) =>
TRANS(rec)(prev)(ComputationF(wf.f, args, t)) // unwrap and retry
case x@ComputationF(f: Unboxed[_], Seq(arg), t) =>
case x @ ComputationF(f: Unboxed[_], Seq(arg), t) =>
prev(arg) // unbox operation, use the previous cell
case x =>
......@@ -198,7 +175,7 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
val lt = new LazyTree[X, Total, CellOpt, cats.Id](ast.tree) {
override def g(rec: CellOpt[ID] => ID)(prev: ID => CellOpt[ID])(
node: Total[ID]): CellOpt[ID] =
node: Total[ID]): CellOpt[ID] =
TRANS(rec)(prev)(node)
}
......@@ -214,14 +191,14 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
val cs = mutable.HashSet[lt.ID]()
val visited = mutable.HashSet[lt.ID]()
val stack = mutable.Stack[lt.ID]()
def push(i: lt.ID) : Unit = { if(!visited.contains(i)) stack.push(i) }
def push(i: lt.ID): Unit = { if(!visited.contains(i)) stack.push(i) }
push(k)
while(stack.nonEmpty) {
val cur = stack.pop()
visited += cur
lt.getInt(cur) match {
case i@CompatibleInput(_, tpe) =>
case i @ CompatibleInput(_, tpe) =>
cs += lt.rec(leq(cst(tpe.min), i))
cs += lt.rec(leq(i, cst(tpe.max)))
case IntermediateExpression(e) =>
......@@ -237,8 +214,8 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
private val internalPrevRoot = lt.rec(lt.getFromOrigID(ast.root))
private val rootValue = IntermediateExpression(
ComputationF(bool.And,
(gatherConstraints(internalPrevRoot) + internalPrevRoot).toSeq,
bool.And.tpe))
(gatherConstraints(internalPrevRoot) + internalPrevRoot).toSeq,
bool.And.tpe))
val root: lt.ID = lt.rec(rootValue)
// val optTree: RootedLazyTree[X, CellOpt, cats.Id] = RootedLazyTree(root, lt)
......@@ -248,11 +225,11 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
val partialTree = new ILazyTree[X, Total, Option] {
val t = lt.map[OptTotal]({
case IntermediateExpression(e) => Some(e)
case CompatibleInput(v, _) => Some(v)
case SupportedInput(v) => Some(v)
case CompatibleConstant(v, _) => Some(v)
case SupportedConstant(v) => Some(v)
case x if x == Unsupported => None
case CompatibleInput(v, _) => Some(v)
case SupportedInput(v) => Some(v)
case CompatibleConstant(v, _) => Some(v)
case SupportedConstant(v) => Some(v)
case x if x == Unsupported => None
})
override def getExt(k: X): Option[Total[ID]] = t.getExt(k)
......@@ -260,11 +237,10 @@ class IntBoolSatisfactionProblem[X](val ast: RootedLazyTree[X, Total, cats.Id])
override def getInt(i: ID): Total[ID] = t.getInt(i) match {
case Some(e) => e
case None => unexpected
case None => unexpected
}
}
val tree = RootedLazyTree(root, partialTree)
}
......
......@@ -17,15 +17,13 @@ import scala.util.{Failure, Success, Try}
import dahu.utils.debug._
case class Config(problemFile: File = null,
minInstances: Int = 1,
maxInstances: Int = 6,
minInstances: Int = 0,
maxInstances: Int = 500,
symBreak: Boolean = true,
useXorForSupport: Boolean = true,
numThreads: Int = 1,
maxRuntime: Int = 300,
warmupTimeSec: Int = 0
)
maxRuntime: Int = 1800,
warmupTimeSec: Int = 0)
object Main extends App {
......@@ -33,7 +31,7 @@ object Main extends App {
head("dahu", "0.x")
opt[Int]("num-threads")
.action((n, c) => c.copy(numThreads = n))
.action((n, c) => c.copy(numThreads = n))
opt[Int]("warmup")
.action((t, c) => c.copy(warmupTimeSec = t))
......@@ -63,12 +61,13 @@ object Main extends App {
info("Warming up...")
dahu.utils.debug.LOG_LEVEL = 0
val warmUpTask = solveTask(cfg.problemFile, System.currentTimeMillis() + cfg.warmupTimeSec * 1000)
val warmUpTask =
solveTask(cfg.problemFile, System.currentTimeMillis() + cfg.warmupTimeSec * 1000)
.map(res => Success(res))
.timeoutTo(cfg.warmupTimeSec.seconds, Task(Failure(new TimeoutException())))
.runAsync
Try(Await.result(warmUpTask, (cfg.warmupTimeSec +10).seconds))
Try(Await.result(warmUpTask, (cfg.warmupTimeSec + 10).seconds))
dahu.utils.debug.LOG_LEVEL = 3
}
......@@ -79,20 +78,19 @@ object Main extends App {
val fw = new FileWriter("dahu-result.txt", true)
try {
fw.write(s"${cfg.problemFile.getName} ${if(solved) "SOLVED" else "FAIL"} $time\n")
}
finally fw.close()
} finally fw.close()
}
val future =
solveTask(cfg.problemFile, System.currentTimeMillis() + cfg.maxRuntime * 1000)
.map(res => Success(res))
.timeoutTo(cfg.maxRuntime.seconds, Task(Failure(new TimeoutException())))
.runAsync
.map(res => Success(res))
.timeoutTo(cfg.maxRuntime.seconds, Task(Failure(new TimeoutException())))
.runAsync
Await.result(future, (cfg.maxRuntime +10).seconds) match {
Await.result(future, (cfg.maxRuntime + 10).seconds) match {
case Success(Some(result)) =>
val runtime = System.currentTimeMillis() - startTime
out(s"== Solution (in ${runtime / 1000}.${(runtime %1000)/10}s) ==")
out(s"== Solution (in ${runtime / 1000}.${(runtime % 1000) / 10}s) ==")
out(result.toString)
writeResult(solved = true, runtime)
case Success(None) =>
......@@ -132,16 +130,17 @@ object Main extends App {
}
}
def solveIncremental(model: core.CoreModel, maxSteps: Int, deadline: Long)(implicit cfg: Config): Option[String] = {
def solveIncremental(model: core.CoreModel, maxSteps: Int, deadline: Long)(
implicit cfg: Config): Option[String] = {
val q = new java.util.concurrent.ConcurrentLinkedQueue[Integer]()
for(i <- cfg.minInstances to cfg.maxInstances)
q.add(i)
val workers = (0 until cfg.numThreads) map { workerID =>
Task {
while (System.currentTimeMillis() < deadline) {
while(System.currentTimeMillis() < deadline) {
val step: Integer = q.poll()
if (step == null)
if(step == null)
return None
info(s"Depth: $step (worker: $workerID)")
......@@ -154,7 +153,7 @@ object Main extends App {
}
}
None
} : Task[Option[String]]
}: Task[Option[String]]
}
val future = Task.raceMany(workers).runAsync
......@@ -164,11 +163,12 @@ object Main extends App {
case Success(solution) =>
solution
case Failure(to: TimeoutException) => None
case Failure(e) => throw e
case Failure(e) => throw e
}
}
def solveIncrementalStep(model: core.CoreModel, step: Int, deadline: Long)(implicit cfg: Config): Option[String] = {
def solveIncrementalStep(model: core.CoreModel, step: Int, deadline: Long)(
implicit cfg: Config): Option[String] = {
if(System.currentTimeMillis() >= deadline)
return None
......
......@@ -19,13 +19,13 @@ class MetaSolver[K <: SubInt](val ast: AST.Aux[_, K], val builder: PartialSolver
case _ => ???
}
def nextSolution(deadline: Long = -1): Option[ast.Assignment] = solver.nextSatisfyingAssignment(deadline) match {
case Some(assignment) =>
val total: ast.Assignment = (x: ast.VID) =>
assignment(x).getOrElse(defaultDomain(x).head) // TODO: use head option or fail early if an input has an empty domain
Some(total)
case None => None
}
def nextSolution(deadline: Long = -1): Option[ast.Assignment] =
solver.nextSatisfyingAssignment(deadline) match {
case Some(assignment) =>
val total: ast.Assignment = (x: ast.VID) => assignment(x).getOrElse(defaultDomain(x).head) // TODO: use head option or fail early if an input has an empty domain
Some(total)
case None => None
}
def enumerateSolutions(maxSolutions: Option[Int] = None,
onSolutionFound: ast.Assignment => Unit = _ => ()): Int = {
......
......@@ -55,7 +55,7 @@ object debug {
def out(msg: String, withDuration: Boolean = false): Unit = {
val time = System.currentTimeMillis()
if(prevNeedsTime)
println(s"\t[${time-lastLog}]")
println(s"\t[${time - lastLog}]")
if(withDuration) {
print(msg)
prevNeedsTime = true
......
......@@ -7,6 +7,20 @@ import scala.reflect.ClassTag
object structures {
object ArrayUtils {
def map[@specialized(Int) A, @specialized(Int) B](array: Array[A])(f: A => B)(
implicit ct: ClassTag[B]): Array[B] = {
val ret = Array.ofDim[B](array.length)
var i = 0
while(i < array.length) {
ret(i) = f(array(i))
i += 1
}
ret
}
}
/** todo: check if we need to specialized this, e.g. requiring `A <: Int` to avoid boxing. */
implicit final class BufferOps[A](val buff: debox.Buffer[A]) extends AnyVal {
......
......@@ -13,12 +13,13 @@ import scala.collection.mutable
import scala.util.{Failure, Success, Try}
import scala.util.control.NonFatal
class TreeBuilder[X, F[_], G, Opt[_]](t: ILazyTree[X, F, Opt], f: F[G] => G)(implicit F: Functor[F], T: TreeNode[F]) {
class TreeBuilder[X, F[_], G, Opt[_]](t: ILazyTree[X, F, Opt], f: F[G] => G)(implicit F: Functor[F],
T: TreeNode[F]) {
private val memo = mutable.HashMap[t.ID, G]()
def build(k: t.ID) : G = {
def build(k: t.ID): G = {
val stack = mutable.Stack[t.ID]()
def push(i: t.ID) : Unit = {
def push(i: t.ID): Unit = {
if(!memo.contains(i))
stack.push(i)
}
......@@ -61,14 +62,14 @@ class Z3PartialSolver[X](_ast: RootedLazyTree[X, Total, cats.Id]) extends Partia
case i: IntNum =>
ast.tree.getExt(id).typ match {
case t: TagIsoInt[_] => Some(t.toValue(i.getInt))
case _ => unexpected
case _ => unexpected
}
case b: BoolExpr =>
b.getBoolValue match {
case enumerations.Z3_lbool.Z3_L_FALSE => Some(Value(false))
case enumerations.Z3_lbool.Z3_L_TRUE => Some(Value(true))
case enumerations.Z3_lbool.Z3_L_TRUE => Some(Value(true))
case enumerations.Z3_lbool.Z3_L_UNDEF => None
case _ => unexpected
case _ => unexpected
}
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment