Skip to content

Commit

Permalink
adjusted fclingo encodings and tests
Browse files Browse the repository at this point in the history
  • Loading branch information
nrueh committed May 31, 2024
1 parent f4bdd3c commit 9199125
Show file tree
Hide file tree
Showing 12 changed files with 83 additions and 69 deletions.
4 changes: 2 additions & 2 deletions examples/coom/travel-bike.coom
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
product {
num .#/g 1-10000 totalWeight
num .#/kg 1-10 maxWeight
num .#/kg 10-10 maxWeight
num .#/l 0-200 totalVolume
num .#/l 0-200 requestedVolume
num .#/l 200-200 requestedVolume
Wheel frontWheel
Wheel rearWheel
Frame frame
Expand Down
2 changes: 1 addition & 1 deletion src/coomsolver/application.py
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@

def _get_valuation(model: Model) -> List[Symbol]:
return [
Function("val", assignment.arguments)
Function("value", assignment.arguments)
for assignment in model.symbols(theory=True)
if assignment.name == CSP
and len(assignment.arguments) == 2
Expand Down
7 changes: 0 additions & 7 deletions src/coomsolver/encodings/base/attribute-fclingo.lp

This file was deleted.

20 changes: 20 additions & 0 deletions src/coomsolver/encodings/base/attributes-fclingo.lp
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
% Always include root instance
include("root").

% Attribute variables are always included when its parents are included
include(X) :- type(X,T), parent(X,P), include(P), attribute(T,_).

range(X,Min,Max) :- type(X,T), attribute(T,"numeric"), Min = #min{ V : domain(T,V) },
Max = #max{ V : domain(T,V) }.

% Generate exactly one value for each attribute if it is included
{ value(X,V) : domain(T,V) } = 1 :- include(X), type(X,T), attribute(T,"discrete").
&in{Min..Max} =: X :- include(X), type(X,T), attribute(T,"numeric"), range(X,Min,Max).



% Show statements
#show .
#show value(X,V) : value(X,V), type(X,T), attribute(T,_).

&show { X : type(X,T), attribute(T,"numeric") }.
6 changes: 3 additions & 3 deletions src/coomsolver/encodings/base/auxiliary-fclingo.lp
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#include "boolean.lp".

% Auxiliary val/2 atoms for constants and numbers.
val(Path,Path) :- constant(Path).
&in{N..N} =: Path :- number(Path,N).
% Auxiliary values for constants and numbers.
value(Path,Path) :- constant(Path).
&in{N..N} =: Path :- number(Path,N).
2 changes: 1 addition & 1 deletion src/coomsolver/encodings/base/auxiliary.lp
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#include "boolean.lp".

% Auxiliary value/2 atoms for constants and numbers.
% Auxiliary values for constants and numbers.
value(P,P) :- constant(P).
value(P,N) :- number(P,N).
18 changes: 9 additions & 9 deletions src/coomsolver/encodings/base/constraints-fclingo.lp
Original file line number Diff line number Diff line change
@@ -1,17 +1,17 @@
#include "constraints.lp".

% Satisfaction of binary relations for numeric values in fclingo
def(F) :- binary(F,X1,_,X2), &df{X1}, &df{X2}.
defined(F) :- binary(F,X1,_,X2), &df{X1}, &df{X2}.

sat(F) :- binary(F,X1,"=", X2), &sum{X1} = X2.
sat(F) :- binary(F,X1,"!=",X2), &sum{X1} != X2.
sat(F) :- binary(F,X1,">", X2), &sum{X1} > X2.
sat(F) :- binary(F,X1,">=",X2), &sum{X1} >= X2.
sat(F) :- binary(F,X1,"<", X2), &sum{X1} < X2.
sat(F) :- binary(F,X1,"<=",X2), &sum{X1} <= X2.
satisfied(F) :- binary(F,X1,"=", X2), &sum{X1} = X2.
satisfied(F) :- binary(F,X1,"!=",X2), &sum{X1} != X2.
satisfied(F) :- binary(F,X1,">", X2), &sum{X1} > X2.
satisfied(F) :- binary(F,X1,">=",X2), &sum{X1} >= X2.
satisfied(F) :- binary(F,X1,"<", X2), &sum{X1} < X2.
satisfied(F) :- binary(F,X1,"<=",X2), &sum{X1} <= X2.


% Satisfaction of combinations tables for numeric values in fclingo
hit_cell(C,ID,(Col,Row)) :- allow(I,(Col,Row),V), combinations(C,ID,Col,X), &sum{X} = V, C=(I,_).
hit_cell(C,ID,(Col,Row)) :- allow(I,(Col,Row),V), column(C,ID,Col,X), &sum{X} = V, C=(I,_).

def(C,ID,Col) :- combinations(C,ID,Col,X), &df{X}.
defined(C,ID,Col) :- column(C,ID,Col,X), &df{X}.
20 changes: 10 additions & 10 deletions src/coomsolver/encodings/base/numeric-fclingo.lp
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
% Derive range for each numeric feature variable
range(X,Min,Max) :- feature(C,F,"num",_,_), range(C,F,Min,Max),
type(X,"num"), feature(X,F), parent(X,P), type(P,C).
range(X,Min,Max) :- range(C,N,Min,Max),
type(X,"num"), name(X,N), parent(X,P), type(P,C).

% Numeric variables are always included when its parents are included
included(X) :- type(X,"num"), parent(X,P), included(P).
include(X) :- type(X,"num"), parent(X,P), include(P).

% Assign a value to a numeric feature
&in{Min..Max} =: X :- type(X,"num"), range(X,Min,Max), included(X).
&in{Min..Max} =: X :- type(X,"num"), range(X,Min,Max), include(X).

% Evaluate functions (aggregates)
&sus{ 1,X : function_path(P,X), included(X) } =: F :- function(F,"count",P).
&sus{ X : function_path(P,X), included(X) } =: F :- function(F,"sum", P).
&min{ X : function_path(P,X), included(X) } =: F :- function(F,"min", P).
&max{ X : function_path(P,X), included(X) } =: F :- function(F,"max", P).
&sus{ 1,X : path(P,X), include(X) } =: F :- function(F,"count",P).
&sus{ X : path(P,X), include(X) } =: F :- function(F,"sum", P).
&min{ X : path(P,X), include(X) } =: F :- function(F,"min", P).
&max{ X : path(P,X), include(X) } =: F :- function(F,"max", P).

% Arithmetics
&sus{ XL; XR } =: F :- binary(F,XL,"+",XR).
Expand All @@ -25,7 +25,7 @@ included(X) :- type(X,"num"), parent(X,P), included(P).
% TODO: Add more arithmetics (division and power)

% Imply statements
&sus{ F } =: X :- imply(X,F), included(X).
&sus{ F } =: X :- imply(X,F), include(X).

% Show statement for numeric values
&show { X : type(X,"num"), included(X) }.
&show { X : type(X,"num"), include(X) }.
3 changes: 1 addition & 2 deletions src/coomsolver/encodings/fclingo-core.lp
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
#include "base/defined.lp".
#include "base/auxiliary-fclingo.lp".
#include "base/enumeration.lp".
#include "base/attribute-fclingo.lp".
#include "base/attributes-fclingo.lp".
#include "base/constraints-fclingo.lp".
6 changes: 3 additions & 3 deletions tests/test_main.py
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ def test_coom_output(self) -> None:
"""
Test the COOM output formatting.
"""
self.assertEqual(format_sym_coom(parse_term('included("carrier[0]")')), "carrier[0]")
self.assertEqual(format_sym_coom(parse_term('val("color[0]", "Blue")')), 'color[0] = "Blue"')
self.assertEqual(format_sym_coom(parse_term('val("wheel[0].size[0]", 27)')), "wheel[0].size[0] = 27")
self.assertEqual(format_sym_coom(parse_term('include("carrier[0]")')), "carrier[0]")
self.assertEqual(format_sym_coom(parse_term('value("color[0]", "Blue")')), 'color[0] = "Blue"')
self.assertEqual(format_sym_coom(parse_term('value("wheel[0].size[0]", 27)')), "wheel[0].size[0] = 27")
self.assertRaises(ValueError, format_sym_coom, parse_term('instance("")'))
4 changes: 2 additions & 2 deletions tests/test_sanity_checks.py
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,9 @@ def test_no_product(self) -> None:

program_enum_attr = """
coom_enumeration("a").
coom_attribute("a",b,"num").
coom_attribute("a","b","num").
coom_option("a", "a1").
coom_attribute_value("a","a1",b,1)."""
coom_attribute_value("a","a1","b",1)."""
run_test(deepcopy(TEST_EMPTY), program=program_enum_attr, profile="core")

def test_no_feature(self) -> None:
Expand Down
60 changes: 31 additions & 29 deletions tests/tests.py
Original file line number Diff line number Diff line change
Expand Up @@ -64,42 +64,42 @@ def holds_for(self, model: Model) -> bool:

TESTS: dict[str, dict[str, AnyType]] = {
"require_with_number": {
"test": Assert(All(), ContainsTheory(('val("root.wheel[0].size[0]",27)'))),
"ftest": Assert(All(), ContainsTheory('val("root.wheel[0].size[0]",27)', check_theory=True)),
"test": Assert(All(), ContainsTheory(('value("root.wheel[0].size[0]",27)'))),
"ftest": Assert(All(), ContainsTheory('value("root.wheel[0].size[0]",27)', check_theory=True)),
"files": ["require_with_number.lp"],
},
"require_with_number_ge": {
"test": Assert(All(), ContainsTheory(('val("root.wheel[0].size[0]",28)'))),
"ftest": Assert(All(), ContainsTheory('val("root.wheel[0].size[0]",28)', check_theory=True)),
"test": Assert(All(), ContainsTheory(('value("root.wheel[0].size[0]",28)'))),
"ftest": Assert(All(), ContainsTheory('value("root.wheel[0].size[0]",28)', check_theory=True)),
"files": ["require_with_number_ge.lp"],
},
"require_with_constant": {
"test": Assert(All(), Contains(('val("root.wheel[0]","W28")'))),
"test": Assert(All(), Contains(('value("root.wheel[0]","W28")'))),
"files": ["require_with_constant.lp"],
},
"require_two_wheels": {
"test": AndTest(
Assert(
Exact(1),
SupersetOf({('val("root.frontWheel[0].size[0]",27)'), ('val("root.rearWheel[0].size[0]",27)')}),
SupersetOf({('value("root.frontWheel[0].size[0]",27)'), ('value("root.rearWheel[0].size[0]",27)')}),
),
Assert(
Exact(1),
SupersetOf({('val("root.frontWheel[0].size[0]",28)'), ('val("root.rearWheel[0].size[0]",28)')}),
SupersetOf({('value("root.frontWheel[0].size[0]",28)'), ('value("root.rearWheel[0].size[0]",28)')}),
),
),
"ftest": AndTest(
Assert(
Exact(1),
SupersetOfTheory(
{('val("root.frontWheel[0].size[0]",27)'), ('val("root.rearWheel[0].size[0]",27)')},
{('value("root.frontWheel[0].size[0]",27)'), ('value("root.rearWheel[0].size[0]",27)')},
check_theory=True,
),
),
Assert(
Exact(1),
SupersetOfTheory(
{('val("root.frontWheel[0].size[0]",28)'), ('val("root.rearWheel[0].size[0]",28)')},
{('value("root.frontWheel[0].size[0]",28)'), ('value("root.rearWheel[0].size[0]",28)')},
check_theory=True,
),
),
Expand All @@ -108,25 +108,25 @@ def holds_for(self, model: Model) -> bool:
},
"condition": {
"test": Assert(
All(), Implies(Contains('val("root.wheelSupport[0]","True")'), Contains('val("root.wheel[0]","Small")'))
All(), Implies(Contains('value("root.wheelSupport[0]","True")'), Contains('value("root.wheel[0]","Small")'))
),
"files": ["condition.lp"],
},
"combination": {
"test": AndTest(
Assert(Any(), SupersetOf({'val("root.wheelSupport[0]","False")', 'val("root.wheel[0]","W20")'})),
Assert(Any(), SupersetOf({'val("root.wheelSupport[0]","False")', 'val("root.wheel[0]","W18")'})),
Assert(Any(), SupersetOf({'val("root.wheelSupport[0]","True")', 'val("root.wheel[0]","W16")'})),
Assert(Any(), SupersetOf({'val("root.wheelSupport[0]","True")', 'val("root.wheel[0]","W14")'})),
Assert(Any(), SupersetOf({'value("root.wheelSupport[0]","False")', 'value("root.wheel[0]","W20")'})),
Assert(Any(), SupersetOf({'value("root.wheelSupport[0]","False")', 'value("root.wheel[0]","W18")'})),
Assert(Any(), SupersetOf({'value("root.wheelSupport[0]","True")', 'value("root.wheel[0]","W16")'})),
Assert(Any(), SupersetOf({'value("root.wheelSupport[0]","True")', 'value("root.wheel[0]","W14")'})),
Assert(Exact(4), True_()),
),
"files": ["combination.lp"],
},
"enumeration": {
"test": AndTest(
Assert(Exact(1), Contains('val("root.color[0]","Red")')),
Assert(Exact(1), Contains('val("root.color[0]","Green")')),
Assert(Exact(1), Contains('val("root.color[0]","Blue")')),
Assert(Exact(1), Contains('value("root.color[0]","Red")')),
Assert(Exact(1), Contains('value("root.color[0]","Green")')),
Assert(Exact(1), Contains('value("root.color[0]","Blue")')),
Assert(Exact(3), True_()),
),
"program": """
Expand All @@ -140,19 +140,21 @@ def holds_for(self, model: Model) -> bool:
},
"bool_enumeration": {
"test": AndTest(
Assert(Exact(1), Contains('val("root.boolean[0]","True")')),
Assert(Exact(1), Contains('val("root.boolean[0]","False")')),
Assert(Exact(1), Contains('value("root.boolean[0]","True")')),
Assert(Exact(1), Contains('value("root.boolean[0]","False")')),
Assert(Exact(2), True_()),
),
"program": """
coom_structure("product").
coom_feature("product","boolean","bool",1,1).""",
},
"attribute": {
"test": Assert(Exact(1), SupersetOfTheory({'val("root.wheel[0].size[0]",14)', 'val("root.wheel[0]","W14")'})),
"test": Assert(
Exact(1), SupersetOfTheory({'value("root.wheel[0].size[0]",14)', 'value("root.wheel[0]","W14")'})
),
"ftest": Assert(
Exact(1),
SupersetOfTheory({'val("root.wheel[0].size[0]",14)', 'val("root.wheel[0]","W14")'}, check_theory=True),
SupersetOfTheory({'value("root.wheel[0].size[0]",14)', 'value("root.wheel[0]","W14")'}, check_theory=True),
),
"program": """
coom_structure("product").
Expand All @@ -165,7 +167,7 @@ def holds_for(self, model: Model) -> bool:
},
"structure": {
"test": AndTest(
Assert(Exact(1), Contains('included("root.wheel[0]")')),
Assert(Exact(1), Contains('include("root.wheel[0]")')),
Assert(Exact(1), True_()),
),
"program": """
Expand All @@ -175,7 +177,7 @@ def holds_for(self, model: Model) -> bool:
},
"structure_optional": {
"test": AndTest(
Assert(Exact(1), Contains('included("root.basket[0]")')),
Assert(Exact(1), Contains('include("root.basket[0]")')),
Assert(Exact(2), True_()),
),
"program": """
Expand All @@ -187,7 +189,7 @@ def holds_for(self, model: Model) -> bool:
"test": AndTest(
Assert(
Exact(1),
SupersetOf({'included("root.carrier[0]")', 'included("root.carrier[0].bag[0]")'}),
SupersetOf({'include("root.carrier[0]")', 'include("root.carrier[0].bag[0]")'}),
),
Assert(Exact(1), True_()),
),
Expand All @@ -200,15 +202,15 @@ def holds_for(self, model: Model) -> bool:
},
"structure_nested_optional": {
"test": AndTest(
Assert(Exact(3), Contains('included("root.carrier[0]")')),
Assert(Exact(2), Contains('included("root.carrier[0].bag[0]")')),
Assert(Exact(3), Contains('include("root.carrier[0]")')),
Assert(Exact(2), Contains('include("root.carrier[0].bag[0]")')),
Assert(
Exact(1),
SupersetOf(
{
'included("root.carrier[0]")',
'included("root.carrier[0].bag[0]")',
'included("root.carrier[0].bag[1]")',
'include("root.carrier[0]")',
'include("root.carrier[0].bag[0]")',
'include("root.carrier[0].bag[1]")',
}
),
),
Expand Down

0 comments on commit 9199125

Please sign in to comment.