#pragma once

#include <vector>
#include "Allocate.h"
#include "CNF.h"

class Clause {
public:
    enum class TYPE {
        UNIT = 0,
        AND = 1,
        OR = 2,
    };

    std::vector<int> vec;
    TYPE type;
    bool positive;

    Clause(): type() {
        positive = true;
    }

    void mergeIntoUNIT() {
        if(type == TYPE::UNIT) return;

        int newId = IDManager::allocate();


        std::string output = "MAP: ";
        for(int i=0; i<vec.size()-1; i++) {
            output +=  std::to_string(vec[i]) + (type == TYPE::AND ? " & " : " | ");
        }
        output += std::to_string(vec[vec.size()-1]);
        output += " -> " + std::to_string(newId);

        CNF::comment(output);

        if(type == TYPE::AND) {
            CNF::add(newId);
            for(auto v : vec) {
                CNF::add(-v);
            }
            CNF::add(0);

            for(auto v : vec) {
                CNF::add(v);
                CNF::add(-newId);
                CNF::add(0);
            }
        } else {
            CNF::add(-newId);
            for(auto v : vec) {
                CNF::add(v);
            }
            CNF::add(0);

            for(auto v : vec) {
                CNF::add(-v);
                CNF::add(newId);
                CNF::add(0);
            }
        }

        vec.clear();
        vec.push_back(newId);
        type = TYPE::UNIT;
    }


    friend Clause operator ~ (Clause hs) {
        for(auto it=hs.vec.begin(); it!=hs.vec.end(); it++ ) {
            *it = -(*it);
        }
        
        if(hs.type == TYPE::AND) hs.type = TYPE::OR;
        else if(hs.type == TYPE::OR) hs.type = TYPE::AND;

        //if(hs.vec.size() == 1 && hs.type != TYPE::UNIT) exit(233);
        return hs;
    }

    friend Clause operator & (Clause lhs, Clause rhs) {

        Clause res;
        res.type = TYPE::AND;

        if(lhs.type == TYPE::OR) lhs.mergeIntoUNIT();
        if(rhs.type == TYPE::OR) rhs.mergeIntoUNIT();

        for(auto v : lhs.vec) res.vec.push_back(v);
        for(auto v : rhs.vec) res.vec.push_back(v);

        return res;
    }

    friend Clause operator | (Clause lhs, Clause rhs) {

        Clause res;
        res.type = TYPE::OR;

        if(lhs.type == TYPE::AND) lhs.mergeIntoUNIT();
        if(rhs.type == TYPE::AND) rhs.mergeIntoUNIT();

        for(auto v : lhs.vec) res.vec.push_back(v);
        for(auto v : rhs.vec) res.vec.push_back(v);

        return res;
    }
};