Product Configuration¶

Documentation generated automatically, showcasing the use of mkdoclingo for a large project where the documentation of predicates is in a separate file.

Tip

Use the icon in the top right to see the source code for this page.

Predicate Summary ¶

Name	Definition	Type
`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
`violated/1`	Whether a constraint is violated (Boolean, table or lower bound)
`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

Encodings ¶

`examples/config/encoding-base-clingo.lp` ¶

Source

#include "base/defined.lp".
#include "doc.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 "base/show-clingo.lp".

Encoding

`examples/config/base/defined.lp` ¶

Source

#defined type/1.
#defined part/1.
#defined cardinality/3.
#defined set/2.

#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 user_include/1.
#defined user_value/2.

Encoding

`examples/config/doc.lp` ¶

Source

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Input predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% Parts and attributes

%*! part(T)

Declares the type of a part

Args:
    - T: The type of the part
*%

%*! discrete(T)

Declares the part of a discrete attribute

Args:
    - T: The type of the attribute
*%

%*! domain(T,V)

Declares a domain element of a discrete attribute

Args:
    - T: The type of the attribute
    - V: The domain element
*%

%*! integer(T)

Declares the part of an integer attribute

Args:
    - T: The type of the attribute
*%

%*! range(T,Min,Max)

Declares the range of an integer attribute

Args:
    - T: The type of the attribute
    - Min: The minimum value of the range
    - Max: The maximum value of the range
*%

%%% Configuration variables

%*! type(X,T)

The type of a variable

Args:
    - X: The variable (either a part or an attribute)
    - T: The type of the variable
*%

%*! parent(X,P)

The parent of a variable

Args:
    - 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

Args:
    - X: The variable (either a part or an attribute)
    - I: The index of the variable
*%

%%% Constraints

%*! constraint(C,T)

Instantiates a constraint

Args:
    - C: The constraint identifier
    - T: The type of the constraint (boolean, table, lowerbound)
*%

%*! binary(F,L,Op,R)

Defines a binary operation

Args:
    - 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

Args:
    - 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

Args:
    - 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)

Args:
    - 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)

Args:
    - C: The constant as a string
*%

%*! number(C,N)

Auxiliary predicate which defines a constant number

Args:
    - C: The number as a string
    - N: The number as an integer
*%

%*! column(C,ID,Col,X)

Defines a column of a table constraint

Args:
    - 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,P,V)

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

Args:
    - Idx: The index of the table constraint (part of the constraint identifier)
    - P: A tuple `(COL,ROW)` identifying the column and row of the table
    - V: The value of the table entry
*%

%*! user_include(X)

An include statement from user input

Args:
    - X: The variable (either a part or an attribute) to be included
*%

%*! user_value(X,V)

An attribute variable value set by user input

Args:
    - X: The attribute variable for which the value is set
    - V: The value of the attribute variable
*%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Encoding predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%*! violated(C)

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

Args:
    - C: The constraint identifier (tuple that differs for each constraint type)
*%

%*! consistent(X)

Whether a user input variable is consistent with the configuration model

Args:
    - 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

Args:
    - 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

Args:
    - X: The variable or (sub)formula
*%

%*! undefined(X)

Whether a variable or (sub)formula is undefined

Args:
    - X: The variable or (sub)formula
*%

%*! satisfied(X)

Whether a variable or (sub)formula is satisfied

Args:
    - X: The variable or (sub)formula
*%

%*! defined(C,ID)

Whether a table constraint is defined

Args:
    - 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

Args:
    - C: The table constraint identifier
    - ID: The identifier of the cross product of the column header variables
*%

%*! hit(C,ID,Pos)

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

Args:
    - 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)`
*%

%*! not_hit(C,ID,Row)

Whether a row of a table constraint is not satisfied

Args:
    - 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

Args:
    - C: The table constraint identifier
    - ID: The identifier of the cross product of the column header variables

*%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Output predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%*! include(X)

Whether a variable is included in the configuration

Args:
    - X: The variable (either a part or an attribute)
*%

%*! value(X,V)

The value of an attribute variable

Args:
    - X: The attribute variable
    - V: The value of the variable
*%

Encoding

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Input predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Parts and attributes %% Configuration variables %% Constraints %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Encoding predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Output predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

`examples/config/base/structure.lp` ¶

Source

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

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

`examples/config/base/discrete.lp` ¶

Source

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

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

`examples/config/base/clingo/integer.lp` ¶

Source

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

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

`examples/config/base/clingo/boolean.lp` ¶

Source

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

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

`examples/config/base/clingo/numerics.lp` ¶

Source

% Evaluate functions (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?

Encoding

Evaluate functions (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?

`examples/config/base/clingo/table.lp` ¶

Source

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

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)

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

`examples/config/base/constraints.lp` ¶

Source

% 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,ID).

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

`examples/config/base/clingo/user.lp` ¶

Source

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

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

`examples/config/base/show-clingo.lp` ¶

Source

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

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

Glossary ¶

`allow(Idx, P, 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)
`P`	A tuple `(COL,ROW)` identifying the column and row of the table
`V`	The value of the table entry

