Commit 174aa6ab authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

Support variable durations of actions.

parent a4770e83
......@@ -5,7 +5,8 @@ import dahu.model.ir.Total
import dahu.model.math.BooleanLike.BooleanOps
import dahu.model.math.Numeric.{NumericBase, NumericOps}
import dahu.model.math._
import dahu.model.types.Tag
import dahu.model.math.obj.Unboxed
import dahu.model.types.{BoxedInt, Tag}
import scala.language.implicitConversions
......@@ -48,6 +49,11 @@ object dsl {
}
implicit class UnboxOps[A](private val lhs: Tentative[A]) extends AnyVal {
def unboxed(implicit tag: BoxedInt[A]): Tentative[Int] =
Computation(new Unboxed[A], lhs)
}
implicit class ProductOps[T[_[_]]](private val lhs: Product[T]) extends AnyVal {
def subjectTo(cond: Product[T] => Tentative[Boolean]): SubjectTo[T[cats.Id]] =
......
......@@ -2,7 +2,16 @@ package dahu.model.math
import dahu.model.functions.{Fun1, Fun2, Fun3, FunN}
import dahu.model.input.Cst
import dahu.model.types.Tag
import dahu.model.types.{BoxedInt, Tag}
object obj {
/** Transforms a boxed int into an int. */
class Unboxed[A](implicit tag: BoxedInt[A]) extends Fun1[A, Int] {
override def of(in: A): Int = tag.toInt(in)
override def name: String = "unbox"
}
}
object double {
......
......@@ -7,6 +7,7 @@ import dahu.model.functions._
import dahu.model.input.Anonymous
import dahu.model.ir._
import dahu.model.math._
import dahu.model.math.obj.Unboxed
import dahu.model.types._
import dahu.utils.errors._
......@@ -91,13 +92,17 @@ class IntBoolSatisfactionProblem[AST <: TotalSubAST[_]](val ast: AST) {
if supportedFunctions.contains(wf.f) && args.forall(sup) =>
TRANS(ComputationF(wf.f, args, t)) // unwrap and retry
case x @ ComputationF(f: Unboxed[_], Seq(arg), t) =>
originalCells(arg) // unbox operation, use the previous cell
case x =>
x.typ match {
case Tag.ofBoolean =>
SupportedInput(InputF(Anonymous(), Tag.ofBoolean))
case t: TagIsoInt[_] =>
CompatibleInput(InputF(Anonymous(), Tag.ofInt), t)
case _ => Unsupported
case _ =>
Unsupported
}
}
......
......@@ -42,6 +42,9 @@ object TagIsoInt {
}
}
/** Marker trait for a type that is a simple container of Int. */
trait BoxedInt[T] extends TagIsoInt[T]
trait ProductTag[P[_[_]]] extends Tag[P[cats.Id]] {
def exprProd: ProductExpr[P, Tentative]
def idProd: ProductExpr[P, cats.Id]
......@@ -92,14 +95,13 @@ object Tag {
def typeOf[T](implicit ttag: universe.WeakTypeTag[T]): universe.Type = ttag.tpe
implicit case object ofInt extends TagIsoInt[Int] {
implicit case object ofInt extends BoxedInt[Int] {
override val typ: Type = typeOf[Int]
override def fromInt(i: Int): Int = i
override def toInt(t: Int): Int = t
// todo: put real bounds
override val min: Int = -100 //Integer.MIN_VALUE /2 +1
override val max: Int = 100 //Integer.MAX_VALUE /2 -1
override val min: Int = Integer.MIN_VALUE / 2 + 1
override val max: Int = Integer.MAX_VALUE / 2 - 1
}
implicit case object ofBoolean extends TagIsoInt[Boolean] {
......
package dahu.planner
import copla.lang.model.core._
import dahu.model.input.{Cst, Ident, Input, Tentative}
import dahu.utils.errors._
import dahu.model.input.{Ident, Input, Tentative}
case class Action[F[_]](name: String,
start: F[Int],
......@@ -13,68 +12,6 @@ case class Action[F[_]](name: String,
object Action {
var counter = 0
// case class Context(pb: ProblemContext, trans: Id => Id, params: Array[(Arg, Instance)])
//
// def updateScope(base: Scope, addLevel: String)(scope: Scope): Scope = {
// scope match {
// case `base` => base + addLevel
// case RootScope => RootScope
// case InnerScope(s, name) => updateScope(base, addLevel)(s) + name
// }
// }
// def updateId(base: Scope, addLevel: String)(id: Id): Id = id match {
// case Id(s, name) => Id(updateScope(base, addLevel)(s), name)
// }
//
// def encode(v: Var)(implicit ctx: Context): Tentative[Instance] =
// v match {
// case LocalVar(id, tpe) => Input(Ident(LocalVar(ctx.trans(id), tpe)))(ctx.pb.specializedTags(tpe))
// case i @ Instance(id, tpe) => Cst(i)(ctx.pb.specializedTags(tpe))
// case x: Arg => ctx.params.find(_._1 == x) match {
// case Some((_, instance)) => Cst(instance)(ctx.pb.specializedTags(instance.typ))
// case None => unexpected
// }
// }
// def encode(tp: TPRef)(implicit ctx: Context): Tentative[Int] = tp match {
// case TPRef(TPId(id), delay) => ctx.pb.encode(TPRef(TPId(ctx.trans(id)), delay))
// }
//
// def eqv(v1: Var, v2: Var)(implicit ctx: Context): Tentative[Boolean] = ctx.pb.eqv(encode(v1), encode(v2))
// def neq(v1: Var, v2: Var)(implicit ctx: Context): Tentative[Boolean] = ctx.pb.neq(encode(v1), encode(v2))
//
// def extend(chronicle: Chronicle, statement: Statement)(implicit ctx: Context): Chronicle = statement match {
// case StaticEqualAssertion(lhs, rhs) =>
// chronicle.copy(constraints = eqv(lhs, rhs) :: chronicle.constraints)
// case StaticDifferentAssertion(lhs, rhs) =>
// chronicle.copy(constraints = neq(lhs, rhs) :: chronicle.constraints)
// }
def primitive(template: ActionTemplate, ctx: ProblemContext)(
args: Array[Literal]): Action[Tentative] = {
def lit2Cst(lit: Literal): Cst[Literal] = lit match {
case x @ ObjLit(instance) => x.asConstant(ctx.specializedTags(instance.typ))
case x: IntLit => x.asConstant(ctx.intTag)
}
counter += 1
val act = template.instance(s"${template.name}_$counter")
assert(act.args.length == args.length)
val argsRewrite: Arg => Tentative[Literal] = x => {
val id = act.args.indexOf(x)
lit2Cst(args(id))
}
val chronicle = act.content.foldLeft(Chronicle.empty(ctx)) {
case (c, s) => c.extended(s)(argsRewrite)
}
Action(act.template.name,
ctx.encode(act.start),
ctx.encode(act.end),
args.toList.map(lit2Cst),
chronicle)
}
def instance(template: ActionTemplate, ctx: ProblemContext): Action[Tentative] = {
counter += 1
val act = template.instance(s"${template.name}_$counter")
......@@ -87,8 +24,8 @@ object Action {
}
Action(act.template.name,
ctx.encode(act.start),
ctx.encode(act.end),
ctx.encode(act.start)(argsRewrite),
ctx.encode(act.end)(argsRewrite),
act.args.toList.map(argsRewrite),
chronicle)
}
......
......@@ -6,7 +6,7 @@ import dahu.model.functions.WrappedFunction
import dahu.model.input._
import dahu.model.input.dsl._
import dahu.model.math.{bool, int}
import dahu.model.types.{ProductTag, Tag, TagIsoInt}
import dahu.model.types.{BoxedInt, Tag, TagIsoInt}
import dahu.utils.errors._
import scala.collection.mutable
......@@ -34,12 +34,10 @@ case class ObjLit(value: Instance) extends Literal {
override def toString: String = value.toString
}
case class ProblemContext(intTag: TagIsoInt[Literal],
case class ProblemContext(intTag: BoxedInt[Literal],
topTag: TagIsoInt[Literal],
specializedTags: Type => TagIsoInt[Literal]) {
private val Equality = WrappedFunction.wrap(int.EQ)(topTag, implicitly[TagIsoInt[Boolean]])
def encode(v: Var)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Literal] =
v match {
case IntLiteral(i) => IntLit(i).asConstant(intTag)
......@@ -53,14 +51,22 @@ case class ProblemContext(intTag: TagIsoInt[Literal],
def anonymousTp(): Tentative[Int] =
Input[Int]().subjectTo(tp => temporalOrigin <= tp && tp <= temporalHorizon)
def encode(ie: IntExpr): Tentative[Int] = ie match {
case VarIntExpr(IntLiteral(d)) => Cst(d)
case Add(lhs, rhs) => encode(lhs) + encode(rhs)
case Minus(x) => -encode(x)
case x => unexpected(s"Unsupported int expression: $x")
}
def encode(ie: IntExpr)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Int] =
ie match {
case VarIntExpr(IntLiteral(d)) => Cst(d)
case VarIntExpr(v: Var) =>
assert(v.typ == Type.Integers)
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): Tentative[Int] = tp match {
def encode(tp: TPRef)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Int] = tp match {
case TPRef(id, VarIntExpr(IntLiteral(0))) if id.toString == "start" =>
temporalOrigin // TODO: match by string....
case TPRef(id, VarIntExpr(IntLiteral(0))) if id.toString == "end" =>
......@@ -77,11 +83,31 @@ case class ProblemContext(intTag: TagIsoInt[Literal],
def eqv(lhs: Var, rhs: Var)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Boolean] =
eqv(encode(lhs), encode(rhs))
private val ObjEquality = WrappedFunction.wrap(int.EQ)(topTag, implicitly[TagIsoInt[Boolean]])
private val IntEquality = WrappedFunction.wrap(int.EQ)(intTag, implicitly[TagIsoInt[Boolean]])
private def isInt(e: Tentative[Literal]): Boolean = e.typ match {
case t: BoxedInt[_] =>
assert(t == intTag)
true
case t: TagIsoInt[_] =>
assert(topTag.min <= t.min && t.max <= topTag.max)
false
case _ =>
unexpected
}
def eqv(lhs: Tentative[Literal], rhs: Tentative[Literal]): Tentative[Boolean] =
(lhs, rhs) match {
case (Cst(x), Cst(y)) if x == y => bool.True
case (Cst(x), Cst(y)) if x != y => bool.False
case _ => Computation(Equality, lhs, rhs)
case _ =>
if(isInt(lhs) && isInt(rhs))
Computation(IntEquality, lhs, rhs)
else if(isInt(lhs) || isInt(rhs))
bool.False
else {
Computation(ObjEquality, lhs, rhs)
}
}
def neq(lhs: Var, rhs: Var)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Boolean] =
......@@ -230,7 +256,7 @@ object ProblemContext {
override def toString: String = s"TOP[$min,$max]"
}
val intTag = new TagIsoInt[IntLit] {
val intTag = new BoxedInt[IntLit] {
override def fromInt(i: Int): IntLit = IntLit(i)
override def toInt(t: IntLit): Int = t.value
......@@ -247,7 +273,7 @@ object ProblemContext {
else
memo.getOrElseUpdate(t, tagOf(t))
ProblemContext(intTag.asInstanceOf[TagIsoInt[Literal]],
ProblemContext(intTag.asInstanceOf[BoxedInt[Literal]],
topTag.asInstanceOf[TagIsoInt[Literal]],
specializedTag.asInstanceOf[Type => TagIsoInt[Literal]])
}
......
......@@ -9,7 +9,7 @@ import copla.lang.model.core
import dahu.model.input.Tentative
case class Config(problemFile: File = null,
encoding: Encoding = Incremental(20),
encoding: Encoding = Incremental(10),
symBreak: Boolean = true,
useXorForSupport: Boolean = true)
sealed trait Encoding
......@@ -35,23 +35,6 @@ object Main extends App {
case None =>
}
// for(i <- Problems.satisfiables) {
// solve(i) match {
// case Some(sol) =>
// println("== Solution ==")
// println(sol)
// case None => unexpected
// }
//
// }
//
// for(i <- Problems.unsatisfiables) {
// solve(i) match {
// case Some(sol) => unexpected("Got solution on unsatisfiable problem.")
// case None => println("No solution")
// }
// }
def solve(problemFile: File)(implicit cfg: Config): Option[Any] = {
println("Parsing...")
lang.parse(problemFile) match {
......@@ -71,33 +54,6 @@ object Main extends App {
}
}
// def solve(anml: String): Option[Any] = {
// solve(lang.parse(anml))
// }
// def solveFull(model: core.CoreModel)(implicit cfg: Config): Option[Any] = {
// println("Encoding...")
// 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 argDomains: Seq[Set[Lite]] = action.args.map(a => {
// val tpe = ctx.specializedTags(a.typ)
// (tpe.min to tpe.max).toSet.map(tpe.fromInt)
// })
// val allParameterCombinations: Set[Array[Instance]] =
// dahu.utils.allCombinations(argDomains).map(_.toArray)
// val actionInstances = allParameterCombinations.map { args =>
// Opt.optional(Action.primitive(action, ctx)(args))
// }
// chronicle.copy(actions = chronicle.actions ++ actionInstances)
// case (chronicle, _) => chronicle
// }
//// println(result)
// val solution = Planner.solve(result)
//// println(solution)
// solution
// }
def solveIncremental(model: core.CoreModel, maxSteps: Int)(implicit cfg: Config): Option[Any] = {
for(i <- 0 to maxSteps) {
......
......@@ -34,7 +34,7 @@ object Planner {
}
.mkString("\n")
)
case _ => unexpected
case x => unexpected(x.toString)
}
case None => 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