Commit eac8550a authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

Lazy processing of DAGs

parent 0fff4e58
......@@ -27,33 +27,33 @@ object GraphColoring extends Family("graph-coloring") {
instances("simple-graph") {
val A = color("A")
val B = color("B")
val C = color("C")
// val C = color("C")
val sat = A =!= B && B =!= C && C =!= A
val sat = A =!= B// && B =!= C// && C =!= A
Seq(
SatProblem.fromSat(sat, 6),
SatProblem.fromSat(sat && A === Green, 2),
SatProblem.fromSat(sat && A =!= Green, 4)
// SatProblem.fromSat(sat && A === Green, 2),
// SatProblem.fromSat(sat && A =!= Green, 4)
)
}
instances("australia") {
val WA = color("WA")
val NT = color("NT")
val SA = color("SA")
val Q = color("QL")
val NSW = color("NSW")
val V = color("Vic")
val vars = Seq(SA, WA, NT, Q, NSW, V)
val sat =
WA =!= NT && WA =!= SA && NT =!= SA && NT =!= Q && Q =!= SA && Q =!= NSW && NSW =!= V && NSW =!= SA && V =!= SA
Seq(
SatProblem.fromSat(sat, 6),
SatProblem.fromSat(sat && SA === Red, 2),
SatProblem.fromSat(sat && SA =!= Red, 4)
)
}
// instances("australia") {
// val WA = color("WA")
// val NT = color("NT")
// val SA = color("SA")
// val Q = color("QL")
// val NSW = color("NSW")
// val V = color("Vic")
//
// val vars = Seq(SA, WA, NT, Q, NSW, V)
//
// val sat =
// WA =!= NT && WA =!= SA && NT =!= SA && NT =!= Q && Q =!= SA && Q =!= NSW && NSW =!= V && NSW =!= SA && V =!= SA
//
// Seq(
// SatProblem.fromSat(sat, 6),
// SatProblem.fromSat(sat && SA === Red, 2),
// SatProblem.fromSat(sat && SA =!= Red, 4)
// )
// }
}
......@@ -6,7 +6,7 @@ import dahu.model.input.dsl._
object Simple extends Family("simple") {
var counter = 0
def variable() =
Input[Int]({ counter += 1; "v" + counter.toString }).subjectTo(x => x >= 0 && x <= 10)
Input[Int]({ counter += 1; "v" + counter.toString }) //.subjectTo(x => x >= 0 && x <= 10)
val v1 = variable()
val v2 = variable().subjectTo(_ > v1)
......
......@@ -17,8 +17,8 @@ import scala.util.{Failure, Success, Try}
import dahu.utils.debug._
case class Config(problemFile: File = null,
minInstances: Int = 0,
maxInstances: Int = 500,
minInstances: Int = 1,
maxInstances: Int = 6,
symBreak: Boolean = true,
useXorForSupport: Boolean = true,
numThreads: Int = 1,
......
......@@ -21,18 +21,8 @@ class MetaSolver[K <: SubInt](val ast: AST.Aux[_, K], val builder: PartialSolver
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) => {
val k2: Option[sat.ID] = sat.subset.to(k)
val k3: Option[sat.VID] = k2.flatMap(sat.asVariableID)
k3.flatMap(i => f(i))
}
val total: ast.Assignment = (x: ast.VID) =>
partial(x) match {
case Some(v) => v
case None =>
defaultDomain(x).head // TODO: use head option or fail early if an input has an empty domain
}
assignment(x).getOrElse(defaultDomain(x).head) // TODO: use head option or fail early if an input has an empty domain
Some(total)
case None => None
}
......
package dahu.solvers
import dahu.constraints.interval.Interval
import dahu.model.ir.TotalSubAST
import dahu.model.ir.{Total, TotalSubAST}
import dahu.model.problem.SatisfactionProblemFAST.RootedLazyTree
import dahu.model.types.Value
import dahu.solvers.problem.IntCSP
abstract class PartialSolver[AST <: TotalSubAST[_]](final val ast: AST) {
abstract class PartialSolver[X](final val ast: RootedLazyTree[X, Total, cats.Id]) {
type K <: ast.ID
type K <: X
def nextSatisfyingAssignment(deadlineMs: Long = -1): Option[ast.PartialAssignment]
def nextSatisfyingAssignment(deadlineMs: Long = -1): Option[X => Option[Value]]
}
object PartialSolver {
trait Builder {
def apply(ast: TotalSubAST[_]): PartialSolver[ast.type]
def apply[X](ast: RootedLazyTree[X, Total, cats.Id]): PartialSolver[X]
}
}
package dahu.solvers.constraints
import dahu.constraints.interval.Interval
import dahu.model.ir.TotalSubAST
import dahu.model.ir.{Total, TotalSubAST}
import dahu.model.problem.IntBoolSatisfactionProblem
import dahu.model.types.TagIsoInt
import dahu.model.problem.SatisfactionProblemFAST.RootedLazyTree
import dahu.model.types.{TagIsoInt, Value}
import dahu.solvers.PartialSolver
import dahu.solvers.problem.IntCSP
import dahu.utils.errors._
class CSPPartialSolver[AST <: TotalSubAST[_]](_ast: AST) extends PartialSolver[AST](_ast) {
class CSPPartialSolver[X](_ast: RootedLazyTree[X, Total, cats.Id]) extends PartialSolver[X](_ast) {
val intBoolPb = new IntBoolSatisfactionProblem[ast.type](ast)
val intBoolPb = new IntBoolSatisfactionProblem[X](ast)
private val intPB = IntCSP.intProblem(intBoolPb)
private val csp = intPB.getSolver
private val intPB = ??? //IntCSP.intProblem(intBoolPb)
private val csp = ??? // intPB.getSolver
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) => {
ass
.get(k)
.map(v =>
ast.tree(k).typ match {
case t: TagIsoInt[_] => t.toValue(v)
case _ => unexpected
})
}
Some(partial)
case None => None
}
override def nextSatisfyingAssignment(deadlineMs: Long = -1): Option[X => Option[Value]] = {
???
// 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) => {
// ass
// .get(k)
// .map(v =>
// ast.tree(k).typ match {
// case t: TagIsoInt[_] => t.toValue(v)
// case _ => unexpected
// })
// }
// Some(partial)
// case None => None
// }
}
}
object CSPPartialSolver {
object builder extends PartialSolver.Builder {
override def apply(ast: TotalSubAST[_]): CSPPartialSolver[ast.type] =
override def apply[X](ast: RootedLazyTree[X, Total, cats.Id]): CSPPartialSolver[X] =
new CSPPartialSolver(ast)
}
}
......@@ -8,6 +8,7 @@ import dahu.maps.{ArrayMap, IMapBuilder, SubInt, SubSubInt}
import dahu.model.functions.Fun
import dahu.model.ir._
import dahu.model.problem.IntBoolSatisfactionProblem
import dahu.model.problem.SatisfactionProblemFAST.RootedLazyTree
import dahu.utils.errors._
object IntProblem {
......@@ -40,7 +41,7 @@ object IntCSP {
def domainOfType(typ: TagIsoInt[_]): IntervalDomain = IntervalDomain(typ.min, typ.max)
def translate[T <: SubInt](id: T, coalgebra: T => Total[T]): Option[IntProblem.Expr] = {
def translate[T <: SubInt](e: Total[T]): Option[IntProblem.Expr] = {
def asIntFunction(f: Fun[_]): Option[Func] = {
IntCompatibleFunc
.compat(f)
......@@ -51,7 +52,7 @@ object IntCSP {
.map(i2iFunc => Func(i2iFunc, Propagator.forward(f), Propagator.backward(f)))
}
coalgebra(id) match {
e match {
case InputF(_, typ: TagIsoInt[_]) =>
Some(Expr(domainOfType(typ), None, typ))
case CstF(value, typ: TagIsoInt[_]) =>
......@@ -60,39 +61,46 @@ object IntCSP {
val expr: Option[Comp] = asIntFunction(f).map(fi => Comp(fi, args.toArray))
Some(Expr(domainOfType(typ), expr, typ))
case _ =>
unexpected(s"${coalgebra(id)} is not supported.")
}
}
def intProblem(ast: IntBoolSatisfactionProblem[_]): IntCSP[IntCSP.Key[ast.K]] = {
type K = IntCSP.Key[ast.K]
val factory = new IMapBuilder[Expr]
ast.algebra.domain
.toIterable()
.map(i => IntCSP.translate(i, ast.algebra.asFunction).map((i, _)))
.foreach {
case Some((i, expr)) =>
factory += (i, expr)
case _ => // not representable or not in candidate set, ignore
}
val conjunction = Set(ast.root.asInstanceOf[K])
new IntCSP[K] {
private val pb: ArrayMap.Aux[K, Expr] =
factory.toImmutableArray.castKey[K]
override def toSatisfy: Set[K] = conjunction
override def dom: K => IntDomain = pb(_).domain
override def exprs: K => Option[Comp] = pb(_).comp
override def vars: Array[K] = pb.domain.toArray
override def getSolver: CSP[K] =
new CSP(pb, toSatisfy)
unexpected(s"$e is not supported.")
}
}
// def intProblem[X](ast: RootedLazyTree[X, Total]): IntCSP[X] = {
//// type K = IntCSP.Key[ast.ID]
//
// val factory = new IMapBuilder[Expr]
//
//// val nodes = ast.nodes
//// .map { case (a, fa) => IntCSP.translate(fa).map((a, _)) }
//// .foreach {
//// case Some((i, expr)) => factory += (i, expr)
//// case _ => // not representable ??? // TODO: doule check that we don't want to raise an error.
//// }
//
//// ast.algebra.domain
//// .toIterable()
//// .map(i => IntCSP.translate(i, ast.algebra.asFunction).map((i, _)))
//// .foreach {
//// case Some((i, expr)) =>
//// factory += (i, expr)
//// case _ => // not representable or not in candidate set, ignore
//// }
////
//// val conjunction = Set(ast.root.asInstanceOf[K])
//// new IntCSP[K] {
//// private val pb: ArrayMap.Aux[K, Expr] =
//// factory.toImmutableArray.castKey[K]
////
//// override def toSatisfy: Set[K] = conjunction
////
//// override def dom: K => IntDomain = pb(_).domain
////
//// override def exprs: K => Option[Comp] = pb(_).comp
////
//// override def vars: Array[K] = pb.domain.toArray
////
//// override def getSolver: CSP[K] =
//// new CSP(pb, toSatisfy)
//// }
// ???
// }
}
......@@ -29,4 +29,13 @@ package object maps {
def untagged[T <: SubInt, F[_]](v: F[T]): F[Int] = v.asInstanceOf[F[Int]]
private def tagged[T <: SubInt, F[_]](v: F[Int]): F[T] = v.asInstanceOf[F[T]]
class Counter {
type ID = Int with Wrapped[this.type]
private var nextValue: Int = 0
def next(): ID = { nextValue += 1; nextValue.asInstanceOf[ID] }
}
object Counter {
type Aux[ID0] = Counter { type ID = ID0 }
}
}
......@@ -38,14 +38,14 @@ object Compiler {
object Ints {
def unapply(args: Seq[Expr]): Option[List[IntExpr]] =
if(args.forall(_.isInstanceOf[IntExpr]))
Some(args.asInstanceOf[List[IntExpr]])
Some(args.toList.asInstanceOf[List[IntExpr]])
else
None
}
object Bools {
def unapply(args: Seq[Expr]): Option[List[BoolExpr]] =
if(args.forall(_.isInstanceOf[BoolExpr]))
Some(args.asInstanceOf[List[BoolExpr]])
Some(args.toList.asInstanceOf[List[BoolExpr]])
else
None
}
......
package dahu.z3
import cats.Functor
import com.microsoft.z3._
import dahu.maps.SubSubInt
import dahu.model.ir._
import dahu.model.problem.IntBoolSatisfactionProblem
import dahu.model.problem.SatisfactionProblemFAST.{ILazyTree, RootedLazyTree, TreeNode}
import dahu.model.types._
import dahu.solvers.PartialSolver
import dahu.utils.errors._
import dahu.recursion.Recursion.hylo
import scala.util.{Failure, Success}
import scala.collection.mutable
import scala.util.{Failure, Success, Try}
import scala.util.control.NonFatal
class Z3PartialSolver[AST <: TotalSubAST[_]](_ast: AST) extends PartialSolver[AST](_ast) {
class TreeBuilder[X, F[_], G, Opt[_]](t: ILazyTree[X, F, Opt], f: F[G] => G)(implicit F: Functor[F], T: TreeNode[F]) {
private val memo = mutable.HashMap[t.ID, G]()
def build(k: t.ID) : G = {
val stack = mutable.Stack[t.ID]()
def push(i: t.ID) : Unit = {
if(!memo.contains(i))
stack.push(i)
}
push(k)
while(stack.nonEmpty) {
val a = stack.pop()
val fa = t.getInt(a)
if(T.children(fa).forall(memo.contains)) {
val g = f(F.map(fa)(memo))
memo += ((a, g))
} else {
push(a)
T.children(fa).foreach(push)
}
}
memo(k)
}
}
class Z3PartialSolver[X](_ast: RootedLazyTree[X, Total, cats.Id]) extends PartialSolver[X](_ast) {
trait Tag
val intBoolPb = new IntBoolSatisfactionProblem[ast.type](ast)
val intBoolPb = new IntBoolSatisfactionProblem[X](ast)
val root = intBoolPb.tree.root
val tree = intBoolPb.tree.tree
private val ctx = new Context()
type OptTotal[T] = Option[Total[T]]
val treeBuilder = new TreeBuilder(tree, Compiler.partialAlgebra(ctx))
// Total
def asExpr(id: ast.ID): Option[com.microsoft.z3.Expr] = {
intBoolPb.algebra.get(id) match {
case Some(e) =>
hylo(intBoolPb.algebra.asFunction, algebra)(id.asInstanceOf[intBoolPb.K]).toOption
case None => None
}
def asExpr(id: X): Option[com.microsoft.z3.Expr] = {
tree.getInternalID(id).map(internalID => treeBuilder.build(internalID))
}
def eval(id: ast.ID, model: com.microsoft.z3.Model): Option[Value] =
def eval(id: X, model: com.microsoft.z3.Model): Option[Value] = {
asExpr(id) match {
case Some(e) =>
model.eval(e, false) match {
case i: IntNum =>
ast.tree(id).typ match {
ast.tree.getExt(id).typ match {
case t: TagIsoInt[_] => Some(t.toValue(i.getInt))
case _ => unexpected
case _ => unexpected
}
case b: BoolExpr =>
b.getBoolValue match {
case enumerations.Z3_lbool.Z3_L_FALSE => Some(Value(false))
case enumerations.Z3_lbool.Z3_L_TRUE => Some(Value(true))
case enumerations.Z3_lbool.Z3_L_TRUE => Some(Value(true))
case enumerations.Z3_lbool.Z3_L_UNDEF => None
case _ => unexpected
case _ => unexpected
}
}
case None => None
}
}
override type K = SubSubInt[ast.ID, Tag]
private val ctx = new Context()
private val algebra = Compiler.algebra(ctx)
val compiled = hylo(intBoolPb.algebra.asFunction, algebra)(intBoolPb.root)
val compiled = Try(treeBuilder.build(root)) //hylo(intBoolPb.algebra.asFunction, algebra)(intBoolPb.root)
private val satProblem = compiled match {
case Success(x: BoolExpr) => x
case Failure(NonFatal(e)) => unexpected("Failure while parsing Z3. Cause: ", e)
......@@ -67,7 +93,7 @@ class Z3PartialSolver[AST <: TotalSubAST[_]](_ast: AST) extends PartialSolver[AS
solver.add(satProblem)
var model: Model = null
override def nextSatisfyingAssignment(deadline: Long = -1): Option[ast.PartialAssignment] = {
override def nextSatisfyingAssignment(deadline: Long = -1): Option[X => Option[Value]] = {
assert(model == null, "Z3 only support extraction of a single solution")
val timeout =
if(deadline < 0)
......@@ -90,10 +116,7 @@ class Z3PartialSolver[AST <: TotalSubAST[_]](_ast: AST) extends PartialSolver[AS
solver.check() match {
case Status.SATISFIABLE =>
model = solver.getModel
val partial = (id: ast.VID) => {
eval(id, model)
}
Some(partial)
Some(id => eval(id, model))
case _ =>
None
}
......@@ -104,7 +127,7 @@ class Z3PartialSolver[AST <: TotalSubAST[_]](_ast: AST) extends PartialSolver[AS
object Z3PartialSolver {
object builder extends PartialSolver.Builder {
override def apply(ast: TotalSubAST[_]): Z3PartialSolver[ast.type] =
new Z3PartialSolver[ast.type](ast)
override def apply[X](ast: RootedLazyTree[X, Total, cats.Id]): Z3PartialSolver[X] =
new Z3PartialSolver[X](ast)
}
}
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