162p7

package miniprologfd.solver

// note the renaming that is being done by these imports
import scala.collection.mutable.{ Map => MMap }
import miniprologfd.interpreter.{ Value, NumValue, SymPlaceholder => Variable }
import miniprologfd.syntax.lowlevel.{
  SymbolicROP => ROP,
  SymEQ => EQ,
  SymNE => NE,
  SymLT => LT,
  SymLE => LE,
  SymGT => GT,
  SymGE => GE
}


// an interval of integers from 0 to Intervals.maxValue, inclusive
case class Interval(low: Int, hi: Int) {
  assert(low >= 0 && hi >= low && hi <= Intervals.maxValue)
  override def toString = "[" + low + ".." + hi + "]"
}

// represents the possible values of a variable as a list of
// intervals. by construction this list contains non-overlapping
// intervals in ascending order.
case class Intervals(ns: List[Interval]) {
  // are there no possible values?
  def isEmpty: Boolean = ns.isEmpty

  // apply function f to every possible value
  def foreach(f: Int => Unit): Unit = {
    var a = 0
    for (interval <- ns) {
      // for loop execution with a range
      for (a <- interval.low to interval.hi) {
        f(a)
      }
    }
  }

  // compute the intersection of these possible values and another set
  // of possible values
  def intersect(i: Intervals): Intervals = {
    val intersectionList = List[Interval]()

    for (i_curr <- ns) {
      for (i_new <- i.ns) {
        intersectIntervalPair(i_curr, i_new) match {
          case Some(intersected_interval_pair) => intersectionList :+ intersected_interval_pair
          case None => intersectionList
        }
      }
    }
    Intervals(intersectionList)
  }

  def intersectIntervalPair(i1: Interval, i2: Interval): Option[Interval] = {
    // overlapping case
    ((i2.low <= i1.hi) && (i1.low <= i2.hi)) match {
      // overlap is true
      case true => (i1.low <= i2.low) match {
        case true => Some(Interval(i1.low, i2.hi))
        case false => Some(Interval(i2.low, i1.hi))
      }
      case false => None
    }
  }

  // is there only a single possible value?
  def singleton: Boolean = {
    if ((ns.length == 1) && (ns.head.low == ns.head.hi)) true else false
  }

  // retrieve the single possible value (only valid if there is only a
  // single possible value to retrieve)
  def getSingleton: Int = {
    assert(singleton, "Not a singleton error")
    ns.head.low
  }

  // remove a possible value from the current set of possible values
  def -(n: Int): Intervals = intersect(Intervals.getIntervals(NE, n))

  // return the lowest currently possible value
  def lowest: Int = if (!isEmpty) ns.head.low else -1

  // return the highest currently possible value
  def highest: Int = if (!isEmpty) ns.reverse.head.hi else -1

  // returns all currently possible values < n
  def LT(n: Int): Intervals = intersect(Intervals.getIntervals(miniprologfd.syntax.lowlevel.SymLT, n))

  // returns all currently possible values ≤ n
  def LE(n: Int): Intervals = intersect(Intervals.getIntervals(miniprologfd.syntax.lowlevel.SymLE, n))

  // returns all currently possible values > n
  def GT(n: Int): Intervals = intersect(Intervals.getIntervals(miniprologfd.syntax.lowlevel.SymGT, n))

  // returns all currently possible values ≥ n
  def GE(n: Int): Intervals = intersect(Intervals.getIntervals(miniprologfd.syntax.lowlevel.SymGE, n))

  override def toString =
    ns.mkString(", ")
}

// companion object with useful functions
object Intervals {
  // maximum possible value
  val maxValue = 500

  // default Intervals value, i.e., the default set of possible values
  // for any variable
  val default = Intervals(0, maxValue)

  // create an Intervals with a single possible value
  def apply(n: Int): Intervals = Intervals(n)

  // create and Intervals with no possible values
  def apply(): Intervals = Intervals(List[Interval]())

  // create an Intervals with a set of contiguous possible values in
  // the range low to hi
  def apply(low: Int, hi: Int): Intervals = Intervals(low, hi)

