Clone wiki

OscaR / ExtendCBLS

Writing invariants

Invariants are meant to incrementally maintain the value of some output variable based on some input variables.

A simple documented invariant is the DenseCluster Invariant. It maintains an array "cluster" of IntSetVar based on an array "values" of IntVar: cluster(j) = {i in index of values | values(i) == j}

/**
 *Maintains a cluster of the indexes of array: 
 * cluster(j) = {i in index of values | values[i] == j}
 * This is considered as a dense cluster because Cluster is an array 
 * and must cover all the possibles values of the values in the array ''values''
 * */
case class DenseCluster(var values:Array[IntVar], clusters:Array[IntSetVar]) 
           extends Invariant {

  //We register the static and dynamic dependencies.
  //Dynamic dependencies are the ones considered for the notifications.
  //Static dependencies are the ones considered for ordering the propagations
  //the "v" is passed back to the callback method to notify a change of values(v) 
  for (v <- values.indices) registerStaticAndDynamicDependency(values(v),v)

  //This must be called once all static dependencies are registered
  //It must be called before the output dependencies are notified
  finishInitialization()

  //We then define the variable that we control
  //By the way, an initial value is set to each of them (SortedSet.empty)
  for(c <- clusters){
    //A variable can only have a single controlling invariant
    c.setDefiningInvariant(this) 
    c.setValue(SortedSet.empty)
  }

  //We then complete the initialization 
  //by setting the output variables to the value they should have
  for(v <- values.indices){
    clusters(values(v).getValue()).insertValue(v)
  }

  //This method is called by each IntVar that is registered 
  //to the dynamic dependency graph.
  //We update the output variabls incrementally based on this update.
  //Notice that besise the IntVar, we also get an Int, 
  //it is the Int passed when registering to the dynamic dependency of variable v. 
  override def notifyIntChanged(v:IntVar,index:Int,OldVal:Int,NewVal:Int){
    assert(values(index) == v)
    clusters(OldVal).deleteValue(index)
    clusters(NewVal).insertValue(index)
  }
}

The code can be found here: https://bitbucket.org/oscarlib/oscar/src/859051da9098/src/main/scala/oscar/cbls/invariants/lib/logic/Cluster.scala

Most invariants actually control a single output variable. To make it more systematic, OScar.cbls proposes the concepts of IntInvariant and IntSetInvariant. These are base classes to extend for such invariants. They offer some additional services, suc has the instantiation of the output variable of the invariant.

A simple example of IntInvariant is the IntVar2IntVarFun Invariant. It is a generic invariant that takes a non-incremental function Int -> Int as a parameter, and applies it whenever the input variables of the invariant have changed.

/** This is a helper to define an invariant from an Int -> Int function.
 * Ths invariant is not incremental, so this should only be used for very simple functions.
 * it maintains output = fun(a)
 * fun is supposed not to listen nor write to any variable in the model
 * @param a the parameter of the function
 * @param fun the function to maintain, 
 * @param MyMin the min value of the output
 * @param MyMax the max value of the output
 */
case class IntVar2IntVarFun(a:IntVar, 
                            fun:Int => Int, 
                            override val MyMin:Int = Int.MinValue, 
                            override val MyMax:Int=Int.MaxValue) 
          extends IntInvariant {

  var output:IntVar=null

  registerStaticAndDynamicDependency(a)
  finishInitialization()

  //This method is called by the IntVar when the method <== is applied
  //Example: MyVar <== my_IntInvariant
  override def setOutputVar(v:IntVar){
    output = v
    output.setDefiningInvariant(this)
    output := fun(a)
  }

  override def notifyIntChanged(v:IntVar,OldVal:Int,NewVal:Int){
    assert(v == a)
    output := fun(NewVal)
  }

  override def checkInternals(){
    assert(output.getValue() == fun(a.getValue()))
  }
}

The code can be found here: https://bitbucket.org/oscarlib/oscar/src/859051da9098/src/main/scala/oscar/cbls/invariants/lib/logic/Helpers.scala

Consider also Set-related invariants, implementing the IntSetInvariant class. A simple example is the Union invariant, maintining the union of two IntSetVar.

/** left UNION right
 * @param left is an intvarset
 * @param right is an intvarset
 * */
case class Union(left:IntSetVar, right:IntSetVar) extends IntSetInvariant {
  assert(left != right)
  var output:IntSetVar = null

  def MyMax = left.getMaxVal.max(right.getMaxVal)
  def MyMin = left.getMinVal.min(right.getMinVal)

  registerStaticAndDynamicDependency(left)
  registerStaticAndDynamicDependency(right)
  finishInitialization()

  override def setOutputVar(v:IntSetVar){
      output = v
      output.setDefiningInvariant(this)
      output := left.union(right.getValue())
  }


  override def notifyInsertOn(v:IntSetVar,value:Int){
    assert(left == v ||right == v)
    output.insertValue(value)
  }

  override def notifyDeleteOn(v:IntSetVar,value:Int){
    assert(left == v ||right == v)
    if(v == left){
      if (!right.contains(value)){
        output.deleteValue(value)
      }
    }else if(v == right){
      if(!left.contains(value)){
        output.deleteValue(value)
      }
    }else{
      assert(false)
    }
  }
}

The complete code can be found here: https://bitbucket.org/oscarlib/oscar/src/859051da9098/src/main/scala/oscar/cbls/invariants/lib/set/BasicSetInvariants.scala

