Skip to content

Commit

Permalink
refactored preprocessing encoding
Browse files Browse the repository at this point in the history
  • Loading branch information
@nrueh
nrueh committed Nov 29, 2024
1 parent 4d39c31 commit 310af01
Show file tree
Hide file tree
Showing 5 changed files with 296 additions and 295 deletions.
299 changes: 4 additions & 295 deletions src/coomsuite/encodings/preprocess.lp
View file
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".
22 changes: 22 additions & 0 deletions src/coomsuite/encodings/preprocess/defined.lp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
#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_unary/3.
#defined coom_path/3.
#defined coom_constant/1.
#defined coom_number/2.

#defined coom_function/4.
#defined coom_imply/3.
Loading

0 comments on commit 310af01

Please sign in to comment.