Commit 3cfe38eb authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

[planner] Split general planner and its use for anml.

parent 72413d87
......@@ -147,12 +147,17 @@ lazy val benchmarks = project
.settings(commonSettings ++ utestSettings: _*)
lazy val planner = project
.in(file("planner"))
.in(file("planning/planner"))
.dependsOn(anmlParser, solvers, z3)
.settings(commonSettings ++ utestSettings: _*)
lazy val anmlPlanner = project
.in(file("planning/anml/planner"))
.dependsOn(anmlParser, planner)
.settings(commonSettings ++ utestSettings: _*)
.settings(
mainClass in assembly := Some("dahu.planner.Main"),
assemblyJarName in assembly := "dahu-planner.jar"
mainClass in assembly := Some("dahu.planning.anml.planner.Main"),
assemblyJarName in assembly := "dahu-anml-planner.jar"
)
.settings(
libraryDependencies ++= Seq(
......
package dahu.planner
package dahu.planning.anml.planner
import dahu.planning.model.core.{ActionTemplate, Statement}
import dahu.utils.errors._
import java.io.{File, FileWriter}
import dahu.planning.anml.parser._
import java.io.File
import dahu.planning.model.core
import dahu.model.input.Tentative
import dahu.planning.anml.parser._
import dahu.planning.model.common.Predef
import monix.eval.{MVar, Task}
import scala.concurrent.duration._
import dahu.planning.model.core
import dahu.planning.model.core.{ActionTemplate, Statement}
import dahu.utils.errors._
import monix.eval.Task
import monix.execution.Scheduler.Implicits.global
import scala.concurrent.{Await, Promise, TimeoutException}
import dahu.planning.planner._
import scala.concurrent.duration._
import scala.concurrent.{Await, TimeoutException}
import scala.util.{Failure, Success, Try}
import dahu.utils.debug._
case class Config(problemFile: File = null,
minInstances: Int = 0,
......@@ -31,8 +31,8 @@ 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]("num-threads")
// .action((n, c) => c.copy(numThreads = n))
opt[Int]("warmup")
.action((t, c) => c.copy(warmupTimeSec = t))
......@@ -46,11 +46,11 @@ object Main extends App {
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))
// 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))
}
......@@ -201,9 +201,9 @@ object Main extends App {
chronicle.copy(actions = chronicle.actions ++ actionInstances)
case (chronicle, _) => chronicle
}
// println(result)
// println(result)
val solution = Planner.solve(result, deadline)
// println(solution)
// println(solution)
solution
}
......
package dahu.planner
package dahu.planning.planner
import dahu.model.input.{Ident, Input, Tentative}
import dahu.planning.model.common._
import dahu.planning.model.core._
import dahu.planning.model.transforms.ActionInstantiation
import dahu.model.input.{Ident, Input, Tentative}
case class Action[F[_]](name: String,
start: F[Int],
end: F[Int],
......
package dahu.planner
package dahu.planning.planner
import dahu.planning.model.common
import dahu.planning.model.common.operators.BinaryOperator
import dahu.planning.model.common.{Cst => _, _}
import dahu.planning.model.core._
import dahu.planning.model.core
import dahu.model.functions.{Fun2, FunN, Reversible}
import dahu.model.input._
import dahu.model.input.dsl._
import dahu.model.math.{bool, int}
import dahu.model.types.{BoxedInt, Tag, TagIsoInt}
import dahu.planning.model.common.operators.BinaryOperator
import dahu.planning.model.common.{Cst => _, _}
import dahu.planning.model.core._
import dahu.planning.model.{common, core}
import dahu.utils.errors._
import scala.collection.mutable
......@@ -146,30 +145,6 @@ case class ProblemContext(intTag: BoxedInt[Literal],
def anonymousTp(): Tentative[Int] =
Input[Int]().subjectTo(tp => temporalOrigin <= tp && tp <= temporalHorizon)
// def encode(ie: IntExpr)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Int] =
// ie match {
// case IntTerm(IntLiteral(d)) => Cst(d)
// case IntTerm(v: Var) =>
// assert(v.typ == Type.Integer)
// val variable = encode(v)
// variable.typ match {
// case tpe: BoxedInt[Literal] => variable.unboxed(tpe)
// case _ => unexpected
// }
// case Add(lhs, rhs) => encode(lhs) + encode(rhs)
// case Minus(x) => -encode(x)
// case x => unexpected(s"Unsupported int expression: $x")
// }
//
// def encode(tp: TPRef)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Int] = tp match {
// case TPRef(id, IntTerm(IntLiteral(0))) if id.toString == "start" =>
// temporalOrigin // TODO: match by string....
// case TPRef(id, IntTerm(IntLiteral(0))) if id.toString == "end" =>
// temporalHorizon // TODO: match by string....
// case TPRef(id, IntTerm(IntLiteral(0))) =>
// Input[Int](Ident(id)).subjectTo(tp => temporalOrigin <= tp && tp <= temporalHorizon)
// case TPRef(id, delay) => encode(TPRef(id)) + encode(delay)
// }
def encode(orig: core.Fluent)(implicit argRewrite: Arg => Tentative[Literal]): Fluent =
Fluent(orig.template, orig.params.map(encode(_)))
......@@ -459,7 +434,7 @@ case class Chronicle(ctx: ProblemContext,
}
}
def toSatProblem(implicit cfg: Config) = {
def toSatProblem = {
var count = 0
val acts: Seq[Opt[Action[Tentative]]] = actions
val effs: Seq[Opt[EffectToken]] =
......@@ -493,10 +468,7 @@ case class Chronicle(ctx: ProblemContext,
persistenceStart <= sc,
ec <= persistenceEnd)
}
if(cfg.useXorForSupport)
implies(pc, xor(disjuncts: _*))
else
implies(pc, or(disjuncts: _*))
implies(pc, or(disjuncts: _*))
}
val allConstraints = consts ++ nonOverlappingEffectsConstraints ++ supportConstraints
......
package dahu.planner
package dahu.planning.planner
case class Operator[F[_]](name: F[String],
args: F[Seq[Literal]],
......
package dahu.planner
package dahu.planning.planner
import cats.implicits._
import dahu.model.compiler.Algebras
import dahu.model.interpreter.Interpreter
import dahu.model.interpreter.Interpreter.Res
import dahu.model.types.Value
import dahu.solvers.MetaSolver
import dahu.z3.Z3PartialSolver
import dahu.utils.errors._
import dahu.utils.debug._
import cats.implicits._
import dahu.utils.errors._
import dahu.z3.Z3PartialSolver
object Planner {
val backend = Z3PartialSolver.builder
def solve(chronicle: Chronicle, deadline: Long)(implicit cfg: Config): Option[String] = {
def solve(chronicle: Chronicle, deadline: Long): Option[String] = {
if(System.currentTimeMillis() > deadline)
return None
val sat = chronicle.toSatProblem
......
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