Encodings for adding incremental constraints

Encodings

src/coomsuite/encodings/multi/inc-constraint.lp

Encoding

constraint(cons,type).

incremental boolean constraints

violated(cons,bound) :- constraint(cons,type), defined(F,bound), not satisfied(F,bound), cons = (C,F), type = "boolean".

violation is only checked at the current max_bound

:- constraint(cons,type), type = "boolean", max_bound(bound),
   violated(cons,bound).

incremental table constraints - for table constraints the table IDs are associated with a specific bound

violated((cons,ID),bound) :- constraint(cons,type), table_bound(cons,ID,bound), defined(cons,ID), not satisfied(cons,ID), type = "table".

• for bound 0 this association does not exist

violated((cons,ID),0) :- constraint(cons,type), defined(cons,ID), not satisfied(cons,ID), type = "table", bound = 0.

violation of table constraints is checked for all active bounds

:- constraint(cons,type), type = "table", active(bound),
   violated((cons,ID),bound), table_bound(cons,ID,bound).

Encodings for incremental boolean constraints

Encodings

src/coomsuite/encodings/multi/inc-function.lp

Encoding

program part for initializing new incremental functions

function(f,agg,p).
defined(f,bound) :- value(f,_,bound).

when an incremental function is initialized the corresponding set may have several elements thus it is necessary to actually use the corresponding aggregates at bound 0 possible objects are not introduced with a bound parameter

value(f,V,bound) :- function(f,agg,p), agg = "count", V = #count{ X  : set(p,X),                 include(X)  }, bound = 0.
value(f,V,bound) :- function(f,agg,p), agg = "count", V = #count{ X  : set(p,X), bound(X,bound), include(X)  }, bound > 0.
value(f,V,bound) :- function(f,agg,p), agg = "sum",   V = #sum{ V',X : set(p,X),                 value(X,V') }, bound = 0.
value(f,V,bound) :- function(f,agg,p), agg = "sum",   V = #sum{ V',X : set(p,X), bound(X,bound), value(X,V') }, bound > 0.
value(f,V,bound) :- function(f,agg,p), agg = "min",   V = #min{ V',X : set(p,X),                 value(X,V') }, bound = 0.
value(f,V,bound) :- function(f,agg,p), agg = "min",   V = #min{ V',X : set(p,X), bound(X,bound), value(X,V') }, bound > 0.
value(f,V,bound) :- function(f,agg,p), agg = "max",   V = #max{ V',X : set(p,X),                 value(X,V') }, bound = 0.
value(f,V,bound) :- function(f,agg,p), agg = "max",   V = #max{ V',X : set(p,X), bound(X,bound), value(X,V') }, bound > 0.

program part for updating incremental functions

function(f,agg,p).
defined(f,bound) :- value(f,_,bound).

compute value step-wise

