//  Copyright (2013) Cédric Coussinet (cedric.coussinet@nomoseed.net)
//
//  This program is free software: you can redistribute it and/or modify
//  it under the terms of the GNU General Public License as published
//  by the Free Software Foundation, either version 3 of the License, or
//  (at your option) any later version.
//
//  This program is distributed in the hope that it will be useful,
//  but WITHOUT ANY WARRANTY; without even the implied warranty of
//  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
//  GNU General Public License for more details.
//
//  You should have received a copy of the GNU General Public License
//  along with this program. If not, see <http://www.gnu.org/licenses/>

#include <QFile>
#include <QStringList>
#include <QRegExp>

#include <libxml/parser.h>
#include <libxml/xpath.h>
#include <libxml/xpathInternals.h>

#include "boolean_logic.h"

QFile error("formalism.log");

QString simplifier(QString txt){
    QString res = txt;
    if (txt.length()!=0)
    {
        QStringList eq = txt.split(":");
        res = "";
        QStringList list = eq[0].split("+");
        for (int i=list.length()-1;i>=0;i--)
        {
            QStringList state = list[i].split(".");
            state.removeDuplicates();
            foreach (const QString &str, state)
            {
               if (!state.filter(str+"^").empty())
                   state.clear();
            }
            if (!state.empty())
            {
                state.sort();
                res = "+" + state.join(".") + res;
            }
        }
        list = res.split('+', QString::SkipEmptyParts);
        list.sort();
        list.removeDuplicates();
        res = list.join("+")+ ":" + eq[1];
    }
    return res;
}

