Commit 9b41a59f authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

Support open/closed intervals in planning model.

parent 667bbe5f
......@@ -3,13 +3,15 @@ package dahu.model.math
import dahu.model.functions._
import dahu.model.types.{Tag, TagIsoInt}
trait Numeric[T, F[_]] {
trait Ordered[T, F[_]] {
def leq(lhs: F[T], rhs: F[T]): F[Boolean]
def eqv(lhs: F[T], rhs: F[T]): F[Boolean]
def geq(lhs: F[T], rhs: F[T]): F[Boolean] = leq(rhs, lhs)
def lt(lhs: F[T], rhs: F[T]): F[Boolean]
def gt(lhs: F[T], rhs: F[T]): F[Boolean] = lt(rhs, lhs)
}
trait Numeric[T, F[_]] extends Ordered[T, F] {
def add(lhs: F[T], rhs: F[T]): F[T]
def negate(term: F[T]): F[T]
......
......@@ -353,7 +353,7 @@ abstract class AnmlParser(val initialContext: Ctx)(implicit predef: Predef) {
val timepoint: P[StaticExpr] =
staticExpr.namedFilter(_.typ.isSubtypeOf(Type.Integers), "of-type-integer")
val interval: Parser[Interval] =
val interval: Parser[ClosedInterval[StaticExpr]] =
("[" ~/
((timepoint ~/ ("," ~/ timepoint).?).map {
case (tp, None) => (tp, tp) // "[end]" becomes "[end, end]"
......@@ -366,7 +366,7 @@ abstract class AnmlParser(val initialContext: Ctx)(implicit predef: Predef) {
}
})) ~
"]").map {
case (tp1, tp2) => Interval(tp1, tp2)
case (tp1, tp2) => ClosedInterval(tp1, tp2)
}
val timedAssertion: Parser[TimedAssertion] = {
......
package dahu.planning.model.common
sealed abstract class Interval[A] {
val start: A
val end: A
def isLeftOpen: Boolean
def isRightOpen: Boolean
def map[B](f: A => B): Interval[B] = this match {
case ClosedInterval(s, e) => ClosedInterval(f(s), f(e))
case LeftOpenInterval(s, e) => LeftOpenInterval(f(s), f(e))
case RightOpenInterval(s, e) => RightOpenInterval(f(s), f(e))
case OpenInterval(s, e) => OpenInterval(f(s), f(e))
}
def substituteWith[B](start: B, end: B): Interval[B] = this match {
case _: ClosedInterval[A] => ClosedInterval(start, end)
case _: LeftOpenInterval[A] => LeftOpenInterval(start, end)
case _: RightOpenInterval[A] => RightOpenInterval(start, end)
case _: OpenInterval[A] => OpenInterval(start, end)
}
}
object Interval {
def point[A](pt: A): Interval[A] = ClosedInterval(pt, pt)
}
case class ClosedInterval[A](start: A, end: A) extends Interval[A] {
override def toString: String = s"[$start, $end]"
override def isLeftOpen: Boolean = false
override def isRightOpen: Boolean = false
}
case class LeftOpenInterval[A](start: A, end: A) extends Interval[A] {
override def toString: String = s"]$start, $end]"
override def isLeftOpen: Boolean = true
override def isRightOpen: Boolean = false
}
case class RightOpenInterval[A](start: A, end: A) extends Interval[A] {
override def toString: String = s"[$start, $end["
override def isLeftOpen: Boolean = false
override def isRightOpen: Boolean = true
}
case class OpenInterval[A](start: A, end: A) extends Interval[A] {
override def toString: String = s"]$start, $end["
override def isLeftOpen: Boolean = true
override def isRightOpen: Boolean = true
}
......@@ -96,8 +96,7 @@ package object core {
}
sealed trait TimedAssertion extends Statement {
def start: Expr
def end: Expr
def itv: Interval[Expr]
def fluent: Fluent
}
......@@ -110,19 +109,18 @@ package object core {
def valueAfterChange: Expr
}
final case class TimedEqualAssertion(start: Expr, end: Expr, fluent: Fluent, value: Expr)
final case class TimedEqualAssertion(itv: Interval[Expr], fluent: Fluent, value: Expr)
extends TimedAssertion
with RequiresSupport {
override def toString: String = s"[$start, $end] $fluent == $value"
override def toString: String = s"$itv $fluent == $value"
}
final case class TimedAssignmentAssertion(start: Expr, end: Expr, fluent: Fluent, value: Expr)
final case class TimedAssignmentAssertion(itv: Interval[Expr], fluent: Fluent, value: Expr)
extends TimedAssertion
with ProvidesChange {
override def valueAfterChange: Expr = value
override def toString: String = s"[$start,$end] $fluent := $value"
override def toString: String = s"$itv $fluent := $value"
}
final case class TimedTransitionAssertion(start: Expr,
end: Expr,
final case class TimedTransitionAssertion(itv: Interval[Expr],
fluent: Fluent,
from: Expr,
to: Expr)
......@@ -130,7 +128,7 @@ package object core {
with RequiresSupport
with ProvidesChange {
override def valueAfterChange: Expr = to
override def toString: String = s"[$start, $end] $fluent == $from :-> $to"
override def toString: String = s"$itv $fluent == $from :-> $to"
}
final case class ActionTemplate(scope: InnerScope, content: Seq[InActionBlock])(
......
......@@ -97,12 +97,6 @@ package object full {
override def toString: String = term.toString
}
case class Interval(start: StaticExpr, end: StaticExpr) {
require(start.typ.isSubtypeOf(Type.Integers))
require(end.typ.isSubtypeOf(Type.Integers))
override def toString: String = s"[$start, $end]"
}
/** A block wrapping other blocks pertaining to the same scope. */
sealed trait Wrapper extends Block {
def wrapped: Seq[Block]
......@@ -154,10 +148,14 @@ package object full {
}
trait TemporalQualifier
case class Equals(interval: Interval) extends TemporalQualifier {
case class Equals(interval: Interval[StaticExpr]) extends TemporalQualifier {
require(interval.start.typ.isSubtypeOf(Type.Integers))
require(interval.end.typ.isSubtypeOf(Type.Integers))
override def toString: String = interval.toString
}
case class Contains(interval: Interval) extends TemporalQualifier {
case class Contains(interval: Interval[StaticExpr]) extends TemporalQualifier {
require(interval.start.typ.isSubtypeOf(Type.Integers))
require(interval.end.typ.isSubtypeOf(Type.Integers))
override def toString: String = s"$interval contains"
}
......
......@@ -33,6 +33,15 @@ object ActionInstantiation {
case Op2(op, lhs, rhs) => Op2(op, map(lhs, f), map(rhs, f))
}
}
implicit object ofInterval extends IdRewrite[Interval[Expr]] {
override def map(a: Interval[Expr], f: Id => Id)(implicit predef: Predef): Interval[Expr] =
a match {
case ClosedInterval(l, r) => ClosedInterval(l.rw(f), r.rw(f))
case LeftOpenInterval(l, r) => LeftOpenInterval(l.rw(f), r.rw(f))
case RightOpenInterval(l, r) => RightOpenInterval(l.rw(f), r.rw(f))
case OpenInterval(l, r) => OpenInterval(l.rw(f), r.rw(f))
}
}
implicit object ofConstantTemplate extends IdRewrite[ConstantTemplate] {
override def map(a: ConstantTemplate, f: Id => Id)(
......@@ -63,12 +72,12 @@ object ActionInstantiation {
case StaticAssignmentAssertion(x: BoundConstant, cst) =>
StaticAssignmentAssertion(new BoundConstant(x.template, x.params.map(_.rw(f))),
cst.rw(f))
case TimedAssignmentAssertion(st, ed, fl, value) =>
TimedAssignmentAssertion(st.rw(f), ed.rw(f), fl.rw(f), value.rw(f))
case TimedEqualAssertion(st, ed, fl, value) =>
TimedEqualAssertion(st.rw(f), ed.rw(f), fl.rw(f), value.rw(f))
case TimedTransitionAssertion(st, ed, fl, from, to) =>
TimedTransitionAssertion(st.rw(f), ed.rw(f), fl.rw(f), from.rw(f), to.rw(f))
case TimedAssignmentAssertion(itv, fl, value) =>
TimedAssignmentAssertion(itv.rw(f), fl.rw(f), value.rw(f))
case TimedEqualAssertion(itv, fl, value) =>
TimedEqualAssertion(itv.rw(f), fl.rw(f), value.rw(f))
case TimedTransitionAssertion(itv, fl, from, to) =>
TimedTransitionAssertion(itv.rw(f), fl.rw(f), from.rw(f), to.rw(f))
case BindAssertion(Constant(template, params), LocalVar(id, tpe)) =>
BindAssertion(Constant(template.rw(f), params.map(_.rw(f))), LocalVar(f(id), tpe))
}
......
......@@ -110,7 +110,13 @@ object FullToCore {
s"Assignment assertions on constant functions are only supported when all parameters are declared instances: $block")
case full.TemporallyQualifiedAssertion(qualifier, assertion) =>
val startEnd: CoreM[(Expr, Expr)] =
def consistency(itv: Interval[Expr]) = itv match {
case ClosedInterval(s, e) => s <= e
case LeftOpenInterval(s, e) => s < e
case RightOpenInterval(s, e) => s < e
case OpenInterval(s, e) => s < e
}
val startEnd: CoreM[Interval[Expr]] =
qualifier match {
case full.Equals(interval)
if ctx.config.mergeTimepoints && assertion.name.startsWith(reservedPrefix) =>
......@@ -119,7 +125,7 @@ object FullToCore {
for {
start <- f2c(interval.start)
end <- f2c(interval.end)
} yield (start, end)
} yield interval.substituteWith(start, end)
case full.Equals(interval) =>
for {
itvStart <- f2c(interval.start)
......@@ -129,7 +135,7 @@ object FullToCore {
_ <- CoreM.unit(core.StaticBooleanAssertion(itvStart === assertion.start))
_ <- CoreM.unit(core.StaticBooleanAssertion(assertion.end === itvEnd))
} yield (assertion.start, assertion.end)
} yield interval.substituteWith(assertion.start, assertion.end)
case full.Contains(interval) =>
for {
itvStart <- f2c(interval.start)
......@@ -137,41 +143,44 @@ object FullToCore {
_ <- CoreM.unit(
core.LocalVarDeclaration(assertion.start),
core.LocalVarDeclaration(assertion.end),
core.StaticBooleanAssertion(itvStart <= assertion.start),
core.StaticBooleanAssertion(assertion.end <= itvEnd)
if(interval.isLeftOpen)
core.StaticBooleanAssertion(itvStart < assertion.start)
else
core.StaticBooleanAssertion(itvStart <= assertion.start),
if(interval.isRightOpen)
core.StaticBooleanAssertion(assertion.end < itvEnd)
else
core.StaticBooleanAssertion(assertion.end <= itvEnd)
)
} yield (assertion.start, assertion.end)
} yield ClosedInterval(assertion.start, assertion.end)
}
assertion match {
case full.TimedEqualAssertion(fluent, value, _, _) =>
for {
se <- startEnd
(start, end) = se
itv <- startEnd
coreFluent <- f2c(fluent)
coreValue <- f2c(value)
_ <- CoreM.unit(core.TimedEqualAssertion(start, end, coreFluent, coreValue),
core.StaticBooleanAssertion(start <= end))
_ <- CoreM.unit(core.TimedEqualAssertion(itv, coreFluent, coreValue),
core.StaticBooleanAssertion(consistency(itv)))
} yield ()
case full.TimedAssignmentAssertion(fluent, value, _, _) =>
for {
se <- startEnd
(start, end) = se
itv <- startEnd
coreFluent <- f2c(fluent)
coreValue <- f2c(value)
_ <- CoreM.unit(core.TimedAssignmentAssertion(start, end, coreFluent, coreValue),
core.StaticBooleanAssertion(start <= end))
_ <- CoreM.unit(core.TimedAssignmentAssertion(itv, coreFluent, coreValue),
core.StaticBooleanAssertion(consistency(itv)))
} yield ()
case full.TimedTransitionAssertion(fluent, fromValue, toValue, _, _) =>
for {
se <- startEnd
(start, end) = se
itv <- startEnd
coreFluent <- f2c(fluent)
coreFrom <- f2c(fromValue)
coreTo <- f2c(toValue)
_ <- CoreM.unit(core.TimedTransitionAssertion(start, end, coreFluent, coreFrom, coreTo),
core.StaticBooleanAssertion(start < end))
_ <- CoreM.unit(core.TimedTransitionAssertion(itv, coreFluent, coreFrom, coreTo),
core.StaticBooleanAssertion(itv.start < itv.end))
} yield ()
}
......
package dahu.planning.pddl.parser
import dahu.planning.model.common.{operators, Arg, LocalVar}
import dahu.planning.model.common._
import dahu.planning.model.full._
import Utils._
import dahu.utils.errors._
......@@ -57,7 +57,7 @@ class ActionFactory(actionName: String, parent: Resolver, model: Model) extends
val assertion = resolver.getTranslator(funcName).condition(e, resolver)
rec(
TemporallyQualifiedAssertion(
Equals(Interval(start, start)),
Equals(ClosedInterval(start, start)),
assertion
)
)
......@@ -68,7 +68,18 @@ class ActionFactory(actionName: String, parent: Resolver, model: Model) extends
val assertion = resolver.getTranslator(funcName).condition(e, resolver)
rec(
TemporallyQualifiedAssertion(
Equals(Interval(end, end)),
Equals(ClosedInterval(end, end)),
assertion
)
)
}
case ast.OverAll(e) =>
e match {
case ast.AssertionOnFunction(funcName) =>
val assertion = resolver.getTranslator(funcName).condition(e, resolver)
rec(
TemporallyQualifiedAssertion(
Equals(ClosedInterval(start, end)),
assertion
)
)
......@@ -84,7 +95,7 @@ class ActionFactory(actionName: String, parent: Resolver, model: Model) extends
val assertion = resolver.getTranslator(funcName).effect(e, resolver)
rec(
TemporallyQualifiedAssertion(
Equals(Interval(start, start)),
Equals(LeftOpenInterval(start, BinaryExprTree(operators.Add, start, predef.Epsilon))),
assertion
)
)
......@@ -95,7 +106,7 @@ class ActionFactory(actionName: String, parent: Resolver, model: Model) extends
val assertion = resolver.getTranslator(funcName).effect(e, resolver)
rec(
TemporallyQualifiedAssertion(
Equals(Interval(end, end)),
Equals(LeftOpenInterval(end, BinaryExprTree(operators.Add, end, predef.Epsilon))),
assertion
)
)
......
......@@ -94,7 +94,7 @@ class ModelFactory(val predef: PddlPredef) extends Factory {
case ast.AssertionOnFunction(funcName) =>
getTranslator(funcName).effect(e, resolver)
}
rec(TemporallyQualifiedAssertion(Equals(Interval(predef.Start, predef.Start)), assertion))
rec(TemporallyQualifiedAssertion(Equals(ClosedInterval(predef.Start, predef.Start)), assertion))
}
private def recordGoal(e: Exp): Unit = e match {
......@@ -104,7 +104,7 @@ class ModelFactory(val predef: PddlPredef) extends Factory {
val assertion = getTranslator(name).condition(e, resolver)
rec(
TemporallyQualifiedAssertion(
Equals(Interval(predef.End, predef.End)),
Equals(ClosedInterval(predef.End, predef.End)),
assertion
))
}
......
......@@ -25,6 +25,8 @@ case class PddlPredef(discretization: Int) extends Predef {
val Number = IntSubType(RootScope / "number", Integers)
val Epsilon = IntLiteral(1)
def discretize(d: Double): Int = (d * discretization).toInt
override def baseModel: Model =
......
......@@ -140,3 +140,16 @@ object AtEnd {
}
}
}
object OverAll {
def unapply(e: Exp): Option[Exp] = {
if(e.getConnective == Connective.OVER_ALL) {
e.getChildren.asScala match {
case Seq(sub) => Some(sub)
case _ => unexpected
}
} else {
None
}
}
}
......@@ -70,7 +70,12 @@ object Main extends App {
parser.parse(domain, problem) match {
case Success(model) =>
Planner.solveIncremental(model, config.maxInstances, Deadline.now + config.maxRuntime)
Planner.solveIncremental(model, config.maxInstances, Deadline.now + config.maxRuntime) match {
case Some(sol) =>
println(sol)
case None =>
println("\nFAIL")
}
case Failure(err) =>
err.printStackTrace()
sys.exit(1)
......
......@@ -10,18 +10,17 @@ import dahu.planning.model.common.{Cst => _, _}
import dahu.planning.model.core._
import dahu.planning.model.{common, core}
import dahu.utils.errors._
import dahu.planning.planner.syntax._
import dahu.planning.planner.syntax.Ordered._
import scala.collection.mutable
case class Fluent(template: FunctionTemplate, args: Seq[Tentative[Literal]])
case class Constant(template: ConstantTemplate, args: Seq[Tentative[Literal]])
case class ConditionToken(start: Tentative[Int],
end: Tentative[Int],
fluent: Fluent,
value: Tentative[Literal])
case class EffectToken(changeStart: Tentative[Int],
changeEnd: Tentative[Int],
case class ConditionToken(itv: Interval[Tentative[Int]], fluent: Fluent, value: Tentative[Literal])
case class EffectToken(changeItv: Interval[Tentative[Int]],
persistenceEnd: Tentative[Int],
fluent: Fluent,
value: Tentative[Literal])
......@@ -99,6 +98,10 @@ case class ProblemContext(intTag: BoxedInt[Literal],
assert(e.typ.isSubtypeOf(Type.Integers))
intUnbox(encode(e))
}
def encodeAsInts(e: common.Interval[common.Expr])(
implicit argRewrite: Arg => Tentative[Literal]): Interval[Tentative[Int]] = {
e.map(encodeAsInt)
}
def applyOperator(op: BinaryOperator,
lhs: Tentative[Literal],
rhs: Tentative[Literal]): Tentative[Literal] = op match {
......@@ -361,8 +364,7 @@ case class Chronicle(ctx: ProblemContext,
case _: ArgDeclaration => this
case BindAssertion(c, v) =>
val cond = ConditionToken(
start = ctx.temporalOrigin,
end = ctx.temporalHorizon,
itv = ClosedInterval(ctx.temporalOrigin, ctx.temporalHorizon),
fluent = encode(c),
value = encode(v)
)
......@@ -370,37 +372,32 @@ case class Chronicle(ctx: ProblemContext,
conditions = cond :: conditions
)
case TimedAssignmentAssertion(start, end, fluent, value) =>
val changeStart = encodeAsInt(start)
val changeEnd = encodeAsInt(end).subjectTo(changeStart <= _)
val persistenceEnd = anonymousTp().subjectTo(changeEnd <= _)
case TimedAssignmentAssertion(itv, fluent, value) =>
val changeItv = itv.map(encodeAsInt)
val persistenceEnd = anonymousTp().subjectTo(changeItv.end <= _)
val token = EffectToken(
changeStart = changeStart,
changeEnd = changeEnd,
changeItv,
persistenceEnd = persistenceEnd,
fluent = encode(fluent),
value = encode(value)
)
copy(effects = token :: effects)
case TimedEqualAssertion(s, e, f, v) =>
val start = encodeAsInt(s)
val end = encodeAsInt(e)
case TimedEqualAssertion(itv, f, v) =>
val token = ConditionToken(
start = start,
end = end,
itv = itv.map(encodeAsInt),
fluent = encode(f),
value = encode(v)
)
copy(conditions = token :: conditions)
case TimedTransitionAssertion(s, e, f, v1, v2) =>
case TimedTransitionAssertion(ClosedInterval(s, e), f, v1, v2) =>
val start = encodeAsInt(s)
val changeStart = start + 1
val changeEnd = encodeAsInt(e).subjectTo(changeStart <= _)
val changeEnd = encodeAsInt(e)
val persistenceEnd = anonymousTp().subjectTo(changeEnd <= _)
val cond = ConditionToken(start, start, encode(f), encode(v1))
val eff = EffectToken(changeStart, changeEnd, persistenceEnd, encode(f), encode(v2))
val cond = ConditionToken(ClosedInterval(start, start), encode(f), encode(v1))
val eff =
EffectToken(LeftOpenInterval(start, changeEnd), persistenceEnd, encode(f), encode(v2))
copy(
conditions = cond :: conditions,
effects = eff :: effects
......@@ -408,8 +405,7 @@ case class Chronicle(ctx: ProblemContext,
case StaticAssignmentAssertion(lhs, rhs) =>
val eff = EffectToken(
changeStart = ctx.temporalOrigin,
changeEnd = ctx.temporalOrigin,
changeItv = ClosedInterval(ctx.temporalOrigin, ctx.temporalOrigin),
persistenceEnd = ctx.temporalHorizon,
fluent = encode(lhs),
value = encode(rhs)
......@@ -451,22 +447,23 @@ case class Chronicle(ctx: ProblemContext,
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)) =>
implies(and(p1, p2, sameFluent(fluent1, fluent2)), end1 < start2 || end2 < start1)
case (Opt(EffectToken(changeItv1, end1, fluent1, _), p1),
Opt(EffectToken(changeItv2, end2, fluent2, _), p2)) =>
implies(and(p1, p2, sameFluent(fluent1, fluent2)),
Interval.point(end1) :< changeItv2 || Interval.point(end2) :< changeItv1)
}
}
val supportConstraints =
conds.map {
case Opt(ConditionToken(sc, ec, fc, vc), pc) =>
case Opt(ConditionToken(persItv, fc, vc), pc) =>
val disjuncts = effs.map {
case Opt(EffectToken(_, persistenceStart, persistenceEnd, fe, ve), pe) =>
case Opt(EffectToken(changeItv, persistenceEnd, fe, ve), pe) =>
and(pe,
sameFluent(fc, fe),
ctx.eqv(vc, ve),
persistenceStart <= sc,
ec <= persistenceEnd)
changeItv <= persItv,
persItv <= Interval.point(persistenceEnd))
}
implies(pc, or(disjuncts: _*))
}
......
package dahu.planning.planner
import dahu.model.input.{Computation, Cst, Tentative}
import dahu.model.math._
import dahu.planning.model.common.Interval
package object syntax {
trait Comparable[A, B] {
type C
def leq(a: A, b: B): C
def lt(a: A, b: B): C
def geq(a: A, b: B): C
def gt(a: A, b: B): C
}
trait Ordered[A] extends Comparable[A, A] {
override def geq(a: A, b: A): C = leq(b, a)
override def gt(a: A, b: A): C = lt(b, a)
}
object Ordered {
type Aux[A, C0] = Ordered[A] { type C = C0 }
implicit val ofTentativeInt: Aux[Tentative[Int], Tentative[Boolean]] =
new Ordered[Tentative[Int]] {
type C = Tentative[Boolean]
override def leq(a: Tentative[Int], b: Tentative[Int]): Tentative[Boolean] =
Computation(int.LEQ, a, b)
override def lt(a: Tentative[Int], b: Tentative[Int]): Tentative[Boolean] =
leq(Computation(int.Add, Seq(a, Cst(1))), b)
}
implicit def intervalComparable[A, C](implicit C: Ordered[A]) =
new Ordered[Interval[A]] {
type C = C.C
override def leq(a: Interval[A], b: Interval[A]): C =
C.leq(a.end, b.start)
override def lt(a: Interval[A], b: Interval[A]): C =
if(a.isRightOpen || b.isLeftOpen)
C.leq(a.end, b.start)
else
C.lt(a.end, b.start)
}
implicit class OrderedOps[A](private val a: A) extends AnyVal {
def <=(b: A)(implicit C: Ordered[A]): C.C = C.leq(a, b)
def :<(b: A)(implicit C: Ordered[A]): C.C = C.lt(a, b)
}
}
}
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