Encodings¶
In this section we show a basic documentation of our encoding in the form of a docstring of the used predicates.
Predicate Summary ¶
| Name | Definition | Type |
|---|---|---|
include/1 |
Whether a variable is included in the configuration |
|
value/2 |
The value of an attribute variable |
|
allow/3 |
Defines an entry of a table constraint (for allowed combinations) |
|
binary/4 |
Defines a binary operation |
|
column/4 |
Defines a column of a table constraint |
|
constant/1 |
Auxiliary predicate which defines a constant (string) |
|
constraint/2 |
Instantiates a constraint |
|
discrete/1 |
Declares the part of a discrete attribute |
|
domain/2 |
Declares a domain element of a discrete attribute |
|
function/3 |
Defines a calculation involving a function |
|
hit/3 |
Whether an entry of a table constraint is satisfied (only for fclingo encoding) |
|
index/2 |
The index of a variable in a cardinality set, for example, "root.frame[1]" has index 1 |
|
integer/1 |
Declares the part of an integer attribute |
|
number/2 |
Auxiliary predicate which defines a constant number |
|
parent/2 |
The parent of a variable |
|
part/1 |
Declares the type of a part |
|
range/3 |
Declares the range of an integer attribute |
|
set/2 |
Defines the members of a set (for cardinalities and aggregate functions) |
|
type/2 |
The type of a variable |
|
unary/3 |
Defines a unary operation |
|
undefined/1 |
Whether a variable or (sub)formula is undefined |
|
user_include/1 |
An include statement from user input |
|
user_value/2 |
An attribute variable value set by user input |
|
consistent/1 |
Whether a user input variable is consistent with the configuration model |
|
consistent/2 |
Whether a user input value is consistent with the configuration model |
|
defined/1 |
Whether a variable or (sub)formula is defined |
|
defined/2 |
Whether a table constraint is defined |
|
not_hit/3 |
Whether a row of a table constraint is not satisfied |
|
satisfied/1 |
Whether a variable or (sub)formula is satisfied |
|
satisfied/2 |
Whether a table constraint is satisfied |
|
undefined/2 |
Whether a table constraint is undefined |
|
violated/1 |
Whether a constraint is violated (Boolean, table or lower bound) |
|
Dependency Graph ¶
flowchart LR
include/1(["include/1"])
include/1 --> include/1
consistent/1 --> include/1
user_include/1 --> include/1
part/1 --> include/1
consistent/2 --> include/1
type/2 --> include/1
user_value/2 --> include/1
value/2(["value/2"])
value/2 --> value/2
range/3 --> value/2
function/3 --> value/2
constant/1 --> value/2
discrete/1 --> value/2
type/2 --> value/2
include/1 --> value/2
integer/1 --> value/2
number/2 --> value/2
unary/3 --> value/2
user_value/2 --> value/2
binary/4 --> value/2
domain/2 --> value/2
consistent/2 --> value/2
set/2 --> value/2
defined/1(["defined/1"])
value/2 --> defined/1
binary/4 --> defined/1
defined/1 --> defined/1
unary/3 --> defined/1
satisfied/1(["satisfied/1"])
binary/4 --> satisfied/1
value/2 --> satisfied/1
unary/3 --> satisfied/1
satisfied/1 --> satisfied/1
violated/1(["violated/1"])
defined/2 --> violated/1
include/1 --> violated/1
parent/2 --> violated/1
satisfied/2 --> violated/1
constraint/2 --> violated/1
defined/1 --> violated/1
set/2 --> violated/1
index/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
allow/3 --> not_hit/3
value/2 --> not_hit/3
satisfied/2(["satisfied/2"])
column/4 --> satisfied/2
allow/3 --> satisfied/2
not_hit/3 --> satisfied/2
consistent/1(["consistent/1"])
user_include/1 --> consistent/1
type/2 --> consistent/1
consistent/2(["consistent/2"])
range/3 --> consistent/2
discrete/1 --> consistent/2
type/2 --> consistent/2
user_value/2 --> consistent/2
integer/1 --> 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"])
undefined/1(["undefined/1"])
hit/3(["hit/3"])
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,undefined/1,hit/3, 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,undefined/1,hit/3, 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,undefined/1,hit/3, 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 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 fclingo (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
src/coomsuite/encodings/show-clingo.lp
¶
Encoding
Glossary ¶
include(X)
¶
Whether a variable is included in the configuration
References
value(X,V)
¶
The value of an attribute variable
References
allow(Idx,(Col,Row),V)
¶
Defines an entry of a table constraint (for allowed combinations)
References
binary(F,L,Op,R)
¶
Defines a binary operation
References
column(C,ID,Col,X)
¶
Defines a column of a table constraint
References
constant(C)
¶
Auxiliary predicate which defines a constant (string)
References
constraint(C,T)
¶
Instantiates a constraint
References
discrete(T)
¶
Declares the part of a discrete attribute
domain(T,V)
¶
Declares a domain element of a discrete attribute
function(F,Fun,Arg)
¶
Defines a calculation involving a function
References
hit(C,ID,(Col,Row))
¶
Whether an entry of a table constraint is satisfied (only for fclingo encoding)
References
index(X,I)
¶
The index of a variable in a cardinality set, for example, "root.frame[1]" has index 1
References
integer(T)
¶
Declares the part of an integer attribute
References
number(C,N)
¶
Auxiliary predicate which defines a constant number
References
parent(X,P)
¶
The parent of a variable
part(T)
¶
Declares the type of a part
References
range(T,Min,Max)
¶
Declares the range of an integer attribute
set(S,X)
¶
Defines the members of a set (for cardinalities and aggregate functions)
References
type(X,T)
¶
The type of a variable
References
unary(F,Op,F')
¶
Defines a unary operation
References
undefined(X)
¶
Whether a variable or (sub)formula is undefined
References
user_include(X)
¶
An include statement from user input
user_value(X,V)
¶
An attribute variable value set by user input
References
consistent(X)
¶
Whether a user input variable is consistent with the configuration model
consistent(X,V)
¶
Whether a user input value is consistent with the configuration model
References
defined(X)
¶
Whether a variable or (sub)formula is defined
References
defined(C,ID)
¶
Whether a table constraint is defined
not_hit(C,ID,Row)
¶
Whether a row of a table constraint is not satisfied
satisfied(X)
¶
Whether a variable or (sub)formula is satisfied
References
satisfied(C,ID)
¶
Whether a table constraint is satisfied
undefined(C,ID)
¶
Whether a table constraint is undefined
violated(C)
¶
Whether a constraint is violated (Boolean, table or lower bound)