Encodings for adding incremental constraints¶

Encodings ¶

`inc-constraint.lp` ¶

Encoding

#program incremental_constraint(cons,type,bound).
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

#external max_bound(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

#external active(bound).
:-
constraint(cons,type)
,
type =
"table"
,
a
c
tive
(
b
o
un
d
)
,
vi
o
late
d
(
(
c
o
n
s
,
ID
)
,
b
o
un
d
)
,
ta
b
le
_
b
o
un
d
(
c
o
n
s
,
ID
,
b
o
un
d
)
.

Encodings for incremental boolean constraints¶

Encodings ¶

`inc-function.lp` ¶

Encoding

program part for initializing new incremental functions

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

program part for updating incremental functions

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

compute value step-wise only take into account new objects with a corresponding bound/2 fact

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' < V,
                     V' = #min{ 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' >= V,
                     V' = #min{ Val,X : set(p,X), bound(X,bound), value(X,Val) }.
value(f,V',N+1)   :- function(f,agg,p), agg = "max", bound = N+1, value(f,V,N), V' > V,
                     V' = #max{ Val,X : set(p,X), bound(X,bound), value(X,Val) }.
value(f,V ,N+1)   :- function(f,agg,p), agg = "max", bound = N+1, value(f,V,N), V' <= V,
                     V' = #max{ Val,X : set(p,X), bound(X,bound), value(X,Val) }.

Encodings ¶

`inc-unary.lp` ¶

Encoding

#program incremental_unary(f,op,x,bound).
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 ¶

`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

#program incremental_binary(f,xl,op,xr,bound).
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
#program incremental_binary_l(f,xl,op,xr,bound).
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
#program incremental_binary_r(f,xl,op,xr,bound).
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 = "&&".

Encodings for adding incremental constraints¶

Encodings ¶

inc-constraint.lp ¶

Encodings for incremental boolean constraints¶

Encodings ¶

inc-function.lp ¶

Encodings ¶

inc-unary.lp ¶

Encodings ¶

inc-binary.lp ¶

`inc-constraint.lp` ¶

`inc-function.lp` ¶

`inc-unary.lp` ¶

`inc-binary.lp` ¶