  // Create an Intervals containing all possible values that have the
  // given relation op with the given integer n.  `max` below refers
  // to the `maxValue` constant defined above.
  //
  // examples: getIntervals(<,  10) = [[0..9]]
  //           getIntervals(=,  10) = [[10..10]]
  //           getIntervals(≠,  10) = [[0..9], [11..max]]
  //           getIntervals(<,   0) = []          // less than minimum
  //           getIntervals(>, max) = []          // greater than maximum
  //           getIntervals(=,  -1) = []          // out of range
  //           getIntervals(>,  -5) = [[0..max]]  // the whole valid range
  def getIntervals(op: ROP, n: Int): Intervals = op match {
    case EQ => n match {
      case v if (v == Intervals.maxValue) => Intervals()
      case v if (v < 0) => default
      case _ => Intervals(n)
    }
    case NE => n match {
      case v if (v == 0) => Intervals(1, maxValue)
      case v if (v < 0 || v > Intervals.maxValue) => default
      case _ => Intervals(List(Interval(0, n - 1), Interval(n + 1, maxValue)))
    }
    case LT => n match {
      case v if (v <= 0) => Intervals()
      case v if (v > Intervals.maxValue) => default
      case _ => Intervals(0, n - 1)
    }
    case LE => n match {
      case v if (v < 0) => Intervals()
      case v if (v > maxValue) => default
      case _ => Intervals(0, n)
    }
    case GT => n match {
      case v if (v >= Intervals.maxValue) => Intervals()
      case v if (n < 0) => default
      case _ => Intervals(n + 1, Intervals.maxValue)
    }
    case GE => n match {
      case v if (v > Intervals.maxValue) => Intervals()
      case v if (n < 0) => default
      case _ => Intervals(n, Intervals.maxValue)
    }
  }
}

// constraints between variables
case class Constraint(op: ROP, x1: Variable, x2: Variable)

