diff --git a/README.md b/README.md index c70d5eb..10844cb 100644 --- a/README.md +++ b/README.md @@ -10,13 +10,313 @@ pip install . -r requirements.txt ## Usage +fclingo is a solver for Answer Set Programming (ASP) combined with founded conditional linear constraints. These constraints enable the user to use integer variables that are not subject to grounding. Integer variables may be undefined and, in line with the philosophy of ASP, there needs to be a justification in the logic program if a variable receives a value in an answer set. Conditionality allows for a generalization of aggregates commonly used in ASP. + +### Relation to clingo +fclingo is an extension of [clingo](https://github.com/potassco/clingo) and accepts as input clingo rules enriched with founded conditional linear constraints. + +### Relation to clingcon +fclingo relies on the constraint answer set programming (CASP) solver [clingcon](https://github.com/potassco/clingo) into whose language a fclingo program is translated. fclingo's two main advantages are foundedness of the integer variables and aggregates over integer variables. The former allows variables to be undefined and only assume a value if a reason for that value can be derived. This differs to the behavior of CASP, where variables are always defined and in absence of any constraint to a variable, all possible values are enumerated. The latter generalizes ASP aggregates to contain integer variables that are not subject to grounding. + +### Assignments +The answer sets of fclingo programs contain atoms `val(x,v)`, where `x` is a integer variable occurring in the program and `v` is the integer value of the variable in the answer set. The absence of such an atom means the variable is undefined. + +### Language overview +fclingo atoms have the following form: +1. `&sum{lt1 : c1;...;ltn : cn} <> l0` +2. `&sus{lt1 : c1;...;ltn : cn} <> l0` +3. `&in{lb..ub} =: x` +4. `&df{x}` +5. `&min{lt1 : c1;...;ltn : cn} <> l0` +6. `&max{lt1 : c1;...;ltn : cn} <> l0` + +where `lti`, `lb`, and `ub` are linear terms, +`ci` is a conjunction of literals for `i` between 0 and `n`, `x` is the name of a variable and `<>` is either `<=`,`=`,`!=`,`<`,`>`, or `>=`. + +To hide and show assignments of specific variables, one can use the directive `&show{v1/a1;...;vn/an}`, where `vi` is the name of the function and `ai` is the arity of the function. For instance, the term `x/0` shows the variable named `x` while `price/1` shows all variables of the form `price()`. Absence of this directive shows all variables, and `&show{}` hides all variables. + +### 1. Sum under clingo semantics +The atom in 1. sums up all linear terms in the set. It can be seen as a generalization of clingo sum aggregates as it similarly removes undefined elements, and therefore always returns a value. It can be used in the head and in the body. + +For example, +``` +price(frame,15). +price(bag,5). + + selected(frame). +{ selected(bag) }. + +&sum{V} = price(P) :- selected(P), price(P,V). +&sum{price(P) : selected(P)} = price(total). + +#show selected/1. +&show{price/1}. +``` +This program configures a bike with a frame that has an optional bag. For both the frame and the optional bag prices are provided, stored in integer variables and then summed up to get the total price. + +Executing ```shell -fclingo -h +fclingo examples/config_optional.lp +``` +yields the answer sets +``` +Answer: 1 +selected(frame) val(price(total),15) val(price(frame),15) +Answer: 2 +selected(frame) selected(bag) val(price(bag),5) val(price(total),20) val(price(frame),15) +``` +As expected, we have two answer sets. The first does not select the optional bag and calculates the total price as 15, same as the price of the frame. The second selects the bag and increases the total price to 20. + +To see the behavior in presence of undefined integer variables, consider following example +``` +price(frame,15). + +pricelimit(14). + + selected(frame). +{ selected(bag) }. + +&sum{V} = price(P) :- selected(P), price(P,V). +:- &sum { price(P) : selected(P) } >= L, + pricelimit(L). + +#show selected/1. +&show{price/1}. +``` +Now, the price of the bag is omitted and instead of calculating the total price, we restrict the sum over the individual prices to be 14. +The call +``` +fclingo examples/config_pricelimit_sum.lp 0 +``` +returns +``` +UNSATISFIABLE +``` +Even if the price for the bag is undefined, the constraint detects that the price limit is breached since the undefined integer variable is removed from the set. + +### 2. Sum under strict semantics + +The atom in 2. sums up the linear terms for the conditions that are true. In contrast to 1., if any of the terms is undefined, resulting from an integer variable being undefined that is contained within, the sum is undefined as well. This results in the atom being false. We will later elaborate how this version of sum is useful for assignments later in this document. The atom may be used in the head or in the body. + +The example `examples/config_optional.lp` behaves identically when we replace `sus` with `sum`. + +Different behavior arises for the price limit. +``` +price(frame,15). + +pricelimit(14). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +:- &sus { price(P) : selected(P) } >= L, + pricelimit(L). + +#show selected/1. +&show{price/1}. +``` + +The call +``` +fclingo examples/config_pricelimit_sus.lp 0 +``` +now returns +``` +Answer: 1 +selected(frame) selected(bag) val(price(frame),15) +``` +The answer with only the frame is removed because its price alone is higher than the limit. +However, when the bag is selected, its price value is undefined and therefore the sum under strict semantics returns undefined as well and the price limit is disregarded. + +### 3. Assignments + +The atom in 3. is a directional assignment of a value between linear terms `lb` and `ub` to the variable `x`. It may only be used in the head of a rule. Only if `lb` and `ub` are defined, `x` will receive a value in between `lb` and `ub`. Note that this is different from using equality to assign a value. For instance, the fact `&sus{y}=x.` would allow `y` as well as `x` to be defined and take on arbitrary values such that `x` and `y` are equal, while `&in{y..y}=:x.` requires some other rule to define `y` and if that is not the case, `x` remains undefined. +One can also use the strict sum and write `&sus{lt1 : c1;..;ltn : cn}=:x`, where `lti` are linear terms conditioned by conjuctions `ci` for `i` between 1 and `n`, and `x` is an integer variable. Using the strict sum that way has two advantages: first, the strict sum can be undefined in contrast to the clingo sum and thefore `x` only receives a value if the strict sum can be calculated, and second, the linear terms may be conditioned and the arity of the sum can be arbitrary. + +For instance, take program +``` +price(frame,15). +default_range(1,2). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +&in{L..U} =: price(P) :- selected(P), not price(P,_), + default_range(L,U). +&sus{price(P) : selected(P)} =: price(total). + +#show selected/1. +&show{price/1}. +``` + +Here, we assign selected parts that are missing the price information a default within a certain range. +Calling + +``` +fclingo examples/config_default_in.lp 0 +``` +results in +``` +Answer: 1 +selected(frame) val(price(total),15) val(price(frame),15) +Answer: 2 +selected(frame) selected(bag) val(price(total),16) val(price(frame),15) val(price(bag),1) +Answer: 3 +selected(frame) selected(bag) val(price(total),17) val(price(frame),15) val(price(bag),2) +``` +were in answers 2 and 3, the two possible defaults for the missing price information of the selected bag is used. + +### 4. Defined + +The atom in 4. may be used in the body to reason about whether a given variable `x` is defined or not. This is useful for instance to provide defaults or detect errors if a certain integer variable does not have a value but should. + +For instance, program +``` +price(frame,15). + +default_price(20). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +&sus{price(P) : selected(P)} =: calc_price(total). + +&sus{price(total)} = calc_price(total) :- &df{calc_price(total)}. +&sus{price(total)} = D :- not &df{calc_price(total)}, + default_price(D). + +#show selected/1. +&show{price/1}. +``` +first tries to calculate the price, and if this calculation has a defined outcome, it is assigned to the total price. If not, a default price is used. + +Calling +``` +fclingo examples/config_default_in.lp 0 +``` +yields the intended two answer sets +``` +Answer: 1 +selected(frame) selected(bag) val(price(frame),15) val(price(total),20) +Answer: 2 +selected(frame) val(price(frame),15) val(price(total),15) +``` +where Answer 1 makes use of the default because the price of the bag is missing and therefore the total price may not be calculated. + +### 5./6. Minimum and maximum aggregates + +Atoms in 5. and 6. determine the minimum and maximum among linear terms in the set that have a defined value, respectively. They may be used in the head as well as in the body. + +``` +price(frame,15). part(frame). +price(bag,5). part(bag). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +&sus{price(P) : selected(P)} = price(total). + +min_price(P) :- &min{price(P') : selected(P')} = price(P), + part(P). +max_price(P) :- &max{price(P') : selected(P')} = price(P), + part(P). + +#show selected/1. +#show min_price/1. +#show max_price/1. +&show{price/1}. +``` +Here, atoms `min_price/1` and `max_price/1` query what selected part has the minimum and the maximum value, respectively. + +The call +``` +fclingo config_minmax_price.lp 0 +``` +yields +``` +Answer: 1 +selected(frame) min_price(frame) max_price(frame) val(price(total),15) val(price(frame),15) +Answer: 2 +selected(frame) selected(bag) min_price(bag) max_price(frame) val(price(total),20) val(price(frame),15) val(price(bag),5) +``` +When the bag is not selected, the frame has the minimum and maximum price. In the second answer, we see that the bag has the minimum price among selected parts, while the frame's price is the maximum. + +### Choices +Similarly to the language of clingo, fclingo allows for choice rules in the head of a rule. Choices have the following form: ``` +&fun{ lt1 :: ca1 : c1;...ltn :: can : cn} <> lt0 +``` +where `fun` is either `sum`, `sus`, `min`, or `max`, +`lti` are linear terms, `cai` are regular atoms that may be chosen, and +`ci` are conjunctions of literals for `i` between 0 and `n`, +and `<>` is either `<=`,`=`,`!=`,`<`,`>`, or `>=`. + +As an example program +``` +part(sportsframe). price(sportsframe,15). type(sportsframe,frame). +part(standardframe). price(standardframe,14). type(standardframe,frame). +part(fancysaddle). price(fancysaddle,6). type(fancysaddle,saddle). +part(standardsaddle). price(standardsaddle,5). type(standardsaddle,saddle). + +&sum{V} = price(P) :- price(P,V). + +pricelimit(20). + +&sum{price(P) :: selected(P) : part(P)} <= X :- pricelimit(X). +:- selected(P), selected(P'), P= rdpos, step(I,I'), - &fsum{ s(I') } > rdlimit. +fine(I') :- &sus{ p(I) } < rdpos, &sus{ p(I') } >= rdpos, step(I,I'), + &sus{ s(I') } > rdlimit. -&fsum {0} =: p(0). -&fsum {80000} =: s(0). +&sus {0} =: p(0). +&sus {80000} =: s(0). acc(11350,4). slow(2301,6). diff --git a/examples/config_assignment.lp b/examples/config_assignment.lp new file mode 100644 index 0000000..55f8e43 --- /dev/null +++ b/examples/config_assignment.lp @@ -0,0 +1,11 @@ +price(frame,15). + + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +&sus{price(P) : selected(P)} =: price(total). + +#show selected/1. +&show{price/1}. \ No newline at end of file diff --git a/examples/config_default.lp b/examples/config_default.lp new file mode 100644 index 0000000..4e0b552 --- /dev/null +++ b/examples/config_default.lp @@ -0,0 +1,11 @@ +price(frame,15). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +&sus{price(P)} = 1 :- selected(P), not price(P,_). +&sus{price(P) : selected(P)} =: price(total). + +#show selected/1. +&show{price/1}. \ No newline at end of file diff --git a/examples/config_default_df.lp b/examples/config_default_df.lp new file mode 100644 index 0000000..ebd3021 --- /dev/null +++ b/examples/config_default_df.lp @@ -0,0 +1,16 @@ +price(frame,15). + +default_price(20). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +&sus{price(P) : selected(P)} =: calc_price(total). + +&sus{price(total)} = calc_price(total) :- &df{calc_price(total)}. +&sus{price(total)} = D :- not &df{calc_price(total)}, + default_price(D). + +#show selected/1. +&show{price/1}. \ No newline at end of file diff --git a/examples/config_default_in.lp b/examples/config_default_in.lp new file mode 100644 index 0000000..19af57d --- /dev/null +++ b/examples/config_default_in.lp @@ -0,0 +1,13 @@ +price(frame,15). +default_range(1,2). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +&in{L..U} =: price(P) :- selected(P), not price(P,_), + default_range(L,U). +&sus{price(P) : selected(P)} =: price(total). + +#show selected/1. +&show{price/1}. \ No newline at end of file diff --git a/examples/config_maxlimit_choice.lp b/examples/config_maxlimit_choice.lp new file mode 100644 index 0000000..3df1a75 --- /dev/null +++ b/examples/config_maxlimit_choice.lp @@ -0,0 +1,16 @@ +part(sportsframe). price(sportsframe,15). type(sportsframe,frame). +part(standardframe). price(standardframe,14). type(standardframe,frame). +part(fancysaddle). price(fancysaddle,6). type(fancysaddle,saddle). +part(standardsaddle). price(standardsaddle,5). type(standardsaddle,saddle). + +&sum{V} = price(P) :- price(P,V). + +maxlimit(14). + +&max{price(P) :: selected(P) : part(P)} <= X :- maxlimit(X). +:- selected(P), selected(P'), P= L, + pricelimit(L). + +#show selected/1. +&show{price/1}. \ No newline at end of file diff --git a/examples/config_pricelimit_sus.lp b/examples/config_pricelimit_sus.lp new file mode 100644 index 0000000..a3448f3 --- /dev/null +++ b/examples/config_pricelimit_sus.lp @@ -0,0 +1,13 @@ +price(frame,15). + +pricelimit(14). + + selected(frame). +{ selected(bag) }. + +&sus{V} = price(P) :- selected(P), price(P,V). +:- &sus { price(P) : selected(P) } >= L, + pricelimit(L). + +#show selected/1. +&show{price/1}. \ No newline at end of file diff --git a/examples/fsD.lp b/examples/fsD.lp deleted file mode 100644 index 2e0ae61..0000000 --- a/examples/fsD.lp +++ /dev/null @@ -1,24 +0,0 @@ -% select a cycle -1 { cycle(T,U) : task(U), U != T } 1 :- task(T). -1 { cycle(T,U) : task(T), U != T } 1 :- task(U). - -% make sure the cycle is connected -reach(M) :- M = #min { T : task(T) }. -reach(U) :- reach(T), cycle(T,U). -:- task(T), not reach(T). - -% select a start point -1 { start(T) : task(T) } 1. - -% obtain an order -permutation(T,U) :- cycle(T,U), not start(U). - -% place tasks sequentially on machines -seq((T,M),(T,M+1),D) :- task(T), duration(T,M,D), machine(M+1). -seq((T1,M),(T2,M),D) :- permutation(T1,T2), duration(T1,M,D). - -&diff { T1-T2 } <= -D :- seq(T1,T2,D). -&diff { 0-(T,M) } <= 0 :- duration(T,M,D). -&diff { (T,M)-bound } <= -D :- duration(T,M,D). - -#show permutation/2. diff --git a/examples/fsE.lp b/examples/fsE.lp deleted file mode 100644 index 3baee37..0000000 --- a/examples/fsE.lp +++ /dev/null @@ -1,25 +0,0 @@ -% select a cycle - -1 { cycle(T,U) : task(U), U != T } 1 :- task(T). -1 { cycle(T,U) : task(T), U != T } 1 :- task(U). - -% make sure the cycle is connected -reach(M) :- M = #min { T : task(T) }. -reach(U) :- reach(T), cycle(T,U). -:- task(T), not reach(T). - -% select a start point -1 { start(T) : task(T) } 1. - -% obtain an order -permutation(T,U) :- cycle(T,U), not start(U). - -% place tasks sequentially on machines -seq((T,M),(T,M+1),D) :- task(T), duration(T,M,D), machine(M+1). -seq((T1,M),(T2,M),D) :- permutation(T1,T2), duration(T1,M,D). - -&sum { T2 - T1 } >= D :- seq(T1,T2,D). -&sum { (T,M) } >= 0 :- duration(T,M,D). -&sum { (T,M) } <= bound-D :- duration(T,M,D). - -#show permutation/2. diff --git a/examples/fsI.lp b/examples/fsI.lp deleted file mode 100644 index 5f30e62..0000000 --- a/examples/fsI.lp +++ /dev/null @@ -1,4 +0,0 @@ - machine(1). machine(2). -task(a). duration(a,1,3). duration(a,2,4). -task(b). duration(b,1,1). duration(b,2,6). -task(c). duration(c,1,5). duration(c,2,5). diff --git a/examples/fsO.lp b/examples/fsO.lp deleted file mode 100644 index e0c439a..0000000 --- a/examples/fsO.lp +++ /dev/null @@ -1,26 +0,0 @@ -% select a cycle - -1 { cycle(T,U) : task(U), U != T } 1 :- task(T). -1 { cycle(T,U) : task(T), U != T } 1 :- task(U). - -% make sure the cycle is connected -reach(M) :- M = #min { T : task(T) }. -reach(U) :- reach(T), cycle(T,U). -:- task(T), not reach(T). - -% select a start point -1 { start(T) : task(T) } 1. - -% obtain an order -permutation(T,U) :- cycle(T,U), not start(U). - -% place tasks sequentially on machines -seq((T,M),(T,M+1),D) :- task(T), duration(T,M,D), machine(M+1). -seq((T1,M),(T2,M),D) :- permutation(T1,T2), duration(T1,M,D). - -&sum { 1*T1 + -1*T2 } <= -D :- seq(T1,T2,D). -&sum { -1*(T,M) } <= 0 :- duration(T,M,D). -&sum { 1*(T,M) + -1*bound } <= -D :- duration(T,M,D). -&minimize { bound }. - -#show permutation/2. diff --git a/examples/golomb.lp b/examples/golomb.lp deleted file mode 100644 index 1ea4d9f..0000000 --- a/examples/golomb.lp +++ /dev/null @@ -1,8 +0,0 @@ -#const l = 35. -#const o = 8. -&dom { 1..l } = p(P) :- P=1..o. - -&sum { p(1) } = 1. -&sum { p(P) } < p(P+1) :- P=1..o-1. - -&distinct{ p(Q) - p(P) : P < Q, P=1..o-1, Q=P+1..o }. diff --git a/examples/money.lp b/examples/money.lp deleted file mode 100644 index 0c3a260..0000000 --- a/examples/money.lp +++ /dev/null @@ -1,12 +0,0 @@ -letter(s;e;n;d;m;o;r;y). - -&dom {0..9} = X :- letter(X). - -&sum { 1000*s + 100*e + 10*n + 1*d - ; 1000*m + 100*o + 10*r + 1*e - } = 10000*m + 1000*o + 100*n + 10*e + 1*y. -&sum { m } != 0. - -&distinct {X : letter(X)}. - -&show {X : letter(X)}. diff --git a/examples/move.lp b/examples/move.lp deleted file mode 100644 index 2cf8f15..0000000 --- a/examples/move.lp +++ /dev/null @@ -1,24 +0,0 @@ -#const end=20. -#const stepsize=7. -step(0..end). - -% domain knowledge -&dom { 0..T*stepsize } = at(T) :- step(T). - -% initial state -&sum {at(0)} = 0. - -% actions -{move(T)} :- step(T); T > 0. - -% effects -&sum {at(T-1); stepsize} = at(T) :- move(T). - -% frame axiom -&sum {at(T-1)} = at(T) :- not move(T); step(T); step(T-1). - -% goals -:- &sum {at(end)} <= 100. - -%&show {at(X):step(X)}. -#show move/1. diff --git a/examples/queens.lp b/examples/queens.lp deleted file mode 100644 index d62ff6f..0000000 --- a/examples/queens.lp +++ /dev/null @@ -1,9 +0,0 @@ -#const n = 10. - -p(1..n). - -&dom { 1..n } = q(N) :- p(N). - -&distinct { q(N)+0 : p(N) }. -&distinct { q(N)-N : p(N) }. -&distinct { q(N)+N : p(N) }. diff --git a/examples/simple.lp b/examples/simple.lp deleted file mode 100644 index 0fc485f..0000000 --- a/examples/simple.lp +++ /dev/null @@ -1,2 +0,0 @@ -&fsum{x}=1 :- &fsum{ 1 : a }>= 0. -a :- &fsum{x}=1. diff --git a/examples/taxes.lp b/examples/taxes.lp index af9ba40..2279618 100644 --- a/examples/taxes.lp +++ b/examples/taxes.lp @@ -12,17 +12,17 @@ deduction(mary, 10000, 10001). 1 { lives(P,R) : region(R) } 1 :- person(P). -&fsum{ 0 } =: deduction(P) :- person(P), not deduction(P,_,_). -&fin{ L..H } =: deduction(P) :- deduction(P,L,H). -&fsum{ T } =: rate(P) :- lives(P,R), income(P,I), +&sus{ 0 } =: deduction(P) :- person(P), not deduction(P,_,_). +&in{ L..H } =: deduction(P) :- deduction(P,L,H). +&sus{ T } =: rate(P) :- lives(P,R), income(P,I), T = #max{ T' : rate(R,L,T'), I>=L}. -&fsum{ I*rate(P)-100*deduction(P) } =: 100*tax(P) :- income(P,I). -&fsum{ tax(P) : lives(P,R) } =: total(R) :- region(R). -&fmin{ tax(P) : person(P) } =: min. -&fmax{ tax(P) : person(P) } =: max. -min_taxes(P) :- &fmin{ tax(P') : person(P') } = tax(P), person(P). -max_taxes(P) :- &fmax{ tax(P') : person(P') } = tax(P), person(P). +&sus{ I*rate(P)-100*deduction(P) } =: 100*tax(P) :- income(P,I). +&sus{ tax(P) : lives(P,R) } =: total(R) :- region(R). +&min{ tax(P) : person(P) } =: min. +&max{ tax(P) : person(P) } =: max. +min_taxes(P) :- &min{ tax(P') : person(P') } = tax(P), person(P). +max_taxes(P) :- &max{ tax(P') : person(P') } = tax(P), person(P). #show lives/2. #show min_taxes/1. diff --git a/examples/tests.lp b/examples/tests.lp deleted file mode 100644 index 8a8f581..0000000 --- a/examples/tests.lp +++ /dev/null @@ -1,96 +0,0 @@ -%* -% Standard GZ unsat -&fsum{x}=1 :- &fsum{ 1 : a }>= 0. -a :- &fsum{x}=1. - - -% TODO: Weird conditional minimum body example (1 or no stable models?) -&fsum{x} = 1. -a :- &fmin{3; x:a} > 2. - - -#show a/0. - - -% Assignment fact -&fsum{1} =: x. -&fsum{z} =: y. - -% Conditional assignment fact - -{a}. -&fsum{z : a; 1} =: x. -&fsum{x} =: y. - -#show __def/1. - -% Assignment head, body check -{a}. -&fsum{1} =: x :- a. -b :- &fsum{x} > 0. - -% In assignment -&fin{0..2} =: x. - -% In assignment, vars undef -&fin{y..z} =: x. - -% In assignment, vars def, unsat - -&fsum{z} = 1. -&fsum{y} = 2. -&fin{y..z} =: x. - -% In assignment, vars def, sat -&fsum{z} = 2. -&fsum{y} = 1. -&fin{y..z} =: x. - -% In assignment, vars def conditional, sat -{a}. -&fsum{z} = 2 :- a. -&fsum{y} = 1. -&fin{y..z} =: x. - -% Conditional linear constraint, head -{a}. -&fsum{1:a} = x. - -% Conditional linear constraint, body -{a}. -&fsum{1} = x. -b :- &fsum{1:a} < x. - -% Minimum assignment fact -&fmin{3;2;1}=:x. - -% Minimum body -&fsum{x} = 1. -a :- &fmin{3;x} < 2. - -% Conditional minimum assignment fact -{a}. -&fmin{3;2;1:a}=:x. - -% Conditional minimum body -{b}. -&fsum{x} = 1. -a :- &fmin{3; x:b} < 2. - -% Maximum assignment fact -&fmax{3;2;1}=:x. - -% Maximum body -&fsum{x} = 3. -a :- &fmax{1;x} > 2. - -% Conditional maximum assignment fact -{a}. -&fmax{3;2;4:a}=:x. - -% Conditional maximum body -{b}. -&fsum{x} = 2. -a :- &fmax{1; x:b} <= 1. - -*% diff --git a/examples/vicious_cycle.lp b/examples/vicious_cycle.lp new file mode 100644 index 0000000..f173e2a --- /dev/null +++ b/examples/vicious_cycle.lp @@ -0,0 +1,2 @@ +&sus{x}=1 :- &sus{ 1 : a }>= 0. +a :- &sus{x}=1. diff --git a/fclingo/__main__.py b/fclingo/__main__.py index 78c1774..7e6c297 100644 --- a/fclingo/__main__.py +++ b/fclingo/__main__.py @@ -6,7 +6,7 @@ import clingo from clingcon import ClingconTheory -from clingo.ast import ProgramBuilder, parse_files +from clingo.ast import ProgramBuilder, parse_files, Location, Position, Rule from fclingo import THEORY from fclingo.parsing import HeadBodyTransformer @@ -154,10 +154,12 @@ def main(self, control, files): hbt = HeadBodyTransformer() parse_files( files, - lambda ast: self._theory.rewrite_ast( - ast, lambda stm: bld.add(hbt.visit(stm)) - ), + lambda stm: bld.add(hbt.visit(stm)), ) + pos = Position('', 1, 1) + loc = Location(pos, pos) + for rule in hbt.rules_to_add: + bld.add(Rule(loc,rule[0],rule[1])) control.add("base", [], THEORY) control.ground([("base", [])]) diff --git a/fclingo/parsing.py b/fclingo/parsing.py index cd66252..25627ff 100644 --- a/fclingo/parsing.py +++ b/fclingo/parsing.py @@ -4,7 +4,7 @@ import clingo from clingo import ast -PREFIX = "__" +PREFIX = "__f" HEAD = "_h" BODY = "_b" THEORY = ( @@ -32,37 +32,47 @@ }; &""" + PREFIX - + """fsum""" + + """sum""" + BODY - + """/0 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, body; + + """/0 : sum_term, {<=,=,!=,<,>,>=}, sum_term, body; &""" + PREFIX - + """fsum""" + + """sum""" + + HEAD + + """/0 : sum_term, {<=,=,!=,<,>,>=}, sum_term, head; + &""" + + PREFIX + + """sus""" + + BODY + + """/0 : sum_term, {<=,=,!=,<,>,>=}, sum_term, body; + &""" + + PREFIX + + """sus""" + HEAD + """/0 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, head; &""" + PREFIX - + """fmax""" + + """max""" + BODY - + """/0 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, body; + + """/0 : sum_term, {<=,=,!=,<,>,>=}, sum_term, body; &""" + PREFIX - + """fmax""" + + """max""" + HEAD + """/0 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, head; &""" + PREFIX - + """fmin""" + + """min""" + BODY - + """/0 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, body; + + """/0 : sum_term, {<=,=,!=,<,>,>=}, sum_term, body; &""" + PREFIX - + """fmin""" + + """min""" + HEAD + """/0 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, head; &""" + PREFIX - + """fin""" + + """in""" + HEAD + """/0 : dom_term, {=:}, sum_term, head; &df/0 : function_term, body @@ -76,6 +86,9 @@ class HeadBodyTransformer(ast.Transformer): Class for tagging location of theory atoms. """ + def __init__(self) -> None: + self.rules_to_add = [] + def _rewrite_tuple(self, element, number): """ Add variables to tuple to ensure multiset semantics. @@ -112,7 +125,7 @@ def visit_TheoryAtom(self, atom, in_lit=False): Rewrite theory atoms depending on location. """ term = atom.term - if term.name in ["fsum", "fin", "fmax", "fmin"] and not term.arguments: + if term.name in ["sum", "sus", "in", "max", "min"] and not term.arguments: loc = BODY if in_lit else HEAD atom = atom.update( term=ast.Function( @@ -124,3 +137,32 @@ def visit_TheoryAtom(self, atom, in_lit=False): elements=self._rewrite_tuples(atom.elements), ) return atom + + def visit_Rule(self,rule): + head = rule.head + location = head.location + if head.ast_type == ast.ASTType.TheoryAtom: + new_elements = [] + for element in head.elements: + term = element.terms[0] + condition = element.condition + if term.ast_type == ast.ASTType.TheoryUnparsedTerm and "::" in str(term): + unparsed_terms = term.elements[:-1] + choice_atom = term.elements[-1].term + assert "::" == term.elements[-1].operators[0] and choice_atom.ast_type in [ast.ASTType.TheoryFunction, ast.ASTType.SymbolicTerm] and len(element.terms) == 1 + if choice_atom.ast_type == ast.ASTType.TheoryFunction: + choice_atom = ast.Literal(location,0,ast.SymbolicAtom(ast.Function(location,choice_atom.name,choice_atom.arguments,0))) + else: + choice_atom = ast.Literal(location,0,ast.SymbolicAtom(choice_atom)) + choice = ast.Aggregate(location, None, [ast.ConditionalLiteral(location,choice_atom,[])], None) + body = [] + body.extend(rule.body) + body.extend(condition) + self.rules_to_add.append((choice,body)) + new_element_condition = [choice_atom] + new_element_condition.extend(condition) + new_elements.append(ast.TheoryAtomElement([ast.TheoryUnparsedTerm(location,unparsed_terms)],new_element_condition)) + else: + new_elements.append(element) + rule.head.elements=new_elements + return rule.update(**self.visit_children(rule)) diff --git a/fclingo/translator.py b/fclingo/translator.py index bc044da..e7c09f7 100644 --- a/fclingo/translator.py +++ b/fclingo/translator.py @@ -87,7 +87,7 @@ def copy(element): if isinstance(element.condition_id, int): condition_id = int(element.condition_id) - return ConstraintElement(terms, None, condition_id) + return ConstraintElement(terms, element.condition, condition_id) class ConstraintTerm: @@ -154,16 +154,16 @@ def __hash__(self): ONE = ConstraintTerm(None, 1, None, clingo.TheoryTermType.Number) ZERO = ConstraintTerm(None, 0, None, clingo.TheoryTermType.Number) SUM_TERM_HEAD = ConstraintTerm( - PREFIX + "sum" + HEAD, None, [], clingo.TheoryTermType.Function + "__sum" + HEAD, None, [], clingo.TheoryTermType.Function ) FSUM_TERM_HEAD = ConstraintTerm( - PREFIX + "fsum" + HEAD, None, [], clingo.TheoryTermType.Function + PREFIX + "sum" + HEAD, None, [], clingo.TheoryTermType.Function ) SUM_TERM_BODY = ConstraintTerm( - PREFIX + "sum" + BODY, None, [], clingo.TheoryTermType.Function + "__sum" + BODY, None, [], clingo.TheoryTermType.Function ) FSUM_TERM_BODY = ConstraintTerm( - PREFIX + "fsum" + BODY, None, [], clingo.TheoryTermType.Function + PREFIX + "sum" + BODY, None, [], clingo.TheoryTermType.Function ) @@ -288,8 +288,7 @@ def _add_defined(self, var, reason=None): def _define_variables(self, atom): assert ( - match(atom.term, PREFIX + "fsum" + HEAD, 0) - or match(atom.term, PREFIX + "sum" + HEAD, 0) + match(atom.term, PREFIX + "sum" + HEAD, 0) or match(atom.term, PREFIX + "sus" + HEAD, 0) or match(atom.term, "__sum" + HEAD, 0) ) and not self.conditional(atom) for var in self.vars(atom.guard[1]): self._add_defined(var, [atom.literal]) @@ -332,18 +331,18 @@ def _translate_conditional(self, atom): self._print_constraints.add(atom) elements = [] neutral = ZERO - if match(atom.term, PREFIX + "fsum" + BODY, 0) or match( - atom.term, PREFIX + "fsum" + HEAD, 0 + if match(atom.term, PREFIX + "sum" + BODY, 0) or match( + atom.term, PREFIX + "sum" + HEAD, 0 ): neutral = ZERO - elif match(atom.term, PREFIX + "fmin" + BODY, 0) or match( - atom.term, PREFIX + "fmin" + HEAD, 0 + elif match(atom.term, PREFIX + "min" + BODY, 0) or match( + atom.term, PREFIX + "min" + HEAD, 0 ): neutral = ConstraintTerm( None, self._config.max_int, None, clingo.TheoryTermType.Number ) - elif match(atom.term, PREFIX + "fmax" + BODY, 0) or match( - atom.term, PREFIX + "fmax" + HEAD, 0 + elif match(atom.term, PREFIX + "max" + BODY, 0) or match( + atom.term, PREFIX + "max" + HEAD, 0 ): neutral = ConstraintTerm( None, self._config.min_int, None, clingo.TheoryTermType.Number @@ -461,9 +460,9 @@ def _translate_max(self, atom): elif ">" in rel: rel = rel.replace(">", "<") type_term = ConstraintTerm( - PREFIX + "fmin" + BODY + PREFIX + "min" + BODY if BODY in atom.term.name - else PREFIX + "fmin" + HEAD, + else PREFIX + "min" + HEAD, None, [], clingo.TheoryTermType.Function, @@ -612,8 +611,7 @@ def _add_fsum_constraint(self, atom): if str(con) == str(sum_con): return con.literal if sum_con.literal is None: - new_lit = self._add_atom() - sum_con.literal = new_lit + sum_con.literal = self._add_atom() if self._config.print_trans: print() print("% Adding fsum constraint:", atom) @@ -622,7 +620,7 @@ def _add_fsum_constraint(self, atom): self._sum_constraints.add(sum_con) clingcon_constraint = ConstraintAtom.copy(sum_con) clingcon_constraint.term.name = ( - PREFIX + "sum" + BODY if BODY in atom.term.name else PREFIX + "sum" + HEAD + "__sum" + BODY if BODY in atom.term.name else "__sum" + HEAD ) clingcon_constraint.literal = None clingcon_lit = self._add_clingcon_constraint(clingcon_constraint) @@ -631,10 +629,8 @@ def _add_fsum_constraint(self, atom): for var in self.vars(element.terms[0]): def_lit = self._add_defined(var) defined.append(def_lit) - self._add_rule([], [sum_con.literal, -def_lit]) for var in self.vars(sum_con.guard[1]): def_lit = self._add_defined(var) - self._add_rule([], [sum_con.literal, -def_lit]) defined.append(def_lit) if HEAD in sum_con.term.name: self._add_rule([clingcon_lit], [sum_con.literal]) @@ -658,20 +654,12 @@ def _translate_constraint(self, atom): var = self.vars(atom.elements[0].terms[0]).pop() def_lit = self._add_defined(var) self._add_rule([atom.literal],[def_lit]) - elif match(atom.term, PREFIX + "sum" + BODY, 0) or match( - atom.term, PREFIX + "sum" + HEAD, 0 - ): - for element in atom.elements: - for var in self.vars(element.terms[0]): - def_lit = self._add_defined(var) - self._add_rule([def_lit], []) - for var in self.vars(atom.guard[1]): - def_lit = self._add_defined(var) - self._add_rule([def_lit], []) elif ( ( - match(atom.term, PREFIX + "fsum" + BODY, 0) - or match(atom.term, PREFIX + "fsum" + HEAD, 0) + match(atom.term, PREFIX + "sum" + BODY, 0) + or match(atom.term, PREFIX + "sum" + HEAD, 0) + or match(atom.term, PREFIX + "sus" + BODY, 0) + or match(atom.term, PREFIX + "sus" + HEAD, 0) ) and not self.conditional(atom) and atom.guard[0] in ("=", "<", ">", "<=", ">=", "!=") @@ -681,15 +669,15 @@ def _translate_constraint(self, atom): self._translate_conditional(atom) elif atom.guard[0] == "=:": self._translate_assignment(atom) - elif match(atom.term, PREFIX + "fmax" + BODY, 0) or match( - atom.term, PREFIX + "fmax" + HEAD, 0 + elif match(atom.term, PREFIX + "max" + BODY, 0) or match( + atom.term, PREFIX + "max" + HEAD, 0 ): self._translate_max(atom) - elif match(atom.term, PREFIX + "fmin" + BODY, 0) or match( - atom.term, PREFIX + "fmin" + HEAD, 0 + elif match(atom.term, PREFIX + "min" + BODY, 0) or match( + atom.term, PREFIX + "min" + HEAD, 0 ): self._translate_min(atom) - elif match(atom.term, PREFIX + "fin" + HEAD, 0): + elif match(atom.term, PREFIX + "in" + HEAD, 0): self._translate_in(atom) else: self._print_constraints.add(ConstraintAtom.copy(atom)) @@ -698,6 +686,25 @@ def _translate_constraints(self, theory_atoms): for atom in theory_atoms: self._translate_constraint(atom) + def _prepare_theory_atoms(self,theory_atoms): + atoms = [] + for atom in theory_atoms: + ca = ConstraintAtom.copy(atom) + if ( + match(ca.term, PREFIX + "sum" + BODY, 0) + or match(ca.term, PREFIX + "sum" + HEAD, 0) + or match(ca.term, PREFIX + "min" + BODY, 0) + or match(ca.term, PREFIX + "min" + HEAD, 0) + or match(ca.term, PREFIX + "max" + BODY, 0) + or match(ca.term, PREFIX + "max" + HEAD, 0) + ): + for element in ca.elements: + variables = self.vars(element.terms[0]) + defined = [self._add_defined(variable) for variable in variables] + element.condition.extend(defined) + atoms.append(ca) + return atoms + def translate(self, theory_atoms): """ Translates ASP program with constraint atoms including assignments and conditionals into a Clingcon program. @@ -705,6 +712,7 @@ def translate(self, theory_atoms): conditional linear constraint atoms and aggregates max and min. Returns sum constraints to be added to Clingcon. """ + theory_atoms = self._prepare_theory_atoms(theory_atoms) self._translate_constraints(theory_atoms) self._fix_undefined() self._prg.cleanup() \ No newline at end of file diff --git a/slides/examples/assignments.lp b/slides/examples/assignments.lp deleted file mode 100644 index 3564d9b..0000000 --- a/slides/examples/assignments.lp +++ /dev/null @@ -1,4 +0,0 @@ - #($\mathtt{\&}t\mathtt{\{}e_1,\dots,e_n\mathtt{\}} = x$#) :- #($\mathtt{\&}t\mathtt{\{}e_1,\dots,e_n\mathtt{\}} := x$#), - def(#($x_1$)#),#(\dots#),def(#($x_n$)#). -&sum{#($l$#)} <= #($x$#) :- #($\mathtt{\&in}\mathtt{\{}l\mathtt{..}u{\}} = x$#). -&sum{#($u$#)} >= #($x$#) :- #($\mathtt{\&in}\mathtt{\{}l\mathtt{..}u{\}} = x$#). diff --git a/slides/examples/conditional.lp b/slides/examples/conditional.lp deleted file mode 100644 index b5e489b..0000000 --- a/slides/examples/conditional.lp +++ /dev/null @@ -1,9 +0,0 @@ -&sum{#($\mathit{aux}_i$#)} = #($\mathit{e}_i$#) :- #($\mathit{c}_i$#), def(#($x_1$)#),#(\dots#),def(#($x_n$)#). -&sum{#($\mathit{aux}_i$#)} = #($0_t$#) :- not #($\mathit{c}_i$#). -&sum{#($\mathit{aux}_i$#)} = #($\mathit{e}_i$#) :- #($\mathit{c}_i$#), def(#($\mathit{aux}_i$#)). -&sum{#($\mathit{aux}_i$#)} = #($0_t$#) :- not #($\mathit{c}_i$#), def(#($\mathit{aux}_i$#)). -{#($\mathit{c}_i$#)} :- def(#($\mathit{aux}_i$#)). -#($\mathtt{\&}t(l)\mathtt{\{}\dots,e_1:c_1,\dots,e_n:c_n,\dots\mathtt{\}} \prec k$#) :- - #($\mathtt{\&}t(l)\mathtt{\{}\dots,\mathit{aux}_1,\dots,\mathit{aux}_n,\dots\mathtt{\}} \prec k$#). -#($\mathtt{\&}t(l)\mathtt{\{}\dots,\mathit{aux}_1,\dots,\mathit{aux}_n,\dots\mathtt{\}} \prec k$#) :- - #($\mathtt{\&}t(l)\mathtt{\{}\dots,e_1:c_1,\dots,e_n:c_n,\dots\mathtt{\}} \prec k$#). diff --git a/slides/examples/cp_lang.lp b/slides/examples/cp_lang.lp deleted file mode 100644 index 6ce76c2..0000000 --- a/slides/examples/cp_lang.lp +++ /dev/null @@ -1,16 +0,0 @@ -#theory csp { - var_term { }; - sum_term { - #($\cdots$#) - }; - dom_term { - #($\cdots$#) - }; - #(\alert<2->{\&sum/1 : sum\_term, \{<=,=,!=,<,>,>=\}, sum\_term, any;} #) - &diff/1 : sum_term, {<=}, sum_term, any; - &minimize/0 : sum_term, directive; - &maximize/0 : sum_term, directive; - &show/0 : sum_term, directive; - &distinct/0 : sum_term, head; - &dom/0 : dom_term, {=}, var_term, head -}. diff --git a/slides/examples/htc_lang.lp b/slides/examples/htc_lang.lp deleted file mode 100644 index f0aa946..0000000 --- a/slides/examples/htc_lang.lp +++ /dev/null @@ -1,19 +0,0 @@ -#theory htc { - sum_term { - - : 3, unary; - ** : 2, binary, right; - * : 1, binary, left; - / : 1, binary, left; - \\ : 1, binary, left; - + : 0, binary, left; - - : 0, binary, left - }; - dom_term { - #($\cdots$#) - .. : 0, binary, left - }; - &sum/1 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, any; - &min/1 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, any; - &max/1 : sum_term, {<=,=,!=,<,>,>=,=:}, sum_term, any; - &in/1 : dom_term, {=:}, sum_term, head -}. diff --git a/slides/examples/minmax.lp b/slides/examples/minmax.lp deleted file mode 100644 index dd2b738..0000000 --- a/slides/examples/minmax.lp +++ /dev/null @@ -1,7 +0,0 @@ -def(#($\mathit{min}$#)) :- def(#($x_1$)#),#(\dots#),def(#($x_n$)#). -:- not &sum(body){$\mathit{min}$} <= $e_i$. -s :- sum(body){$\mathit{min}$} = $e_i$. -:- not s, def(#($\mathit{min}$#)). -&min$(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k$ :- &sum$(l)\{\mathit{min}\} \prec k$, def(#($\mathit{min}$#)). -&min$(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k$ :- &sum$(l)\{\mathit{min}\} \prec k$. -&sum$(l)\{\mathit{min}\} \prec k$ :- &min$(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k$. diff --git a/slides/examples/semantics.lp b/slides/examples/semantics.lp deleted file mode 100644 index 3933467..0000000 --- a/slides/examples/semantics.lp +++ /dev/null @@ -1,23 +0,0 @@ -a :- &sum{x} = 1. -a :- &sum(body){x} = 1. -&sum(head){ #($e_1,\dots,e_n$#) } #($\prec k$#) -def(x) :- &sum(head){ #($e_1,\dots,e_n$#) } #($\prec k$#). -&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#) -&sum(#($l$#)){ #($e_1,\dots,e_n$#) } #($\prec k$#). -&sum{x} = 0 :- not def(x). -&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#) -'&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)' - :- &sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#), - def(x#($_1$#)),#($\dots$#),def(x#($_n$#)). -{&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)}. -c :- &sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#), - def(x#($_1$#)),#($\dots$#),def(x#($_n$#)). -{&sum(body){ #($e_1,\dots,e_n$#) } #($\prec k$#)}. -a :- '&sum{x} = 1'. -'&sum{x} = 1' :- &sum{x} = 1, def(x). -{&sum{x} = 1}. -&sum{x} = 0 :- not def(x). -a :- c. -c :- &sum{x} = 1, def(x). -{&sum{x} = 1}. -&sum{x} = 0 :- not def(x). diff --git a/slides/examples/taxes.lp b/slides/examples/taxes.lp deleted file mode 100644 index 4773142..0000000 --- a/slides/examples/taxes.lp +++ /dev/null @@ -1,29 +0,0 @@ -person(paul;mary). -region(luxemburg;germany). -rate(germany, 25000, 15). -rate(germany, 50000, 25). -rate(germany, 100000, 35). -rate(luxemburg, 38700, 14). -rate(luxemburg, 58000, 23). -rate(luxemburg, 96700, 30). -income(paul, 60000). -income(mary, 120000). -deduction(mary, 10000, 10001). - -1 { lives(P,R) : region(R) } 1 :- person(P). - -&sum{ 0 } =: deduction(P) :- person(P), not deduction(P,_,_). -&in{ L..H } =: deduction(P) :- deduction(P,L,H). -&sum{ T } =: rate(P) :- lives(P,R), income(P,I), - T = #max{ T' : rate(R,L,T'), I>=L}. - -&sum{ I*rate(P)-100*deduction(P) } =: 100*tax(P) :- income(P,I). -&sum{ tax(P) : lives(P,R) } =: total(R) :- region(R). -&min{ tax(P) : person(P) } =: min. -&max{ tax(P) : person(P) } =: max. -min_taxes(P) :- &min{ tax(P') : person(P') } = tax(P), person(P). -max_taxes(P) :- &max{ tax(P') : person(P') } = tax(P), person(P). - -#show lives/2. -#show min_taxes/1. -#show max_taxes/1. diff --git a/slides/examples/vicious.lp b/slides/examples/vicious.lp deleted file mode 100644 index 1586429..0000000 --- a/slides/examples/vicious.lp +++ /dev/null @@ -1,34 +0,0 @@ -&sum{x} = 1 :- &sum{ 1 : a } >= 0. -a :- &sum{x} = 1. -&sum(head){x} = 1 :- &sum(body){ 1 : a } >= 0. -a :- '&sum(body){x} = 1'. - -def(x) :- &sum(head){x} = 1. -'&sum(body){x} = 1' :- def(x), &sum(body){x} = 1. -{&sum(body){x} = 1}. - -&sum(head){aux(0)} = 1 :- a. -def(aux(0)) :- &sum(head){aux(0)} = 1. -&sum(head){aux(0)} = 0 :- not a. -def(aux(0)) :- &sum(head){aux(0)} = 0. -{a} :- def(aux(0)). -'&sum(body){aux(0)} >= 0' :- &sum(body){ 1 : a } >= 0. -&sum(body){ 1 : a } >=0 :- '&sum(body){aux(0)} >= 0'. -'&sum(body){aux(0)} >= 0' :- def(aux(0)), &sum(body){aux(0)} >= 0. -{&sum(body){aux(0)} >= 0}. - -&sum(head){x} = 0 :- not def(x). -&sum(head){aux(0)} = 0 :- not def(aux(0)). - -&sum(head){x} = 1 :- &sum(body){ 1 : a } >= 0. -def(x) :- &sum(head){x} = 1. -'&sum(body){x} = 1' :- def(x), &sum(body){x} = 1. -a :- '&sum(body){x} = 1'. -&sum(head){aux(0)} = 1 :- a. -'&sum(body){aux(0)} >= 0' :- def(aux(0)), &sum(body){aux(0)} >= 0. -&sum(body){ 1 : a } >=0 :- '&sum(body){aux(0)} >= 0'. - -&sum(head){aux(0)} = 1 :- a. -def(aux(0)) :- &sum(head){aux(0)} = 1. -{a} :- def(aux(0)). - a :- '&sum(body){x} = 1'. diff --git a/slides/listings.tex b/slides/listings.tex deleted file mode 100644 index 8d2ae14..0000000 --- a/slides/listings.tex +++ /dev/null @@ -1,68 +0,0 @@ -% The language definitions below require the following packages: -% -% \usepackage{courier} -% \usepackage{xcolor} -% \usepackage{relsize} -% -% \input{listings} -% \renewcommand{\Underscore}{\textscale{1}{\textunderscore}} -% -% Without extra packages I had to provide an alternative underscore definition -% to get decent looking underscores. -% -% As an alternative to courier, it is also possible to use the `lmodern` -% package. -% -% \usepackage[T1]{fontenc} -% \usepackage{lmodern} -% \usepackage{xcolor} -% \usepackage{relsize} -% -% \input{listings} -% -% When the python or clingo language is given, tex code can be embedded -% escaping it in `#( ... #)`, which is treated like a comment in Python. -% Furthermore, for logic programs the character sequence is `%%` is not output. -% This can be used to add labels at the end of lines. For example, in a logic -% program one can write -% -% H :- B.%%#( \label{lst:rule} #) -% -% to refer to the rule from the document without having to worry about changing -% line numbers when refactoring. The annotated program will still be runnable -% with clingo. - -\providecommand{\Underscore}{\textunderscore} - -\lstdefinelanguage{clingo}{% - basicstyle=\ttfamily,% - keywordstyle=[1]\bfseries,% - keywordstyle=[2]\bfseries,% - keywordstyle=[3]\bfseries,% - showstringspaces=false,% - literate={_}{\Underscore}1 {\%\%}{}0,% - escapeinside={\#(}{\#)},% - alsoletter={\#,\&},% - keywords=[1]{not,from,import,def,if,else,elif,return,while,break,and,or,for,in,del,and,class,with,as,is,yield,async},% - keywords=[2]{\#const,\#show,\#minimize,\#base,\#theory,\#count,\#external,\#program,\#script,\#end,\#heuristic,\#edge,\#project,\#show,\#sum},% - keywords=[3]{&,&dom,&sum,&diff,&show},% - morecomment=[l]{\#\ },% - morecomment=[l]{\%\ },% - morestring=[b]",% - stringstyle={\itshape},% - commentstyle={\color{darkgray}}% -} - -\lstdefinelanguage{python}{% - basicstyle=\ttfamily,% - keywordstyle=[1]\bfseries,% - showstringspaces=false,% - literate={_}{\Underscore}{1},% - escapeinside={\#(}{\#)},% - alsoletter={\#,\&},% - keywords=[1]{not,from,import,def,if,else,elif,return,while,break,and,or,for,in,del,and,class,with,as,is,yield,async},% - morecomment=[l]{\#\ },% - morestring=[b]",% - stringstyle={\itshape},% - commentstyle={\color{darkgray}}% -} diff --git a/slides/macro.tex b/slides/macro.tex deleted file mode 100644 index bfdeaee..0000000 --- a/slides/macro.tex +++ /dev/null @@ -1,172 +0,0 @@ -%!TEX root = paper.tex - -\newtheorem{proposition}{Proposition} -\newcommand{\den}[1]{\llbracket \, #1 \, \rrbracket} -% \newcommand{\denc}[3]{\llbracket \, #3 \, \rrbracket_{\langle#1,#2\rangle}} -% \newcommand{\inter}[2]{\ensuremath{\mathcal{I}_{#1,#2}}} -% \newcommand{\CC}{\ensuremath{\mathcal{C^+}}} % {\ensuremath{\mathcal{C_C}}} % {\ensuremath{\mathcal{CC}}} -% \newcommand{\TC}[1]{\ensuremath{\mathcal{T_{#1}}}} -% \newcommand{\cond}[2]{\ensuremath{|#1:#2|}} -\newcommand{\ctermm}[3]{\ensuremath{{#1|#2}{:\,}#3}} -\newcommand{\cterm}[3]{\ensuremath{(\ctermm{#1}{#2}{#3})}} % {\ensuremath{({#1|#2}\mathrel{:}#3})} -% \newcommand{\ct}[1]{\ensuremath{\mathit{ct}(#1)}} -% \newcommand{\cte}[2]{\ensuremath{\mathit{ct}_{\langle #1\rangle}(#2)}} -\newcommand{\close}[1]{\ensuremath{#1\raisebox{1pt}{$\uparrow$}}} - -\newcommand{\htag}[2]{\ensuremath{\mathit{#1}\agg{#2}}} -\newcommand{\htagg}[4]{\ensuremath{\mathit{#1}\agg{#2}\mathrel{#3}#4}} -\newcommand{\htaggg}[4]{\ensuremath{\mathit{#1} {#2 }\mathrel{#3}#4}} -\newcommand{\vals}[2]{\ensuremath{\mathcal{V}_{#1,#2}}} -\newcommand{\eval}[2]{\ensuremath{\mathit{eval}}_{\langle #1,#2\rangle}} -% \newcommand{\evalgz}[2]{\ensuremath{\mathit{eval}^{\gz}_{\langle #1,#2\rangle}}} -% \newcommand{\evalf}[2]{\ensuremath{\mathit{eval}^{\f}_{\langle #1,#2\rangle}}} -% \newcommand{\evals}[3]{\ensuremath{\mathit{eval}^{#1}_{\langle #2,#3\rangle}}} -% \newcommand{\evalcl}[1]{\ensuremath{\mathit{eval}_{#1}}} - -\newcommand{\evalgz}[2]{\ensuremath{{\gz}_{\langle #1,#2\rangle}}} -\newcommand{\evalf}[2]{\ensuremath{{\f}_{\langle #1,#2\rangle}}} -\newcommand{\evals}[3]{\ensuremath{{#1}_{\langle #2,#3\rangle}}} -\newcommand{\evalcl}[1]{\ensuremath{\mathit{eval}_{#1}}} -\newcommand{\evall}[1]{\ensuremath{\mathit{eval}}_{#1}} -\newcommand{\evallgz}[1]{\ensuremath{\mathit{eval}^{\mathtt{gz}}_{#1}}} - -\newcommand{\modelscl}{\ensuremath{\models_{cl}}} -\newcommand{\eqdef}{% - \mathrel{\vbox{\offinterlineskip\ialign{% - \hfil##\hfil\cr% - $\scriptscriptstyle\mathrm{def}$\cr% - \noalign{\kern1pt}% - $=$\cr% - \noalign{\kern-0.1pt}% -}}}} - -\newcommand{\sysfont}{\textit} -\newcommand{\clingo}{\sysfont{clingo}} -\newcommand{\clingcon}{\sysfont{clingcon}} -\newcommand{\clingoDL}{\clingo{\small\textnormal{[}\textsc{DL}\textnormal{]}}} -\newcommand{\dlprogram}{\textit{DL}-program} -\newcommand{\code}[1]{\texttt{#1}} -\newcommand{\ground}{variable-free} -\newcommand{\modelsgz}{\models_{\gz}} -\newcommand{\modelsf}{\models_{\f}} -\newcommand{\modelss}{\models_{\sem}} -\newcommand{\modelsp}[1]{\models_{#1}} -\newcommand{\Atoms}{\mathit{Atoms}} -\newcommand{\Head}{\mathit{H}} -\newcommand{\HeadA}{\mathit{\Head_A}} -\newcommand{\HeadB}{\mathit{\Head_B}} -\newcommand{\Headp}{\mathit{\Head^+}} -\newcommand{\Headn}{\mathit{\Head^-}} -\newcommand{\Body}{\mathit{B}} -\newcommand{\Bodyp}{\mathit{\Body^+}} -\newcommand{\Bodyn}{\mathit{\Body^-}} -\newcommand{\var}{\mathit{var}} -\newcommand{\Cond}{\mathit{Cond}} -\newcommand{\tuple}[1]{\langle #1 \rangle} -\newcommand{\restr}[2]{{#1|}_{\hspace{-1pt}#2}} -\newcommand{\df}[1]{\mathit{def}(#1)} -\newcommand{\HTC}{\ensuremath{\mathit{HT}_{\!C}}} % {\mathit{HT}_C} -\newcommand{\HT}{\ensuremath{\mathit{HT}}} -\newcommand{\X}{\ensuremath{\mathcal{X}}} -\newcommand{\D}{\ensuremath{\mathcal{D}}} -\newcommand{\Du}{\ensuremath{\mathcal{D}_{\mathbf{u}}}} -\newcommand{\T}{\ensuremath{\mathcal{T}}} -\newcommand{\C}{\ensuremath{\mathcal{C}}} -\newcommand{\ET}{\ensuremath{\mathcal{T}^e}} -\newcommand{\BT}{\ensuremath{\mathcal{T}^b}} -\newcommand{\BC}{\ensuremath{\mathcal{C}^b}} -\newcommand{\Cgr}{\ensuremath{\mathcal{C}^*}} -\newcommand{\F}{\ensuremath{\mathcal{F}}} -\newcommand{\I}{\ensuremath{\mathcal{I}}} -\newcommand{\V}{\ensuremath{\mathcal{V}}} -%\newcommand{\P}{\ensuremath{\mathcal{P}}} -\newcommand{\A}{\ensuremath{\mathcal{A}}} -\newcommand{\Piref}[1]{\Pi_{\ref{#1}}} -\newcommand{\vars}[1]{\ensuremath{\mathit{vars}(#1)}} -\newcommand{\varsp}[1]{\ensuremath{\mathit{vars}^{a}(#1)}} -\newcommand{\atoms}[1]{\ensuremath{\mathit{atoms}(#1)}} -\newcommand{\At}[1]{\ensuremath{\mathit{At}(#1)}} -\newcommand{\val}{\ensuremath{v}} % {V} -% \newcommand{\t}{\ensuremath{\mathbf{t}}} % {\boldsymbol{t}} -\newcommand{\gz}{\ensuremath{\mathit{vc}}} % {\boldsymbol{f}} -\newcommand{\f}{\ensuremath{\mathit{df}}} % {\boldsymbol{f}} -\newcommand{\ff}{\ensuremath{\mathit{F}}} % {\boldsymbol{f}} -\newcommand{\undefined}{\ensuremath{\mathbf{u}}} % {\boldsymbol{u}} -\newcommand{\sem}{\ensuremath{\kappa}} % {\boldsymbol{u}} -\newcommand{\ass}[3]{#1 := #2 \, .. \, #3} -\newcommand{\LC}{\ensuremath{\mathit{LC}}} -\newcommand{\DF}{\ensuremath{\boldsymbol{D\hspace{-1.2pt}F}}} % {\mathbf{DF}} -\newcommand{\agg}[1]{\ensuremath{\dot{\{}#1\dot{\}}}} % {\text{\"\{}#1\text{\"\}}} -\newcommand{\Z}{\ensuremath{\mathbb{Z}}} -\newcommand{\LX}{\ensuremath{\mathbb{X}}} -\newcommand{\HU}{\ensuremath{\mathbb{U}}} -\newcommand{\Gra}{\ensuremath{\mathit{G}^a}} -\newcommand{\Gr}{\ensuremath{\mathit{G}}} -\newcommand{\Def}{\delta} -\newcommand{\grsep}{\,\big|\hspace{-3pt}\big|\hspace{-3pt}\big|\,} -\newcommand{\isint}[1]{\ensuremath{\mathit{int}(#1)}} - - - - -\let\olditem\item -\let\oldenumerate\enumerate -\let\oldendenumerate\endenumerate -\let\olditemize\itemize -\let\oldenditemize\enditemize -\newcommand{\deitemize}{% -\def\itemize{\def\item{}} -\def\enditemize{\let\item\olditem} -\def\enumerate{\let\item\olditem\oldenumerate} -\def\endenumerate{\oldendenumerate\def\item{}} -} - -\newcommand{\reitemize}{% -\def\itemize{\olditemize} -\def\enditemize{\oldenditemize} -} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%% with bullets - -\newenvironment{Itemize}{\begin{itemize}[leftmargin=0pt]}{\end{itemize}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%% without bullets - -\renewenvironment{Itemize}{\let\item\relax}{\let\item\olditemize} -\renewenvironment{itemize}{\let\item\olditem\olditemize}{\oldenditemize\let\item\relax} -\renewenvironment{enumerate}{\let\item\olditem\oldenumerate}{\oldendenumerate\let\item\relax} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -% Some aggregate names -\def\sumf{\mathit{sum}} -\newcommand\op{\mathit{op}} -\newcommand\EX{\mathcal{EX}} - -\newcommand{\appendblank}{\ensuremath{\circ}} -\newcommand\theory[2]{\tuple{#1,#2}} -\newcommand{\aggs}{\mathit{agg}} -\newcommand{\levels}{\ell} -\newcommand{\level}[1]{\levels(#1)} -\newcommand{\gzsemantics}{\mbox{\gz-semantics}\xspace} -\newcommand{\fsemantics}{\mbox{\f-semantics}\xspace} -\newcommand{\sequilibrium}{\mbox{\sem-equilibrium}\xspace} -\newcommand{\gzequilibrium}{\mbox{\gz-equilibrium}\xspace} -\newcommand{\fequilibrium}{\mbox{\f-equilibrium}\xspace} -\newcommand{\sstable}{\mbox{\sem-stable}\xspace} -\newcommand{\gzstable}{\mbox{\gz-stable}\xspace} -\newcommand{\fstable}{\mbox{\f-stable}\xspace} -\def\kmapping{selection function} -\def\kmappings{{\kmapping}s} -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "paper" -%%% End: diff --git a/slides/slides.tex b/slides/slides.tex deleted file mode 100644 index 40bd0d4..0000000 --- a/slides/slides.tex +++ /dev/null @@ -1,277 +0,0 @@ -\documentclass[11pt]{beamer} -\usetheme{Warsaw} -\usepackage[utf8]{inputenc} -\usepackage{amsmath} -\usepackage{amsthm} -\usepackage{amsfonts} -\usepackage{amssymb} -\usepackage{stmaryrd} -\usepackage{listings} -\author[Cabalar et al.]{Pedro Cabalar and Jorge Fandinno and Torsten Schaub and Philipp Wanko} -\title[Implementing $\mathit{HT}_C$ using CASP]{Implementing (part of) $\mathit{HT}_C$ using Constraint Answer Set Programming: A prototype} -%\setbeamercovered{transparent} -%\setbeamertemplate{navigation symbols}{} -%\logo{} -%\institute{} -\date{} -%\subject{} -\begin{document} - -\input{macro} -\input{listings} - -\begin{frame} -\titlepage -\end{frame} - -\begin{frame}{Recap} -\begin{itemize} -\item \emph{Logic of Here-and-There with Constraints (\HTC)} allows for capturing non-monotonic reasoning over arbitrary constraints involving \emph{constraint variables} and \emph{conditional expressions} -\pause -\item Flexible syntax, \emph{constraint atoms} are (infinite) strings of symbols that may refer to variables and domain elements -\begin{align*} -"x-y\leq d"\quad"a"\quad"\mathit{sum}\agg{ \, s_1, s_2, \dots \, } = s_0" -\end{align*} -\vspace*{-.5cm} -\pause -\item Flexible semantics, \emph{denotations} assign constraint atoms sets of satisfying \emph{valuations} -\begin{align*} - \den{x-y\leq d} - = - \{v\in\mathcal{V}\mid v(x),v(y), d\in \mathbb{Z}, v(x)-v(y)\leq d\} -\end{align*} -\end{itemize} -\end{frame} - -\begin{frame}{Recap} -\begin{itemize} -\item \emph{Conditional constraint atoms} may contain \emph{conditional expressions} $(\ctermm{s}{s'}{\varphi})$ -\pause -\item \emph{Evaluation function} replaces conditional expressions $\tau=(\ctermm{s}{s'}{\varphi})$: - \begin{align*} - \eval{h}{t}(\tau) - &= - \left\{ - \begin{array}{ll} - s & \text{if } \langle h,t\rangle\models\varphi\\ - s' & \text{if } \langle t,t\rangle \hspace{2pt}\not\models\varphi\\ - \undefined & \text{otherwise} - \end{array} - \right. - \end{align*} -\vspace*{-.5cm} -\pause -\item \emph{Interpretations} $\tuple{h,t}$ are pairs of valuations with $h\subseteq t$ -\pause -\item Syntax, semantics of \emph{formulas} are standard \HT\ but for condition: -$\langle h,t \rangle \models c \text{ if } h\in \den{\eval{h}{t}(c)}$ -\end{itemize} -\end{frame} - -\begin{frame}{Motivation} -\begin{align*} - \mathit{total}(R) := \mathit{sum}\agg{ \, \mathit{tax}(P) : \mathit{lives}(P,R) \, } \ \leftarrow \ \mathit{region}(R) -\end{align*} -\pause -\small\lstinputlisting[linerange={21-21},numbers=none,mathescape=true,basicstyle={\ttfamily},language=clingo]{examples/taxes.lp} -\quad -\pause -\begin{itemize} - \item Linear, modular translation to CASP using the \clingo\ Python API - \pause - \item Python version of \clingcon\ as solver - \pause - \item Bonus goal: implementation only by adding atoms and rules for each theory atom via the backend -\end{itemize} -\end{frame} - -\begin{frame} -\tableofcontents -\end{frame} - -\section{\HTC\ to \emph{CASP}: Syntactic and semantic differences} - -\begin{frame}{Input language} -\scriptsize\lstinputlisting[mathescape=true,basicstyle={\ttfamily},language=clingo]{examples/htc_lang.lp} -\end{frame} - -\begin{frame}{Example} -\scriptsize\lstinputlisting[linerange={13-29},mathescape=true,basicstyle={\ttfamily},language=clingo]{examples/taxes.lp} -\end{frame} - -\begin{frame}{Target language} -\scriptsize\lstinputlisting[mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/cp_lang.lp} -\end{frame} - -\begin{frame}{Semantic differences} - \begin{itemize} - \item \emph{CASP} does not allow variables to be undefined - \pause - \item \clingcon\ treats theory atoms in the body as \emph{strict, external} and theory atoms in the head as \emph{non-strict, defined} - \pause - \item \HTC\ stable models require values of variables to be \emph{founded}, variables may be undefined, no implicit choice for body atoms - \pause - \item - \lstinputlisting[linerange={1-1},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - \pause - \begin{tabular}{ll} - \clingcon : & $\{\{(\mathtt{x},v)\} \mid v \ne 1 \} \cup \{\{\mathtt{a}, (\mathtt{x},1)\}\}$\\ - \pause - \HTC : & $\{\emptyset\}$ - \end{tabular} - \pause - \item Add rules, sum constraints and auxiliary variables to implement constructs foreign to language of \clingcon - \end{itemize} -\end{frame} - - -\begin{frame}{Preprocessing: Seperate head from body} - \begin{itemize} - \item Use the abstract syntax tree to mark body and head theory atoms while parsing - \pause - \[ -\mathtt{\&}t\mathtt{\{}e_1:c_1,\dots,e_n:c_n\mathtt{\}} \prec k\pause \Rightarrow \mathtt{\&}t\mathtt{(}\mathit{l}\mathtt{)}\mathtt{\{}e_1:c_1,\dots,e_n:c_n\mathtt{\}}\prec k - \] - where $t$ is the name of the theory atom, $e_i$ are tuples of symbols, $c_i$ are conditions (both non-ground), $k$ is a theory term, $\prec$ is a relation symbol and $l\in\{\mathtt{head},\mathtt{body}\}$ - \pause - \item - \lstinputlisting[linerange={1-1},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - $\Rightarrow$ - \lstinputlisting[linerange={2-2},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - \end{itemize} -\end{frame} - -\section{Founding variable values} - -\begin{frame}{Define variables} - \begin{itemize} - \item For every variable \texttt{x} occurring in the program, capture definedness with atom \texttt{def(x)} and add the rule -\lstinputlisting[linerange={7-7},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - \pause - \item For every condition-free linear constraint atom - \lstinputlisting[linerange={3-3},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - add rule - \lstinputlisting[linerange={4-4},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - for every $\mathtt{x} \in \vars{e_1}\cup\dots\cup\vars{e_n}\cup\vars{k}$ - \end{itemize} -\end{frame} - -\begin{frame}{Translating linear constraint atoms in the body} - For every condition-free linear constraint atom - \lstinputlisting[linerange={8-8},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - \pause - \begin{itemize} - \item Copy the linear constraint and assign it to fresh atom - \pause - \item Do not communicate original linear constraint to \clingcon\ \pause - \item Add rules - \only<4>{\lstinputlisting[linerange={9-12},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}} - \only<5>{\lstinputlisting[linerange={13-15},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}} - where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_1}\cup\dots\cup\vars{e_n}\cup\vars{k}$ - \end{itemize} -\end{frame} - -\begin{frame}{Example} - We translate - \lstinputlisting[linerange={1-1},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp} - \pause - to - \only<2>{\lstinputlisting[linerange={16-19},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}} - \only<3->{\lstinputlisting[linerange={20-23},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/semantics.lp}} - \pause - \pause - \begin{tabular}{ll} - \clingcon : & $\{\{(x,0)\}\}$\\ - \pause - \HTC : & $\{\emptyset\}$ - \end{tabular} -\end{frame} - -\section{Translating conditional terms} -\begin{frame}{Translating conditional terms} - \[ -\mathtt{\&}t(l)\mathtt{\{}\dots,e_1:c_1,\dots,e_n:c_n,\dots\mathtt{\}} \prec k - \] - \vspace*{-.3cm} - \pause - \begin{itemize} - \item For every $e_i:c_i$, introduce auxiliary variable $\mathit{aux}_i$\pause\ and add following rules where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_i}$ - \small\lstinputlisting[linerange={1-5},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/conditional.lp} - \pause - \item Replace conditional terms with respective auxiliary variables - \small\lstinputlisting[linerange={6-9},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/conditional.lp} - \end{itemize} -\end{frame} - -\begin{frame}{Example: Vicious cycle} - \only<1>{\lstinputlisting[linerange={1-2},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp}} - \only<2>{\scriptsize\lstinputlisting[linerange={3-21},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp}} -\end{frame} - -\begin{frame}{Example: Vicious cycle} - Value for \texttt{x} is unfounded due to loop through: - \scriptsize\lstinputlisting[linerange={23-30},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp} -\end{frame} - -\begin{frame}{Example: Vicious cycle} - Value for \texttt{aux(0)} is unfounded due to loop through: - \small\lstinputlisting[linerange={31-34},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/vicious.lp} -\end{frame} - -\section{Translating assignments, range, minimum/maximum constraint} -\begin{frame}{Translating assignments and range constraints} - \begin{itemize} - \item For assignment $\mathtt{\&}t\mathtt{\{}e_1,\dots,e_n\mathtt{\}} =: x$, we add - \pause - \lstinputlisting[linerange={1-2},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/assignments.lp} - where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_1}\cup\dots\cup\vars{e_n}$ - \pause - \item For range constraint $\mathtt{\&in}\mathtt{\{}l\mathtt{..}u{\}} = x$, we add - \pause - \lstinputlisting[linerange={3-4},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/assignments.lp} - \end{itemize} -\end{frame} - -\begin{frame}{Translating minimum constraints} -\[\mathtt{\&min}(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k\] -\pause - \begin{itemize} - \item Add auxiliary variable $\mathit{min}$ and for every $e_i$, add following rules where $\{\mathtt{x}_1,\dots,\mathtt{x}_n\}=\vars{e_i}$ - \lstinputlisting[linerange={1-3},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp} - \pause - \item Check whether a correct value was selected - \lstinputlisting[linerange={4-4},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp} - \end{itemize} -\end{frame} - -\begin{frame}{Translating minimum constraints} -\[\mathtt{\&min}(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k\] -\pause - \begin{itemize} - \item If $l=\mathtt{body}$ - \lstinputlisting[linerange={5-5},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp} - \pause - \item If $l=\mathtt{head}$ - \lstinputlisting[linerange={6-7},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily},language=clingo]{examples/minmax.lp} - \end{itemize} -\end{frame} - -\begin{frame}{Translating maximum constraints} -\[\mathtt{\&max}(l)\mathtt{\{}e_1,\dots,e_n\mathtt{\}} \prec k\] -translates to -\[\mathtt{\&min}(l)\mathtt{\{}-e_1,\dots,-e_n\mathtt{\}} \prec' -k\] - \begin{itemize} - \item If $\prec=$ \texttt{<=}, $\prec'=$ \texttt{>=} - \item If $\prec=$ \texttt{>=}, $\prec'=$ \texttt{<=} - \item If $\prec=$ \texttt{<}, $\prec'=$ \texttt{>} - \item If $\prec=$ \texttt{>}, $\prec'=$ \texttt{<} - \item If $\prec=$ \texttt{=}, $\prec'=$ \texttt{=} - \end{itemize} -\end{frame} - -\section{Demonstration} -\begin{frame}{Let's do our taxes!} - \huge\centering\textcolor{blue}{Demo} -\end{frame} - -\end{document} diff --git a/slides/slides.toc b/slides/slides.toc deleted file mode 100644 index 94fd31c..0000000 --- a/slides/slides.toc +++ /dev/null @@ -1,5 +0,0 @@ -\beamer@sectionintoc {1}{\ensuremath {\mathit {HT}_{\tmspace -\thinmuskip {.1667em}C}}\ to \emph {CASP}: Syntactic and semantic differences}{15}{0}{1} -\beamer@sectionintoc {2}{Founding variable values}{30}{0}{2} -\beamer@sectionintoc {3}{Translating conditional terms}{42}{0}{3} -\beamer@sectionintoc {4}{Translating assignments, range, minimum/maximum constraint}{50}{0}{4} -\beamer@sectionintoc {5}{Demonstration}{61}{0}{5} diff --git a/test.lp b/test.lp new file mode 100644 index 0000000..c1ba258 --- /dev/null +++ b/test.lp @@ -0,0 +1,26 @@ +%* +weight(frame,42). +selected(frame). +selected(basket). + +&sus{ weight(P) } = W :- selected(P), weight(P,W). +:- &sus { weight(P) : selected(P) } >= 40. +:- &sum { weight(P) : selected(P) } >= 40. +*% + + +part(sportsframe). price(sportsframe,15). type(sportsframe,frame). +part(standardframe). price(standardframe,14). type(standardframe,frame). +part(fancysaddle). price(fancysaddle,6). type(fancysaddle,saddle). +part(standardsaddle). price(standardsaddle,5). type(standardsaddle,saddle). + +&sum{price(P)} = V :- price(P,V). + +pricelimit(20). +&sum{price(P) :: selected(P) : part(P)} <= X :- pricelimit(X). +:- selected(P), selected(P'), P', 1, 1) + loc = Location(pos, pos) + for rule in hbt.rules_to_add: + bld.add(Rule(loc,rule[0],rule[1])) self.prg.ground([("base", [])]) translator = Translator(self.prg, Config(self.maxint, self.minint, False, DEF)) diff --git a/tests/test_csp.py b/tests/test_csp.py deleted file mode 100644 index 46c9ff6..0000000 --- a/tests/test_csp.py +++ /dev/null @@ -1,323 +0,0 @@ -""" -Basic tests checking the whole system. -""" - -import unittest - -from tests import Solver, solve - -# pylint: disable=missing-docstring - - -class TestMain(unittest.TestCase): - def test_simple(self): - self.assertEqual( - solve( - """\ - &sum { 1 *y + (-5)*x } <= 0. - &sum { (-1)*y + 5 *x } <= 0. - &sum { 15*x } <= 15. - &sum { 10*x } <= 7. - """ - ), - [ - [("x", -4), ("y", -20)], - [("x", -3), ("y", -15)], - [("x", -2), ("y", -10)], - [("x", -1), ("y", -5)], - [("x", 0), ("y", 0)], - ], - ) - - self.assertEqual( - solve( - """\ - &sum { 1 *even + (-2)*_i } <= 0. - &sum { (-1)*even + 2 *_i } <= 0. - &sum { 1 *odd + (-2)*_i } <= 1. - &sum { (-1)*odd + 2 *_i } <= -1.""", - -2, - 2, - ), - [[("even", -2), ("odd", -1)], [("even", 0), ("odd", 1)]], - ) - - self.assertEqual( - solve( - """\ - a :- &sum{-1*x} <= 0. - b :- &sum{1*x} <= 5. - :- not a. - :- not b.""" - ), - [ - ["a", "b", ("x", 0)], - ["a", "b", ("x", 1)], - ["a", "b", ("x", 2)], - ["a", "b", ("x", 3)], - ["a", "b", ("x", 4)], - ["a", "b", ("x", 5)], - ], - ) - - self.assertEqual( - solve( - """\ - &sum { 1 * x + (-1) * y } <= -1. - &sum { 1 * y + (-1) * x } <= -1. - """ - ), - [], - ) - - self.assertEqual( - solve( - """\ - &sum { 1 } <= 2. - """ - ), - [[]], - ) - - self.assertEqual( - solve( - """\ - &sum { 2 } <= 1. - """ - ), - [], - ) - - self.assertEqual( - solve( - """\ - {a}. - &sum { 1 *x } <= -5 :- a. - &sum { (-1)*x } <= -5 :- not a. - """, - -6, - 6, - ), - [[("x", 5)], [("x", 6)], ["a", ("x", -6)], ["a", ("x", -5)]], - ) - - def test_parse(self): - self.assertEqual(solve("&sum { x(f(1+2)) } <= 0.", 0, 0), [[("x(f(3))", 0)]]) - self.assertEqual(solve("&sum { x(f(1-2)) } <= 0.", 0, 0), [[("x(f(-1))", 0)]]) - self.assertEqual(solve("&sum { x(f(-2)) } <= 0.", 0, 0), [[("x(f(-2))", 0)]]) - self.assertEqual(solve("&sum { x(f(2*2)) } <= 0.", 0, 0), [[("x(f(4))", 0)]]) - self.assertEqual(solve("&sum { x(f(4/2)) } <= 0.", 0, 0), [[("x(f(2))", 0)]]) - self.assertEqual(solve("&sum { x(f(9\\2)) } <= 0.", 0, 0), [[("x(f(1))", 0)]]) - self.assertEqual(solve("&sum { (a,b) } <= 0.", 0, 0), [[("(a,b)", 0)]]) - self.assertEqual(solve("&sum { x } = 5."), [[("x", 5)]]) - self.assertEqual( - solve("&sum { x } != 0.", -3, 3), - [[("x", -3)], [("x", -2)], [("x", -1)], [("x", 1)], [("x", 2)], [("x", 3)]], - ) - self.assertEqual( - solve("&sum { x } < 2.", -3, 3), - [[("x", -3)], [("x", -2)], [("x", -1)], [("x", 0)], [("x", 1)]], - ) - self.assertEqual(solve("&sum { x } > 1.", -3, 3), [[("x", 2)], [("x", 3)]]) - self.assertEqual( - solve("&sum { x } >= 1.", -3, 3), [[("x", 1)], [("x", 2)], [("x", 3)]] - ) - self.assertEqual( - solve("a :- &sum { x } >= 1.", -3, 3), - [ - [("x", -3)], - [("x", -2)], - [("x", -1)], - [("x", 0)], - ["a", ("x", 1)], - ["a", ("x", 2)], - ["a", ("x", 3)], - ], - ) - self.assertEqual( - solve("a :- &sum { x } = 1.", -3, 3), - [ - [("x", -3)], - [("x", -2)], - [("x", -1)], - [("x", 0)], - [("x", 2)], - [("x", 3)], - ["a", ("x", 1)], - ], - ) - self.assertEqual( - solve("&sum { 5*x + 10*y } = 20.", -3, 3), - [[("x", -2), ("y", 3)], [("x", 0), ("y", 2)], [("x", 2), ("y", 1)]], - ) - self.assertEqual( - solve("&sum { -5*x + 10*y } = 20.", -3, 3), - [[("x", -2), ("y", 1)], [("x", 0), ("y", 2)], [("x", 2), ("y", 3)]], - ) - - def test_singleton(self): - self.assertEqual(solve("&sum { x } <= 1.", 0, 2), [[("x", 0)], [("x", 1)]]) - self.assertEqual(solve("&sum { x } >= 1.", 0, 2), [[("x", 1)], [("x", 2)]]) - self.assertEqual( - solve("a :- &sum { x } <= 1.", 0, 2), - [[("x", 2)], ["a", ("x", 0)], ["a", ("x", 1)]], - ) - self.assertEqual(solve(":- &sum { x } <= 1.", 0, 2), [[("x", 2)]]) - self.assertEqual( - solve(":- not &sum { x } <= 1.", 0, 2), [[("x", 0)], [("x", 1)]] - ) - self.assertEqual( - solve("a :- &sum { x } <= 1. b :- not &sum { x } > 1.", 0, 2), - [[("x", 2)], ["a", "b", ("x", 0)], ["a", "b", ("x", 1)]], - ) - self.assertEqual( - solve(" :- &sum { x } <= 1. :- not &sum { x } > 1.", 0, 2), [[("x", 2)]] - ) - - def test_distinct(self): - self.assertEqual( - solve("&distinct { x; y }.", 0, 1), - [[("x", 0), ("y", 1)], [("x", 1), ("y", 0)]], - ) - self.assertEqual( - solve("&distinct { 2*x; 3*y }.", 2, 3), - [[("x", 2), ("y", 2)], [("x", 2), ("y", 3)], [("x", 3), ("y", 3)]], - ) - self.assertEqual(solve("&distinct { 0*x; 0*y }.", 0, 1), []) - self.assertEqual(solve("&distinct { 0 }.", 0, 1), [[]]) - self.assertEqual(solve("&distinct { 0; 0+0 }.", 0, 1), []) - self.assertEqual(solve("&distinct { 0; 1 }.", 0, 1), [[]]) - self.assertEqual(solve("&distinct { 2*x; (1+1)*x }.", 0, 1), []) - self.assertEqual( - solve("&distinct { y-x; x-y }.", 0, 1), - [[("x", 0), ("y", 1)], [("x", 1), ("y", 0)]], - ) - self.assertEqual( - solve("&distinct { x; y } :- c. &sum { x } = y :- not c. {c}.", 0, 1), - [ - [("x", 0), ("y", 0)], - [("x", 1), ("y", 1)], - ["c", ("x", 0), ("y", 1)], - ["c", ("x", 1), ("y", 0)], - ], - ) - self.assertEqual( - solve("&dom{1..1}=x. &dom{1..2}=y. &dom{1..3}=z. &distinct{x;y;z}."), - [[("x", 1), ("y", 2), ("z", 3)]], - ) - self.assertEqual( - solve("&dom{1..3}=x. &dom{2..3}=y. &dom{3..3}=z. &distinct{x;y;z}."), - [[("x", 1), ("y", 2), ("z", 3)]], - ) - self.assertEqual( - solve( - """\ - &dom { 1..2 } = x. - &dom { 1..2 } = y. - &dom { 1..2 } = z. - &distinct { 2*x+3*y+5*z; 5*x+2*y+3*z; 3*x+5*y+2*z }. - """ - ), - [ - [("x", 1), ("y", 1), ("z", 2)], - [("x", 1), ("y", 2), ("z", 1)], - [("x", 1), ("y", 2), ("z", 2)], - [("x", 2), ("y", 1), ("z", 1)], - [("x", 2), ("y", 1), ("z", 2)], - [("x", 2), ("y", 2), ("z", 1)], - ], - ) - self.assertEqual( - solve( - """\ - &dom { 1..2 } = x. - &dom { 1..2 } = y. - &dom { 1..2 } = z. - &distinct { 2*x+3*y+5*z+1; 5*x+2*y+3*z; 3*x+5*y+2*z-1 }. - """ - ), - [ - [("x", 1), ("y", 1), ("z", 1)], - [("x", 1), ("y", 1), ("z", 2)], - [("x", 1), ("y", 2), ("z", 2)], - [("x", 2), ("y", 1), ("z", 1)], - [("x", 2), ("y", 2), ("z", 2)], - ], - ) - - def test_dom(self): - self.assertEqual( - solve("&dom { 0;1..2;2..3;5 } = x.", -10, 10), - [[("x", 0)], [("x", 1)], [("x", 2)], [("x", 3)], [("x", 5)]], - ) - self.assertEqual( - solve( - "1 {a; b} 1. &dom { 0;2;4 } = x :- a. &dom { 1;3;5 } = x :- b.", -10, 10 - ), - [ - ["a", ("x", 0)], - ["a", ("x", 2)], - ["a", ("x", 4)], - ["b", ("x", 1)], - ["b", ("x", 3)], - ["b", ("x", 5)], - ], - ) - self.assertEqual( - solve("&dom { 0-1..0+1 } = x.", -10, 10), - [[("x", -1)], [("x", 0)], [("x", 1)]], - ) - - def test_multishot(self): - s = Solver(0, 3) - self.assertEqual( - s.solve("&sum { x } <= 2."), [[("x", 0)], [("x", 1)], [("x", 2)]] - ) - self.assertEqual(s.solve(""), [[("x", 0)], [("x", 1)], [("x", 2)]]) - self.assertEqual(s.solve("&sum { x } <= 1."), [[("x", 0)], [("x", 1)]]) - self.assertEqual(s.solve("&sum { x } <= 0."), [[("x", 0)]]) - self.assertEqual(s.solve("&sum { x } <= 1."), [[("x", 0)]]) - self.assertEqual(s.solve("&sum { x } <= 2."), [[("x", 0)]]) - - def test_shift(self): - self.assertEqual( - solve("{a}. :- a, &sum { x } < 3. :- not a, &sum { x } > 0.", 0, 3), - [[("x", 0)], ["a", ("x", 3)]], - ) - - def test_show(self): - self.assertEqual( - solve( - "&sum { p(X) } = 0 :- X=1..3. &sum { q(X) } = 0 :- X=1..3. &show { }." - ), - [[]], - ) - self.assertEqual( - solve( - "&sum { p(X) } = 0 :- X=1..3. &sum { q(X) } = 0 :- X=1..3. &show { p/1 }." - ), - [[("p(1)", 0), ("p(2)", 0), ("p(3)", 0)]], - ) - self.assertEqual( - solve( - "&sum { p(X) } = 0 :- X=1..3. &sum { q(X) } = 0 :- X=1..3. &show { p(1); p(2); q(1) }." - ), - [[("p(1)", 0), ("p(2)", 0), ("q(1)", 0)]], - ) - self.assertEqual( - solve( - "&sum { p(X) } = 0 :- X=1..3. &sum { q(X) } = 0 :- X=1..3. &show { p/1; q(1) }." - ), - [[("p(1)", 0), ("p(2)", 0), ("p(3)", 0), ("q(1)", 0)]], - ) - - def test_set(self): - self.assertEqual(solve("&sum { 1;1 } = x."), [[("x", 2)]]) - self.assertEqual(solve("&sum { 1 : X=1..3 } = x."), [[("x", 3)]]) - self.assertEqual(solve("&sum { 1 : X=(1;2;3) } = x."), [[("x", 3)]]) - self.assertEqual( - solve( - "&sum { v(X) } = X :- X=1..3. &sum { v(X) : X=1..2; v(X) : X=2..3 } = x." - ), - [[("v(1)", 1), ("v(2)", 2), ("v(3)", 3), ("x", 8)]], - ) diff --git a/tests/test_fs.py b/tests/test_fs.py deleted file mode 100644 index 1e7abcd..0000000 --- a/tests/test_fs.py +++ /dev/null @@ -1,209 +0,0 @@ -""" -Basic tests checking the whole system. -""" - -import unittest - -from tests import solve - -FSI = """\ - machine(1). machine(2). -task(a). duration(a,1,3). duration(a,2,4). -task(b). duration(b,1,1). duration(b,2,6). -task(c). duration(c,1,5). duration(c,2,5). -""" - -FSE = """\ -1 { cycle(T,U) : task(U), U != T } 1 :- task(T). -1 { cycle(T,U) : task(T), U != T } 1 :- task(U). - -reach(M) :- M = #min { T : task(T) }. -reach(U) :- reach(T), cycle(T,U). -:- task(T), not reach(T). - -1 { start(T) : task(T) } 1. - -permutation(T,U) :- cycle(T,U), not start(U). - -seq((T,M),(T,M+1),D) :- task(T), duration(T,M,D), machine(M+1). -seq((T1,M),(T2,M),D) :- permutation(T1,T2), duration(T1,M,D). - -&sum { 1*T1 + -1*T2 } <= -D :- seq(T1,T2,D). -&sum { -1*(T,M) } <= 0 :- duration(T,M,D). -&sum { 1*(T,M) } <= B :- duration(T,M,D), B=bound-D. - -#show permutation/2. -""" - -FSD = """\ -1 { cycle(T,U) : task(U), U != T } 1 :- task(T). -1 { cycle(T,U) : task(T), U != T } 1 :- task(U). - -reach(M) :- M = #min { T : task(T) }. -reach(U) :- reach(T), cycle(T,U). -:- task(T), not reach(T). - -1 { start(T) : task(T) } 1. - -permutation(T,U) :- cycle(T,U), not start(U). - -seq((T,M),(T,M+1),D) :- task(T), duration(T,M,D), machine(M+1). -seq((T1,M),(T2,M),D) :- permutation(T1,T2), duration(T1,M,D). - -&diff { T1-T2 } <= -D :- seq(T1,T2,D). -&diff { 0-(T,M) } <= 0 :- duration(T,M,D). -&sum { (T,M)-0 } <= B :- duration(T,M,D), B=bound-D. - -#show permutation/2. -""" - -SOL11 = [ - [ - "permutation(a,c)", - "permutation(b,a)", - ("(a,1)", 1), - ("(a,2)", 7), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 4), - ("(c,2)", 11), - ], - [ - "permutation(a,c)", - "permutation(b,a)", - ("(a,1)", 1), - ("(a,2)", 7), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 5), - ("(c,2)", 11), - ], - [ - "permutation(a,c)", - "permutation(b,a)", - ("(a,1)", 1), - ("(a,2)", 7), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 6), - ("(c,2)", 11), - ], - [ - "permutation(a,c)", - "permutation(b,a)", - ("(a,1)", 2), - ("(a,2)", 7), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 5), - ("(c,2)", 11), - ], - [ - "permutation(a,c)", - "permutation(b,a)", - ("(a,1)", 2), - ("(a,2)", 7), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 6), - ("(c,2)", 11), - ], - [ - "permutation(a,c)", - "permutation(b,a)", - ("(a,1)", 3), - ("(a,2)", 7), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 6), - ("(c,2)", 11), - ], -] - -SOL16 = SOL11 + [ - [ - "permutation(b,c)", - "permutation(c,a)", - ("(a,1)", 6), - ("(a,2)", 12), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 1), - ("(c,2)", 7), - ], - [ - "permutation(b,c)", - "permutation(c,a)", - ("(a,1)", 7), - ("(a,2)", 12), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 1), - ("(c,2)", 7), - ], - [ - "permutation(b,c)", - "permutation(c,a)", - ("(a,1)", 7), - ("(a,2)", 12), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 2), - ("(c,2)", 7), - ], - [ - "permutation(b,c)", - "permutation(c,a)", - ("(a,1)", 8), - ("(a,2)", 12), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 1), - ("(c,2)", 7), - ], - [ - "permutation(b,c)", - "permutation(c,a)", - ("(a,1)", 8), - ("(a,2)", 12), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 2), - ("(c,2)", 7), - ], - [ - "permutation(b,c)", - "permutation(c,a)", - ("(a,1)", 9), - ("(a,2)", 12), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 1), - ("(c,2)", 7), - ], - [ - "permutation(b,c)", - "permutation(c,a)", - ("(a,1)", 9), - ("(a,2)", 12), - ("(b,1)", 0), - ("(b,2)", 1), - ("(c,1)", 2), - ("(c,2)", 7), - ], -] - - -# pylint: disable=missing-docstring - - -class TestMain(unittest.TestCase): - def test_fse(self): - self.assertEqual(solve(FSE + FSI, maxint=10, options=["-c", "bound=16"]), []) - self.assertEqual(solve(FSE + FSI, maxint=11, options=["-c", "bound=16"]), SOL11) - self.assertEqual(solve(FSE + FSI, options=["-c", "bound=16"]), SOL16) - - def test_fsd(self): - self.assertEqual(solve(FSD + FSI, maxint=10, options=["-c", "bound=16"]), []) - self.assertEqual(solve(FSD + FSI, maxint=11, options=["-c", "bound=16"]), SOL11) - self.assertEqual(solve(FSD + FSI, options=["-c", "bound=16"]), SOL16) diff --git a/tests/test_htc.py b/tests/test_htc.py index 7a7c39e..8963dff 100644 --- a/tests/test_htc.py +++ b/tests/test_htc.py @@ -199,7 +199,7 @@ def test_naming(self): self.assertEqual( solve( """\ - &fsum{x((),y)}=4.""", + &sus{x((),y)}=4.""", -10, 10, ), @@ -208,7 +208,7 @@ def test_naming(self): self.assertEqual( solve( """\ - &fsum{4}=x(y,()).""", + &sus{4}=x(y,()).""", -10, 10, ), @@ -238,7 +238,7 @@ def test_defined(self): solve( """\ b :- &df{x}. - &fsum{x} = 0.""", + &sus{x} = 0.""", -10, 10, ), @@ -248,7 +248,7 @@ def test_defined(self): solve( """\ b :- &df{x}. - &fsum{y} =: x.""", + &sus{y} =: x.""", -10, 10, ), @@ -258,8 +258,8 @@ def test_defined(self): solve( """\ b :- &df{x}. - &fsum{y} =: x. - &fsum{y} = 2.""", + &sus{y} =: x. + &sus{y} = 2.""", -10, 10, ), @@ -270,7 +270,7 @@ def test_multiset(self): self.assertEqual( solve( """\ - &fsum{1;1}=2.""", + &sus{1;1}=2.""", -10, 10, ), @@ -279,7 +279,7 @@ def test_multiset(self): self.assertEqual( solve( """\ - &fsum{N:N=1..2; M:M=2..3} = 8.""", + &sus{N:N=1..2; M:M=2..3} = 8.""", -10, 10, ), @@ -288,7 +288,7 @@ def test_multiset(self): self.assertEqual( solve( """\ - &fsum{x;x} = 2*x.""", + &sus{x;x} = 2*x.""", 2, 2, ), @@ -297,7 +297,7 @@ def test_multiset(self): self.assertEqual( solve( """\ - &fsum{x(N):N=1..2;x(M):M=2..3} = x(1)+2*x(2)+x(3).""", + &sus{x(N):N=1..2;x(M):M=2..3} = x(1)+2*x(2)+x(3).""", 2, 2, ), @@ -309,7 +309,7 @@ def test_conditionals(self): solve( """\ {a}. - &fsum{1:a} = x. + &sus{1:a} = x. """, -10, 10, @@ -320,8 +320,8 @@ def test_conditionals(self): solve( """\ {a}. - &fsum{1} = x. - b :- &fsum{1:a} < x. + &sus{1} = x. + b :- &sus{1:a} < x. """, -10, 10, @@ -331,8 +331,8 @@ def test_conditionals(self): self.assertEqual( solve( """\ - &fsum{x}=1 :- &fsum{ 1 : a }>= 0. - a :- &fsum{x}=1. + &sus{x}=1 :- &sus{ 1 : a }>= 0. + a :- &sus{x}=1. """, -10, 10, @@ -343,7 +343,7 @@ def test_conditionals(self): solve( """\ {a;b}. - &fsum{1:a,b;2:a;3:b} = x. + &sus{1:a,b;2:a;3:b} = x. """, -10, 10, @@ -354,7 +354,7 @@ def test_conditionals(self): solve( """\ {a;b}. - &fsum{1:a,b} = x. + &sus{1:a,b} = x. """, -10, 10, @@ -364,7 +364,7 @@ def test_conditionals(self): self.assertEqual( solve( """\ - b :- &fsum{ v : not b } >= 1. + b :- &sus{ v : not b } >= 1. """, -10, 10, @@ -375,7 +375,7 @@ def test_conditionals(self): solve( """\ {a;b}. - &fsum{1:a, not b} = x. + &sus{1:a, not b} = x. """, -10, 10, @@ -387,8 +387,8 @@ def test_assignments(self): self.assertEqual( solve( """\ - &fsum{1} =: x. - &fsum{z} =: y. + &sus{1} =: x. + &sus{z} =: y. """, -10, 10, @@ -399,8 +399,8 @@ def test_assignments(self): solve( """\ {a}. - &fsum{z : a; 1} =: x. - &fsum{x} =: y. + &sus{z : a; 1} =: x. + &sus{x} =: y. """, -10, 10, @@ -411,8 +411,8 @@ def test_assignments(self): solve( """\ {a}. - &fsum{1} =: x :- a. - b :- &fsum{x} > 0. + &sus{1} =: x :- a. + b :- &sus{x} > 0. """, -10, 10, @@ -422,7 +422,7 @@ def test_assignments(self): self.assertEqual( solve( """\ - &fin{0..2} =: x. + &in{0..2} =: x. """, -10, 10, @@ -432,7 +432,7 @@ def test_assignments(self): self.assertEqual( solve( """\ - &fin{y..z} =: x. + &in{y..z} =: x. """, -10, 10, @@ -442,9 +442,9 @@ def test_assignments(self): self.assertEqual( solve( """\ - &fsum{z} = 1. - &fsum{y} = 2. - &fin{y..z} =: x. + &sus{z} = 1. + &sus{y} = 2. + &in{y..z} =: x. """, -10, 10, @@ -454,9 +454,9 @@ def test_assignments(self): self.assertEqual( solve( """\ - &fsum{z} = 2. - &fsum{y} = 1. - &fin{y..z} =: x. + &sus{z} = 2. + &sus{y} = 1. + &in{y..z} =: x. """, -10, 10, @@ -470,9 +470,9 @@ def test_assignments(self): solve( """\ {a}. - &fsum{z} = 2 :- a. - &fsum{y} = 1. - &fin{y..z} =: x. + &sus{z} = 2 :- a. + &sus{y} = 1. + &in{y..z} =: x. """, -10, 10, @@ -488,7 +488,7 @@ def test_min(self): self.assertEqual( solve( """\ - &fmin{3;2;1}=:x. + &min{3;2;1}=:x. """, -10, 10, @@ -498,8 +498,8 @@ def test_min(self): self.assertEqual( solve( """\ - &fsum{x} = 1. - a :- &fmin{3;x} < 2. + &sus{x} = 1. + a :- &min{3;x} < 2. """, -10, 10, @@ -510,7 +510,7 @@ def test_min(self): solve( """\ {a}. - &fmin{3;2;1:a}=:x. + &min{3;2;1:a}=:x. """, -10, 10, @@ -529,8 +529,8 @@ def test_min(self): solve( """\ {b}. - &fsum{x} = 1. - a :- &fmin{3; x:b} < 2. + &sus{x} = 1. + a :- &min{3; x:b} < 2. """, -10, 10, @@ -549,7 +549,7 @@ def test_min(self): self.assertEqual( solve( """\ - a :- &fmin{1:a} > 0. + a :- &min{1:a} > 0. """, -10, 10, @@ -561,7 +561,7 @@ def test_max(self): self.assertEqual( solve( """\ - &fmax{3;2;1}=:x. + &max{3;2;1}=:x. """, -10, 10, @@ -571,8 +571,8 @@ def test_max(self): self.assertEqual( solve( """\ - &fsum{x} = 3. - a :- &fmax{1;x} > 2. + &sus{x} = 3. + a :- &max{1;x} > 2. """, -10, 10, @@ -583,7 +583,7 @@ def test_max(self): solve( """\ {a}. - &fmax{3;2;4:a}=:x. + &max{3;2;4:a}=:x. """, -10, 10, @@ -602,8 +602,8 @@ def test_max(self): solve( """\ {b}. - &fsum{x} = 2. - a :- &fmax{1; x:b} <= 1. + &sus{x} = 2. + a :- &max{1; x:b} <= 1. """, -10, 10, @@ -620,6 +620,156 @@ def test_max(self): ], ) + def test_choice_sum(self): + self.assertEqual( + solve( + """\ + &sum{ 4 :: a } = 4. + """, + -10, + 10, + ), + [["a"]], + ) + self.assertEqual( + solve( + """\ + &sum{ x :: a } = 4. + """, + -10, + 10, + ), + [['a', ('x', 4)]], + ) + self.assertEqual( + solve( + """\ + &sum{ x } = 2. + &sum{ x :: a } = 4. + """, + -10, + 10, + ), + [], + ) + self.assertEqual( + solve( + """\ + &sum{ x :: a ; y :: b ; 2} = 4. + """, + -2, + 2, + ), + [['a', ('x', 2), ('y', 0)], ['a', 'b', ('x', 0), ('y', 2)], ['a', 'b', ('x', 0), ('y', 2)], ['a', 'b', ('x', 1), ('y', 1)], ['a', 'b', ('x', 2), ('y', 0)], ['a', 'b', ('x', 2), ('y', 0)], ['b', ('x', 0), ('y', 2)]], + ) + self.assertEqual( + solve( + """\ + &sum{ 2*x-12 :: a } = 4. + """, + -10, + 10, + ), + [['a', ('x', 8)]], + ) + self.assertEqual( + solve( + """\ + r(1). {r(2)}. + &sum{ x(P) :: a(P) : r(P) } = 4. + """, + -2, + 2, + ), + [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 2), ('x(2)', 2)]], + ) + self.assertEqual( + solve( + """\ + r(1). {r(2)}. + &sum{ x(P) :: a(P) : r(P) } = 4 :- r(P). + """, + -4, + 4, + ), + [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 4), ('x(2)', 4)], ['a(1)', 'r(1)', ('x(1)', 4), ('x(2)', 0)]], + ) + + def test_choice_sus(self): + self.assertEqual( + solve( + """\ + &sus{ 4 :: a } = 4. + """, + -10, + 10, + ), + [["a"]], + ) + self.assertEqual( + solve( + """\ + &sus{ x :: a } = 4. + """, + -10, + 10, + ), + [['a', ('x', 4)]], + ) + self.assertEqual( + solve( + """\ + &sus{ x } = 2. + &sus{ x :: a } = 4. + """, + -10, + 10, + ), + [], + ) + self.assertEqual( + solve( + """\ + &sus{ x :: a ; y :: b ; 2} = 4. + """, + -2, + 2, + ), + [['a', ('x', 2), ('y', 0)], ['a', 'b', ('x', 0), ('y', 2)], ['a', 'b', ('x', 1), ('y', 1)], ['a', 'b', ('x', 2), ('y', 0)], ['b', ('x', 0), ('y', 2)]], + ) + self.assertEqual( + solve( + """\ + &sus{ 2*x-12 :: a } = 4. + """, + -10, + 10, + ), + [['a', ('x', 8)]], + ) + self.assertEqual( + solve( + """\ + r(1). {r(2)}. + &sus{ x(P) :: a(P) : r(P) } = 4. + """, + -2, + 2, + ), + [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 2), ('x(2)', 2)]], + ) + self.assertEqual( + solve( + """\ + r(1). {r(2)}. + &sus{ x(P) :: a(P) : r(P) } = 4 :- r(P). + """, + -4, + 4, + ), + [['a(1)', 'a(2)', 'r(1)', 'r(2)', ('x(1)', 4), ('x(2)', 4)], ['a(1)', 'r(1)', ('x(1)', 4), ('x(2)', 0)]], + ) + def test_taxes(self): answers = solve( """\ @@ -637,17 +787,17 @@ def test_taxes(self): 1 { lives(P,R) : region(R) } 1 :- person(P). - &fsum{ 0 } =: deduction(P) :- person(P), not deduction(P,_,_). - &fin{ L..H } =: deduction(P) :- deduction(P,L,H). - &fsum{ T } =: rate(P) :- lives(P,R), income(P,I), + &sus{ 0 } =: deduction(P) :- person(P), not deduction(P,_,_). + &in{ L..H } =: deduction(P) :- deduction(P,L,H). + &sus{ T } =: rate(P) :- lives(P,R), income(P,I), T = #max{ T' : rate(R,L,T'), I>=L}. - &fsum{ I*rate(P)-100*deduction(P) } =: 100*tax(P) :- income(P,I). - &fsum{ tax(P) : lives(P,R) } =: total(R) :- region(R). - &fmin{ tax(P) : person(P) } =: min. - &fmax{ tax(P) : person(P) } =: max. - min_taxes(P) :- &fmin{ tax(P') : person(P') } = tax(P), person(P). - max_taxes(P) :- &fmax{ tax(P') : person(P') } = tax(P), person(P). + &sus{ I*rate(P)-100*deduction(P) } =: 100*tax(P) :- income(P,I). + &sus{ tax(P) : lives(P,R) } =: total(R) :- region(R). + &min{ tax(P) : person(P) } =: min. + &max{ tax(P) : person(P) } =: max. + min_taxes(P) :- &min{ tax(P') : person(P') } = tax(P), person(P). + max_taxes(P) :- &max{ tax(P') : person(P') } = tax(P), person(P). #show lives/2. #show min_taxes/1. @@ -668,23 +818,23 @@ def test_car(self): #const n = 8. time(0..n). step(I,I+1) :- time(I), I < n. - &fsum {s(I)+D} =: s(I') :- acc(D,I'), step(I,I'). - &fsum {s(I)-D} =: s(I') :- slow(D,I'), step(I,I'). + &sus {s(I)+D} =: s(I') :- acc(D,I'), step(I,I'). + &sus {s(I)-D} =: s(I') :- slow(D,I'), step(I,I'). - &fsum {s(I)} =: s(I') :- not &fsum{ s(I') } != s(I), step(I,I'). + &sus {s(I)} =: s(I') :- not &sus{ s(I') } != s(I), step(I,I'). - def_s(I) :- time(I), &fsum{s(I); -s(I)}=0. + def_s(I) :- time(I), &sus{s(I); -s(I)}=0. - &fsum {p(I)+s(I)} =: p(I') :- def_s(I), step(I,I'). + &sus {p(I)+s(I)} =: p(I') :- def_s(I), step(I,I'). - &fsum {400000} =: rdpos. - &fsum {90000} =: rdlimit. % <<< ADDED <<< + &sus {400000} =: rdpos. + &sus {90000} =: rdlimit. % <<< ADDED <<< - fine(I') :- &fsum{ p(I) } < rdpos, &fsum{ p(I') } >= rdpos, step(I,I'), - &fsum{ s(I') } > rdlimit. + fine(I') :- &sus{ p(I) } < rdpos, &sus{ p(I') } >= rdpos, step(I,I'), + &sus{ s(I') } > rdlimit. - &fsum {0} =: p(0). - &fsum {80000} =: s(0). + &sus {0} =: p(0). + &sus {80000} =: s(0). acc(11350,4). slow(2301,6). diff --git a/tests/test_money.py b/tests/test_money.py deleted file mode 100644 index 9e67c88..0000000 --- a/tests/test_money.py +++ /dev/null @@ -1,56 +0,0 @@ -""" -Basic tests checking the whole system. - -Note: this would also a good example to check show, domain and distinct -constraints should we ever implement them. -""" - -import unittest - -from tests import solve - -DOM = """\ -&sum { X } <= 9 :- _letter(X). -&sum { X } >= 0 :- _letter(X). -""" - -DOMC = """\ -&dom {0..9} = X :- _letter(X). -""" - -DIST = """\ -&sum { X } != Y :- _letter(X), _letter(Y), X < Y. -""" - -DISTC = """\ -&distinct {X : _letter(X)}. -""" - -SMM = """\ -_letter(s;e;n;d;m;o;r;y). - -&sum { 1000*s + 100*e + 10*n + 1*d - ; 1000*m + 100*o + 10*r + 1*e - } = 10000*m + 1000*o + 100*n + 10*e + 1*y. -&sum { m } != 0. - -%&show {X : _letter(X)}. -""" - -SOL = [[("d", 7), ("e", 5), ("m", 1), ("n", 6), ("o", 0), ("r", 8), ("s", 9), ("y", 2)]] -SOL10 = [ - [("d", 5), ("e", 8), ("m", 1), ("n", 0), ("o", 2), ("r", 7), ("s", 10), ("y", 3)], - [("d", 6), ("e", 8), ("m", 1), ("n", 0), ("o", 2), ("r", 7), ("s", 10), ("y", 4)], -] + SOL - - -# pylint: disable=missing-docstring - - -class TestMain(unittest.TestCase): - def test_smm(self): - for dist in (DIST, DISTC): - for dom in (DOM, DOMC): - self.assertEqual(solve(dist + dom + SMM), SOL) - self.assertEqual(solve(dist + SMM, minint=0, maxint=9), SOL) - self.assertEqual(solve(dist + SMM, minint=0, maxint=10), SOL10)