package de.uni_hildesheim.sse.trans.out;

import java.io.IOException;
import java.io.Writer;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree;
import de.uni_hildesheim.sse.model.cst.OCLFeatureCall;
import de.uni_hildesheim.sse.model.cst.Variable;
import de.uni_hildesheim.sse.model.varModel.AbstractVariable;
import de.uni_hildesheim.sse.model.varModel.Constraint;
import de.uni_hildesheim.sse.model.varModel.IvmlKeyWords;
import de.uni_hildesheim.sse.model.varModel.Project;
import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords;
import de.uni_hildesheim.sse.model.varModel.filter.ConstraintFinder;
import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder;
import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder.VisibilityType;
import de.uni_hildesheim.sse.model.varModel.filter.FilterType;
import de.uni_hildesheim.sse.trans.Main;
import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory;
import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger;

/**
 * Writer to write the given project into the DIMACS format.
 * Only works on projects that have their constraints in CNF.
 *
 * @author Adam Krafcyk
 */
public class DimacsWriter implements IModelWriter {
    public static final String HELP =
        // Tristates
        "\r\nc Explanation of Tristate variables:\r\n"
        + "c VAR VAR_Module Meaning\r\n"
        + "c  0       0     VAR is disabled (selection is 'n')\r\n"
        + "c  1       0     VAR is permanetely selected (selection is 'y')\r\n"
        + "c  0       1     Illegal state\r\n"
        + "c  1       1     VAR is selected as module (selection is 'm')\r\n"
        + "c As a consequence, if KConfig specifies that a tristate variable shall be selected \r\n"
        + "c (permanetely or as a module), only the VAR variable has to be checked.\r\n\r\n"
        // String, Integer, Hex
        + "c Explanation of String, Integer, and Hex variables:\r\n"
        + "c Variable   Meaning\r\n"
        + "c STR        Variable STR will (0 = not) exist / be selectable\r\n"
        + "c STR_Empty  Variable STR must (0 = not) be empty\r\n"
        + "c STR=Value  Variable STR must (0 = not) have the value \"Value\"\r\n\r\n"
        // End of help: Start of translation
        + "c Start of translation:\r\n";
    
    private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(DimacsWriter.class, Main.ID);
    
    private Project project;
    private Map<String, Integer> variables;
    private Writer writer;
    
    /**
     * Creates the writer for the given project.
     * @param project The project which shall be saved.
     * @param writer Writer which should be used for writing the output.
     */
    public DimacsWriter(Project project, Writer writer) {
        this.project = project;
        this.writer = writer;
        variables = new HashMap<String, Integer>();
    }
    
    /**
     * Writes the DIMACS format to the {@link Writer}.
     * @throws IOException If writing to the stream fails
     */
    public void write() throws IOException {
        // Get all variables
        DeclarationFinder declarationFinder = new DeclarationFinder(project, FilterType.ALL, null);
        List<AbstractVariable> variableDeclarations = declarationFinder.getVariableDeclarations(VisibilityType.ALL);
        Collections.sort(variableDeclarations, new Comparator<AbstractVariable>() {
            public int compare(AbstractVariable o1, AbstractVariable o2) {
                return o1.getName().compareTo(o2.getName());
            }
        });
        
        // Get all Constraints
        ConstraintFinder constraintFinder = new ConstraintFinder(project);
        List<Constraint> constraints = constraintFinder.getConstraints();
        
        // Write variables
        Integer i = 1;
        for (AbstractVariable variable : variableDeclarations) {
            variables.put(variable.getName(), i);
            writer.append("c ");
            writer.append(i.toString());
            writer.append(" ");
            writer.append(variable.getName());
            writer.append(IvmlKeyWords.LINEFEED);
            i++;
        }
        
        writer.append("p CNF " + variableDeclarations.size() + " " + constraints.size());
        writer.append(IvmlKeyWords.LINEFEED);
        
        for (Constraint constraint : constraints) {
            ConstraintSyntaxTree tree = constraint.getConsSyntax();
            writeTree(tree);
            writer.append("0");
            writer.append(IvmlKeyWords.LINEFEED);
        }
        
        writer.flush();
    }
    
    /**
     * Writes the {@link ConstraintSyntaxTree} in the DIMACS format.
     * Assumes that the {@link ConstraintSyntaxTree} is in CNF.
     * @param tree The {@link ConstraintSyntaxTree} to be written.
     * @throws IOException When writing to the {@link Writer} fails
     */
    private void writeTree(ConstraintSyntaxTree tree) throws IOException {
        if (tree instanceof Variable) {
            AbstractVariable variable = ((Variable) tree).getVariable();
            int number = variables.get(variable.getName());
            writer.append(number + " ");
        } else if (tree instanceof OCLFeatureCall) {
            OCLFeatureCall call = (OCLFeatureCall) tree;
            if (call.getOperation().equals(OclKeyWords.OR)) {
                writeTree(call.getParameter(0));
                writeTree(call.getOperand());
            } else if (call.getOperation().equals(OclKeyWords.NOT)) {
                writer.append("-");
                writeTree(call.getOperand());
            } else {
                LOGGER.debug("Unexpected Operation in model... skipping"); // TODO
            }
        } else {
            LOGGER.debug("Unexpected ConstraintSyntaxTree in model... skipping"); // TODO
        }
    }

    @Override
    public void write(String comment, String version) {
        try {
            if (comment != null) {
                writer.append("c ");
                writer.append(comment);
                writer.append(IvmlKeyWords.LINEFEED);
            }
            if (version != null) {
                writer.append("c Version ");
                writer.append(version);
                writer.append(IvmlKeyWords.LINEFEED);
            }
            // Readme ;-)
            writer.append(HELP);
            write();
        } catch (IOException e) {
            LOGGER.exception(e);
        }
    }
}
