#include "vision.h"
#include <bits/stdc++.h>
using namespace std;
void construct_network(int H, int W, int K) {
int qidx = H * W;
vector<int> base(100);
vector<int> Ns;
base[1] = H * W; // 1: FALSE | TRUE
add_xor({0, 0}), qidx++;
add_not(qidx - 1), qidx++;
// ----------
base[10] = qidx; // 10: row[i] >= 1
for (int i = 0; i < H; i++) {
Ns.clear();
for (int j = 0; j < W; j++) {
Ns.push_back(i * W + j);
}
add_or(Ns), qidx++;
}
base[11] = qidx; // 11: row[i] == 0
for (int i = 0; i < H; i++) {
add_not(base[10] + i), qidx++;
}
base[12] = qidx; // 12: count(row[i]) == 1
for (int i = 0; i < H; i++) {
Ns.clear();
for (int j = 0; j < W; j++) {
Ns.push_back(i * W + j);
}
add_xor(Ns), qidx++;
}
base[13] = qidx; // 13: count(row[i]) == 2
for (int i = 0; i < H; i++) {
add_xor({base[10] + i, base[12] + i}), qidx++;
}
base[14] = qidx; // 14: count(row[i]) >= 1 AND count(row[i+d]) >= 1 (d=[1,H/2))
for (int d = 1; d < H / 2; d++) {
for (int i = 0; i + d < H; i++) {
add_and({base[10] + i, base[10] + i + d}), qidx++;
}
}
base[15] = qidx; // X
int lb = 0, rb = H - 1 - (H % 2 == 0);
while (lb < rb) {
Ns.clear();
for (int i = 0; i <= lb; i++) {
Ns.push_back(base[10] + i);
}
add_or(Ns), qidx++;
Ns.clear();
for (int i = rb; i < H; i++) {
Ns.push_back(base[11] + i);
}
add_and(Ns), qidx++;
add_and({qidx - 1, qidx - 2}), qidx++;
lb++, rb--;
}
base[16] = qidx; // 16: pre[0] + ... + pre[l] >= 1 AND pre[r] + ... + pre[H-1] == 0
for (int i = 0, idx = base[15] + 2; idx < base[16]; i++, idx += 3) {
add_and({idx}), qidx++;
}
base[17] = qidx; // X
lb = 0, rb = H - 1 - (H % 2 == 0);
while (lb < rb) {
Ns.clear();
for (int i = 0; i <= lb; i++) {
Ns.push_back(base[11] + i);
}
add_and(Ns), qidx++;
Ns.clear();
for (int i = rb; i < H; i++) {
Ns.push_back(base[10] + i);
}
add_or(Ns), qidx++;
add_and({qidx - 1, qidx - 2}), qidx++;
lb++, rb--;
}
base[18] = qidx; // 18: pre[0] + ... + pre[l] == 0 AND pre[r] + ... + pre[H-1] >= 1
for (int i = 0, idx = base[17] + 2; idx < base[18]; i++, idx += 3) {
add_and({idx}), qidx++;
}
base[30] = qidx; // 30: diff of row <= d (-1~H)
add_and({base[1]}), qidx++; // -1 (FALSE)
Ns.clear(); // 0
for (int i = 0; i < H; i++) {
Ns.push_back(base[13] + i);
}
add_or(Ns), qidx++;
for (int d = 1; d < H / 2; d++) { // 1 ~ H/2-1
Ns.clear();
for (int i = 0; i + d < H; i++) {
Ns.push_back(base[14] + i);
}
add_or(Ns), qidx++;
}
for (int d = H / 2, idx = 0; d <= H - 2; d++, idx++) { // H/2 ~ H-2
Ns.clear();
for (int i = d; i < H - d; i++) {
Ns.push_back(base[10] + i);
}
Ns.push_back(base[16] + (d - H / 2));
Ns.push_back(base[18] + (d - H / 2));
add_or(Ns), qidx++;
}
add_and({base[1] + 1}), qidx++; // H-1 (TRUE)
// ----------
base[40] = qidx; // 40: col[j] >= 1
for (int j = 0; j < W; j++) {
Ns.clear();
for (int i = 0; i < H; i++) {
Ns.push_back(i * W + j);
}
add_or(Ns), qidx++;
}
base[41] = qidx; // 41: col[j] == 0
for (int j = 0; j < W; j++) {
add_not(base[40] + j), qidx++;
}
base[42] = qidx; // 42: count(col[j]) == 1
for (int j = 0; j < W; j++) {
Ns.clear();
for (int i = 0; i < H; i++) {
Ns.push_back(i * W + j);
}
add_xor(Ns), qidx++;
}
base[43] = qidx; // 43: count(col[j]) == 2
for (int j = 0; j < W; j++) {
add_xor({base[40] + j, base[42] + j}), qidx++;
}
base[44] = qidx; // 44: count(col[j]) >= 1 AND count(col[j+d]) >= 1 (d=[1,W/2))
for (int d = 1; d < W / 2; d++) {
for (int j = 0; j + d < W; j++) {
add_and({base[40] + j, base[40] + j + d}), qidx++;
}
}
base[45] = qidx; // X
lb = 0, rb = W - 1 - (W % 2 == 0);
while (lb < rb) {
Ns.clear();
for (int j = 0; j <= lb; j++) {
Ns.push_back(base[40] + j);
}
add_or(Ns), qidx++;
Ns.clear();
for (int j = rb; j < W; j++) {
Ns.push_back(base[41] + j);
}
add_and(Ns), qidx++;
add_and({qidx - 1, qidx - 2}), qidx++;
lb++, rb--;
}
base[46] = qidx; // 46: pre[0] + ... + pre[l] >= 1 AND pre[r] + ... + pre[W-1] == 0
for (int j = 0, idx = base[45] + 2; idx < base[46]; j++, idx += 3) {
add_and({idx}), qidx++;
}
base[47] = qidx; // X
lb = 0, rb = W - 1 - (W % 2 == 0);
while (lb < rb) {
Ns.clear();
for (int j = 0; j <= lb; j++) {
Ns.push_back(base[41] + j);
}
add_and(Ns), qidx++;
Ns.clear();
for (int j = rb; j < W; j++) {
Ns.push_back(base[40] + j);
}
add_or(Ns), qidx++;
add_and({qidx - 1, qidx - 2}), qidx++;
lb++, rb--;
}
base[48] = qidx; // 48: pre[0] + ... + pre[l] == 0 AND pre[r] + ... + pre[W-1] >= 1
for (int j = 0, idx = base[47] + 2; idx < base[48]; j++, idx += 3) {
add_and({idx}), qidx++;
}
base[60] = qidx; // 60: diff of row <= d (-1~W)
add_and({base[1]}), qidx++; // -1 (FALSE)
Ns.clear(); // 0
for (int j = 0; j < W; j++) {
Ns.push_back(base[43] + j);
}
add_or(Ns), qidx++;
for (int d = 1; d < W / 2; d++) { // 1 ~ W/2-1
Ns.clear();
for (int j = 0; j + d < W; j++) {
Ns.push_back(base[44] + j);
}
add_or(Ns), qidx++;
}
for (int d = W / 2, idx = 0; d <= W - 2; d++, idx++) { // W/2 ~ W-2
Ns.clear();
for (int j = d; j < W - d; j++) {
Ns.push_back(base[40] + j);
}
Ns.push_back(base[46] + (d - W / 2));
Ns.push_back(base[48] + (d - W / 2));
add_or(Ns), qidx++;
}
add_and({base[1] + 1}), qidx++; // W-1 (TRUE)
// ----------
base[80] = qidx; // get row positions
for (int i = 0; i < H; i++) {
add_xor({base[30] + i, base[30] + i + 1}), qidx++;
}
base[81] = qidx; // get col positions
for (int j = 0; j < W; j++) {
add_xor({base[60] + j, base[60] + j + 1}), qidx++;
}
base[82] = qidx;
for (int i = 0; i < H; i++) {
int j = K - i;
if (j >= 0 && j < W) {
add_and({base[80] + i, base[81] + j}), qidx++;
}
}
base[83] = qidx;
Ns.clear();
for (int x = base[82]; x < base[83]; x++) {
Ns.push_back({x});
}
add_or(Ns), qidx++;
}
