package de.uni_hildesheim.sse.trans.convert;

import java.math.BigInteger;
import java.util.Arrays;
import java.util.Comparator;
import java.util.HashMap;
import java.util.Map;
import java.util.Set;

import de.uni_hildesheim.sse.model.confModel.AssignmentState;
import de.uni_hildesheim.sse.model.confModel.Configuration;
import de.uni_hildesheim.sse.model.confModel.ConfigurationException;
import de.uni_hildesheim.sse.model.confModel.IDecisionVariable;
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.cstEvaluation.EvaluationVisitor;
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.DeclrationInConstraintFinder;
import de.uni_hildesheim.sse.model.varModel.values.BooleanValue;
import de.uni_hildesheim.sse.trans.Main;
import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory;
import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger;

/**
 * Converts a boolean formula in a list of disjunction terms by means of
 * <a href="http://de.wikipedia.org/w/index.php?title=Konjunktive_Normalform&oldid=130361119
 * #Beispiel_f.C3.BCr_die_Bildung">max terms</a>.
 * @author Adam Krafczyk
 * @author El-Sharkawy
 *
 */
public class MaxTermConverter implements ICNFConvertStrategy {
    public static final BigInteger TWO = BigInteger.valueOf(2);
    private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(MaxTermConverter.class, Main.ID);

    private Project project;
    private Map<AbstractVariable, Variable> variablesCache = new HashMap<AbstractVariable, Variable>();
    
    /**
     * Returns a {@link Variable} for the given {@link AbstractVariable}.
     * This method will cache already created {@link Variable}s to reduce memory consumption.
     * @param decl A {@link AbstractVariable} for which a {@link Variable} shall be created.
     * @return A cached {@link Variable} for the given {@link AbstractVariable} or a new one
     *     if no cached variable exists, a new one is created and will be cached for future calls.
     */
    protected final Variable getVariable(AbstractVariable decl) {
        Variable variable = variablesCache.get(decl);
        if (null == variable) {
            variable = new Variable(decl);
            variablesCache.put(decl, variable);
        }
        
        return variable;
    }
    
    @Override
    public void convert(Constraint constraint) {
        project = (Project) constraint.getTopLevelParent();
        
        createCNFParts(constraint.getConsSyntax());
    }
    
    /**
     * Converts the given expression into CNF and adds it via
     * {@link MaxTermConverter#addConstraint(ConstraintSyntaxTree)}.
     * @param originalConstraint A boolean expression
     */
    private void createCNFParts(ConstraintSyntaxTree originalConstraint) {
        if (originalConstraint instanceof Parenthesis) {
            // Unpack constraint if there are parenthesis at the top level
            createCNFParts(((Parenthesis) originalConstraint).getExpr()); 
        } else if (originalConstraint instanceof OCLFeatureCall
            && OclKeyWords.AND.equals(((OCLFeatureCall) originalConstraint).getOperation())) {
            
            // Split top level AND calls into two separate terms
            OCLFeatureCall call = (OCLFeatureCall) originalConstraint;
            createCNFParts(call.getOperand());
            createCNFParts(call.getParameter(0));
        } else {
            // Stop recursion!
            
            // Get an array of all variables in the constraint
            DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(originalConstraint);
            Set<AbstractVariable> declarations = finder.getDeclarations();
            AbstractVariable[] declarationArray = declarations.toArray(new AbstractVariable[] {});
            Arrays.sort(declarationArray, new Comparator<AbstractVariable>() {
                public int compare(AbstractVariable o1, AbstractVariable o2) {
                    return o1.getName().compareTo(o2.getName());
                }
            });
            
            // Create a project which only contains our single Constraint
            Project singleConstraintProject = new Project("SingleConstraintProject");
            Constraint constraintCopy = null;
            try {
                constraintCopy = new Constraint(originalConstraint, singleConstraintProject);
            } catch (CSTSemanticException e) {
                // Cannot happen
                LOGGER.exception(e);
            }
            singleConstraintProject.add(constraintCopy);
            for (AbstractVariable var : declarationArray) {
                singleConstraintProject.add(var);
            }
            
            // Create a configuration object for the singleConstraintProject
            Configuration config = new Configuration(singleConstraintProject);
            
            if (declarationArray.length >= 16) {
    //            System.out.println("Handling big constraint: " + declarationArray.length);
                handleBigConstraint(originalConstraint, declarationArray, config);
    //            System.out.println("Done.");
            } else {
                handleSmallConstraint(originalConstraint, declarationArray, config);
            }
        }
    }

