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
_hit/3
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
default/2	Defines a default value
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 flingo 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
include/1	Whether a variable is included in the configuration
value/2	The value of an attribute variable
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"])
    type/2(["type/2"])
    part/1(["part/1"])
    value/2(["value/2"])
    discrete/1(["discrete/1"])
    integer/1(["integer/1"])
    parent/2(["parent/2"])
    index/2(["index/2"])
    set/2(["set/2"])
    constraint/2(["constraint/2"])
    domain/2(["domain/2"])
    constant/1(["constant/1"])
    range/3(["range/3"])
    number/2(["number/2"])
    defined/1(["defined/1"])
    binary/4(["binary/4"])
    unary/3(["unary/3"])
    satisfied/1(["satisfied/1"])
    violated/1(["violated/1"])
    function/3(["function/3"])
    undefined/2(["undefined/2"])
    column/4(["column/4"])
    defined/2(["defined/2"])
    not_hit/3(["not_hit/3"])
    allow/3(["allow/3"])
    satisfied/2(["satisfied/2"])
    _hit/3(["_hit/3"])
    default/2(["default/2"])
    consistent/2(["consistent/2"])
    user_value/2(["user_value/2"])
    consistent/1(["consistent/1"])
    user_include/1(["user_include/1"])
    undefined/1(["undefined/1"])
    hit/3(["hit/3"])



    consistent/1 --> include/1
    include/1 --> include/1
    part/1 --> include/1
    consistent/2 --> include/1
    user_value/2 --> include/1
    type/2 --> include/1
    user_include/1 --> include/1
    domain/2 --> value/2
    value/2 --> value/2
    include/1 --> value/2
    binary/4 --> value/2
    allow/3 --> value/2
    default/2 --> value/2
    range/3 --> value/2
    set/2 --> value/2
    unary/3 --> value/2
    consistent/2 --> value/2
    integer/1 --> value/2
    function/3 --> value/2
    column/4 --> value/2
    type/2 --> value/2
    constant/1 --> value/2
    number/2 --> value/2
    user_value/2 --> value/2
    discrete/1 --> value/2
    unary/3 --> defined/1
    value/2 --> defined/1
    defined/1 --> defined/1
    binary/4 --> defined/1
    unary/3 --> satisfied/1
    value/2 --> satisfied/1
    binary/4 --> satisfied/1
    satisfied/1 --> satisfied/1
    parent/2 --> violated/1
    include/1 --> violated/1
    defined/1 --> violated/1
    set/2 --> violated/1
    index/2 --> violated/1
    defined/2 --> violated/1
    constraint/2 --> violated/1
    column/4 --> undefined/2
    column/4 --> defined/2
    allow/3 --> not_hit/3
    column/4 --> not_hit/3
    allow/3 --> satisfied/2
    _hit/3 --> satisfied/2
    column/4 --> satisfied/2
    domain/2 --> consistent/2
    range/3 --> consistent/2
    integer/1 --> consistent/2
    user_value/2 --> consistent/2
    type/2 --> consistent/2
    discrete/1 --> consistent/2
    user_include/1 --> consistent/1
    type/2 --> consistent/1

    value/2 -.-> value/2
    satisfied/1 -.-> satisfied/1
    satisfied/2 -.-> violated/1
    include/1 -.-> violated/1
    satisfied/1 -.-> violated/1
    include/1 -.-> undefined/2
    undefined/2 -.-> defined/2
    value/2 -.-> not_hit/3
    range/3 -.-> consistent/2
    classDef all fill:#00000000;
    classDef out stroke:#52BF54,stroke-width:3px;
    classDef aux stroke:#848484,stroke-width:0.2px;
    classDef in stroke:#9178C6,stroke-width:3px;


    class include/1,type/2,part/1,value/2,discrete/1,integer/1,parent/2,index/2,set/2,constraint/2,domain/2,constant/1,range/3,number/2,defined/1,binary/4,unary/3,satisfied/1,violated/1,function/3,undefined/2,column/4,defined/2,not_hit/3,allow/3,satisfied/2,_hit/3,default/2,consistent/2,user_value/2,consistent/1,user_include/1,undefined/1,hit/3 all;




    class include/1,value/2 out;




    class type/2,part/1,discrete/1,integer/1,parent/2,index/2,set/2,constraint/2,domain/2,constant/1,range/3,number/2,defined/1,binary/4,unary/3,satisfied/1,violated/1,function/3,undefined/2,column/4,defined/2,not_hit/3,allow/3,satisfied/2,_hit/3,default/2,consistent/2,user_value/2,consistent/1,user_include/1,undefined/1,hit/3 aux;




    class type/2,part/1,discrete/1,integer/1,parent/2,index/2,set/2,constraint/2,domain/2,constant/1,range/3,number/2,binary/4,unary/3,function/3,column/4,allow/3,_hit/3,default/2,user_value/2,user_include/1,undefined/1,hit/3 in;

