#include "clasplayer.h"

#include <clasp/program_builder.h>        // for defining logic programs
#include <clasp/unfounded_check.h>      // unfounded set checkers
#include <clasp/model_enumerators.h>  // for enumerating answer sets
#include <clasp/clasp_facade.h>

#include <clingocontrol.hh>

#include <iostream>
#include <clingo_lib.hh>

using namespace std;

namespace xreate {
    bool
    ClaspLayer::onModel(Gringo::Model const &model) {
        std::list<std::string> warnings;
        cout << "Model: " << endl;
        for (Gringo::Value atom : model.atoms(Gringo::Model::ATOMS)) {
            atom.print(cout);
            cout << endl;

            auto hookI = __hooks.find(*(atom.name()));

            if (hookI != __hooks.end()) {
                warnings.push_back(hookI->second);
            }
        }

        for (auto warning: warnings) {
            cout << "Warning: " << warning << endl;
        }
    }

    QStringList multiplyLists(std::list<QStringList> &&lists) {
        QStringList result = lists.front();
        lists.pop_front();

        for (QStringList &list: lists) {
            QStringList::const_iterator end = result.end();
            for (QStringList::iterator expr1I = result.begin(); expr1I < end; ++expr1I) {
                if (list.size() == 0) continue;

                QStringList::const_iterator expr2I = list.begin();
                for (int expr2No = 0, size = list.size() - 1; expr2No < size; ++expr2No, ++expr1I)
                    result.append(QString("%1, %2").arg(*expr1I).arg(*expr2I));

                *expr1I = QString("%1, %2").arg(*expr1I).arg(*expr2I);
            }
        }

        return result;
    }

    void
    ClaspLayer::addCFGData(CFGraph &&graph) {
        ostream &cout = __partGeneral;

        cout << endl << "%\t\tStatic analysis: CFG" << endl;

        for (const std::pair<FID, FID> &relation: graph.__relations) {
            const string &tagFrom = graph.__nodes.at(relation.first);
            const string &tagTo = graph.__nodes.at(relation.second);

            cout << (QString("call(%1, %2) .").arg(tagFrom.c_str()).arg(tagTo.c_str())).toStdString() << endl;
        }
    }

    void
    ClaspLayer::addFunctionTags(const std::string &function, const std::vector<Tag> &tags) {
        ostream &cout = __partTags;

        cout << (QString("function(%1) .").arg(function.c_str())).toStdString() << std::endl;

        int tagsCount = 0;
        for (const Tag &tag: tags) {
            QStringList tagRaw = compile(tag.first);
            assert(tagRaw.size() == 1);

            cout << QString("tag(%1, %2).").arg(function.c_str()).arg(tagRaw.at(0)).toStdString() << endl;
            ++tagsCount;
        }
        if (tagsCount == 0) {
            cout << "%no tags at all" << endl;
        }
    }

    void
    ClaspLayer::addRuleWarning(const RuleWarning &rule) {
        //__partGeneral << rule << endl;

        QStringList domains;
        std::transform(rule.__args.begin(), rule.__args.end(), std::inserter(domains, domains.begin()),
                [](const std::pair<std::string, DomainAnnotation> &argument) {
                    char *domain;
                    switch (argument.second) {
                        case DomainAnnotation::FUNCTION:
                            domain = "function";
                            break;
                        case DomainAnnotation::VARIABLE:
                            domain = "variable";
                            break;
                    }

                    return QString("%1(%2)").arg(domain).arg(argument.first.c_str());
                });

        QStringList vars;
        std::transform(rule.__args.begin(), rule.__args.end(), std::inserter(vars, vars.begin()),
                [](const std::pair<std::string, DomainAnnotation> &argument) {
                    return argument.first.c_str();
                });

        std::list<QStringList> guardsRaw;
        std::transform(rule.__guards.begin(), rule.__guards.end(), std::inserter(guardsRaw, guardsRaw.begin()),
                [this](const Expression &guard) {
                    return compile(guard);
                });

        QStringList guards = multiplyLists(std::move(guardsRaw));
        QStringList &&branches = compileNeg(rule.__condition);

        for (const QString &guardsJoined: guards)
            for (const QString &branch: branches) {
                const std::string &&hook = registerHook(rule.__message);

                QString result = QString("%1(%2):-%3, %4, %5.")
                        .arg(hook.c_str())
                        .arg(vars.join(", "))
                        .arg(branch)
                        .arg(guardsJoined)
                        .arg(domains.join(", "));

                __partGeneral << result.toStdString() << endl;
            }
    }