A more elaborated invariant is the SumElements. It takes an array "vars" of IntVar, and an IntSetVar "cond". It maintains the sum of the IntVar found in the array where the indexes belong to "cond". sum(i in cond) vars(i). This invariant is an IntInvariant. This invariant updates its dynamic dependencies to the variables in the array, based on the value found in cond. The updates to the dynamic dependency graph are made with the help of a system of keys. When an invariant registers to a variable in the dynamic graph, it gets a key, which is needed to unregister to this variable.

case class SumElements(var vars: Array[IntVar], cond: IntSetVar) extends IntInvariant {
  assert(vars.size > 0, "Invariant SumElements declared with zero vars to max")
  assert(cond != null, "cond cannot be null for SumElements")

  def MyMin = Int.MinValue
  def MyMax = Int.MaxValue
  var output: IntVar = null
  val keyForRemoval: Array[KeyForElementRemoval] = Array.fill(vars.indices.end) {null}
  registerStaticDependency(cond)
  registerDeterminingDependency(cond)
  for(v <- vars)registerStaticDependency(v)
  for(i <- cond.getValue()){
    keyForRemoval.update(i, registerDynamicDependency(vars(i),i))
  }
  finishInitialization()

  override def setOutputVar(v: IntVar) {
    output = v
    output.setDefiningInvariant(this)
    output := cond.getValue().foldLeft(0)((acc, i) => acc + vars(i))
  }

  override def notifyIntChanged(v: IntVar, index:Int, OldVal: Int, NewVal: Int) {
    //it is always a listened one, but we could check this here
    assert(vars(index)==v)
    assert(keyForRemoval(index)!=null)
    output := output.getValue() - OldVal + NewVal
  }

  override def notifyInsertOn(v: IntSetVar, value: Int) {
    assert(v == cond)
    assert(keyForRemoval(value) == null)
    keyForRemoval.update(value, registerDynamicDependency(vars(value),value))
    output := output.getValue() + vars(value).getValue()
  }

  override def notifyDeleteOn(v: IntSetVar, value: Int) {
    assert(v == cond)
    assert(keyForRemoval(value) != null)
    unregisterDynamicDependency(keyForRemoval(value))
    keyForRemoval.update(value, null)
    output := output.getValue() - vars(value).getValue()
  }
} 

https://bitbucket.org/oscarlib/oscar/src/859051da9098/src/main/scala/oscar/cbls/invariants/lib/numeric/Advanced.scala

Finally, Oscar.cbls proposes a unique mechanism called bulking, that enables the efficient declaration of dependencies of a set of invariant to the same array of variables. It is best illustrated in the IntElement invariant.

/** inputarray[index]
 * @param inputarray is an array of IntVar
 * @param index is the index accessing the array*/

case class IntElement(index:IntVar, var inputarray:Array[IntVar]) 
                       extends IntInvariant with Bulked[IntVar,((Int,Int))]{
  var output:IntVar = null
  var KeyToCurrentVar:KeyForElementRemoval = null

  registerStaticDependency(index)
  registerDeterminingDependency(index)
  if(inputarray != null){
    registerStaticDependencyAll(inputarray)
    KeyToCurrentVar = registerDynamicDependency(inputarray(index))
    MyMax = inputarray.foldLeft(Int.MinValue)
                  ((acc,intvar) => if (acc < intvar.MaxVal) intvar.MaxVal else acc)

    MyMin = inputarray.foldLeft(Int.MaxValue)
                   ((acc,intvar) => if (acc > intvar.MinVal) intvar.MinVal else acc)

  }
  finishInitialization()

  def BulkLoad(bulkedVar: Array[IntVar],bcr:(Int,Int)){
    inputarray = bulkedVar
    KeyToCurrentVar = registerDynamicDependency(inputarray(index))
    MyMin = bcr._1
    MyMax = bcr._2
  }

  override def toString:String= {
    inputarray.toList.toString+"[" + index.toString + "]"
  }

  var MyMax = 0
  var MyMin = 0

  override def performBulkComputation(bulkedVar: Array[IntVar]):(Int,Int) = {
    val MyMax = bulkedVar.foldLeft(Int.MinValue)
                         ((acc,intvar) => if (acc < intvar.MaxVal) intvar.MaxVal else acc)
    val MyMin = bulkedVar.foldLeft(Int.MaxValue)
                         ((acc,intvar) => if (acc > intvar.MinVal) intvar.MinVal else acc)
    (MyMin,MyMax)
  }

  override def setOutputVar(v:IntVar){
    output = v
    output.setDefiningInvariant(this)
    output := inputarray.apply(index)
  }

  override def notifyIntChanged(v:IntVar,OldVal:Int,NewVal:Int){
    if (v == index){
      output := inputarray(NewVal)
      //update the dynamic dependency graph
      unregisterDynamicDependency(KeyToCurrentVar)
      KeyToCurrentVar = registerDynamicDependency(inputarray(NewVal))
    }else{
      assert(v == inputarray.apply(index),"access notified for non listened var")
      output := NewVal
    }
  }

  override def checkInternals(){
    assert(output.getValue() == inputarray(index.getValue()).getValue(), this)
  }
}

https://bitbucket.org/oscarlib/oscar/src/859051da9098/src/main/scala/oscar/cbls/invariants/lib/logic/Accesses.scala

The use of the bulking mechanism is well illustrated in the BinPacking Constraint The illustrating snippet is as follows:

val itemviolations:Array[IntVar] = {
   val tmp = items.map(itemval => IntElement(itemval,null))
   //notice that the array given to IntElement is null
   BulkLoad(tmp,binviolations)
   tmp.map(intelement => intelement.toIntVar)
} 

The complete code is here: https://bitbucket.org/oscarlib/oscar/src/859051da9098/src/main/scala/oscar/cbls/constraints/lib/global/MultiKnapsack.scala

Updated