`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

`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

`constant(C)` ¶

Auxiliary predicate which defines a constant (string)

Parameter	Description
`C`	The constant as a string

`constraint(C, T)` ¶

Instantiates a constraint

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

`discrete(T)` ¶

Declares the part of a discrete attribute

Parameter	Description
`T`	The type of the attribute

`domain(T, V)` ¶

Declares a domain element of a discrete attribute

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

`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

`hit(C, ID, Pos)` ¶

Whether an entry of a table constraint is satisfied (only for fclingo 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)`

`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

`integer(T)` ¶

Declares the part of an integer attribute

Parameter	Description
`T`	The type of the attribute

`number(C, N)` ¶

Auxiliary predicate which defines a constant number

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

`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

`part(T)` ¶

Declares the type of a part

Parameter	Description
`T`	The type of the part

`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

`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

`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

`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

`undefined(X)` ¶

Whether a variable or (sub)formula is undefined

Parameter	Description
`X`	The variable or (sub)formula

`user_include(X)` ¶

An include statement from user input

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

`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

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

`include(X)` ¶

Whether a variable is included in the configuration

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

`value(X, V)` ¶

The value of an attribute variable

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

`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

`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

`defined(X)` ¶

Whether a variable or (sub)formula is defined

Parameter	Description
`X`	The variable or (sub)formula

`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

`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

`satisfied(X)` ¶

Whether a variable or (sub)formula is satisfied

Parameter	Description
`X`	The variable or (sub)formula

`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

`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

Product Configuration¶

Predicate Summary ¶

Encodings ¶

examples/config/encoding-base-clingo.lp ¶

examples/config/base/defined.lp ¶

examples/config/doc.lp ¶

examples/config/base/structure.lp ¶

examples/config/base/discrete.lp ¶

examples/config/base/clingo/integer.lp ¶

examples/config/base/clingo/boolean.lp ¶

examples/config/base/clingo/numerics.lp ¶

examples/config/base/clingo/table.lp ¶

examples/config/base/constraints.lp ¶

examples/config/base/clingo/user.lp ¶

examples/config/base/show-clingo.lp ¶

Glossary ¶

allow(Idx, P, V) ¶

binary(F, L, Op, R) ¶

column(C, ID, Col, X) ¶

constant(C) ¶

constraint(C, T) ¶

discrete(T) ¶

domain(T, V) ¶

function(F, Fun, Arg) ¶

hit(C, ID, Pos) ¶

index(X, I) ¶

integer(T) ¶

number(C, N) ¶

parent(X, P) ¶

part(T) ¶

range(T, Min, Max) ¶

set(S, X) ¶

type(X, T) ¶

unary(F, Op, F') ¶

undefined(X) ¶

user_include(X) ¶

user_value(X, V) ¶

violated(C) ¶

include(X) ¶

value(X, V) ¶

consistent(X) ¶

consistent(X, V) ¶

defined(X) ¶

defined(C, ID) ¶

not_hit(C, ID, Row) ¶

satisfied(X) ¶

satisfied(C, ID) ¶

undefined(C, ID) ¶

`examples/config/encoding-base-clingo.lp` ¶

`examples/config/base/defined.lp` ¶

`examples/config/doc.lp` ¶

`examples/config/base/structure.lp` ¶

`examples/config/base/discrete.lp` ¶

`examples/config/base/clingo/integer.lp` ¶

`examples/config/base/clingo/boolean.lp` ¶

`examples/config/base/clingo/numerics.lp` ¶

`examples/config/base/clingo/table.lp` ¶

`examples/config/base/constraints.lp` ¶

`examples/config/base/clingo/user.lp` ¶

`examples/config/base/show-clingo.lp` ¶

`allow(Idx, P, V)` ¶

`binary(F, L, Op, R)` ¶

`column(C, ID, Col, X)` ¶

`constant(C)` ¶

`constraint(C, T)` ¶

`discrete(T)` ¶

`domain(T, V)` ¶

`function(F, Fun, Arg)` ¶

`hit(C, ID, Pos)` ¶

`index(X, I)` ¶

`integer(T)` ¶

`number(C, N)` ¶

`parent(X, P)` ¶

`part(T)` ¶

`range(T, Min, Max)` ¶

`set(S, X)` ¶

`type(X, T)` ¶

`unary(F, Op, F')` ¶

`undefined(X)` ¶

`user_include(X)` ¶

`user_value(X, V)` ¶

`violated(C)` ¶

`include(X)` ¶

`value(X, V)` ¶

`consistent(X)` ¶

`consistent(X, V)` ¶

`defined(X)` ¶

`defined(C, ID)` ¶

`not_hit(C, ID, Row)` ¶

`satisfied(X)` ¶

`satisfied(C, ID)` ¶

`undefined(C, ID)` ¶