Commit 0fff4e58 authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

WIP

parent 08a13f9e
......@@ -32,7 +32,11 @@ lazy val commonSettings = Seq(
// "-Ywarn-unused",
"-feature",
"-language:higherKinds",
"-language:existentials"
"-language:existentials",
// experimental option to speed up the build
//"-Ycache-plugin-class-loader",
//"-Ycache-macro-class-loader"
),
addCompilerPlugin("org.spire-math" %% "kind-projector" % "0.9.6"),
//addCompilerPlugin("io.tryp" % "splain" % "0.2.10" cross CrossVersion.patch),
......@@ -116,7 +120,14 @@ lazy val planner = project
.in(file("dahu-planner"))
.dependsOn(anml, solvers, z3)
.settings(commonSettings ++ utestSettings: _*)
.settings(libraryDependencies += "com.github.scopt" %% "scopt" % "X.Y.Z")
.settings(
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"
))
resolvers += Resolver.sonatypeRepo("releases")
......
......@@ -138,7 +138,11 @@ case class ProblemContext(intTag: BoxedInt[Literal],
}
}
def xor(disjuncts: Tentative[Boolean]*): Tentative[Boolean] = {
Computation(bool.XOr, disjuncts.filter(_ != bool.False))
val noFalse = disjuncts.filter(_ != bool.False)
if(noFalse.isEmpty)
bool.False
else
Computation(bool.XOr, noFalse)
}
def implies(cond: Tentative[Boolean], effect: Tentative[Boolean]): Tentative[Boolean] = {
if(cond == bool.False)
......@@ -373,6 +377,7 @@ case class Chronicle(ctx: ProblemContext,
}
def toSatProblem(implicit cfg: Config) = {
var count = 0
val acts: Seq[Opt[Action[Tentative]]] = actions
val effs: Seq[Opt[EffectToken]] =
effects.map(Opt.present) ++
......@@ -386,6 +391,7 @@ case class Chronicle(ctx: ProblemContext,
val nonOverlappingEffectsConstraints =
for(e1 <- effs; e2 <- effs if e1 != e2) yield {
count += 1
(e1, e2) match {
case (Opt(EffectToken(start1, _, end1, fluent1, _), p1),
Opt(EffectToken(start2, _, end2, fluent2, _), p2)) =>
......@@ -405,13 +411,15 @@ case class Chronicle(ctx: ProblemContext,
ec <= persistenceEnd)
}
if(cfg.useXorForSupport)
implies(pc, Computation(bool.XOr, disjuncts))
implies(pc, xor(disjuncts: _*))
else
implies(pc, or(disjuncts: _*))
}
val allConstraints = consts ++ nonOverlappingEffectsConstraints ++ supportConstraints
val tmp = and(allConstraints: _*)
val view = acts.map {
case Opt(a, present) =>
Product(
......
......@@ -3,46 +3,124 @@ package dahu.planner
import copla.lang
import copla.lang.model.core.{ActionTemplate, Instance, Statement}
import dahu.utils.errors._
import java.io.File
import java.io.{File, FileWriter}
import copla.lang.model.core
import dahu.model.input.Tentative
import monix.eval.{MVar, Task}
import scala.concurrent.duration._
import monix.execution.Scheduler.Implicits.global
import scala.concurrent.{Await, Promise, TimeoutException}
import scala.util.{Failure, Success, Try}
import dahu.utils.debug._
case class Config(problemFile: File = null,
encoding: Encoding = Incremental(10),
minInstances: Int = 0,
maxInstances: Int = 500,
symBreak: Boolean = true,
useXorForSupport: Boolean = true)
sealed trait Encoding
case object Full extends Encoding
case class Incremental(maxSteps: Int) extends Encoding
useXorForSupport: Boolean = true,
numThreads: Int = 1,
maxRuntime: Int = 300,
warmupTimeSec: Int = 0
)
object Main extends App {
val parser = new scopt.OptionParser[Config]("dahu") {
head("dahu", "0.x")
opt[Int]("num-threads")
.action((n, c) => c.copy(numThreads = n))
opt[Int]("warmup")
.action((t, c) => c.copy(warmupTimeSec = t))
opt[Int]("max-depth")
.action((d, c) => c.copy(maxInstances = d))
opt[Int]("timeout")
.action((t, c) => c.copy(maxRuntime = t))
opt[Boolean]("use-xor")
.action((b, c) => c.copy(useXorForSupport = b))
opt[Boolean]("sym-break")
.action((b, c) => c.copy(symBreak = b))
arg[File]("XXXX.pb.anml").action((f, c) => c.copy(problemFile = f))
}
import dahu.utils.debug._
parser.parse(args, Config()) match {
case Some(cfg) =>
implicit val cfgImpl = cfg
solve(cfg.problemFile) match {
case Some(sol) =>
println("== Solution ==")
println(sol)
case None => unexpected
if(cfg.warmupTimeSec > 0) {
info("Warming up...")
dahu.utils.debug.LOG_LEVEL = 0
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))
dahu.utils.debug.LOG_LEVEL = 3
}
val startTime = System.currentTimeMillis()
def writeResult(solved: Boolean, time: Long): Unit = {
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()
}
val future =
solveTask(cfg.problemFile, System.currentTimeMillis() + cfg.maxRuntime * 1000)
.map(res => Success(res))
.timeoutTo(cfg.maxRuntime.seconds, Task(Failure(new TimeoutException())))
.runAsync
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(result.toString)
writeResult(solved = true, runtime)
case Success(None) =>
out("Max depth or time reached")
case Failure(_: TimeoutException) =>
out("Timeout")
writeResult(solved = false, System.currentTimeMillis() - startTime)
case Failure(exception) =>
out("Crash")
exception.printStackTrace()
}
sys.exit(0)
case None =>
}
def solve(problemFile: File)(implicit cfg: Config): Option[Any] = {
println("Parsing...")
def solveTask(problemFile: File, deadline: Long)(implicit cfg: Config): Task[Option[Any]] = {
Task {
info(problemFile.getName)
solve(problemFile, deadline)
}
}
def solve(problemFile: File, deadline: Long)(implicit cfg: Config): Option[String] = {
info("Parsing...")
lang.parse(problemFile) match {
case lang.Success(model) =>
cfg.encoding match {
case Full => sys.error("Unsupported option.")
case Incremental(maxSteps) => solveIncremental(model, maxSteps)
}
solveIncremental(model, cfg.maxInstances, deadline)
case lang.ParseError(fail) =>
println("Parsing failed:")
println(fail.format)
......@@ -52,22 +130,49 @@ object Main extends App {
err.foreach(_.printStackTrace())
sys.exit(1)
}
}
def solveIncremental(model: core.CoreModel, maxSteps: Int)(implicit cfg: Config): Option[Any] = {
for(i <- 0 to maxSteps) {
println(s"Step: $i")
solveIncrementalStep(model, i) match {
case Some(sol) => return Some(sol)
case None =>
}
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) {
val step: Integer = q.poll()
if (step == null)
return None
info(s"Depth: $step (worker: $workerID)")
solveIncrementalStep(model, step.toInt, deadline) match {
case Some(sol) =>
info(s" Solution found at depth $step (worker: $workerID)")
return Some(sol)
case None =>
info(s" No solution at depth $step (worker: $workerID)")
}
}
None
} : Task[Option[String]]
}
val future = Task.raceMany(workers).runAsync
Try {
Await.result(future, (deadline - System.currentTimeMillis()).millis)
} match {
case Success(solution) =>
solution
case Failure(to: TimeoutException) => None
case Failure(e) => throw e
}
None
}
def solveIncrementalStep(model: core.CoreModel, step: Int)(implicit cfg: Config): Option[Any] = {
println("Encoding...")
def solveIncrementalStep(model: core.CoreModel, step: Int, deadline: Long)(implicit cfg: Config): Option[String] = {
if(System.currentTimeMillis() >= deadline)
return None
info(" Processing ANML model...")
val ctx = ProblemContext.extract(model)
val result = model.foldLeft(Chronicle.empty(ctx)) {
case (chronicle, statement: Statement) => chronicle.extended(statement)(_ => unexpected)
......@@ -100,7 +205,7 @@ object Main extends App {
case (chronicle, _) => chronicle
}
// println(result)
val solution = Planner.solve(result)
val solution = Planner.solve(result, deadline)
// println(solution)
solution
}
......
......@@ -7,20 +7,23 @@ import dahu.model.types.Value
import dahu.solvers.MetaSolver
import dahu.z3.Z3PartialSolver
import dahu.utils.errors._
import dahu.utils.debug._
object Planner {
val backend = Z3PartialSolver.builder
def solve(chronicle: Chronicle)(implicit cfg: Config): Option[String] = {
def solve(chronicle: Chronicle, deadline: Long)(implicit cfg: Config): Option[String] = {
if(System.currentTimeMillis() > deadline)
return None
val sat = chronicle.toSatProblem
println("Building meta-solver...")
info(" Encoding...")
val solver = MetaSolver.of(Algebras.parse(sat), backend)
val evaluatedSolution: solver.ast.Assignment => Interpreter.Result[Value] =
(ass: solver.ast.Assignment) => {
Interpreter.evalWithFailureCause(solver.ast)(ass)
}
solver.nextSolution() match {
solver.nextSolution(deadline) match {
case Some(ass) =>
evaluatedSolution(ass) match {
case Res(operators) =>
......
......@@ -19,7 +19,7 @@ class MetaSolver[K <: SubInt](val ast: AST.Aux[_, K], val builder: PartialSolver
case _ => ???
}
def nextSolution(): Option[ast.Assignment] = solver.nextSatisfyingAssignment() match {
def nextSolution(deadline: Long = -1): Option[ast.Assignment] = solver.nextSatisfyingAssignment(deadline) match {
case Some(assignment) =>
val f: sat.PartialAssignment = assignment
val partial: ast.PartialAssignment = (k: ast.VID) => {
......
......@@ -8,7 +8,7 @@ abstract class PartialSolver[AST <: TotalSubAST[_]](final val ast: AST) {
type K <: ast.ID
def nextSatisfyingAssignment(): Option[ast.PartialAssignment]
def nextSatisfyingAssignment(deadlineMs: Long = -1): Option[ast.PartialAssignment]
}
object PartialSolver {
......
......@@ -15,7 +15,9 @@ class CSPPartialSolver[AST <: TotalSubAST[_]](_ast: AST) extends PartialSolver[A
private val intPB = IntCSP.intProblem(intBoolPb)
private val csp = intPB.getSolver
override def nextSatisfyingAssignment(): Option[ast.PartialAssignment] = {
override def nextSatisfyingAssignment(deadlineMs: Long = -1): Option[ast.PartialAssignment] = {
if(deadlineMs != -1)
dahu.utils.debug.warning("CSP Partial solver does not support deadlines yet.")
csp.nextSolution() match {
case Some(ass) =>
val partial: ast.PartialAssignment = (k: ast.VID) => {
......
......@@ -19,7 +19,7 @@ import scala.annotation.elidable._
object debug {
var DEBUG_LEVEL = 3
val LOG = 0
var LOG_LEVEL = 3
@elidable(ASSERTION)
@inline
......@@ -49,8 +49,29 @@ object debug {
throw new java.lang.AssertionError("assertion failed: " + message)
}
final def warning(msg: => String): Unit = if(LOG >= 1) println("warning: " + msg)
final def info(msg: => String): Unit = if(LOG >= 3) println("info: " + msg)
private var lastLog = System.currentTimeMillis()
private var prevNeedsTime = false
def out(msg: String, withDuration: Boolean = false): Unit = {
val time = System.currentTimeMillis()
if(prevNeedsTime)
println(s"\t[${time-lastLog}]")
if(withDuration) {
print(msg)
prevNeedsTime = true
lastLog = time
} else {
println(msg)
prevNeedsTime = false
}
}
@inline final def warning(msg: => String): Unit = if(LOG_LEVEL >= 1) println("warning: " + msg)
@inline final def info(msg: => String): Unit =
if(LOG_LEVEL >= 3) {
out("info: " + msg, withDuration = true)
}
/** Use to annotate blocks that should not be in hot paths, typically here to maintain genericity.
*
......
......@@ -67,9 +67,26 @@ class Z3PartialSolver[AST <: TotalSubAST[_]](_ast: AST) extends PartialSolver[AS
solver.add(satProblem)
var model: Model = null
override def nextSatisfyingAssignment(): Option[ast.PartialAssignment] = {
override def nextSatisfyingAssignment(deadline: Long = -1): Option[ast.PartialAssignment] = {
assert(model == null, "Z3 only support extraction of a single solution")
println("Check with Z3...")
val timeout =
if(deadline < 0)
None
else if(deadline >= System.currentTimeMillis())
Some((deadline - System.currentTimeMillis()).toInt)
else
Some(0)
timeout match {
case Some(0) => return None // deadline passed, to not attempt to solve
case Some(t) =>
val params = ctx.mkParams()
params.add("timeout", t)
solver.setParameters(params)
case None =>
}
dahu.utils.debug.info(" Solving with Z3...")
solver.check() match {
case Status.SATISFIABLE =>
model = solver.getModel
......
addSbtPlugin("com.dwijnand" % "sbt-dynver" % "2.1.0")
addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.14.6")
\ No newline at end of file
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