package de.uni_hildesheim.sse.trans.convert;

import java.util.Collection;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import de.uni_hildesheim.sse.model.cst.CSTSemanticException;
import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree;
import de.uni_hildesheim.sse.model.cst.OCLFeatureCall;
import de.uni_hildesheim.sse.model.cst.Parenthesis;
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.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.DeclrationInConstraintFinder;
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;

/**
 * Optimizes a model with constraints in CNF in various ways.
 * 
 * @author Adam Krafczyk
 */
public class ModelOptimizer {
    private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(ModelOptimizer.class, Main.ID);

    private Project model;
    
    /**
     * Creates a {@link ModelOptimizer} for the given project.
     * @param model The project to be checked by this checker
     */
    public ModelOptimizer(Project model) {
        this.model = model;
    }
    
    /**
     * Removes all unused variables (i.e. variables that are not used in constraints) from the project.
     * 
     * @return The number of removed variables.
     */
    public int removeUnusedVariables() {
        ConstraintFinder cFinder = new ConstraintFinder(model);
        DeclarationFinder varFinder = new DeclarationFinder(model, FilterType.ALL, null);
        
        List<AbstractVariable> varList = varFinder.getVariableDeclarations(VisibilityType.ALL);
        Set<AbstractVariable> varSet = new HashSet<AbstractVariable>(varList);
        
        // 1) Go through all constraints and remove used variables from the set
        List<Constraint> constraints = cFinder.getConstraints();
        for (int i = 0, n = constraints.size(); i < n; i++) {
            Constraint constraint = constraints.get(i);
            DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(constraint.getConsSyntax());
            Set<AbstractVariable> declarations = finder.getDeclarations();
            varSet.removeAll(declarations);
        }
        
        // 2) All remaining variables in the set are unused
        for (AbstractVariable var : varSet) {
            model.removeElement(var);
        }
        
        return varSet.size();
    }
    
    /**
     * Check for variables that always have to be true or false and update all other constraints accordingly.
     * 
     * @return The number of removed constraints.
     */
    public int handleConstantVariables() {
        Set<AbstractVariable> alwaysTrueVariables = new HashSet<AbstractVariable>();
        Set<AbstractVariable> alwaysFalseVariables = new HashSet<AbstractVariable>();
        
        ConstraintFinder cFinder = new ConstraintFinder(model);
        List<Constraint> constraints = cFinder.getConstraints();
        
        // 1) Go through all constraints and find variables that always have to be true or false
        findConstantVariables(constraints, alwaysTrueVariables, alwaysFalseVariables);
        
        // 2) Remove all constraints that contain a not negated alwaysTrueVariable or contain a negated
        //    alwaysFalseVariable.
        int numRemoved = 0;
        for (int i = 0, n = constraints.size(); i < n; i++) {
            Constraint constraint = constraints.get(i);
            ConstraintSyntaxTree tree = constraint.getConsSyntax();
            
            DeclrationInConstraintFinder declarationFinder = new DeclrationInConstraintFinder(tree);
            Set<AbstractVariable> declarations = declarationFinder.getDeclarations();
            
            // Skip constraints with only 1 variable since this are the constraints that define the constant variables
            if (declarations.size() <= 1) {
                continue;
            }
            
            for (AbstractVariable var : declarations) {
                if (alwaysFalseVariables.contains(var)) {
                    if (isVariableNegated(tree, var)) {
                        tree = null;
                    } else {
                        try {
                            constraint.setConsSyntax(removeVariable(tree, var));
                        } catch (CSTSemanticException e) {
                            LOGGER.exception(e);
                        }
                    }
                    break;
                } else if (alwaysTrueVariables.contains(var)) {
                    if (!isVariableNegated(tree, var)) {
                        tree = null;
                    } else {
                        try {
                            constraint.setConsSyntax(removeVariable(tree, var));
                        } catch (CSTSemanticException e) {
                            LOGGER.exception(e);
                        }
                    }
                    break;
                }
            }
            
            if (tree == null) {
                model.removeElement(constraint);
                numRemoved++;

                /*
                 *  Release constraint to deallocate memory.
                 *  set(index, null) avoids Array.copy
                 */
                constraints.set(i, null);
            }
        }
        
        return numRemoved;
    }
    
