AoC 2018 - 16

#include <bits/stdc++.h>
using namespace std;

struct st{
    long long r[4];
};

st addr(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] + q.r[b];
    return q;
}
st addi(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] + b;
    return q;
}
st mulr(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] * q.r[b];
    return q;
}
st muli(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] * b;
    return q;
}
st banr(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] & q.r[b];
    return q;
}
st bani(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] & b;
    return q;
}
st borr(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] | q.r[b];
    return q;
}
st bori(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] | b;
    return q;
}
st setr(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a];
    return q;
}
st seti(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = a ;
    return q;
}
st gtir(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = a > q.r[b]?1:0;
    return q;
}
st gtri(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] > b?1:0;
    return q;
}
st gtrr(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] > q.r[b]?1:0;
    return q;
}
st eqir(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = a == q.r[b]?1:0;
    return q;
}
st eqri(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] == b?1:0;
    return q;
}
st eqrr(const long long* in, long long a, long long b, long long c) {
    st q = {.r={in[0], in[1], in[2], in[3]}};
    q.r[c] = q.r[a] == q.r[b]?1:0;
    return q;
}

st (*op[])(const long long*, long long, long long, long long)={addr, addi, mulr, muli, banr, bani, borr, bori, setr, seti, gtir, gtri, gtrr, eqir, eqri, eqrr};
string opn[]={"addr", "addi", "mulr", "muli", "banr", "bani", "borr", "bori", "setr", "seti", "gtir", "gtri", "gtrr", "eqir", "eqri", "eqrr"};

st (*rop[])(const long long*, long long, long long, long long)={eqri, banr, bori, mulr, seti, bani, muli, gtrr, setr, addi, gtir, borr, addr, eqrr, gtri, eqir};
int main() {
    //int r[4]= {0,0,1,0};
    //st b = addr(r, 3, 2, 1);
    //cout << r[1] << ' ' << b.r[1] << '\n';
    int top=0;
    for(int i=0; i<16; i++) cout << "(declare-const " << opn[i] << " Int)\n";
    while(true) {
        string prs, pos, ops;
        getline(cin, prs);
        if (prs.length() == 0) break;
        getline(cin, ops);
        getline(cin, pos);
        string sace;
        getline(cin, sace);
//      cout << prs << ops <<pos << '|' << sace << "------------------\n";
        long long pr[4] = {prs[9]-'0', prs[12]-'0', prs[15]-'0', prs[18]-'0'};
        long long po[4] = {pos[9]-'0', pos[12]-'0', pos[15]-'0', pos[18]-'0'};
        int o; long long a,b,c;
        if (ops[1] == ' ') {
            o = ops[0]-'0'; a=ops[2]-'0'; b=ops[4]-'0'; c=ops[6]-'0';
        } else {
            o = 10*(ops[0]-'0')+(ops[1]-'0'); a=ops[3]-'0'; b=ops[5]-'0'; c=ops[7]-'0';
        }
        int z=0;
        cout << "(assert (or";
        for(int j=0; j<16; j++) {
            st q = op[j](pr, a,b,c);
            bool e=true;
            for(int i=0; i<4; i++) {
                if (q.r[i] != po[i]) {
                    e=false; break;
                }
            }
            if(e) {
                z++;
                cout << " (= " << o << " " << opn[j] << ")";
            }
        }
        cout << "))\n";
        if (z>=3)       top++;
    }
    cout << "(check-sat) (get-model)\n";
    cout << ';' << top <<'\n';
    long long reg[4] = {0,0,0,0};
    int t=0;
    while (true) {
        t++;
        int o,a,b,c;
        cin >> o;
        if (o<0) break;
        cin >> a >> b >> c;
        st q = rop[o](reg, a,b,c);
        for(int i=0; i<4;i++) reg[i]=q.r[i];
        //cout << t << ": (" <<o << ' ' << a << ' ' << b << ' ' << c << ") " << reg[0]<< ' ' << reg[1] << ' ' << reg[2] << ' ' << reg[3] << '\n';
    }
    cout << ';' << reg[0] << '\n';// ' ' << t << '\n';
    return 0;
}