value(f,V+V',N+1) :- function(f,agg,p), agg = "count", bound = N+1, value(f,V,N), V' = #count{ X   : set(p,X), bound(X,bound), include(X)   }.
value(f,V+V',N+1) :- function(f,agg,p), agg = "sum",   bound = N+1, value(f,V,N), V' = #sum{ Val,X : set(p,X), bound(X,bound), value(X,Val) }.
value(f,V',N+1)   :- function(f,agg,p), agg = "min",   bound = N+1, value(f,V,N), V' = #min{ Val,X : set(p,X), bound(X,bound), value(X,Val) }, V' < V.
value(f,V ,N+1)   :- function(f,agg,p), agg = "min",   bound = N+1, value(f,V,N), V' = #min{ Val,X : set(p,X), bound(X,bound), value(X,Val) }, V' >= V.
value(f,V',N+1)   :- function(f,agg,p), agg = "max",   bound = N+1, value(f,V,N), V' = #max{ Val,X : set(p,X), bound(X,bound), value(X,Val) }, V' > V.
value(f,V ,N+1)   :- function(f,agg,p), agg = "max",   bound = N+1, value(f,V,N), V' = #max{ Val,X : set(p,X), bound(X,bound), value(X,Val) }, V' <= V.

Encodings

src/coomsuite/encodings/multi/inc-unary.lp

Encoding

unary(f,op,x).
defined(f,bound) :- unary(f,op,x), defined(x,bound).
defined(f,bound) :- unary(f,op,x), value(f,_,bound).
value(f, V,bound) :- unary(f,op,x), value(x,V,bound), op = "()".
value(f, V,bound) :- unary(f,op,x), value(x,V,bound), op = "+".
value(f, V,bound) :- unary(f,op,x), value(x,V,bound), op = "-".
satisfied(f,bound) :- unary(f,op,x), not satisfied(x,bound), op = "!".
satisfied(f,bound) :- unary(f,op,x),     satisfied(x,bound), op = "()".

Encodings

src/coomsuite/encodings/multi/inc-binary.lp

Encoding

for incremental binary expressions we have to distinguish whether both sub-expressions or only one are incremental as well (note that at least one of the sub-expressions needs to incremental) case 1: both sub-expressions are incremental

binary(f,xl,op,xr).
defined(f,bound) :- binary(f,xl,op,xr), defined(xl,bound), defined(xr,bound).
defined(f,bound) :- binary(f,xl,op,xr), value(f,_,bound).
value(f,VL+VR,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), value(xr,VR,bound), op = "+".
value(f,VL-VR,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), value(xr,VR,bound), op = "-".
value(f,VL*VR,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), value(xr,VR,bound), op = "*".
value(f, VL,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), not value(xr,_,bound), op = "+".
value(f, VR,bound) :- binary(f,xl,op,xr), value(xr,VR,bound), not value(xl,_,bound), op = "+".
value(f, VL,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), not value(xr,_,bound), op = "-".
value(f,-VR,bound) :- binary(f,xl,op,xr), value(xr,VR,bound), not value(xl,_,bound), op = "-".
satisfied(f,bound) :- binary(f,xl,op,xr), VL =  VR, value(xl,VL,bound), value(xr,VR,bound), op = "=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL != VR, value(xl,VL,bound), value(xr,VR,bound), op = "!=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL >  VR, value(xl,VL,bound), value(xr,VR,bound), op = ">".
satisfied(f,bound) :- binary(f,xl,op,xr), VL >= VR, value(xl,VL,bound), value(xr,VR,bound), op = ">=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL <  VR, value(xl,VL,bound), value(xr,VR,bound), op = "<".
satisfied(f,bound) :- binary(f,xl,op,xr), VL <= VR, value(xl,VL,bound), value(xr,VR,bound), op = "<=".
satisfied(f,bound) :- binary(f,xl,op,xr), 1 <= { satisfied(xl,bound); satisfied(xr,bound) }, op = "||".
satisfied(f,bound) :- binary(f,xl,op,xr), satisfied(xl,bound), satisfied(xr,bound), op = "&&".

case 2: for the case that only on sub-expression is incremental we have to distinguish whether this is the left or right one 2.a: only the left sub-expression is incremental

binary(f,xl,op,xr).
defined(f,bound) :- binary(f,xl,op,xr), defined(xl,bound), defined(xr).
defined(f,bound) :- binary(f,xl,op,xr), value(f,_,bound).
value(f,VL+VR,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), value(xr,VR), op = "+".
value(f,VL-VR,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), value(xr,VR), op = "-".
value(f,VL*VR,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), value(xr,VR), op = "*".
value(f, VL,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), not value(xr,_),       op = "+".
value(f, VR,bound) :- binary(f,xl,op,xr), value(xr,VR),       not value(xl,_,bound), op = "+".
value(f, VL,bound) :- binary(f,xl,op,xr), value(xl,VL,bound), not value(xr,_),       op = "-".
value(f,-VR,bound) :- binary(f,xl,op,xr), value(xr,VR),       not value(xl,_,bound), op = "-".
satisfied(f,bound) :- binary(f,xl,op,xr), VL =  VR, value(xl,VL,bound), value(xr,VR), op = "=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL != VR, value(xl,VL,bound), value(xr,VR), op = "!=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL >  VR, value(xl,VL,bound), value(xr,VR), op = ">".
satisfied(f,bound) :- binary(f,xl,op,xr), VL >= VR, value(xl,VL,bound), value(xr,VR), op = ">=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL <  VR, value(xl,VL,bound), value(xr,VR), op = "<".
satisfied(f,bound) :- binary(f,xl,op,xr), VL <= VR, value(xl,VL,bound), value(xr,VR), op = "<=".
satisfied(f,bound) :- binary(f,xl,op,xr), 1 <= { satisfied(xl,bound); satisfied(xr) }, op = "||".
satisfied(f,bound) :- binary(f,xl,op,xr), satisfied(xl,bound), satisfied(xr), op = "&&".

2.b: only the right sub-expression is incremental

binary(f,xl,op,xr).
defined(f,bound) :- binary(f,xl,op,xr), defined(xl), defined(xr,bound).
defined(f,bound) :- binary(f,xl,op,xr), value(f,_,bound).
value(f,VL+VR,bound) :- binary(f,xl,op,xr), value(xl,VL), value(xr,VR,bound), op = "+".
value(f,VL-VR,bound) :- binary(f,xl,op,xr), value(xl,VL), value(xr,VR,bound), op = "-".
value(f,VL*VR,bound) :- binary(f,xl,op,xr), value(xl,VL), value(xr,VR,bound), op = "*".
value(f, VL,bound) :- binary(f,xl,op,xr), value(xl,VL),       not value(xr,_,bound), op = "+".
value(f, VR,bound) :- binary(f,xl,op,xr), value(xr,VR,bound), not value(xl,_),       op = "+".
value(f, VL,bound) :- binary(f,xl,op,xr), value(xl,VL),       not value(xr,_,bound), op = "-".
value(f,-VR,bound) :- binary(f,xl,op,xr), value(xr,VR,bound), not value(xl,_),       op = "-".
satisfied(f,bound) :- binary(f,xl,op,xr), VL =  VR, value(xl,VL), value(xr,VR,bound), op = "=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL != VR, value(xl,VL), value(xr,VR,bound), op = "!=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL >  VR, value(xl,VL), value(xr,VR,bound), op = ">".
satisfied(f,bound) :- binary(f,xl,op,xr), VL >= VR, value(xl,VL), value(xr,VR,bound), op = ">=".
satisfied(f,bound) :- binary(f,xl,op,xr), VL <  VR, value(xl,VL), value(xr,VR,bound), op = "<".
satisfied(f,bound) :- binary(f,xl,op,xr), VL <= VR, value(xl,VL), value(xr,VR,bound), op = "<=".
satisfied(f,bound) :- binary(f,xl,op,xr), 1 <= { satisfied(xl); satisfied(xr,bound) }, op = "||".
satisfied(f,bound) :- binary(f,xl,op,xr), satisfied(xl), satisfied(xr,bound), op = "&&".