#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>
#include <QString>
#include <QStringList>
using namespace std;

bool
ClaspLayer::onModel(Gringo::Model const & model)
{
    cout << "Model: " << endl;
    for (Gringo::Value atom : model.atoms(Gringo::Model::ATOMS))
    {
        atom.print(cout);
        cout << 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;

            StringList::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(Tag tag: tags)
    {
        cout << QString("tag(%1, %2).").arg(function.c_str()).arg(tag.first.c_str()).toStdString() << endl;
        ++tagsCount;
    }
    if (tagsCount == 0)
    {
     cout << "%no tags at all" << endl;
    }
}

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

    std::QStringList domains;
    std::transform(rule->__args.begin(), rule->__args.end(), std::inserter(domains, domains.begin()),
        [](const auto& 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());
    });

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

    std::QStringList guards;
    std::transform(rule->__guards.begin(), rule->__guards.end(), std::inserter(guards, guards.begin()),
        [](const MetaExpression& guard) {
            return compile(guard)._c_str();
    });

    QStringList&& branches = compileNeg(rule->__condition);

    for(const std::string& branch: branches)
    {
        std::string listener = registerListener(rule->__message);

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

        __partGeneral<< result << endl;
    }
}

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

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

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

            QStringList&& operands_ = multiplyLists(operands);
            result.append(QString("%1(%2)").arg(e.__valueS.c_str()).arg(operands_.join(", ")));
            break;

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

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

                    default:
                        assert(true);
                }
            break;
    }

    return result;
}

QStringList compileNeg(const Expression& e) const
{
    QStringList result;
    switch(__op)
    {
        case Operator::IMPL:
            assert(e.__state == 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;

        default:
            assert(true);
    }

    return result;
}

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.insert(make_pair(function, move(tag)));
}

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

void
CFGraph::addLink(FID nodeFrom, FID nodeTo)
{
    assert(__nodes.count(nodeFrom));
    assert(__nodes.count(nodeTo));

    __relations.insert(std::make_pair(nodeFrom, nodeTo));
}