// a map from variables to their possible values
case class Values(vs: Map[Variable, Intervals] = Map()) {
  // retrieve the possible values for the given variable; if the
  // variable isn't in vs then return the default set of possible
  // values
  def apply(x: Variable): Intervals = vs.getOrElse(x,Intervals.default)

  // return a mutable copy of this map
  def mutableCopy: MValues = collection.mutable.Map() ++ vs


// a mutable map from variables to their possible values
case class MValues(vs: MMap[Variable, Intervals] = MMap()) {
  // retrieve the possible values for the given variable; if the
  // variable isn't in vs then return the default set of possible
  // values
  def apply(x: Variable): Intervals = vs.getOrElse(x,Intervals.default)

  // update the possible values of the given variable
  def update(x: Variable, i: Intervals) {
    vs += (x -> i)
  }

  // clear the map
  def clear() {
    vs.clear
  }

  // is the map empty?
  def isEmpty: Boolean = vs.isEmpty

  // return an immutable copy of this map
  def immutableCopy: Values = collection.immutable.Map() ++ vs
}

// a map from variables to the constraints mentioning that variable
case class Constraints(cs: Map[Variable, Set[Constraint]] = Map()) {
  // retrieve the constraint set for the given variable; if the
  // variable isn't in cs then return the empty set
  def apply(x: Variable): Set[Constraint] = cs.getOrElse(x,Set[Constraint]())

  // add constraint c to the constraints sets for variables x1 and x2
  // mentioned in constraint c
  // Constraint(op: ROP, x1: Variable, x2: Variable)
  def +(c: Constraint): Constraints = {
    val newset1 = cs(c.x1) + c
    val newset2 = cs(c.x2) + c
    cs + (c.x1 -> newset1, c.x2 -> newset2)
}

// this is the actual solver, including an API used by the
// miniprolog-fd interpreter to insert constraints and query for
// satisfiable values.
case class ConstraintStore(
  // map from variable to intervals (possible values for that variable)
  values: Values = Values(),
  // a map from variables to the constraints mentioning that variable
  constraints: Constraints = Constraints()) {

  ////////// API FOR INTERPRETER //////////

  // insert a new constraint into the constraint store. the return
  // value is None if the new constraint is inconsistent with existing
  // constraints, otherwise it is Some(the updated constraint store).
  def insert(op: ROP, v1: Value, v2: Value): Option[ConstraintStore] = (v1,v2) match {
    // have to switch them
    case (n@NumValue, v@Variable) =>
    {

      // add new constraint
      val newConstraints = constraints + Constraint(op, x1, x2)
      val possibleValues =  Intervals.getIntervals(reverseOp(op), n)
      var vmc = values.mutableCopy
      propagate(vmc, v, possibleValues)
      if(!vmc.isEmpty) Some(ConstraintStore(vmc.immutableCopy,newConstraints)) else None
    }
    // regular case
    case (n@Variable, v@NumValue) => {
      // add new constraint
      val newConstraints = constraints + Constraint(op, x1, x2)
      val possibleValues =  Intervals.getIntervals(op, n)
      var vmc = values.mutableCopy
      propagate(vmc, v, possibleValues)
      if(!vmc.isEmpty) Some(ConstraintStore(vmc.immutableCopy,newConstraints)) else None
    }

    // if two variables
    case (v1@Variable, v2@Variable) => values.vs(v1).singleton && values.vs(v2).singleton match {
      // both variables singletons
      case true => compare(values.vs(v1).getSingleton,op,values.vs(v2).getSingleton) match {
        // constraint holds
        case true => Some(ConstraintStore(values,constraints))
        // constraint does not hold
        case false => None
      }
      // variables not both singletons
      case false => {
        // add new constraint to constraints
        val newConstraints = constraints + Constraint(op, x1, x2)
        // solve(values, [x1,x2]) => gives you Option[Values]
        solve(values,List(v1,v2)) match {
          case Some(_) => ConstraintStore(values,constraints) //satisfiable
          case None => None
        }
      }
    }

  }


  // Compares two integers with respect to the given operator.
  def compare(n1: Int, op: ROP, n2: Int): Boolean = op match {
    case GT => if(n1 > n2) true else false
    case LT => if(n1 < n2) true else false
    case LE => if (n1 <= n2) true else false
    case GE => if (n1 >= n2) true else false
    case EQ => if(n1 == n2) true else false
    case NE => if(n1 != n2) true else false
  }

  // query the constraint store for single satisfying values for the given
  // list of variables
  def SAT(xs: List[Variable]): List[NumValue] = solve(values,xs) match {
    // if there is a singleton solution for each variable given all of the variable constraints
    case Some(vals) => {
      // get all the singleton values for each variable, put them in the same order as the original list by folding right
      xs.foldright(List[NumValue]())((value:Variable, accumulator:List[NumValue])=> NumValue(vals(value))::accumulator)
    }
    // no satisfiable solution
    case None => List[NumValue]()
  }

  ////////// INTERNAL METHODS //////////

  // given the current possible values for all the variables, compute
  // satisfying values for the given list of variables

  def solve(currValues: Values, xs: List[Variable]): Option[Values] = {
    val x = xs.head
    val tl = xs.tail
    // for each possible value of x
    for (v <- currValues(x)) {
      // strip out all the values of x that don't work,
      // and propagate these changes for all the other
      // variables that depend on x
      var mutableCV = currValues.mutableCopy
      propagate(mutableCV,x,v)
      // if there was a satisfiable solution for x
      if(!mutableCV.isEmpty){
        var currValuesN = mutableCV.immutableCopy
        // repeat recursively if there are more variables
        if(!tl.isEmpty){
          solve(currValuesN,tl) match {
            case None => None
            case Some(cv) => return Some(cv)
          }
        }
        else return Some(currValuesN)
      }
    }
  }

  // constraint propagation: restrict the possible values of x to only
  // include values in ranges. if that makes x unsatisfiable then
  // return; if that changes the possible values of x then recursively
  // propagate those changes to the other variables.
  //
  // IMPORTANT NOTE: because mutableCV returns a default set of
  // possible values for any variable not contained in the mapping, we
  // can't just iterate through all the constraints as done in the
  // pseudocode (it would incorrectly propagate default values if
  // mutableCV is made empty in some recursive call to
  // propagate). instead, we need to explicitly check after each
  // recursive call to propagate whether mutableCV is empty, and if so
  // then explicitly return from the function.
  def propagate(mutableCV: MValues, x: Variable, ranges: Intervals) {
    ??? // FILL ME IN
  }

  // narrow the current possible values of x1 (given as rangesX1)
  // according to the constraint c, which is between x1 and some
  // variable x2 (where rangesX2 gives the possible values of x2)
  def narrow(x1: Variable, rangesX1: Intervals, c: Constraint, rangesX2: Intervals): Intervals =
    ??? // FILL ME IN

  // reverse the meaning of a relational operator (e.g., < becomes >
  // and ≤ becomes ≥)
  def reverseOp(op: ROP): ROP =
    op match {
      case EQ => EQ
      case NE => NE
      case LT => GT
      case LE => GE
      case GT => LT
      case GE => LE
    }
}