Encodings¶
In this section we show a basic documentation of our encoding in the form of a docstring of the used predicates.
Predicate Summary ¶
Dependency Graph ¶
flowchart LR
include/1(["include/1"])
user_include/1 --> include/1
type/2 --> include/1
user_value/2 --> include/1
part/1 --> include/1
include/1 --> include/1
consistent/2 --> include/1
consistent/1 --> include/1
value/2(["value/2"])
range/3 --> value/2
integer/1 --> value/2
consistent/2 --> value/2
discrete/1 --> value/2
constant/1 --> value/2
value/2 --> value/2
type/2 --> value/2
user_value/2 --> value/2
function/3 --> value/2
number/2 --> value/2
domain/2 --> value/2
include/1 --> value/2
set/2 --> value/2
binary/4 --> value/2
unary/3 --> value/2
defined/1(["defined/1"])
defined/1 --> defined/1
binary/4 --> defined/1
value/2 --> defined/1
unary/3 --> defined/1
satisfied/1(["satisfied/1"])
binary/4 --> satisfied/1
value/2 --> satisfied/1
satisfied/1 --> satisfied/1
unary/3 --> satisfied/1
violated/1(["violated/1"])
parent/2 --> violated/1
defined/1 --> violated/1
satisfied/2 --> violated/1
defined/2 --> violated/1
index/2 --> violated/1
include/1 --> violated/1
set/2 --> violated/1
constraint/2 --> violated/1
satisfied/1 --> violated/1
undefined/2(["undefined/2"])
column/4 --> undefined/2
include/1 --> undefined/2
defined/2(["defined/2"])
column/4 --> defined/2
undefined/2 --> defined/2
not_hit/3(["not_hit/3"])
column/4 --> not_hit/3
value/2 --> not_hit/3
allow/3 --> not_hit/3
satisfied/2(["satisfied/2"])
column/4 --> satisfied/2
not_hit/3 --> satisfied/2
allow/3 --> satisfied/2
consistent/1(["consistent/1"])
user_include/1 --> consistent/1
type/2 --> consistent/1
consistent/2(["consistent/2"])
range/3 --> consistent/2
integer/1 --> consistent/2
discrete/1 --> consistent/2
type/2 --> consistent/2
user_value/2 --> consistent/2
domain/2 --> consistent/2
type/2(["type/2"])
parent/2(["parent/2"])
set/2(["set/2"])
index/2(["index/2"])
constraint/2(["constraint/2"])
domain/2(["domain/2"])
discrete/1(["discrete/1"])
constant/1(["constant/1"])
integer/1(["integer/1"])
range/3(["range/3"])
number/2(["number/2"])
binary/4(["binary/4"])
unary/3(["unary/3"])
function/3(["function/3"])
column/4(["column/4"])
allow/3(["allow/3"])
user_include/1(["user_include/1"])
user_value/2(["user_value/2"])
part/1(["part/1"])
classDef all fill:#00000000
class __tmp,include/1,value/2,defined/1,satisfied/1,violated/1,undefined/2,defined/2,not_hit/3,satisfied/2,consistent/1,consistent/2,type/2,parent/2,set/2,index/2,constraint/2,domain/2,discrete/1,constant/1,integer/1,range/3,number/2,binary/4,unary/3,function/3,column/4,allow/3,user_include/1,user_value/2,part/1, all;
classDef out stroke:#52BF54,stroke-width:3px;
class __tmp,include/1,value/2, out;
classDef aux stroke:#848484,stroke-width:0.2px;
class __tmp,defined/1,satisfied/1,violated/1,undefined/2,defined/2,not_hit/3,satisfied/2,consistent/1,consistent/2,type/2,parent/2,set/2,index/2,constraint/2,domain/2,discrete/1,constant/1,integer/1,range/3,number/2,binary/4,unary/3,function/3,column/4,allow/3,user_include/1,user_value/2,part/1, aux;
classDef in stroke:#9178C6,stroke-width:3px;
class type/2,parent/2,set/2,index/2,constraint/2,domain/2,discrete/1,constant/1,integer/1,range/3,number/2,binary/4,unary/3,function/3,column/4,allow/3,user_include/1,user_value/2,part/1, in;Encodings ¶
src/coomsuite/encodings/encoding-base-clingo-show.lp
¶
Encoding
#include "base/defined.lp".
#include "base/structure.lp".
#include "base/discrete.lp".
#include "base/clingo/integer.lp".
#include "base/clingo/boolean.lp".
#include "base/clingo/numerics.lp".
#include "base/clingo/table.lp".
#include "base/constraints.lp".
#include "base/clingo/user.lp".
#include "doc.lp".
#include "show-clingo.lp".
src/coomsuite/encodings/base/defined.lp
¶
Encoding
#defined type/1.
#defined part/1.
#defined discrete/1.
#defined domain/2.
#defined integer/1.
#defined range/3.
#defined type/2.
#defined index/2.
#defined parent/2.
#defined constraint/2.
#defined binary/4.
#defined unary/3.
#defined table/1.
#defined column/4.
#defined allow/3.
#defined constant/1.
#defined number/2.
#defined function/3.
#defined set/2.
#defined minimize/2.
#defined maximize/2.
#defined user_include/1.
#defined user_value/2.
src/coomsuite/encodings/base/structure.lp
¶
Encoding
Always include root object
Generate include predicates for objects
Do not include an object if its parent is not included
Indices in ascending order
src/coomsuite/encodings/base/discrete.lp
¶
Encoding
src/coomsuite/encodings/base/clingo/integer.lp
¶
Encoding
src/coomsuite/encodings/base/clingo/boolean.lp
¶
Encoding
Definedness of formulas
defined(X) :- value(X,_).
defined(F) :- binary(F,XL,_,XR), defined(XL), defined(XR).
defined(F) :- unary(F,_,F'), defined(F').
Satisfaction of binary comparison relations
satisfied(F) :- binary(F,XL,"=", XR), VL = VR, value(XL,VL), value(XR,VR).
satisfied(F) :- binary(F,XL,"!=",XR), VL != VR, value(XL,VL), value(XR,VR).
satisfied(F) :- binary(F,XL,">", XR), VL > VR, value(XL,VL), value(XR,VR).
satisfied(F) :- binary(F,XL,">=",XR), VL >= VR, value(XL,VL), value(XR,VR).
satisfied(F) :- binary(F,XL,"<", XR), VL < VR, value(XL,VL), value(XR,VR).
satisfied(F) :- binary(F,XL,"<=",XR), VL <= VR, value(XL,VL), value(XR,VR).
Satisfaction of unary/binary logical relations
satisfied(F) :- unary(F,"!",F'), not satisfied(F').
satisfied(F) :- unary(F,"()",F'), satisfied(F').
satisfied(F) :- binary(F,XL,"||",XR), 1 <= { satisfied(XL); satisfied(XR) }.
satisfied(F) :- binary(F,XL,"&&",XR), satisfied(XL), satisfied(XR).
A Boolean formula is violated if it is defined and not satisfied
src/coomsuite/encodings/base/clingo/numerics.lp
¶
Encoding
Evaluate aggregates
value(F,V) :- function(F,"count",P), V = #count{ X : set(P,X), include(X) }.
value(F,V) :- function(F,"sum", P), V = #sum { V',X : set(P,X), value(X,V') }.
value(F,V) :- function(F,"min", P), V = #min { V',X : set(P,X), value(X,V') }.
value(F,V) :- function(F,"max", P), V = #max { V',X : set(P,X), value(X,V') }.
Arithmetics
value(F,VL+VR) :- binary(F,XL,"+",XR), value(XL,VL), value(XR,VR).
value(F,VL-VR) :- binary(F,XL,"-",XR), value(XL,VL), value(XR,VR).
value(F,VL*VR) :- binary(F,XL,"*",XR), value(XL,VL), value(XR,VR).
value(F, V) :- unary(F,"()",X), value(X,V).
value(F, V) :- unary(F,"+", X), value(X,V).
value(F,-V) :- unary(F,"-", X), value(X,V).
TODO: Add more arithmetics (division and power)
Default arithmetics
value(F,VL) :- binary(F,XL,"+",XR), value(XL,VL), not value(XR,_).
value(F,VR) :- binary(F,XL,"+",XR), value(XR,VR), not value(XL,_).
value(F,VL) :- binary(F,XL,"-",XR), value(XL,VL), not value(XR,_).
value(F,-VR) :- binary(F,XL,"-",XR), value(XR,VR), not value(XL,_).
TODO: More rules for multiplication?
src/coomsuite/encodings/base/clingo/table.lp
¶
Encoding
A table constraint is defined if none of its columns are undefined
undefined(C,ID) :- column(C,ID,_,X), not include(X).
defined(C,ID) :- column(C,ID,_,_), not undefined(C,ID).
A row of a table is not satisfied if any of its entries is not satisfied.
Note that a table entry can contain multiple values.
This is incompatible with flingo (mixed check of values).
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).
A table constraint is satisfied if one of its rows is satisfied (not not satisfied)
A table constraint is violated if is defined and not satisfied
src/coomsuite/encodings/base/constraints.lp
¶
Encoding
A lower bound (cardinality) constraint is violated if less than the minimum number of objects are included
(objects are included in ascending order of indices)
(maximum does not need to be checked)
violated((X',P)) :- constraint((P,Min),"lowerbound"), set(P,X), index(X,Min-1), not include(X), parent(X,X'), include(X').
Constraints cannot be violated
src/coomsuite/encodings/base/clingo/user.lp
¶
Encoding
consistent(X) :- user_include(X), type(X,_).
consistent(X,V) :- user_value(X,V), type(X,T), discrete(T), domain(T,V).
consistent(X,V) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), Min <= V <= Max.
consistent(X,V) :- user_value(X,V), type(X,T), integer(T), not range(T,_,_).
include(X) :- user_include(X), consistent(X).
include(X) :- user_value(X,V), consistent(X,V).
value(X,V) :- user_value(X,V), consistent(X,V).
src/coomsuite/encodings/doc.lp
¶
Encoding
part(T).¶
Declares the type of a part
parameters¶
- T : The type of the part
discrete(T).¶
Declares the part of a discrete attribute
parameters¶
- T : The type of the attribute
domain(T,V).¶
Declares a domain element of a discrete attribute
parameters¶
- T : The type of the attribute
- V : The domain element
integer(T).¶
Declares the part of an integer attribute
parameters¶
- T : The type of the attribute
range(T,Min,Max).¶
Declares the range of an integer attribute
parameters¶
- T : The type of the attribute
- Min : The minimum value of the range
- Max : The maximum value of the range
type(X,T).¶
The type of a variable
parameters¶
- X : The variable (either a part or an attribute)
- T : The type of the variable
parent(X,P).¶
The parent of a variable
parameters¶
- X : The variable (either a part or an attribute)
- P : The parent of the variable
index(X,I).¶
The index of a variable in a cardinality set, for example, "root.frame[1]" has index 1
parameters¶
- X : The variable (either a part or an attribute)
- I : The index of the variable
constraint(C,T).¶
Instantiates a constraint
parameters¶
- C : The constraint identifier
- T : The type of the constraint (boolean, table, lowerbound)
binary(F,L,Op,R).¶
Defines a binary operation
parameters¶
- F : The identifier of the complete formula
- L : The identifier of the left operand
- Op : The operator
- R : The identifier of the right operand
unary(F,Op,F').¶
Defines a unary operation
parameters¶
- F : The identifier of the complete formula
- Op : The operator
- F' : The identifier of the operand
function(F,Fun,Arg).¶
Defines a calculation involving a function
parameters¶
- F : The identifier of the complete formula
- Fun : The function type
- Arg : The argument of the function
set(S,X).¶
Defines the members of a set (for cardinalities and aggregate functions)
parameters¶
- S : The identifier of the set
- X : The variable (either a part or an attribute) which is a member of the set
constant(C).¶
Auxiliary predicate which defines a constant (string)
parameters¶
- C : The constant as a string
number(C,N).¶
Auxiliary predicate which defines a constant number
parameters¶
- C : The number as a string
- N : The number as an integer
column(C,ID,Col,X).¶
Defines a column of a table constraint
parameters¶
- C : The identifier of the constraint
- ID : The identifier of the cross product of the table header variables
- Col : The column number
- X : The header variable of the column
allow(Idx,(Col,Row),V).¶
Defines an entry of a table constraint (for allowed combinations)
parameters¶
- Idx : The index of the table constraint (part of the constraint identifier)
- Col : The column number
- Row : The row number
- V : The value of the table entry
user_include(X).¶
An include statement from user input
parameters¶
- X : The variable (either a part or an attribute) to be included
user_value(X,V).¶
An attribute variable value set by user input
parameters¶
- X : The attribute variable for which the value is set
- V : The value of the attribute variable
violated(C).¶
Whether a constraint is violated (Boolean, table or lower bound)
parameters¶
- C : The constraint identifier (tuple that differs for each constraint type)
consistent(X).¶
Whether a user input variable is consistent with the configuration model
parameters¶
- X : The variable (either a part or an attribute) to be included
consistent(X,V).¶
Whether a user input value is consistent with the configuration model
parameters¶
- X : The attribute variable for which the value is set
- V : The value of the attribute variable
defined(X).¶
Whether a variable or (sub)formula is defined
parameters¶
- X : The variable or (sub)formula
undefined(X).¶
Whether a variable or (sub)formula is undefined
parameters¶
- X : The variable or (sub)formula
satisfied(X).¶
Whether a variable or (sub)formula is satisfied
parameters¶
- X : The variable or (sub)formula
defined(C,ID).¶
Whether a table constraint is defined
parameters¶
- C : The table constraint identifier
- ID : The identifier of the cross product of the column header variables
undefined(C,ID).¶
Whether a table constraint is undefined
parameters¶
- C : The table constraint identifier
- ID : The identifier of the cross product of the column header variables
hit(C,ID,(Col,Row)).¶
Whether an entry of a table constraint is satisfied (only for flingo encoding)
parameters¶
- C : The table constraint identifier
- ID : The identifier of the cross product of the column header variables
- Col : The column number
- Row : The row number
not_hit(C,ID,Row).¶
Whether a row of a table constraint is not satisfied
parameters¶
- C : The table constraint identifier
- ID : The identifier of the cross product of the column header variables
- Row : The row number
satisfied(C,ID).¶
Whether a table constraint is satisfied
parameters¶
- C : The table constraint identifier
- ID : The identifier of the cross product of the column header variables
include(X).¶
Whether a variable is included in the configuration
parameters¶
- X : The variable (either a part or an attribute)
value(X,V).¶
The value of an attribute variable
parameters¶
- X : The attribute variable
- V : The value of the variable
src/coomsuite/encodings/show-clingo.lp
¶
Encoding