    QStringList
    ClaspLayer::compile(const Expression &e) const {
        QStringList result;

        switch (e.__op) {
            case Operator::CALL: {
                assert(e.__state == Expression::COMPOUND);

                std::list<QStringList> operands;
                std::transform(e.operands.begin(), e.operands.end(), std::inserter(operands, operands.begin()),
                        [this](const Expression &e) {
                            return compile(e);
                        });

                QStringList &&operands_ = multiplyLists(std::move(operands));
                result.append(QString("%1(%2)").arg(e.__valueS.c_str()).arg(operands_.join(", ")));
                break;
            }
            case Operator::NEG: {
                assert(e.operands.size() == 1);

                const Expression &op = e.operands.at(0);
                QStringList &&rawOp = compile(op);

                assert(rawOp.size() == 1);
                result.append(QString("not %1").arg(rawOp.at(0)));
                break;
            };

            case Operator::NONE: {
                switch (e.__state) {
                    case Expression::IDENT:
                        result.append(QString(e.__valueS.c_str()));
                        break;

                    case Expression::NUMBER:
                        result.append(QString::number(e.__valueD));
                        break;

                    default:
                        assert(true);
                }
                break;
            }
        }

        return result;
    }

    QStringList
    ClaspLayer::compileNeg(const Expression &e) const {
        QStringList result;
        switch (e.__op) {
            case Operator::IMPL: {
                assert(e.__state == Expression::COMPOUND);
                assert(e.operands.size() == 2);
                QStringList operands1 = compile(e.operands.at(0));
                QStringList operands2 = compile(e.operands.at(1));

                for (const auto &op1: operands1)
                    for (const auto &op2: operands2) {
                        result.append(QString("%1, not %2").arg(op1).arg(op2));
                    }
                break;
            }
            case Operator::NEG: {
                assert(e.operands.size() == 1);

                const Expression &op = e.operands.at(0);
                QStringList &&rawOp = compile(op);

                assert(rawOp.size() == 1);
                result.append(rawOp.at(0));
                break;
            };

            default:
                assert(true);
        }

        return result;
    }

    std::string
    ClaspLayer::registerHook(const std::string &message) {
        static int i = 0;
        std::string hookId = "hook" + std::to_string(++i);
        __hooks.insert(make_pair(hookId, message));

        return hookId;
    }

    void
    ClaspLayer::run() {
        ostringstream program;
        program << __partTags.str() << __partGeneral.str();
        cout << program.str() << endl;

        const char *argv[] = {nullptr, nullptr};
        ClingoLib ctl(2, argv);

        //prg.add("p", ["t"], "q(t).")
        Gringo::FWStringVec vars{};
        ctl.add("base", vars, program.str());

        //prg.ground([("p", [2])])
        Gringo::Control::GroundVec vals{std::make_pair("base", Gringo::FWValVec {})};
        ctl.ground(vals, Gringo::Any());

        //solve
        Gringo::Control::Assumptions as;
        Gringo::SolveResult result = ctl.solve(Gringo::Control::ModelHandler([&](Gringo::Model const &model) {
            return this->onModel(model);
        }), std::move(as));

        if (result == Gringo::SolveResult::SAT) {
            cout << "SUCCESSFULLY" << endl;
        } else {
            cout << "UNSUCCESSFULLY" << endl;
        }
    }

    ClaspLayer::ClaspLayer() {
    }

/*
void AspOutPrinter::reportSolution(const Clasp::Solver&, const Clasp::Enumerator&, bool complete) {
    if (complete) std::cout << "No more models!" << std::endl;
    else          std::cout << "More models possible!" << std::endl;
}


void AspOutPrinter::reportModel(const Clasp::Solver& s, const Clasp::Enumerator&) {
    std::cout << "Model " << s.stats.solve.models << ": \n";
// get the symbol table from the solver
    const Clasp::AtomIndex& symTab = *s.strategies().symTab;
    for (Clasp::AtomIndex::const_iterator it = symTab.begin(); it != symTab.end(); ++it)
    {
// print each named atom that is true w.r.t the current assignment
    }
    std::cout << std::endl;
}

*/
/*****************************************
 *                      CFGraph
 *****************************************
 */

void
CFGraph::addNode(FID function, std::string&& tag)
{
    __nodes.emplace(function, tag);
}

bool
CFGraph::existsNode(FID function) const
{
    return __nodes.count(function);
}

void
CFGraph::addLink(FID nodeFrom, FID nodeTo)
{
    __relations.insert(std::make_pair(nodeFrom, nodeTo));
}
}