% Albert Cao
                % Pizza Problem - Ordering pizza for the boys.
                
                % https://www.minizinc.org/doc-2.5.3/en/part_2_tutorial.html
                
                % Given:
                int: n;
                int: m;
                
                set of int: pizzas = 1..n; % n
                set of int: coupons = 1..m; % m
                array[pizzas] of int: price; % of each pizza
                array[coupons] of int: buy; % we must buy a certain number of pizzas to use each coupon
                array[coupons] of int: free; % each coupon we use lets us get some number of pizzas free
                int: costBound; % the amount of money we have to spend.
                
                % Find:
                var set of pizzas: paid; % set of pizzas we will pay for
                var set of coupons: used; % set of coupons we will use
                array[coupons, pizzas] of var bool: justifies; % holds if pizza p is one of the pizzas purchased to justify using coupon c
                array[coupons, pizzas] of var bool: usedFor; % holds if we are getting pizza p free by using coupon c (p = price, c = buy)
                var int: cost = sum(p in paid)(price[p]); % the final amount of money spent.
                
                % Constraint 1 - we pay for exactly the pizzas we don't get for free by using coupons.
                % For all pizzas p, p is in paid if and only if there is not a coupon c that was used to get p.
                % Defines the set of paid pizzas.
                constraint 
                    forall(p in pizzas) (
                    (p in paid) <-> not exists(c in used)(usedFor[c, p])
                    );
                    
                % Constraint 2 - Used is the set of coupons we use.
                % For all coupons c, c is in used if and only if there is a pizza p that was received by using c.
                % Defines the set of used coupons.
                constraint
                    forall(c in coupons) (
                    (c in used) <-> exists(p in pizzas)(usedFor[c, p])
                    );
                
                % Constraint 3 - Any coupon we used must be justified by enough paid pizzas.
                % For all coupons c, if c is in used, then the number of pizzas p that we used to justify applying c is at least as many as the number of pizzas c says we have to buy.
                constraint
                    forall(c in coupons) (
                    (c in used) -> sum(p in pizzas)(justifies[c, p]) >= (buy[c])
                    );
                    
                % Constraint 4 - No coupon is used for too many pizzas.
                % For all coupons c, the number of pizzas we get for free by applying a coupon is at most the number of pizzas c says we're allowed to get free.
                constraint
                    forall(c in coupons) (
                    sum(p in pizzas)(usedFor[c, p]) <= (free[c])
                    );
                
                % Constraint 5 - Each free pizza costs at most as much as the cheapest pizza purchased to justify the coupon used.
                % For all coupons c, and every 2 pizzas p1, p2 (that are not identical), if we used c to justify getting p1 for free, and we bought p2 to justify applying c, 
                % then the price of p1 must be at most the price of p2.
                constraint
                    forall(c in coupons, p1, p2 in pizzas where p1 != p2) (
                    (usedFor[c, p1] /\ justifies[c, p2]) -> (price[p1] <= price[p2])
                    );
                
                % Constraint 6 - We pay for all pizzas that justify using coupons.
                % For all coupons c and pizzas p, if p is used to justify applying c, then we must pay for p.
                constraint
                    forall(c in coupons, p in pizzas) (
                    justifies[c, p] -> (p in paid)
                    );
                    
                % Constraint 7 - The total cost is not too high.
                % The price of the sum over all pizzas p that are paid for is at most costBound.
                constraint
                    sum(p in paid)(price[p]) <= costBound;
                
                % Constraint 8 - Justifies and UsedFor hold only of coupon-pizza pairs.
                % For all coupons c and pizzas p, if justifies(c, p) then c has to be a coupon and p has to be a pizza.
                % For all coupons c and pizzas p, if usedFor(c, p) then c has to be a coupon and p has to be a pizza. 
                constraint
                    forall(c in coupons, p in pizzas) (
                    (justifies[c, p] -> (1 <= c /\ c <= m /\ 1 <= p /\ p <= n)) /\
                    (usedFor[c, p] -> (1 <= c /\ c <= m /\ 1 <= p /\ p <= n))
                    );
                    
                % Bonus Constraint - For all coupons c and pizzas p, if c has been used to justify getting p, then it cannot be used again.
                % For all coupons c and pizzas p, if justifies(c, p) then there is not a coupon q not equal to c that was used to justify getting p.
                constraint
                    forall(c in coupons, p in pizzas) (
                    (justifies[c,p] -> not exists(q in coupons where c != q)(justifies[q,p]))
                    );
                
                % Such that: we get all pizzas, cost is less than or equal to costBound, and coupons are used only if justified.
                solve minimize cost;
                
                % Print output.
                output ["cost(" ++ show(cost) ++ ")\n" ++ "costBound(" ++ show(costBound) ++ ")\n"];
            

                n = 4;
                price = [10,5,20,15];
                m = 2;
                buy = [1,2];
                free = [1,1];
                costBound = 50;