Encodings

src/coomsuite/encodings/encoding-base-clingo-show.lp

Encoding

src/coomsuite/encodings/encoding-base-clingo.lp

Encoding

src/coomsuite/encodings/show-clingo.lp

Encoding

#show .
#show include(X) : include(X), type(X,T), part(T), X != "root".
#show value(X,V) : value(X,V), type(X,T), discrete(T).
#show value(X,V) : value(X,V), type(X,T), integer(T).

src/coomsuite/encodings/base/defined.lp

Encoding

src/coomsuite/encodings/base/structure.lp

Encoding

Always include root object

include("root").

Generate include predicates for objects

{ include(X) : type(X,_) }.

% Always include minimal number of objects % Commented out because we wanted to include no optimizations currently % include(X) :- feature(C,,T,Min,), type(X,T), index(X,I), I < Min, % parent(X,P), include(P), type(P,C). Do not include an object if its parent is not included

:- include(X), parent(X,P), not include(P).

Indices in ascending order

:-  include(X),  set(P,X ), index(X, I), I > 0,
not include(X'), set(P,X'), index(X',I-1), constraint((P,_),_).

src/coomsuite/encodings/base/discrete.lp

Encoding

Generate exactly one value for each discrete attribute if it is included

{ value(X,V) : domain(T,V) } = 1 :- include(X), type(X,T), discrete(T).

{ value(X,O) : type(X,T), enumeration(T), option(T,O) } 1. % No value if variable has not been included :- type(X,T), value(X,), not include(X). % Exactly one value if variable has been included :- attribute(T,), type(X,T), include(X), not { value(X,_) } = 1. Auxiliary values for (non-numeric) constants

value(P,P) :- constant(P).

src/coomsuite/encodings/base/clingo/integer.lp

Encoding

Generate exactly one value for each (numeric) integer attribute if it is included

{ value(X,V) : V = Min..Max } = 1 :- include(X), type(X,T), integer(T), range(T,Min,Max).

Auxiliary values for numbers.

value(P,N) :- number(P,N).

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

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

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)

satisfied(C,ID) :- allow(Idx,(_,Row),_), column(C,ID,_,_), C=(Idx,_), not not_hit(C,ID,Row).

A table constraint is violated if is defined and not satisfied

violated((C,ID)) :- constraint(C,"table"), defined(C,ID), not satisfied(C,ID).

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

:- violated(C).

src/coomsuite/encodings/base/clingo/defaults.lp

Encoding

value(X,V) :- default(X,V), include(X), #false : user_value(X,_), consistent(X,_).

TODO: Check this

src/coomsuite/encodings/base/clingo/optimization.lp

Encoding

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Input predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Parts and attributes %% Configuration variables %% Constraints %% User input %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Encoding predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Boolean constraints %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Output predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

---

Glossary

_hit(A, B, C)

References

satisfied(C,ID) :- allow(Idx,(_,Row),_), column(C,ID,_,_), C=(Idx,_), not not_hit(C,ID,Row).

allow(Idx, Pos, V)

Defines an entry of a table constraint (for allowed combinations)

Parameter	Description
Idx	The index of the table constraint (part of the constraint identifier)
Pos	The position of the entry as a tuple (Col,Row)
V	The value of the table entry

References

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).

binary(F, L, Op, R)

Defines a binary operation

Parameter	Description
F	The identifier of the complete formula
L	The identifier of the left operand
Op	The operator
R	The identifier of the right operand

References

defined(F) :- binary(F,XL,_,XR), defined(XL), defined(XR).

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).

satisfied(F) :- binary(F,XL,"||",XR), 1 <= { satisfied(XL); satisfied(XR) }.

satisfied(F) :- binary(F,XL,"&&",XR), satisfied(XL), satisfied(XR).

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,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,_).

column(C, ID, Col, X)

Defines a column of a table constraint

Parameter	Description
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

References

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).

constant(C)

Auxiliary predicate which defines a constant (string)

Parameter	Description
C	The constant as a string

References

value(P,P) :- constant(P).

constraint(C, T)

Instantiates a constraint

Parameter	Description
C	The constraint identifier
T	The type of the constraint (boolean, table, lowerbound)

References

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

violated((C,ID)) :- constraint(C,"table"), defined(C,ID), not satisfied(C,ID).

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

