generated from potassco/python-project-template
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #27 from potassco/nico/fragments
Nico/fragments
- Loading branch information
Showing
11 changed files
with
360 additions
and
302 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,56 @@ | ||
# COOM language fragments | ||
As covered by our encodings | ||
|
||
## **COOM core** | ||
### Configuration tree / Product hierarchy | ||
- Root is `product` with features | ||
- Every feature has cardinality 1 | ||
- Only features allowed are `enumeration` | ||
- which can have `attribute` | ||
|
||
### Constraints | ||
- `behavior` | ||
- `require` and `require` with single `condition` (both not nested) | ||
- Binary comparison operators: `=`, `!=`, `<`, `<=`, `>`, `>=` | ||
- Unary logical operators: `!`, `()` | ||
- Binary logical operators: `||`, `&&` | ||
- *Example*: `require ! (color = Red && size = XXL)` | ||
- `combinations` | ||
- only `allow` | ||
- `forbid` not yet implemented | ||
- table entries can be tuples | ||
- wildcard `-*-` supported | ||
|
||
## COOM[P] | ||
Everything from **COOM core** plus | ||
|
||
### Configuration tree / Product hierarchy | ||
- Features can have cardinalities (`0..1 Basket basket`) | ||
- No open cardinalities | ||
- Features can also be `structure` | ||
|
||
### Constraints | ||
- Constraints can be specified locally for a structure, eg. `behavior Bag {...}` | ||
- This enables longer path expressions, eg. `carrier.bag.capacity.volume` | ||
|
||
## COOM[X] | ||
Everything from **COOM[P]** plus | ||
|
||
### Configuration tree / Product hierarchy | ||
- Features can be numeric, eg. `num .#/g 1-10000 totalWeight` | ||
- no open ranges | ||
- number of decimals and SI units have no effect | ||
|
||
### Constraints | ||
- Aggregate functions (`count`, `sum`, `min`, `max`) | ||
- Arithmetics | ||
- Unary: `()`, `+`, `-` | ||
- Binary: `+`, `-`, `*` | ||
- no support yet for `/` and `^` | ||
- fclingo only supports linear calculations (no multiplication of two variables) | ||
|
||
|
||
|
||
## Future work | ||
- Open cardinalities | ||
- Open numeric intervals |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,295 +1,4 @@ | ||
%%% Instantiate complete instance tree | ||
% Root is always included | ||
type_aux((),"product") :- coom_structure("product"). | ||
|
||
% Create auxiliary predicate for every feature | ||
type_aux((F,(X,I)),T) :- coom_feature(Ctx,F,T,_,Max), type_aux(X,Ctx), I = 0..Max-1, T != "num". | ||
type_aux((F,(X,I)),@join(Ctx,F)) :- coom_feature(Ctx,F,"num",_,Max), type_aux(X,Ctx), I = 0..Max-1. | ||
|
||
% Create auxiliary prediate for attribute variables | ||
type_aux((A,(X,0)),A) :- type_aux(X,T), coom_enumeration(T), coom_attribute_value(T,_,A,_). | ||
|
||
|
||
%%% Constraints | ||
% Get formula context | ||
formula_context(F,Ctx) :- coom_binary(F,_,_,_), coom_require(C,F), coom_context(C,Ctx). | ||
formula_context(F,Ctx) :- coom_binary(F,_,_,_), coom_condition(C,F), coom_context(C,Ctx). | ||
formula_context(F,Ctx) :- coom_binary(F,_,_,_), coom_imply(C,_,F), coom_context(C,Ctx). | ||
|
||
formula_context(F,Ctx) :- coom_unary(F,_,_), coom_require(C,F), coom_context(C,Ctx). | ||
formula_context(F,Ctx) :- coom_unary(F,_,_), coom_condition(C,F), coom_context(C,Ctx). | ||
formula_context(F,Ctx) :- coom_unary(F,_,_), coom_imply(C,_,F), coom_context(C,Ctx). | ||
|
||
formula_context(L,Ctx) :- coom_binary(L,_,_,_), coom_binary(F,L,_,_), formula_context(F,Ctx). | ||
formula_context(R,Ctx) :- coom_binary(R,_,_,_), coom_binary(F,_,_,R), formula_context(F,Ctx). | ||
|
||
formula_context(L,Ctx) :- coom_unary(L,_,_), coom_binary(F,L,_,_), formula_context(F,Ctx). | ||
formula_context(R,Ctx) :- coom_unary(R,_,_), coom_binary(F,_,_,R), formula_context(F,Ctx). | ||
|
||
formula_context(F',Ctx) :- coom_binary(F',_,_,_), coom_unary(F,_,F'), formula_context(F,Ctx). | ||
formula_context(F',Ctx) :- coom_unary(F',_,_), coom_unary(F,_,F'), formula_context(F,Ctx). | ||
|
||
% Instantiate paths | ||
path_start(X,P) :- coom_binary(F,P,_,_), coom_path(P,0,_), type_aux(X,Ctx), formula_context(F,Ctx). | ||
path_start(X,P) :- coom_binary(F,_,_,P), coom_path(P,0,_), type_aux(X,Ctx), formula_context(F,Ctx). | ||
path_start(X,P) :- coom_unary(F,_,P), coom_path(P,0,_), type_aux(X,Ctx), formula_context(F,Ctx). | ||
path_start(X,P) :- coom_combinations(C,_,P), coom_path(P,0,_), type_aux(X,Ctx), coom_context(C,Ctx). | ||
path_start(X,P) :- coom_function(Ctx,_,_,P), coom_path(P,0,_), type_aux(X,Ctx). | ||
path_start(X,P) :- coom_imply(C,P,_), coom_path(P,0,_), type_aux(X,Ctx), coom_context(C,Ctx). | ||
|
||
% Determine all ground paths | ||
path_to(X,P,0,X') :- coom_path(P,0,N), | ||
path_start(X,P), type_aux(X',_), X' =(N,(X,_)). | ||
path_to(X,P,I,X'') :- coom_path(P,I,N), | ||
path_to(X,P,I-1,X'), type_aux(X'',_), X''=(N,(X',_)). | ||
|
||
path_to(X,P,@dotpath(X')) :- not coom_path(P,I+1,_), path_to(X,P,I,X'). | ||
|
||
% Constants and numbers | ||
path_to(X,P,P) :- coom_binary(F,_,_,P), coom_constant(P), formula_context(F,T), type_aux(X,T). | ||
path_to(X,P,P) :- coom_binary(F,P,_,_), coom_constant(P), formula_context(F,T), type_aux(X,T). | ||
path_to(X,P,P) :- coom_binary(F,_,_,P), coom_number(P,_), formula_context(F,T), type_aux(X,T). | ||
path_to(X,P,P) :- coom_binary(F,P,_,_), coom_number(P,_), formula_context(F,T), type_aux(X,T). | ||
|
||
% Instantiate binaries and unaries | ||
binary(X,F,@binary(XL,Op,XR),XL,Op,XR) :- coom_binary(F,L,Op,R), | ||
formula_context(F,C), | ||
type_aux(X,C), path_to(X,L,XL), path_to(X,R,XR). | ||
|
||
unary(X,F,@unary(X',Op),Op,X') :- coom_unary(F,Op,F'), | ||
formula_context(F,C), | ||
type_aux(X,C), path_to(X,F',X'). | ||
|
||
ground_formula(X,F,G) :- binary(X,F,G,_,_,_). | ||
ground_formula(X,F,G) :- unary(X,F,G,_,_). | ||
|
||
% Default binaries for arithmetics if one side is undefined | ||
% TODO: Does this always give desired behavior? | ||
ground_formula(X,F,XL) :- coom_binary(F,L,"+",R), | ||
formula_context(F,C), | ||
type_aux(X,C), path_to(X,L,XL), not path_to(X,R,_). | ||
|
||
ground_formula(X,F,XR) :- coom_binary(F,L,"+",R), | ||
formula_context(F,C), | ||
type_aux(X,C), not path_to(X,L,_), path_to(X,R,XR). | ||
|
||
|
||
% Instantiate functions | ||
function(X,F,T,P) :- coom_function(C,F,T,P), type_aux(X,C). | ||
|
||
% Auxiliary paths for formulas and functions | ||
path_to(X,F,G) :- ground_formula(X,F,G). | ||
path_to(X,F,@function(T,X,P)) :- function(X,F,T,P). | ||
|
||
% Auxiliary paths for cardinalities | ||
path_to(X,N,@dotpath(X')) :- coom_feature(Ctx,N,_,_,_), type_aux(X,Ctx), type_aux(X',_), X' =(N,(X,_)). | ||
path_to(X,A,@dotpath(X')) :- coom_attribute(T,A,_), type_aux(X,T), type_aux(X',_), X' =(A,(X,_)). | ||
|
||
% Instantiate conditional requirements | ||
conditional_requirement(C,G,G') :- coom_context(C,Ctx), coom_condition(C,F), ground_formula(X,F,G), | ||
type_aux(X,Ctx), coom_require(C,F'), ground_formula(X,F',G'). | ||
|
||
% Instantiate combination tables | ||
table(C,X) :- coom_combinations(C,_,_), coom_context(C,Ctx), type_aux(X,Ctx). | ||
|
||
combinations_tuple((C,Ctx),Col,(X,())) :- table(C,Ctx), | ||
coom_combinations(C,Col,P), not coom_combinations(C,Col+1,_), | ||
path_to(Ctx,P,X). | ||
combinations_tuple((C,Ctx),Col,(X',X)) :- combinations_tuple((C,Ctx),Col+1,X), | ||
coom_combinations(C,Col,P), Col >= 0, | ||
path_to(Ctx,P,X'). | ||
combinations_tuple(C,CT) :- combinations_tuple(C,0,CT). | ||
|
||
tuple_order(C,CT,ID) :- combinations_tuple(C,CT), ID = #count{ CT': combinations_tuple(C,CT'), CT'<CT }. | ||
|
||
in_tuple((X,CT'),CT',X) :- combinations_tuple(_,CT), CT=(X,CT'). | ||
in_tuple(CT,CT',X) :- in_tuple(CT,(X,CT'),_). | ||
in_tuple(CT,X) :- in_tuple(CT,_,X). | ||
|
||
% Instantiate imply statements | ||
imply(C,X',G) :- coom_imply(C,P,F), coom_context(C,Ctx), type_aux(X,Ctx), path_to(X,P,X'), ground_formula(X,F,G). | ||
imply(C,X',@function(T,X,P')) :- coom_imply(C,P,F), coom_context(C,Ctx), type_aux(X,Ctx), path_to(X,P,X'), function(X,F,T,P'). | ||
|
||
% Instantiate attribute constraints | ||
attribute_constraint((T,X)) :- coom_attribute(T,_,_), type(X,T). | ||
attribute_constraint_column(T,Col+1,A) :- coom_attribute(T,A,_), Col = #count{ A' : coom_attribute(T,A',_), A' < A }. | ||
|
||
% Instantiate cardinality constraints | ||
cardinality_aux(X,N,Min) :- coom_feature(C,N,_,Min,_), type_aux(X,C). | ||
cardinality_aux(X,A,1) :- coom_attribute(T,A,_), type_aux(X,T). | ||
|
||
% Always include boolean enumeration | ||
coom_enumeration("bool"). | ||
coom_option("bool", "True"). | ||
coom_option("bool", "False"). | ||
|
||
|
||
%%% Output atoms | ||
% Attributes of the model (enumerations and numeric features in COOM) | ||
discrete(T) :- coom_enumeration(T). | ||
domain(T,V) :- coom_option(T,V). | ||
|
||
% Enumeration attributes | ||
discrete(@join(T,A)) :- coom_attribute(T,A,"str"). | ||
domain(@join(T,A),V) :- coom_attribute_value(T,_,A,V), coom_attribute(T,A,"str"). | ||
|
||
integer(@join(T,A)) :- coom_attribute(T,A,"num"), not discrete. | ||
range(@join(T,A),Min,Max) :- coom_attribute(T,A,"num"), not discrete, | ||
Min = #min { V: coom_attribute_value(T,_,A,V) }, | ||
Max = #max { V: coom_attribute_value(T,_,A,V) }. | ||
|
||
% Temporary fix: For clingo, huge ranges might make grounding to large, translate numeric attributes to discrete attributes | ||
discrete(@join(T,A)) :- coom_attribute(T,A,"num"), discrete. | ||
domain(@join(T,A),V) :- coom_attribute_value(T,_,A,V), coom_attribute(T,A,"num"), discrete. | ||
|
||
% Numeric features | ||
integer(@join(Ctx,N)) :- coom_feature(Ctx,N,"num",_,_). | ||
range(@join(Ctx,N),Min,Max) :- coom_feature(Ctx,N,"num",_,_), coom_range(Ctx,N,Min,Max). | ||
|
||
#show discrete/1. | ||
#show domain/2. | ||
|
||
#show integer/1. | ||
#show range/3. | ||
|
||
% Instances (of structures, enumerations and attributes in COOM) | ||
type("root","product") :- coom_structure("product"). | ||
|
||
type(@dotpath(X),T) :- type_aux(X,T), not coom_attribute(_,T,_). | ||
type(@dotpath(X),@join(T,A)) :- type_aux(X,A), coom_attribute(T,A,_), type_aux(P,T), X=(_,(P,_)). | ||
|
||
index(@dotpath(X),Idx) :- type_aux(X,T), X=((_,(_,Idx))). | ||
parent(@dotpath(X),@dotpath(P)) :- type_aux(X,_), X=(_,(P,_)). | ||
|
||
#show type/2. | ||
#show index/2. | ||
#show parent/2. | ||
|
||
%%% Constraints | ||
% Formulas | ||
constraint((C,G),"boolean") :- coom_require(C,F), ground_formula(_,F,G), not coom_condition(C,_). | ||
|
||
constraint((C,@implication(Con,Req)),"boolean") :- conditional_requirement(C,Con,Req). | ||
binary(@implication(Con,Req),@neg(Con),"||",Req) :- conditional_requirement(_,Con,Req). | ||
unary(@neg(Con),"!",Con) :- conditional_requirement(_,Con,Req). | ||
|
||
binary(G,L,Op,R) :- binary(_,_,G,L,Op,R). | ||
unary(G,Op,F) :- unary(_,_,G,Op,F). | ||
|
||
#show constraint/2. | ||
#show binary/4. | ||
#show unary/3. | ||
|
||
% Table constraints | ||
constraint((C,@dotpath(X)),"table") :- table(C,X). | ||
column((C,@dotpath(X)),ID,Col,@dotpath(X')) :- coom_combinations(C,Col,P), | ||
path_to(X,P,X'), in_tuple(CT,X'), tuple_order((C,X),CT,ID). | ||
allow(C,XY,V) :- coom_allow(C,XY,V). | ||
|
||
#show column/4. | ||
#show allow/3. | ||
|
||
% Attribute constraints | ||
% table constraint guarantees that correct values are assigned to enumeration attributes | ||
constraint(C,"table") :- attribute_constraint(C). | ||
column((T,X),0,0,X) :- attribute_constraint((T,X)). | ||
column((T,P),0,Col,X) :- attribute_constraint((T,P)), parent(X,P), type(X,@join(T,A)), attribute_constraint_column(T,Col,A). | ||
|
||
allow(T,(0,I),O) :- attribute_constraint((T,_)), coom_option(T,O), I = #count{ O' : coom_option(T,O'), O' < O}. | ||
allow(T,(Col,Row),V) :- attribute_constraint((T,_)), allow(T,(0,Row),O), coom_attribute_value(T,O,A,V), attribute_constraint_column(T,Col,A). | ||
|
||
% Imply statements | ||
constraint((C,@binary(X',"=",G)),"boolean") :- imply(C,X',G). | ||
binary(@binary(X',"=",G),X',"=",G) :- imply(C,X',G). | ||
|
||
% Functions | ||
function(@function(T,X,P),T,@join(X,P)) :- function(X,_,T,P). | ||
set(@join(X,P),X') :- function(X,_,_,P), path_to(X,P,X'). | ||
|
||
#show function/3. | ||
#show set/2. | ||
|
||
% Partonomy and cardinality constraints | ||
part(T) :- coom_structure(T). | ||
|
||
constraint((@join(X,N),Min),"lowerbound") :- cardinality_aux(X,N,Min). | ||
set(@join(X,N),X') :- cardinality_aux(X,N,_), path_to(X,N,X'). | ||
|
||
#show part/1. | ||
|
||
% Constants and numbers | ||
constant(C) :- coom_constant(C). | ||
number(C,N) :- coom_number(C,N). | ||
|
||
#show constant/1. | ||
#show number/2. | ||
|
||
% Python helper functions | ||
#script (python) | ||
from clingo import String, SymbolType | ||
import math | ||
|
||
def dotpath(path): | ||
if path.type in (SymbolType.String, SymbolType.Number): | ||
return path | ||
path = unpack(path, []) | ||
return String(".".join(["root"]+[f"{p[0]}[{p[1]}]" for p in path])) | ||
|
||
def unpack(p, l): | ||
""" | ||
Recursively unpacks a nested path expression into a list of tuples. | ||
""" | ||
if str(p) != "()": | ||
t = (p.arguments[0].string, str(p.arguments[1].arguments[1].number)) | ||
l.insert(0, t) | ||
unpack(p.arguments[1].arguments[0], l) | ||
return l | ||
|
||
def binary(l,op,r): | ||
return String(f"{l.string}{op.string}{r.string}") | ||
|
||
def unary(f,op): | ||
if op.string == "()": | ||
return String(f"({f.string})") | ||
else: | ||
return String(f"{op.string}{f.string}") | ||
|
||
def join(p1,p2): | ||
context = dotpath(p1).string | ||
if context == "": | ||
return p2 | ||
else: | ||
return String(f"{context}.{p2.string}") | ||
|
||
def function(f,c,p): | ||
joined = join(c,p).string | ||
return String(f"{f.string}({joined})") | ||
|
||
def implication(a,b): | ||
return String(f"{neg(a).string}||{b.string}") | ||
|
||
def neg(a): | ||
return String(f"!{a.string}") | ||
#end. | ||
|
||
#defined coom_structure/1. | ||
#defined coom_feature/5. | ||
#defined coom_range/4. | ||
#defined coom_enumeration/1. | ||
#defined coom_option/2. | ||
#defined coom_attribute/3. | ||
#defined coom_attribute_value/4. | ||
|
||
#defined coom_behavior/1. | ||
#defined coom_context/2. | ||
#defined coom_require/2. | ||
#defined coom_condition/2. | ||
#defined coom_combinations/3. | ||
#defined coom_allow/3. | ||
#defined coom_binary/4. | ||
#defined coom_path/3. | ||
#defined coom_constant/1. | ||
#defined coom_number/2. | ||
|
||
#defined coom_function/4. | ||
#defined coom_imply/3. | ||
#include "preprocess/instantiate.lp". | ||
#include "preprocess/output.lp". | ||
#include "preprocess/python.lp". | ||
#include "preprocess/defined.lp". |
Oops, something went wrong.