Commit 667bbe5f authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

Use Deadline and FiniteDuration from the stdlib.

parent 958fce27
......@@ -150,6 +150,9 @@ lazy val planner = project
.in(file("planning/planner"))
.dependsOn(anmlParser, solvers, z3)
.settings(commonSettings ++ utestSettings: _*)
.settings(libraryDependencies ++= Seq(
"org.typelevel" %% "cats-effect" % "1.0.0-RC"
))
lazy val anmlPlanner = project
.in(file("planning/anml/planner"))
......@@ -162,7 +165,20 @@ lazy val anmlPlanner = project
.settings(
libraryDependencies ++= Seq(
"com.github.scopt" %% "scopt" % "3.7.0",
"io.monix" %% "monix" % "3.0.0-RC1"
"org.typelevel" %% "cats-effect" % "1.0.0-RC"
))
lazy val pddlPlanner = project
.in(file("planning/pddl/planner"))
.dependsOn(pddlParser, planner)
.settings(commonSettings ++ utestSettings: _*)
.settings(
mainClass in assembly := Some("dahu.planning.pddl.planner.Main"),
assemblyJarName in assembly := "dahu-pddl-planner.jar"
)
.settings(
libraryDependencies ++= Seq(
"com.github.scopt" %% "scopt" % "3.7.0"
))
resolvers += Resolver.sonatypeRepo("releases")
......
......@@ -6,15 +6,23 @@ import dahu.planning.model.full
import dahu.planning.model.full._
object AnmlPredef extends dahu.planning.model.common.Predef {
override val Time: IRealType = IntSubType(Id(RootScope, "time"), Integers)
override val Boolean: BooleanType = BooleanType(Id(RootScope, "boolean"))
val StartSym = "start"
val EndSym = "end"
val TrueSym = "true"
val FalseSym = "false"
val TimeSym = "time"
val BooleanSym = "boolean"
override val True: Instance = Instance(Id(RootScope, "true"), Boolean)
override val False: Instance = Instance(Id(RootScope, "false"), Boolean)
override val Time: IRealType = IntSubType(RootScope / TimeSym, Integers)
override val Start = LocalVar(Id(RootScope, "start"), Time)
override val End = LocalVar(Id(RootScope, "end"), Time)
override val Boolean: BooleanType = BooleanType(RootScope / BooleanSym)
override val True: Instance = Instance(RootScope / TrueSym, Boolean)
override val False: Instance = Instance(RootScope / FalseSym, Boolean)
override val Start = LocalVar(RootScope / StartSym, Time)
override val End = LocalVar(RootScope / EndSym, Time)
override def baseModel: full.Model =
(Model() ++ Seq(
......
......@@ -2,17 +2,10 @@ package dahu.planning.anml.planner
import java.io.File
import dahu.model.input.Tentative
import dahu.planning.anml.parser.{Config => _, _}
import dahu.planning.model.common.Predef
import dahu.planning.model.core
import dahu.planning.model.core.{ActionTemplate, Statement}
import dahu.utils.errors._
import cats.effect.IO
import dahu.utils.debug._
import monix.eval.Task
import monix.execution.Scheduler.Implicits.global
import dahu.planning.planner._
import dahu.planning.anml.parser.{Config => _, _}
import scala.concurrent.duration._
import scala.concurrent.{Await, TimeoutException}
......@@ -24,8 +17,8 @@ case class Config(problemFile: File = null,
symBreak: Boolean = true,
useXorForSupport: Boolean = true,
numThreads: Int = 1,
maxRuntime: Int = 1800,
warmupTimeSec: Int = 0)
maxRuntime: FiniteDuration = 1800.seconds,
warmupTimeSec: FiniteDuration = 0.seconds)
object Main extends App {
......@@ -36,7 +29,7 @@ object Main extends App {
// .action((n, c) => c.copy(numThreads = n))
opt[Int]("warmup")
.action((t, c) => c.copy(warmupTimeSec = t))
.action((t, c) => c.copy(warmupTimeSec = t.seconds))
opt[Int]("min-depth")
.action((d, c) => c.copy(minInstances = d))
......@@ -45,7 +38,7 @@ object Main extends App {
.action((d, c) => c.copy(maxInstances = d))
opt[Int]("timeout")
.action((t, c) => c.copy(maxRuntime = t))
.action((t, c) => c.copy(maxRuntime = t.seconds))
// opt[Boolean]("use-xor")
// .action((b, c) => c.copy(useXorForSupport = b))
......@@ -60,59 +53,49 @@ object Main extends App {
case Some(cfg) =>
implicit val cfgImpl = cfg
if(cfg.warmupTimeSec > 0) {
if(cfg.warmupTimeSec.toSeconds > 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))
solveTask(cfg.problemFile, Deadline.now + cfg.warmupTimeSec)
.map(res => Success(res))
.unsafeRunTimed(cfg.warmupTimeSec)
dahu.utils.debug.LOG_LEVEL = 3
}
val startTime = System.currentTimeMillis()
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)) =>
solveTask(cfg.problemFile, Deadline.now + cfg.maxRuntime)
.unsafeRunTimed(cfg.maxRuntime) match {
case Some(Some(result)) =>
val runtime = System.currentTimeMillis() - startTime
out(s"== Solution (in ${runtime / 1000}.${(runtime % 1000) / 10}s) ==")
out(result.toString)
case Success(None) =>
case None =>
out("Time out")
case Some(None) =>
out("Max depth or time reached")
case Failure(_: TimeoutException) =>
out("Timeout")
case Failure(exception) =>
out("Crash")
exception.printStackTrace()
}
sys.exit(0)
case None =>
}
def solveTask(problemFile: File, deadline: Long)(implicit cfg: Config): Task[Option[Any]] = {
Task {
def solveTask(problemFile: File, deadline: Deadline)(implicit cfg: Config): IO[Option[Any]] = {
IO {
info(problemFile.getName)
solve(problemFile, deadline)
}
}
def solve(problemFile: File, deadline: Long)(implicit cfg: Config): Option[String] = {
def solve(problemFile: File, deadline: Deadline)(implicit cfg: Config): Option[String] = {
implicit val plannerConf: PlannerConfig =
PlannerConfig(minInstances = cfg.minInstances, maxInstances = cfg.maxInstances)
info("Parsing...")
parse(problemFile) match {
case ParseSuccess(model) =>
solveIncremental(model, cfg.maxInstances, deadline)
Planner.solveIncremental(model, cfg.maxInstances, deadline)
case fail: ParseFailure =>
println("Parsing failed:")
println(fail.format)
......@@ -124,86 +107,4 @@ object Main extends App {
}
}
def solveIncremental(model: core.CoreModel, maxSteps: Int, deadline: Long)(
implicit cfg: Config,
predef: Predef): 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
}
}
def solveIncrementalStep(model: core.CoreModel, step: Int, deadline: Long)(
implicit cfg: Config,
predef: Predef): 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)
case (chronicle, action: ActionTemplate) =>
val actionInstances: Seq[Opt[Action[Tentative]]] =
if(cfg.symBreak) {
import dahu.model.input.dsl._
(0 until step).foldLeft(List[Opt[Action[Tentative]]]()) {
case (Nil, _) => // first action
Opt.optional(Action.instance(action, ctx)) :: Nil
case (last :: rest, _) =>
// not first, enforce that this action is only present if the last one is and that its start no earliest that the last one
val act = Opt.optional(Action.instance(action, ctx))
val presence = act.present implies last.present
val after = act.a.start >= last.a.start
val withSymBreak: Opt[Action[Tentative]] = act.copy(
a = act.a.copy(
chronicle = act.a.chronicle.copy(
constraints = presence :: after :: act.a.chronicle.constraints
)))
withSymBreak :: last :: rest
}
} else {
(0 until step).map { _ =>
Opt.optional(Action.instance(action, ctx))
}
}
chronicle.copy(actions = chronicle.actions ++ actionInstances)
case (chronicle, _) => chronicle
}
// println(result)
val solution = Planner.solve(result, deadline)
// println(solution)
solution
}
}
......@@ -145,6 +145,13 @@ package object common {
val Start: Var
val End: Var
val StartSym: String
val EndSym: String
val TrueSym: String
val FalseSym: String
val TimeSym: String
val BooleanSym: String
def baseModel: Model
}
......
......@@ -164,13 +164,13 @@ package object core {
lazy val start: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), predef.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, predef.StartSym), predef.Time)) => tp
}
.getOrElse(sys.error("No start timepoint in this action"))
lazy val end: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), predef.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, predef.EndSym), predef.Time)) => tp
}
.getOrElse(sys.error("No end timepoint in this action"))
}
......
......@@ -10,7 +10,7 @@ import scala.util.Try
class Parser(opt: Options) {
implicit private val predef: PddlPredef = PddlPredef(opt.discretization)
implicit val predef: PddlPredef = PddlPredef(opt.discretization)
def parseToFull(domain: File, problem: File): Try[Model] = Try {
val parser = new fr.uga.pddl4j.parser.Parser()
......
package dahu.planning.pddl.planner
import java.io.File
import dahu.planning.pddl.parser._
import dahu.planning.model.common.Predef
import dahu.planning.planner._
import scala.concurrent.duration._
import scala.concurrent.{Await, TimeoutException}
import scala.util.{Failure, Success, Try}
case class Config(problemFile: File = null,
domainFile: Option[File] = None,
minInstances: Int = 0,
maxInstances: Int = 500,
symBreak: Boolean = true,
useXorForSupport: Boolean = true,
numThreads: Int = 1,
maxRuntime: FiniteDuration = 1800.seconds,
warmupTimeSec: Int = 0,
discretization: Int = 1)
object Main extends App {
val optionsParser = new scopt.OptionParser[Config]("dahu") {
head("dahu", "0.x")
opt[Int]("min-depth")
.action((d, c) => c.copy(minInstances = d))
opt[Int]("max-depth")
.action((d, c) => c.copy(maxInstances = d))
opt[Int]("timeout")
.action((t, c) => c.copy(maxRuntime = t.seconds))
arg[Seq[File]]("[XXX.dom.pddl] XXXX.YY.pb.pddl").action {
case (Seq(pb), cfg) => cfg.copy(problemFile = pb)
case (Seq(dom, pb), cfg) => cfg.copy(domainFile = Some(dom), problemFile = pb)
}
}
optionsParser.parse(args, Config()) match {
case Some(cfg) =>
val pb = cfg.problemFile
val dom = cfg.domainFile match {
case Some(f) => f
case None =>
pb.getName.split('.') match {
case Array(d, _, "pb", "pddl") => new File(pb.getParent, s"$d.dom.pddl")
case _ =>
System.err.println(
"No domain file provided and problem file is not of the form XXXX.YY.pb.pddl")
sys.exit(1)
}
}
solve(dom, pb, cfg)
case None => sys.exit(1)
}
type Plan = String
def solve(domain: File, problem: File, config: Config): Option[Plan] = {
val pddlOptions = Options(discretization = config.discretization)
val parser = new Parser(pddlOptions)
implicit val plannerConfig: PlannerConfig =
PlannerConfig(config.minInstances, config.maxInstances)
implicit val predef: Predef = parser.predef
parser.parse(domain, problem) match {
case Success(model) =>
Planner.solveIncremental(model, config.maxInstances, Deadline.now + config.maxRuntime)
case Failure(err) =>
err.printStackTrace()
sys.exit(1)
}
None
}
}
package dahu.planning.planner
import cats.effect.IO
import cats.implicits._
import dahu.model.compiler.Algebras
import dahu.model.input.Tentative
import dahu.model.interpreter.Interpreter
import dahu.model.interpreter.Interpreter.Res
import dahu.model.types.Value
import dahu.planning.model.common.Predef
import dahu.planning.model.core
import dahu.planning.model.core.{ActionTemplate, Statement}
import dahu.solvers.MetaSolver
import dahu.utils.debug._
import dahu.utils.errors._
import dahu.z3.Z3PartialSolver
import scala.concurrent.duration._
case class PlannerConfig(minInstances: Int, maxInstances: Int, symBreak: Boolean = true)
object Planner {
val backend = Z3PartialSolver.builder
def solve(chronicle: Chronicle, deadline: Long): Option[String] = {
if(System.currentTimeMillis() > deadline)
def solveIncremental(model: core.CoreModel, maxSteps: Int, deadline: Deadline)(
implicit cfg: PlannerConfig,
predef: Predef): Option[String] = {
val q = new java.util.concurrent.ConcurrentLinkedQueue[Integer]()
for(i <- cfg.minInstances to cfg.maxInstances)
q.add(i)
val task: IO[Option[String]] = IO {
while(deadline.hasTimeLeft) {
val step: Integer = q.poll()
if(step == null)
return None
info(s"Depth: $step")
solveIncrementalStep(model, step.toInt, deadline) match {
case Some(sol) =>
info(s" Solution found at depth $step")
return Some(sol)
case None =>
info(s" No solution at depth $step")
}
}
None
}
task.unsafeRunTimed(deadline.timeLeft).flatten
// Try {
// Await.result(future, (deadline - System.currentTimeMillis()).millis)
// } match {
// case Success(solution) =>
// solution
// case Failure(to: TimeoutException) => None
// case Failure(e) => throw e
// }
}
def solveIncrementalStep(model: core.CoreModel, step: Int, deadline: Deadline)(
implicit cfg: PlannerConfig,
predef: Predef): Option[String] = {
if(deadline.isOverdue())
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)
case (chronicle, action: ActionTemplate) =>
val actionInstances: Seq[Opt[Action[Tentative]]] =
if(cfg.symBreak) {
import dahu.model.input.dsl._
(0 until step).foldLeft(List[Opt[Action[Tentative]]]()) {
case (Nil, _) => // first action
Opt.optional(Action.instance(action, ctx)) :: Nil
case (last :: rest, _) =>
// not first, enforce that this action is only present if the last one is and that its start no earliest that the last one
val act = Opt.optional(Action.instance(action, ctx))
val presence = act.present implies last.present
val after = act.a.start >= last.a.start
val withSymBreak: Opt[Action[Tentative]] = act.copy(
a = act.a.copy(
chronicle = act.a.chronicle.copy(
constraints = presence :: after :: act.a.chronicle.constraints
)))
withSymBreak :: last :: rest
}
} else {
(0 until step).map { _ =>
Opt.optional(Action.instance(action, ctx))
}
}
chronicle.copy(actions = chronicle.actions ++ actionInstances)
case (chronicle, _) => chronicle
}
// println(result)
val solution = Planner.solve(result, deadline)
// println(solution)
solution
}
def solve(chronicle: Chronicle, deadline: Deadline): Option[String] = {
if(deadline.isOverdue)
return None
val sat = chronicle.toSatProblem
info(" Encoding...")
......@@ -24,7 +114,7 @@ object Planner {
(ass: solver.ast.Assignment) => {
Interpreter.evalWithFailureCause(solver.ast)(ass)
}
solver.nextSolution(deadline) match {
solver.nextSolution(Some(deadline)) match {
case Some(ass) =>
evaluatedSolution(ass) match {
case Res(operators) =>
......
......@@ -6,6 +6,8 @@ import dahu.model.problem.SatisfactionProblem
import dahu.model.types.{TagIsoInt, Value}
import dahu.solvers.constraints.CSPPartialSolver
import scala.concurrent.duration.{Deadline, FiniteDuration}
class MetaSolver[K <: SubInt](val ast: AST.Aux[_, K], val builder: PartialSolver.Builder) {
val sat = SatisfactionProblem.satisfactionSubAST(ast)
val solver = builder(sat)
......@@ -19,7 +21,7 @@ class MetaSolver[K <: SubInt](val ast: AST.Aux[_, K], val builder: PartialSolver
case _ => ???
}
def nextSolution(deadline: Long = -1): Option[ast.Assignment] =
def nextSolution(deadline: Option[Deadline] = None): 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
......
......@@ -6,11 +6,13 @@ import dahu.model.problem.SatisfactionProblem.RootedLazyTree
import dahu.model.types.Value
import dahu.solvers.problem.IntCSP
import scala.concurrent.duration.Deadline
abstract class PartialSolver[X](final val ast: RootedLazyTree[X, Total, cats.Id]) {
type K <: X
def nextSatisfyingAssignment(deadlineMs: Long = -1): Option[X => Option[Value]]
def nextSatisfyingAssignment(deadlineMs: Option[Deadline]): Option[X => Option[Value]]
}
object PartialSolver {
......
......@@ -9,6 +9,8 @@ import dahu.solvers.PartialSolver
import dahu.solvers.problem.IntCSP
import dahu.utils.errors._
import scala.concurrent.duration.Deadline
class CSPPartialSolver[X](_ast: RootedLazyTree[X, Total, cats.Id]) extends PartialSolver[X](_ast) {
val intBoolPb = new IntBoolSatisfactionProblem[X](ast)
......@@ -16,7 +18,8 @@ class CSPPartialSolver[X](_ast: RootedLazyTree[X, Total, cats.Id]) extends Parti
private val intPB = ??? //IntCSP.intProblem(intBoolPb)
private val csp = ??? // intPB.getSolver
override def nextSatisfyingAssignment(deadlineMs: Long = -1): Option[X => Option[Value]] = {
override def nextSatisfyingAssignment(
deadlineMs: Option[Deadline]): Option[X => Option[Value]] = {
???
// if(deadlineMs != -1)
// dahu.utils.debug.warning("CSP Partial solver does not support deadlines yet.")
......
......@@ -10,6 +10,7 @@ import dahu.utils.SFunctor
import dahu.utils.errors._
import scala.collection.mutable
import scala.concurrent.duration.Deadline
import scala.reflect.ClassTag
import scala.util.{Failure, Success, Try}
import scala.util.control.NonFatal
......@@ -98,21 +99,14 @@ class Z3PartialSolver[X](_ast: RootedLazyTree[X, Total, cats.Id]) extends Partia
solver.add(satProblem)
var model: Model = null
override def nextSatisfyingAssignment(deadline: Long = -1): Option[X => Option[Value]] = {
override def nextSatisfyingAssignment(deadline: Option[Deadline]): Option[X => Option[Value]] = {
assert(model == null, "Z3 only support extraction of a single solution")
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
deadline match {
case Some(dl) if dl.isOverdue => return None // deadline passed, to not attempt to solve
case Some(t) =>
val params = ctx.mkParams()
params.add("timeout", t)
params.add("timeout", t.timeLeft.toMillis.toInt)
solver.setParameters(params)
case None =>
}
......
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