:-  include(X),  set(P,X ), index(X, I), I > 0,
not include(X'), set(P,X'), index(X',I-1), constraint((P,_),_).

default(X, V)

Defines a default value

Parameter	Description
X	The variable that gets assigned a default value
V	The default value

References

value(X,V) :- default(X,V), include(X), #false : user_value(X,_), consistent(X,_).

discrete(T)

Declares the part of a discrete attribute

Parameter	Description
T	The type of the attribute

References

consistent(X,V) :- user_value(X,V), type(X,T), discrete(T), domain(T,V).

{ value(X,V) : domain(T,V) } = 1 :- include(X), type(X,T), discrete(T).

#show value(X,V) : value(X,V), type(X,T), discrete(T).

domain(T, V)

Declares a domain element of a discrete attribute

Parameter	Description
T	The type of the attribute
V	The domain element

References

consistent(X,V) :- user_value(X,V), type(X,T), discrete(T), domain(T,V).

{ value(X,V) : domain(T,V) } = 1 :- include(X), type(X,T), discrete(T).

function(F, Fun, Arg)

Defines a calculation involving a function

Parameter	Description
F	The identifier of the complete formula
Fun	The function type
Arg	The argument of the function

References

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')   }.

hit(C, ID, Pos)

Whether an entry of a table constraint is satisfied (only for flingo encoding)

Parameter	Description
C	The table constraint identifier
ID	The identifier of the cross product of the column header variables
Pos	The position of the table entry as a tuple (Col,Row)

References

index(X, I)

The index of a variable in a cardinality set, for example, "root.frame[1]" has index 1

Parameter	Description
X	The variable (either a part or an attribute)
I	The index of the variable

References

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

:-  include(X),  set(P,X ), index(X, I), I > 0,
not include(X'), set(P,X'), index(X',I-1), constraint((P,_),_).

integer(T)

Declares the part of an integer attribute

Parameter	Description
T	The type of the attribute

References

{ value(X,V) : V = Min..Max } = 1 :- include(X), type(X,T), integer(T), range(T,Min,Max).

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,_,_).

#show value(X,V) : value(X,V), type(X,T), integer(T).

number(C, N)

Auxiliary predicate which defines a constant number

Parameter	Description
C	The number as a string
N	The number as an integer

References

value(P,N) :- number(P,N).

parent(X, P)

The parent of a variable

Parameter	Description
X	The variable (either a part or an attribute)
P	The parent of the variable

References

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

:- include(X), parent(X,P), not include(P).

part(T)

Declares the type of a part

Parameter	Description
T	The type of the part

References

#show include(X) : include(X), type(X,T), part(T), X != "root".

range(T, Min, Max)

Declares the range of an integer attribute

Parameter	Description
T	The type of the attribute
Min	The minimum value of the range
Max	The maximum value of the range

References

{ value(X,V) : V = Min..Max } = 1 :- include(X), type(X,T), integer(T), range(T,Min,Max).

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,_,_).

set(S, X)

Defines the members of a set (for cardinalities and aggregate functions)

Parameter	Description
S	The identifier of the set
X	The variable (either a part or an attribute) which is a member of the set

References

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')   }.

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

:-  include(X),  set(P,X ), index(X, I), I > 0,
not include(X'), set(P,X'), index(X',I-1), constraint((P,_),_).

type(X, T)

The type of a variable

Parameter	Description
X	The variable (either a part or an attribute)
T	The type of the variable

References

{ value(X,V) : V = Min..Max } = 1 :- include(X), type(X,T), integer(T), range(T,Min,Max).

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,_,_).

{ value(X,V) : domain(T,V) } = 1 :- include(X), type(X,T), discrete(T).

{ include(X) : type(X,_) }.

#show include(X) : include(X), type(X,T), part(T), X != "root".

#show value(X,V) : value(X,V), type(X,T), discrete(T).

#show value(X,V) : value(X,V), type(X,T), integer(T).

unary(F, Op, F')

Defines a unary operation

Parameter	Description
F	The identifier of the complete formula
Op	The operator
F'	The identifier of the operand

References

defined(F) :- unary(F,_,F'), defined(F').

satisfied(F) :- unary(F,"!",F'), not satisfied(F').

satisfied(F) :- unary(F,"()",F'),    satisfied(F').

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).

undefined(X)

Whether a variable or (sub)formula is undefined

Parameter	Description
X	The variable or (sub)formula

References

user_include(X)

An include statement from user input

Parameter	Description
X	The variable (either a part or an attribute) to be included

References

consistent(X)   :- user_include(X), type(X,_).

include(X) :- user_include(X), consistent(X).

user_value(X, V)

An attribute variable value set by user input

Parameter	Description
X	The attribute variable for which the value is set
V	The value of the attribute variable