    /**
     * Removes all duplicated constraints from the model. Alternative implementation with equivalence classes.
     * 
     * @return Number of removed constraints
     */
    public int removeDuplicatedConstraints() {
        // Takes ~10 seconds
        Collection<List<ConstraintContainer>> equivalenceClasses = createEquivalenceClasses();
        
        int removed = 0;
        int step = 1;
        for (List<ConstraintContainer> constraintList : equivalenceClasses) {
            LOGGER.info("Step " + step++ + " of " + equivalenceClasses.size());
            for (int i = 0, n = constraintList.size(); i < n - 1; i++) {
                ConstraintContainer firstContainer = constraintList.get(i);
                if (firstContainer == null) {
                    continue;
                }
                
                ConstraintSyntaxTree tree = firstContainer.getConstraint().getConsSyntax();
                Set<String> firstLiterals = firstContainer.getLiterals();
                DeclrationInConstraintFinder declFinder =
                    new DeclrationInConstraintFinder(firstContainer.getConstraint().getConsSyntax());
                Set<AbstractVariable> declarations = declFinder.getDeclarations();
                AbstractVariable[] declarationArray = declarations.toArray(new AbstractVariable[] {});
                
                for (int j = i + 1; j < n; j++) {
                    ConstraintContainer otherContainer = constraintList.get(j);
                    if (otherContainer == null) {
                        continue;
                    }
                    
                    ConstraintSyntaxTree otherTree = otherContainer.getConstraint().getConsSyntax();
                    Set<String> secondLiterals = otherContainer.getLiterals();
                    
                    // Could be removed theoretically (double checking)
                    if (secondLiterals.containsAll(firstLiterals)) {
                        boolean equal = true;

                        for (int k = 0; k < declarationArray.length; k++) {
                            if (isVariableNegated(tree, declarationArray[k])
                                    != isVariableNegated(otherTree, declarationArray[k])) {
                                equal = false;
                                break;
                            }
                        }
                        
                        if (equal) {
                            model.removeElement(otherContainer.getConstraint());
                            constraintList.set(j, null);
                            removed++;
                        }
                    }
                }
                
                /*
                 *  Release constraint to deallocate memory.
                 *  set(index, null) avoids Array.copy
                 */
                constraintList.set(i, null);
            }
        }
        
        return removed;
    }
    
    /**
     * Finds all constant variables in the given list of constraints.
     * @param constraints The list of constraints to search
     * @param alwaysTrueVariables A set where all variables that always have to be true will be stored
     * @param alwaysFalseVariables A set where all variables that always have to be false will be stored
     */
    private void findConstantVariables(List<Constraint> constraints, Set<AbstractVariable> alwaysTrueVariables,
            Set<AbstractVariable> alwaysFalseVariables) {
        
        for (int i = 0, n = constraints.size(); i < n; i++) {
            ConstraintSyntaxTree tree = constraints.get(i).getConsSyntax();
            // TODO: check if there is only 1 variable and use EvaluationVistor instead?
            
            if (tree instanceof Variable) {
                Variable var = (Variable) tree;
                alwaysTrueVariables.add(var.getVariable());
            } else if (tree instanceof OCLFeatureCall) {
                OCLFeatureCall call = (OCLFeatureCall) tree;
                if (call.getOperation().equals(OclKeyWords.NOT) && call.getOperand() instanceof Variable) {
                    Variable var = (Variable) call.getOperand();
                    alwaysFalseVariables.add(var.getVariable());
                }
            }
        }
    }
    
    /**
     * Split all constraints of the project into equivalence classes according to their length.
     * @return An {@link Collection} of lists with constraint that all have the same length.
     */
    private Collection<List<ConstraintContainer>> createEquivalenceClasses() {
        ConstraintFinder cFinder = new ConstraintFinder(model);
        List<Constraint> constraints = cFinder.getConstraints();
        
        ConstraintMap<Integer, ConstraintContainer> map = new ConstraintMap<Integer, ConstraintContainer>();
        
        for (int i = 0, n = constraints.size(); i < n; i++) {
            Constraint constraint = constraints.get(i);
            ConstraintSyntaxTree tree = constraint.getConsSyntax();
            LiteralFinder finder = new LiteralFinder(tree);
            Set<String> declarations = finder.getDeclarations();
            
            map.getList(declarations.size()).add(new ConstraintContainer(constraint, declarations));
            
            /*
             *  Release constraint to deallocate memory.
             *  set(index, null) avoids Array.copy
             */
            constraints.set(i, null);
        }
        return map.allLists();
    }
    
