Encodings for adding simple constraints

The following encodings contain the rules of the standard COOM encoding split up into program parts for the part of a constraint they specify, i.e. the constraint itself, one of the sub-expressions of a boolean constraint (binary, unary, function), or parts of a table constraint (allow, column).

The active/1 externals is used here to only check for constraint violations of bounds that are active.

Encodings

new-constraint.lp

Encoding

#program new_constraint(c,type,bound).
#external active(bound).
constraint(c,type).

boolean constraints

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

table constraints

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

lower bound constraints

violated((X',P)) :- c = (P,MIN), constraint((P,Min),type), set(P,X), index(X,Min-1), not include(X), parent(X,X'), include(X'), type ="lowerbound".

% constraint violations are only checked if the bound is active
:- violated(C), active(bound).

Encodings for boolean constraints

Encodings

new-function.lp

Encoding

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

Encodings

new-unary.lp

Encoding

#program new_unary(f,op,f').
unary(f,op,f').

boolean unaries

defined(f) :- unary(f,op,f'), defined(f').
satisfied(f) :- unary(f,op,f'), not satisfied(f'), op = "!".
satisfied(f) :- unary(f,op,f'),     satisfied(f'), op = "()".

% numeric unaries
defined(f) :- unary(f,op,f'), value(f,_).

value(f, V) :- unary(f,op,f'), value(f',V), op = "()".
value(f, V) :- unary(f,op,f'), value(f',V), op = "+".
value(f,-V) :- unary(f,op,f'), value(f',V), op = "-".

Encodings

new-binary.lp

Encoding

#program new_binary(f,xl,op,xr).
binary(f,xl,op,xr).

boolean binaries

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

% numeric binaries
defined(f) :- binary(f,xl,op,xr), value(f,_).

value(f,VL+VR) :- binary(f,xl,op,xr), value(xl,VL), value(xr,VR), op = "+".
value(f,VL-VR) :- binary(f,xl,op,xr), value(xl,VL), value(xr,VR), op = "-".
value(f,VL*VR) :- binary(f,xl,op,xr), value(xl,VL), value(xr,VR), op = "*".

value(f, VL) :- binary(f,xl,op,xr), value(xl,VL), not value(xr,_), op = "+".
value(f, VR) :- binary(f,xl,op,xr), value(xr,VR), not value(xl,_), op = "+".
value(f, VL) :- binary(f,xl,op,xr), value(xl,VL), not value(xr,_), op = "-".
value(f,-VR) :- binary(f,xl,op,xr), value(xr,VR), not value(xl,_), op = "-".

Encodings for table constraints

Encodings

new-allow.lp

Encoding

#program new_allow(idx,pos,value).
allow(idx,pos,value).

Encodings

new-column.lp

Encoding

#program new_column(c,id,col,x,bound).
column(c,id,col,x).

table_bound is only needed if the corresponding table constraint is incremental

table_bound(c,id,bound).
undefined(c,id) :- column(c,id,_,x), not include(x).
defined(c,id)   :- column(c,id,_,_), not undefined(c,id).
not_hit(c,id,Row) :- allow(Idx,(col,Row),_), column(c,id,col,x), c=(Idx,_), not value(x,V) : allow(Idx,(col,Row),V).
satisfied(c,id) :- allow(Idx,(_,Row),_), column(c,id,_,_), c=(Idx,_), not not_hit(c,id,Row).