References

value(X,V) :- default(X,V), include(X), #false : user_value(X,_), consistent(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_value(X,V), consistent(X,V).

value(X,V) :- user_value(X,V), consistent(X,V).

include(X)

Whether a variable is included in the configuration

Parameter	Description
X	The variable (either a part or an attribute)

References

value(X,V) :- default(X,V), include(X), #false : user_value(X,_), consistent(X,_).

{ value(X,V) : V = Min..Max } = 1 :- include(X), type(X,T), integer(T), range(T,Min,Max).

value(F,V) :- function(F,"count",P), V = #count{ X    : set(P,X), include(X) }.

undefined(C,ID) :- column(C,ID,_,X), not include(X).

include(X) :- user_include(X), consistent(X).

include(X) :- user_value(X,V), consistent(X,V).

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

{ value(X,V) : domain(T,V) } = 1 :- include(X), type(X,T), discrete(T).

include("root").

{ include(X) : type(X,_) }.

:- include(X), parent(X,P), not include(P).

:-  include(X),  set(P,X ), index(X, I), I > 0,
not include(X'), set(P,X'), index(X',I-1), constraint((P,_),_).

#show include(X) : include(X), type(X,T), part(T), X != "root".

value(X, V)

The value of an attribute variable

Parameter	Description
X	The attribute variable
V	The value of the variable

References

defined(X) :- value(X,_).

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).

value(X,V) :- default(X,V), include(X), #false : user_value(X,_), consistent(X,_).

{ value(X,V) : V = Min..Max } = 1 :- include(X), type(X,T), integer(T), range(T,Min,Max).

value(P,N) :- number(P,N).

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')   }.

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).

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,_).

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).

value(X,V) :- user_value(X,V), consistent(X,V).

{ value(X,V) : domain(T,V) } = 1 :- include(X), type(X,T), discrete(T).

value(P,P) :- constant(P).

#show value(X,V) : value(X,V), type(X,T), discrete(T).

#show value(X,V) : value(X,V), type(X,T), integer(T).

consistent(X)

Whether a user input variable is consistent with the configuration model

Parameter	Description
X	The variable (either a part or an attribute) to be included

References

consistent(X)   :- user_include(X), type(X,_).

include(X) :- user_include(X), consistent(X).

consistent(X, V)

Whether a user input value is consistent with the configuration model

Parameter	Description
X	The attribute variable for which the value is set
V	The value of the attribute variable

References

value(X,V) :- default(X,V), include(X), #false : user_value(X,_), consistent(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_value(X,V), consistent(X,V).

value(X,V) :- user_value(X,V), consistent(X,V).

defined(X)

Whether a variable or (sub)formula is defined

Parameter	Description
X	The variable or (sub)formula

References

defined(X) :- value(X,_).

defined(F) :- binary(F,XL,_,XR), defined(XL), defined(XR).

defined(F) :- unary(F,_,F'), defined(F').

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

defined(C, ID)

Whether a table constraint is defined

Parameter	Description
C	The table constraint identifier
ID	The identifier of the cross product of the column header variables

References

defined(C,ID)   :- column(C,ID,_,_), not undefined(C,ID).

violated((C,ID)) :- constraint(C,"table"), defined(C,ID), not satisfied(C,ID).

not_hit(C, ID, Row)

Whether a row of a table constraint is not satisfied

Parameter	Description
C	The table constraint identifier
ID	The identifier of the cross product of the column header variables
Row	The row number

References

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(X)

Whether a variable or (sub)formula is satisfied

Parameter	Description
X	The variable or (sub)formula

References

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).

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).

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

satisfied(C, ID)

Whether a table constraint is satisfied

Parameter	Description
C	The table constraint identifier
ID	The identifier of the cross product of the column header variables

References

satisfied(C,ID) :- allow(Idx,(_,Row),_), column(C,ID,_,_), C=(Idx,_), not not_hit(C,ID,Row).

violated((C,ID)) :- constraint(C,"table"), defined(C,ID), not satisfied(C,ID).

undefined(C, ID)

Whether a table constraint is undefined

Parameter	Description
C	The table constraint identifier
ID	The identifier of the cross product of the column header variables

References

undefined(C,ID) :- column(C,ID,_,X), not include(X).

defined(C,ID)   :- column(C,ID,_,_), not undefined(C,ID).

violated(C)

Whether a constraint is violated (Boolean, table or lower bound)

Parameter	Description
C	The constraint identifier (tuple that differs for each constraint type)

References

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

violated((C,ID)) :- constraint(C,"table"), defined(C,ID), not satisfied(C,ID).

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

:- violated(C).