    /**
     * Returns whether the given CNF formula contains the variable negated or not. The tree must contain the variable.
     * @param tree The {@link ConstraintSyntaxTree} with the variable in CNF
     * @param variable The variable to search
     * @return Whether the variable is in a NOT call or not
     */
    private boolean isVariableNegated(ConstraintSyntaxTree tree, AbstractVariable variable) {
        return isVariableNegated(tree, variable, false);
    }
    
    /**
     * Returns whether the given CNF formula contains the variable negated or not. The tree must contain the variable.
     * @param tree The {@link ConstraintSyntaxTree} with the variable in CNF
     * @param variable The variable to search
     * @param negated If the previous recursion step is a NOT call
     * @return Whether the variable is in a NOT call or not
     */
    private boolean isVariableNegated(ConstraintSyntaxTree tree, AbstractVariable variable, boolean negated) {
        
        boolean result = false;
        
        if (tree instanceof OCLFeatureCall) {
            OCLFeatureCall call = (OCLFeatureCall) tree;
            if (call.getOperation().equals(OclKeyWords.NOT)) {
                result = isVariableNegated(call.getOperand(), variable, true);
            } else {
                if (containsVariable(call.getOperand(), variable)) {
                    result = isVariableNegated(call.getOperand(), variable, negated);
                } else if (containsVariable(call.getParameter(0), variable)) {
                    result = isVariableNegated(call.getParameter(0), variable, negated);
                } else {
                    // TODO
                    LOGGER.error("Unexpected operator in CNF formula.");
                }
            }
        } else if (tree instanceof Variable) {
            Variable var = (Variable) tree;
            if (var.getVariable().equals(variable)) {
                result = negated;
            }
        } else if (tree instanceof Parenthesis) {
            Parenthesis parenthesis = (Parenthesis) tree;
            result = isVariableNegated(parenthesis.getExpr(), variable, negated);
        } else {
            // TODO
            LOGGER.error("Unexpected ConstraintSyntaxTree in CNF formula.");
        }
        
        return result;
    }
    
    /**
     * Checks whether the given {@link ConstraintSyntaxTree} contains the variable.
     * @param tree The {@link ConstraintSyntaxTree} to check
     * @param variable The variable to find
     * @return true if the {@link ConstraintSyntaxTree} contains the variable
     */
    private boolean containsVariable(ConstraintSyntaxTree tree, AbstractVariable variable) {
        DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(tree);
        return finder.getDeclarations().contains(variable);
    }
    
    /**
     * Removes the given variable from the {@link ConstraintSyntaxTree}.
     * @param tree The {@link ConstraintSyntaxTree} that contains the variable
     * @param variable The variable to be removed
     * @return The {@link ConstraintSyntaxTree} without the variable
     */
    private ConstraintSyntaxTree removeVariable(ConstraintSyntaxTree tree, AbstractVariable variable) {
        
        ConstraintSyntaxTree result = null;
        
        if (tree instanceof OCLFeatureCall) {
            OCLFeatureCall call = (OCLFeatureCall) tree;
            if (call.getOperation().equals(OclKeyWords.NOT)) {
                ConstraintSyntaxTree operand = removeVariable(call.getOperand(), variable);
                if (operand != null) {
                    result = new OCLFeatureCall(operand, OclKeyWords.NOT);
                }
            } else {
                ConstraintSyntaxTree operand = removeVariable(call.getOperand(), variable);
                ConstraintSyntaxTree parameter = removeVariable(call.getParameter(0), variable);
                if (operand == null && parameter == null) {
                    result = null;
                } else if (parameter != null) {
                    result = parameter;
                } else if (operand != null) {
                    result = operand;
                } else {
                    result = call;
                }
            }
        } else if (tree instanceof Variable) {
            Variable var = (Variable) tree;
            if (!var.getVariable().equals(variable)) {
                result = var;
            }
        } else if (tree instanceof Parenthesis) {
            Parenthesis parenthesis = (Parenthesis) tree;
            result = removeVariable(parenthesis.getExpr(), variable);
        } else {
            // TODO
            LOGGER.error("Unexpected ConstraintSyntaxTree in CNF formula.");
        }
        
        return result;
    }
    
}