    /**
     * Converts a small constraint into a CNF formula.
     * This constraint must have at maximum 15 different {@link AbstractVariable}s.
     * @param originalConstraint The constraint which shall be converted into CNF formula.
     *     this constraint may consists only of AND, OR, and NOT operations.
     * @param declarationArray The {@link AbstractVariable}s, which are used inside the <tt>originalConstraint</tt>.
     * @param config A temporary {@link Configuration} containing only <tt>originalConstraint</tt>
     *     and <tt>declarationArray</tt>
     */
    protected void handleSmallConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
        Configuration config) {
        
        EvaluationVisitor evalVisitor = new EvaluationVisitor();
        evalVisitor.init(config, null, false, null);
        // for each combination of the variables (true or false)
        for (int i = 0; i < Math.pow(2, declarationArray.length); i++) {
            boolean[] state = new boolean[declarationArray.length];
            for (int j = 0; j < state.length; j++) {
                IDecisionVariable decisionVar = config.getDecision(declarationArray[j]);
                /*
                 * i is a bit-field where each bit represents one variable
                 * j is the current variable
                 * To test if variable #j is true check if the bit #j in i is 0 or 1
                 */
                if ((i & (1 << j)) != 0) {
                    state[j] = true;
                    try {
                        decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED);
                    } catch (ConfigurationException e) {
                        // TODO
                        LOGGER.exception(e);
                    }
                } else {
                    state[j] = false;
                    try {
                        decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED);
                    } catch (ConfigurationException e) {
                        // TODO
                        LOGGER.exception(e);
                    }
                }
            }
            
            // get the result
            originalConstraint.accept(evalVisitor);
            boolean result = evalVisitor.constraintFulfilled();
            
            // if the result it false, add the negated combination to the list of expressions
            if (!result) {
                addConstraint(createNegatedORExpression(declarationArray, state)); 
            }
            
            // 1 * init() + n * clearResult() is much faster than n * (init() + clear())
            evalVisitor.clearResult();
        }
    }
    
    /**
     * Converts a constraint into a CNF formula.
     * This constraint can have any number of {@link AbstractVariable}s, but for small constraints
     * {@link MaxTermConverter#handleSmallConstraint} is recommended.
     * @param originalConstraint The constraint which shall be converted into CNF formula.
     *     this constraint may consists only of AND, OR, and NOT operations.
     * @param declarationArray The {@link AbstractVariable}s, which are used inside the <tt>originalConstraint</tt>.
     * @param config A temporary {@link Configuration} containing only <tt>originalConstraint</tt>
     *     and <tt>declarationArray</tt>
     */
    protected void handleBigConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
            Configuration config) {
        
        EvaluationVisitor evalVisitor = new EvaluationVisitor();
        evalVisitor.init(config, null, false, null);
        // for each combination of the variables (true or false)
        for (BigInteger i = BigInteger.ZERO; i.compareTo(TWO.pow(declarationArray.length)) == -1;
            i = i.add(BigInteger.ONE)) {
            
            boolean[] state = new boolean[declarationArray.length];
            for (int j = 0; j < state.length; j++) {
                IDecisionVariable decisionVar = config.getDecision(declarationArray[j]);
                /*
                 * i is a bit-field where each bit represents one variable
                 * j is the current variable
                 * To test if variable #j is true check if the bit #j in i is 0 or 1
                 */
                if (i.testBit(j)) {
                    state[j] = true;
                    try {
                        decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED);
                    } catch (ConfigurationException e) {
                        // TODO
                        LOGGER.exception(e);
                    }
                } else {
                    state[j] = false;
                    try {
                        decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED);
                    } catch (ConfigurationException e) {
                        // TODO
                        LOGGER.exception(e);
                    }
                }
            }
            
            // get the result
            originalConstraint.accept(evalVisitor);
            boolean result = evalVisitor.constraintFulfilled();
            
            // if the result it false, add the negated combination to the list of expressions
            if (!result) {
                addConstraint(createNegatedORExpression(declarationArray, state)); 
            }
            
            // 1 * init() + n * clearResult() is much faster than n * (init() + clear())
            evalVisitor.clearResult();
        }
    }
    
    /**
     * Creates an {@link ConstraintSyntaxTree} with the variables negated and OR'd together.
     * @param variables Array of Variables
     * @param states Array whether each variable is true or false
     * @return the {@link ConstraintSyntaxTree}
     */
    protected ConstraintSyntaxTree createNegatedORExpression(AbstractVariable[] variables, boolean[] states) {
        ConstraintSyntaxTree call = null;
        if (!states[0]) {
            call = getVariable(variables[0]);
        } else {
            call = new OCLFeatureCall(getVariable(variables[0]), OclKeyWords.NOT);
        }
        
        for (int i = 1; i < states.length; i++) {
            ConstraintSyntaxTree variable = getVariable(variables[i]);
            if (states[i]) {
                variable = new OCLFeatureCall(variable, OclKeyWords.NOT);
            }
            call = new OCLFeatureCall(call, OclKeyWords.OR, variable);
        }
        return call;
    }

    /**
     * Adds the given constraint to the project.
     * @param cst The constraint to add.
     */
    protected void addConstraint(ConstraintSyntaxTree cst) {
        Constraint constraint = new Constraint(project);
        try {
            constraint.setConsSyntax(cst);
        } catch (CSTSemanticException e) {
            LOGGER.exception(e);
        }
        
        project.add(constraint);
    }
}