QString nettoyerOr(QString txt){
    QRegExp rx("(^|[\\+\\(])\\([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(?![\\^\\.\\*])", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C;
    int first, last;
    first = rx.indexIn(txt);
    while (first != -1)
    {
        last = rx.matchedLength();
        A = txt.mid(0,first);
        B = rx.cap(0);
        if (B[0]=='(')
            B.remove(0,1);
        else
            B.remove(1,1);
        B.remove(B.length()-1,1);
        C = txt.mid(first+last);
        txt = A + B + C;
        first = rx.indexIn(txt);
    }
    txt.remove("^^");
    return txt;
}

QString resoudreOrAnd(QString txt){
    QRegExp rx("\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(\\.[a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)+(?![\\^\\.])", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C, D;
    int first, last;
    first = rx.indexIn(txt);
    if (first != -1)
    {
        last = rx.matchedLength();
        A = txt.mid(0,first);
        B = rx.cap(0);
        QRegExp rxand("\\)(\\.[a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)+");
        int f = rxand.indexIn(B)+1;
        D = rxand.cap().remove(0,1);
        B.remove(f,rxand.matchedLength());
        B.replace(")",D+")");
        B.replace("+",D+"+");
        C = txt.mid(first+last);
        txt = A + B + C;
    }
    return txt;
}

QString resoudreAndOr(QString txt){
    QRegExp rx("([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?\\.)+\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(?![\\^\\.])", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C, D;
    int first, last;
    first = rx.indexIn(txt);
    if (first != -1)
    {
        last = rx.matchedLength();
        A = txt.mid(0,first);
        B = rx.cap(0);
        QRegExp rxand("([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?\\.)+");
        int f = rxand.indexIn(B);
        D = rxand.cap();
        B.remove(f,rxand.matchedLength());
        B.replace("+","+"+D);
        B.replace("(","("+D);
        C = txt.mid(first+last);
        txt = A + B + C;
    }
    return txt;
}

QString resoudreAndAnd(QString txt){
    QRegExp rx("\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)\\.\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(?![\\^])", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C, D, E;
    int first, last;
    first = rx.indexIn(txt);
    if (first != -1)
    {
        last = rx.matchedLength();
        A = txt.mid(0,first);
        B = rx.cap(0);
        QRegExp rxand("\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)\\.");
        int f = rxand.indexIn(B);
        D = rxand.cap();
        B.remove(f,rxand.matchedLength());
        B.replace("+","+"+D);
        B = "(" + D + B.remove(0,1);
        C = txt.mid(first+last);
        txt = A + B + C;
    }
    return txt;
}

QString mettreParenthese(QString txt){
    QRegExp rx("([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)+", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B;
    int first, last;
    first = rx.indexIn(txt);
    while (first != -1)
    {
        last = rx.matchedLength();
        B = rx.cap(0);
        A = A + txt.mid(0,first) +"(" + B + ")";
        txt = txt.mid(first+last);
        first = rx.indexIn(txt);
    }
    return A + txt;
}

QString resoudreOrMorgan(QString txt){
    QRegExp rx("\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*([\\+][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)\\^", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C;
    int first, last;
    first = rx.indexIn(txt);
    if (first != -1)
    {
        last = rx.matchedLength();
        A = txt.mid(0,first);
        B = rx.cap(0);
        B = mettreParenthese(B);
        B.replace("+","^.");
        B.remove(B.length()-2,2);
        C = txt.mid(first+last);
        txt = A + B + "^)" + C;
    }
    return txt;
}

QString resourdreNotXor(QString txt){
    QRegExp rx("\\((((?!\\.)[a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)|\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(?![\\^]))\\*(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)|\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\.\\+][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(?![\\^]))\\)\\^", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C;
    QStringList list;
    int first, last;
    first = rx.indexIn(txt);
    if (first != -1)
    {
       last = rx.matchedLength();
       A = txt.mid(0,first);
       B = rx.cap(0).remove(0,1);
       B.remove(B.length()-2,2);
       list = B.split("*");
       C = txt.mid(first+last);
       txt = A + list[1] + "." + list[0] + "+" + list[1] + "^." + list[0] + "^" + C;
    }
    return txt;
}

QString resourdreXor(QString txt){
    QRegExp rx("(((?!\\.)[a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)|\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(?![\\^]))\\*(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)|\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\.\\+][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)*\\)(?![\\^]))", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C;
    QStringList list;
    int first, last;
    first = rx.indexIn(txt);
    if (first != -1)
    {
       last = rx.matchedLength();
       A = txt.mid(0,first);
       B = rx.cap(0);
       list = B.split("*");
       C = txt.mid(first+last);
       txt = A + list[1] + "." + list[0] + "^+" + list[1] + "^." + list[0] + C;
    }
    return txt;
}

QString resoudreAndMorgan(QString txt){
    QRegExp rx("\\(([a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)([\\.][a-zA-Z]+[a-zA-Z0-9_]*[\\^]?)+\\)\\^", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString A, B, C;
    int first, last;
    first = rx.indexIn(txt);
    if (first != -1)
    {
        last = rx.matchedLength();
        A = txt.mid(0,first);
        B = rx.cap(0);
        B.replace(".","^+");
        B.remove(B.length()-2,2);
        C = txt.mid(first+last);
        txt = A + B + "^)" + C;
    }
    return txt;
}

bool verifier(QString txt){
    QRegExp rx("([\\(\\[]*[a-zA-Z]+[a-zA-Z0-9_]*[\\)\\]]*(\\^)*[\\)\\]]?(([\\+\\*\\.][\\(\\[]*)[a-zA-Z]+[a-zA-Z0-9_]*[\\)\\]]*(\\^)?[\\)\\]]*)*)?[:][a-zA-Z]+[a-zA-Z0-9_]*(\\^)?(\\,[a-zA-Z]+[a-zA-Z0-9_]*(\\^)?)*", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    if(rx.exactMatch(txt)){
        if(rx.cap(0).count("(") !=  rx.cap(0).count(")")){
            if (rx.cap(0).count("(") >  rx.cap(0).count(")"))
                error.write("Formalism logic_boolean : too many opening parenthesis in > " + txt.toUtf8() + "\n");
            else
                error.write("Formalism logic_boolean : too many closing parenthesis in > " + txt.toUtf8() + "\n");
            return false;
        }
        if (rx.cap(0).count("[") !=  rx.cap(0).count("]")){
            if (rx.cap(0).count("[") >  rx.cap(0).count("]"))
                error.write("Formalism logic_boolean : too many opening square bracket in > " + txt.toUtf8() + "\n");
            else
                error.write("Formalism logic_boolean : too many closing square bracket in > " + txt.toUtf8() + "\n");
            return false;
        }
        QRegExp _xor("([\\*\\.][a-zA-Z]+[a-zA-Z0-9_]*(\\^)?)+\\*|\\*([a-zA-Z]+[a-zA-Z0-9_]*(\\^)?[\\*\\.])+", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
        if (_xor.indexIn(txt) != -1){
            error.write("Formalism logic_boolean : disjunctive or is ambiguous in > " + txt.toUtf8() + "\n");
            return false;
        }
    }
    else{
        error.write("Formalism logic_boolean : syntax error in > " + txt.toUtf8() + "\n");
    }
    return true;
}

QString fnd(QString txt){
    QRegExp canon("([a-zA-Z]+[a-zA-Z0-9_]*(\\^)?([\\+\\.][a-zA-Z]+[a-zA-Z0-9_]*(\\^)?)*)?[:][a-zA-Z]+[a-zA-Z0-9_]*(\\^)?(\\,[a-zA-Z]+[a-zA-Z0-9_]*(\\^)?)*", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);

    int i = 0;

    while (!canon.exactMatch(txt) && i<1000)
    {
        txt = nettoyerOr (txt);
        txt = resourdreNotXor (txt);
        txt = resourdreXor (txt);
        txt = resoudreAndAnd (txt);
        txt = resoudreAndOr (txt);
        txt = resoudreOrAnd (txt);
        txt = resoudreOrMorgan (txt);
        txt = resoudreAndMorgan (txt);
        i++;
    }
    txt = simplifier (txt);
    if (canon.exactMatch(txt))
         return txt;
    else
        return "#";
}

QString gererIntermediaire (QStringList& list, QString txt){
    QRegExp rx("[\\[][\\(]*[a-zA-Z]+[a-zA-Z0-9_]*[\\)]*(\\^)*[\\)]?(([\\+\\*\\.][\\(]*)[a-zA-Z]+[a-zA-Z0-9_]*[\\)]*(\\^)?[\\)]*)*[\\]]", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    int first, last;
    QString A, B, C, id;
    QStringList l;
    first = rx.indexIn(txt);
    while (first != -1)
    {
        last = rx.matchedLength();
        A = txt.mid(0,first);

        B = rx.cap(0).remove(QRegExp("[\\[\\]]"));
        id = "i" + QString::number(list.length());
        B = B + ":" + id;
        B = fnd(B);
        l = list.filter(B.split(":")[0] + ":");
        if (l.empty())
            list.append(B);
        else
            id =l[0].split(":")[1];
        C = txt.mid(first+last);
        txt = A + id + C;
        first = rx.indexIn(txt);
    }
    return txt;
}

QStringList detailler (QString txt){
    QStringList answer;
    QStringList list = txt.split(QRegExp("[:,]"));
    QStringList list2 = list[0].split(QRegExp("[+]"));
    for (int i=1; i < list.length(); i++)
    {
        if (!list2.empty())
            for (int j=0; j < list2.length(); j++)
            {
                answer.append(list2[j] + ":" + list[i]);
            }
        else
            answer.append(list[0] + ":" + list[i]);
    }
    return answer;
}

xmlNodePtr modelsXML(const QString conjonctions, const QString name){
   xmlNsPtr nsprogram = xmlNewNs(NULL,(xmlChar*)"http://www.nomoseed.org/program", NULL);
   xmlNsPtr nsmodel = xmlNewNs(NULL,(xmlChar*)"http://www.nomoseed.org/model", NULL);
   xmlNodePtr models = xmlNewNode(nsprogram, (const xmlChar*) "models");
   xmlNodePtr instance = xmlNewNode(nsprogram, (const xmlChar*) "new");
   xmlSetProp (instance, (const xmlChar*) "instance", (const xmlChar*) name.toUtf8().constData());
   xmlAddChild (models, instance);
   xmlNodePtr model = xmlNewNode(nsmodel, (const xmlChar*) "model");
   xmlSetProp (model, (const xmlChar*) "name", (const xmlChar*) name.toUtf8().constData());
   xmlSetProp (model, (const xmlChar*) "xmlns", (const xmlChar*) "http://www.nomoseed.org/model");
   xmlAddChild (instance, model);
   xmlNodePtr definition = xmlNewNode(nsmodel, (const xmlChar*) "definition");
   xmlAddChild (model, definition);
   QString eq = conjonctions;
   eq.remove("^");
   QStringList types = eq.split(QRegExp ("[\\.:\\|]"), QString::SkipEmptyParts);
   types.removeDuplicates();
   foreach (const QString &str, types){
       xmlNodePtr type = xmlNewNode(nsmodel, (const xmlChar*) "conception_type");
       xmlSetProp (type, (const xmlChar*) "name", (const xmlChar*) str.toUtf8().constData());
       xmlAddChild (definition, type);
       xmlNodePtr items = xmlNewNode(nsmodel, (const xmlChar*) "items");
       xmlAddChild (type, items);
       xmlNodePtr itemT = xmlNewNode(nsmodel, (const xmlChar*) "item");
       xmlSetProp (itemT, (const xmlChar*) "name", (const xmlChar*) "true");
       xmlAddChild (items, itemT);
       xmlNodePtr itemF = xmlNewNode(nsmodel, (const xmlChar*) "item");
       xmlSetProp (itemF, (const xmlChar*) "name", (const xmlChar*) "false");
       xmlAddChild (items, itemF);
   }
   return models;
}

xmlNodePtr schemeInitialXML(const QString conjonctions, const QString model){
    xmlNsPtr ns = xmlNewNs(NULL,(xmlChar*)"http://www.nomoseed.org/program", NULL);
    xmlNodePtr scheme = xmlNewNode(ns, (const xmlChar*) "scheme");
    xmlSetProp (scheme, (const xmlChar*) "name", (const xmlChar*) "initialization");
    QStringList rules = conjonctions.split("|");
    rules = rules.filter(QRegExp ("^:"));
    QString type;
    QString value;
    foreach (const QString &str, rules){
        if (str[str.length()-1] == '^') {
            type = str.mid(1,str.length()-2);
            value = "false";
        }
        else {
            type = str.mid(1);
            value = "true";
        }
        xmlNodePtr rule = xmlNewNode(ns, (const xmlChar*) "rule");
        xmlSetProp (rule, (const xmlChar*) "name", (const xmlChar*) ("initialize_" + type).toUtf8().constData());
        xmlSetProp (rule, (const xmlChar*) "relevance", (const xmlChar*) "0");
        xmlAddChild (scheme, rule);
        xmlNodePtr conclusion = xmlNewNode(ns, (const xmlChar*) "conclusion");
        xmlSetProp (conclusion, (const xmlChar*) "category", (const xmlChar*) "conception");
        xmlSetProp (conclusion, (const xmlChar*) "model", (const xmlChar*) model.toUtf8().constData());
        xmlSetProp (conclusion, (const xmlChar*) "type", (const xmlChar*) type.toUtf8().constData());
        xmlAddChild (rule, conclusion);
        xmlNodePtr information = xmlNewNode(ns, (const xmlChar*) "information");
        xmlSetProp (information, (const xmlChar*) "value", (const xmlChar*) value.toUtf8().constData());
        xmlSetProp (information, (const xmlChar*) "delay", (const xmlChar*) "MAX");
        xmlAddChild (conclusion, information);
    }
    return scheme;
}

xmlNodePtr GetFrontXML (const QString type, const QString model, const QString value, const xmlNsPtr ns){
    xmlNodePtr rule = xmlNewNode(ns, (const xmlChar*) "rule");
    xmlSetProp (rule, (const xmlChar*) "name", (const xmlChar*) ("consolidate_" + type + "_to_" + value).toUtf8().constData());
    xmlNodePtr premise = xmlNewNode(ns, (const xmlChar*) "premise");
    xmlSetProp (premise, (const xmlChar*) "category", (const xmlChar*) "conception");
    xmlSetProp (premise, (const xmlChar*) "model", (const xmlChar*) model.toUtf8().constData());
    xmlSetProp (premise, (const xmlChar*) "type", (const xmlChar*) type.toUtf8().constData());
    xmlAddChild (rule, premise);
    xmlNodePtr information = xmlNewNode(ns, (const xmlChar*) "information");
    xmlSetProp (information, (const xmlChar*) "value", (const xmlChar*) value.toUtf8().constData());
    xmlSetProp (information, (const xmlChar*) "tolerance", (const xmlChar*) "0");
    xmlAddChild (premise, information);
    xmlNodePtr credibility = xmlNewNode(ns, (const xmlChar*) "credibility");
    xmlSetProp (credibility, (const xmlChar*) "value", (const xmlChar*) "1");
    xmlSetProp (credibility, (const xmlChar*) "tolerance", (const xmlChar*) "INF");
    xmlAddChild (premise, credibility);
    xmlNodePtr timespan = xmlNewNode(ns, (const xmlChar*) "timespan");
    xmlSetProp (timespan, (const xmlChar*) "value", (const xmlChar*) "0");
    xmlSetProp (timespan, (const xmlChar*) "tolerance", (const xmlChar*) "0");
    xmlAddChild (premise, timespan);
    xmlNodePtr conclusion = xmlNewNode(ns, (const xmlChar*) "conclusion");
    xmlSetProp (conclusion, (const xmlChar*) "category", (const xmlChar*) "conception");
    xmlSetProp (conclusion, (const xmlChar*) "model", (const xmlChar*) model.toUtf8().constData());
    xmlSetProp (conclusion, (const xmlChar*) "type", (const xmlChar*) type.toUtf8().constData());
    xmlAddChild (rule, conclusion);
    information = xmlNewNode(ns, (const xmlChar*) "information");
    xmlSetProp (information, (const xmlChar*) "value", (const xmlChar*) value.toUtf8().constData());
    xmlSetProp (information, (const xmlChar*) "delay", (const xmlChar*) "MAX");
    xmlAddChild (conclusion, information);
    return rule;
}

xmlNodePtr schemeManagementXML(const QString txt,const QString model){
    QString eq = txt;
    eq.remove("^");
    QStringList rules = eq.split(QRegExp ("[\\.:\\|]"), QString::SkipEmptyParts);
    rules.removeDuplicates();
    xmlNsPtr ns = xmlNewNs(NULL,(xmlChar*)"http://www.nomoseed.org/program", NULL);
    xmlNodePtr scheme = xmlNewNode(ns, (const xmlChar*) "scheme");
    xmlSetProp (scheme, (const xmlChar*) "name", (const xmlChar*) "management");
    foreach (const QString &type, rules){
        xmlAddChild (scheme, GetFrontXML (type ,model, "true", ns));
        xmlAddChild (scheme, GetFrontXML (type ,model, "false", ns));
    }
    return scheme;
}

xmlNodePtr GetEqXML (QString eq, const QString model, int number, const xmlNsPtr ns){
    QString type = eq.split(":")[1];
    QString value = "false";
    if (type[type.length()-1]!='^')
        value = "true";
    else
        type.remove(type.length()-1,1);
    xmlNodePtr rule = xmlNewNode(ns, (const xmlChar*) "rule");
    xmlSetProp (rule, (const xmlChar*) "name", (const xmlChar*) ("conjunction_" + QString::number(number)).toUtf8().constData());
    xmlNodePtr conclusion = xmlNewNode(ns, (const xmlChar*) "conclusion");
    xmlSetProp (conclusion, (const xmlChar*) "category", (const xmlChar*) "conception");
    xmlSetProp (conclusion, (const xmlChar*) "model", (const xmlChar*) model.toUtf8().constData());
    xmlSetProp (conclusion, (const xmlChar*) "type", (const xmlChar*) type.toUtf8().constData());
    xmlNodePtr information = xmlNewNode(ns, (const xmlChar*) "information");
    xmlSetProp (information, (const xmlChar*) "value", (const xmlChar*) value.toUtf8().constData());
    xmlSetProp (information, (const xmlChar*) "delay", (const xmlChar*) "MAX");
    xmlAddChild (conclusion, information);
    xmlNodePtr premise = xmlNewNode(ns, (const xmlChar*) "premise");
    xmlSetProp (premise, (const xmlChar*) "category", (const xmlChar*) "conception");
    xmlSetProp (premise, (const xmlChar*) "model", (const xmlChar*) model.toUtf8().constData());
    xmlSetProp (premise, (const xmlChar*) "type", (const xmlChar*) type.toUtf8().constData());
    xmlSetProp (premise, (const xmlChar*) "inhibitor", (const xmlChar*) "true");
    information = xmlNewNode(ns, (const xmlChar*) "information");
    xmlSetProp (information, (const xmlChar*) "value", (const xmlChar*) value.toUtf8().constData());
    xmlSetProp (information, (const xmlChar*) "tolerance", (const xmlChar*) "0");
    xmlAddChild (premise, information);
    xmlNodePtr credibility = xmlNewNode(ns, (const xmlChar*) "credibility");
    xmlSetProp (credibility, (const xmlChar*) "value", (const xmlChar*) "1");
    xmlSetProp (credibility, (const xmlChar*) "tolerance", (const xmlChar*) "INF");
    xmlAddChild (premise, credibility);
    xmlNodePtr timespan = xmlNewNode(ns, (const xmlChar*) "timespan");
    xmlSetProp (timespan, (const xmlChar*) "value", (const xmlChar*) "-1");
    xmlSetProp (timespan, (const xmlChar*) "tolerance", (const xmlChar*) "INF");
    xmlAddChild (premise, timespan);
    xmlAddChild (rule, premise);
    foreach(const QString &prem, eq.split(":")[0].split(".")){
        type = prem;
        QString value = "false";
        if (type[type.length()-1]!='^')
            value = "true";
        else
            type.remove(type.length()-1,1);
        premise = xmlNewNode(ns, (const xmlChar*) "premise");
        xmlSetProp (premise, (const xmlChar*) "category", (const xmlChar*) "conception");
        xmlSetProp (premise, (const xmlChar*) "model", (const xmlChar*) model.toUtf8().constData());
        xmlSetProp (premise, (const xmlChar*) "type", (const xmlChar*) type.toUtf8().constData());
        xmlAddChild (rule, premise);
        information = xmlNewNode(ns, (const xmlChar*) "information");
        xmlSetProp (information, (const xmlChar*) "value", (const xmlChar*) value.toUtf8().constData());
        xmlSetProp (information, (const xmlChar*) "tolerance", (const xmlChar*) "0");
        xmlAddChild (premise, information);
        credibility = xmlNewNode(ns, (const xmlChar*) "credibility");
        xmlSetProp (credibility, (const xmlChar*) "value", (const xmlChar*) "1");
        xmlSetProp (credibility, (const xmlChar*) "tolerance", (const xmlChar*) "INF");
        xmlAddChild (premise, credibility);
        timespan = xmlNewNode(ns, (const xmlChar*) "timespan");
        xmlSetProp (timespan, (const xmlChar*) "value", (const xmlChar*) "-1");
        xmlSetProp (timespan, (const xmlChar*) "tolerance", (const xmlChar*) "INF");
        xmlAddChild (premise, timespan);
    }
    xmlAddChild (rule, conclusion);
    return rule;
}

xmlNodePtr schemeEqXML( const QString conjonctions, const QString model){
    QStringList list = conjonctions.split("|").filter(QRegExp ("^[^:]"));
    xmlNsPtr ns = xmlNewNs(NULL,(xmlChar*)"http://www.nomoseed.org/program", NULL);
    xmlNodePtr scheme = xmlNewNode(ns, (const xmlChar*) "scheme");
    xmlSetProp (scheme, (const xmlChar*) "name", (const xmlChar*) "conjunctions");
    int i = 0;
    foreach (const QString &eq, list){
        i++;
        xmlAddChild (scheme, GetEqXML(eq, model, i, ns));
    }
    return scheme;
}

QString extraireFormules(QString txt){
    txt.remove(QRegExp("//[^\\n]*[\\n]|$", Qt::CaseSensitive, QRegExp::W3CXmlSchema11));
    QRegExp rx("[^:]*[:]\\s*[a-zA-Z]+[a-zA-Z0-9_]*(\\^)?(\\,[\\s]*[a-zA-Z]+[a-zA-Z0-9_]*(\\^)?)*[\\s]*", Qt::CaseSensitive, QRegExp::W3CXmlSchema11);
    QString eq;
    QStringList list;
    QStringList intermediaire;
    int first, last;
    first = rx.indexIn(txt);
    while (first != -1){
        if (first != 0){
            list.append("#");
            first = -1;
        }
        else {
            eq = rx.cap(0).remove(QRegExp("[\\s$]"));
            if (verifier(eq))
            {
                eq=gererIntermediaire(intermediaire,eq);
                list = list + detailler(fnd(eq));
                last = rx.matchedLength();
                txt = txt.mid(first+last);
                first = rx.indexIn(txt);
            }
            else {
                list.append("#");
                first = -1;
            }
        }
    }
    for (int i=0;i<intermediaire.length();i++)
        list = list + detailler(intermediaire[i]);
    list.removeDuplicates();
    if (list.join("|").replace("^|","|").split("|").removeDuplicates() > 0)
        list.append("#");
    return list.join("|");
}

void formalismActualize(const char* file){
    error.open(QFile::WriteOnly);
    xmlDocPtr doc = xmlReadFile(file, "UTF-8", 0);
    xmlXPathInit();
    xmlXPathContextPtr ctxt = xmlXPathNewContext(doc);
    xmlXPathRegisterNs(ctxt, (const xmlChar*)"sdk",(const xmlChar*)"http://www.nomoseed.org/sdk");
    xmlXPathObjectPtr xpathRes = xmlXPathEvalExpression((const xmlChar*)"/*/*/sdk:formalism/*/text()", ctxt);
    QString code = QString((char*) xmlXPathCastToString(xpathRes));
    xmlNodePtr txt = xpathRes->nodesetval->nodeTab[0];
    xmlXPathFreeObject(xpathRes);
    xmlXPathRegisterNs(ctxt, (const xmlChar*)"program",(const xmlChar*)"http://www.nomoseed.org/program");
    xpathRes = xmlXPathEvalExpression((const xmlChar*)"/program:program/@name", ctxt);
    const QString name = QString((char*) xmlXPathCastToString(xpathRes));
    xmlXPathFreeObject(xpathRes);
    QString conjonctions = extraireFormules(code);
    if (!conjonctions.isEmpty() && conjonctions.count("#") == 0){
        xmlNsPtr ns = xmlSearchNsByHref(doc, xmlDocGetRootElement(doc), (const xmlChar*)"http://www.nomoseed.org/program");
        xmlNodePtr body = xmlNewNode(ns, (const xmlChar*) "body");
        xmlAddChild (body, modelsXML(conjonctions, name));
        xmlNodePtr scheme = xmlNewNode(ns, (const xmlChar*) "scheme");
        xmlAddChild (scheme, schemeInitialXML(conjonctions, name));
        xmlAddChild (scheme, schemeManagementXML(conjonctions, name));
        xmlAddChild (scheme, schemeEqXML(conjonctions, name));
        xmlAddChild (body, scheme);
        xpathRes = xmlXPathEvalExpression((const xmlChar*)"/*/program:body", ctxt);
        if (xmlXPathCastToBoolean(xpathRes)){
            xmlFreeNode (xmlReplaceNode(xpathRes->nodesetval->nodeTab[0],body));
        }
        else{
            xmlXPathFreeObject(xpathRes);
            xpathRes = xmlXPathEvalExpression((const xmlChar*)"/*/program:sdk", ctxt);
            xmlAddPrevSibling (xpathRes->nodesetval->nodeTab[0], body);
        }
        xmlXPathFreeObject(xpathRes);
        const int pos = code.lastIndexOf("// Atomic conjunctions");
        if  (pos != -1)
            code = code.left(pos);
        else
            code.append("\n\n");
        code.append("// Atomic conjunctions\n// ");
        code.append(conjonctions.replace("|","\n// "));
        code.append("\n");
        xmlReplaceNode(txt,xmlNewText((const xmlChar*) code.toUtf8().constData()));
    }
    xmlSaveFileEnc(file, doc, "UTF-8");
    xmlFreeNode(txt);
    xmlXPathFreeObject(xpathRes);
    xmlXPathFreeContext(ctxt);
    xmlFreeDoc(doc);
    error.close();
}
