package de.uni_hildesheim.sse.trans.convert;

import java.math.BigInteger;
import java.text.NumberFormat;

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.ConstraintSyntaxTree;
import de.uni_hildesheim.sse.model.cstEvaluation.EvaluationVisitor;
import de.uni_hildesheim.sse.model.varModel.AbstractVariable;
import de.uni_hildesheim.sse.model.varModel.values.BooleanValue;
import de.uni_hildesheim.sse.persistency.StringProvider;
import de.uni_hildesheim.sse.trans.Main;
import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory;
import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger;

/**
 * Alternative implementation of {@link MaxTermConverter}, which uses a backtracking algorithm
 * instead of iteration to find all max terms.
 * 
 * @author Adam Krafczyk
 * @author El-Sharkawy
 */
public class MaxTermConverter2 extends MaxTermConverter {
    private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(MaxTermConverter2.class, Main.ID);
    private static final NumberFormat PERCENT_FORMAT = NumberFormat.getPercentInstance();
    static {
        PERCENT_FORMAT.setMaximumFractionDigits(3);
    }
    
    private long lastTime;
    private BigInteger totalSteps;
    private BigInteger elapsedSteps;
    private EvaluationVisitor evaluationVisitor;

    @Override
    protected void handleSmallConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
        Configuration config) {
        
        handleBigConstraint(originalConstraint, declarationArray, config);
    }
    
    @Override
    protected void handleBigConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
        Configuration config) {
        
        lastTime = System.currentTimeMillis();
        totalSteps = TWO.pow(declarationArray.length);
        elapsedSteps = BigInteger.ZERO;
        evaluationVisitor = new EvaluationVisitor(config, null, false, null);
        
        // SE: Arrays with 21 variables are not supported inside my 32 Bit JVM
        if (declarationArray.length < 21 || "64".equals(System.getProperty("sun.arch.data.model"))) {
            handleConstraint(originalConstraint, declarationArray, config, 0);            
        } else {
            LOGGER.debug(StringProvider.toIvmlString(originalConstraint));
        }
    }
    
    /**
     * Converts a constraint into a CNF formula.
     * @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>
     * @param var the variable to change
     */
    private void handleConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
        Configuration config, int var) {
        
        if (System.currentTimeMillis() - lastTime > 10000) {
            lastTime = System.currentTimeMillis();
            LOGGER.info("Progress: (" + declarationArray.length + " vars) "
                + PERCENT_FORMAT.format(elapsedSteps.doubleValue() / totalSteps.doubleValue()));
        }
        
        if (var >= declarationArray.length) {
            return;
        }
        
        try {
            IDecisionVariable decisionVar = config.getDecision(declarationArray[var]);
            
            // First, try positive solution
            decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED);
            checkConstraint(originalConstraint, declarationArray, config, var);
            
            // Second, try negative solution
            decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED);
            checkConstraint(originalConstraint, declarationArray, config, var);
            
            // third, backtracking
            decisionVar.setValue(null, AssignmentState.UNDEFINED);
            
        } catch (ConfigurationException e) {
            LOGGER.exception(e);
        }
    }

    /**
     * Part of the {@link #handleConstraint(ConstraintSyntaxTree, AbstractVariable[], Configuration, int)} method.
     * Calls {@link #checkConstraint(ConstraintSyntaxTree, Configuration)} and starts a recusive call of the
     * {@link #handleConstraint(ConstraintSyntaxTree, AbstractVariable[], Configuration, int)} method if needed.
     * @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>
     * @param var the variable to change
     */
    private void checkConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
        Configuration config, int var) {
        
        int result = checkConstraint(originalConstraint, config);
        switch (result) {
        case 0:
            BigInteger skipped = TWO.pow(declarationArray.length - (var + 1));
            elapsedSteps = elapsedSteps.add(skipped);
            addExpression(declarationArray, var, config);
            break;
        case -1:
            handleConstraint(originalConstraint, declarationArray, config, var + 1);
            break;
        case 1:
            skipped = TWO.pow(declarationArray.length - (var + 1));
            elapsedSteps = elapsedSteps.add(skipped);
            break;
        default:
            LOGGER.error("Unexpected while creating max terms.");
            break;
        }
    }
    
    /**
     * Checks whether the constraint is already true, false or still undefined with the given variables set.
     * 
     * @param constraint The {@link ConstraintSyntaxTree} that represents the boolean expression
     * @param config the {@link Configuration} that holds the variable states
     * 
     * @return 0 if the expression is false; 1 if the expression is true; -1 if the expression is undefined
     */
    private int checkConstraint(ConstraintSyntaxTree constraint, Configuration config) {
        constraint.accept(evaluationVisitor);
        
        int result = -1;
        if (evaluationVisitor.constraintFailed()) {
            result = 0;
        } else if (evaluationVisitor.constraintFulfilled()) {
            result = 1;
        }
        
        evaluationVisitor.clearResult();
        
        return result;
    }
    
    /**
     * Adds the boolean expression to the model via {@link MaxTermConverter#addConstraint(ConstraintSyntaxTree)}.
     * 
     * @param declarationArray Array with all variable declarations
     * @param var The number of variables that is defined (0 to var -1 in the declaration array)
     * @param config The {@link Configuration} that holds the states of the variables
     */
    private void addExpression(AbstractVariable[] declarationArray, int var, Configuration config) {
        boolean[] state = new boolean[var + 1];
        for (int i = 0; i < state.length; i++) {
            state[i] = ((BooleanValue) config.getDecision(declarationArray[i]).getValue()) == BooleanValue.TRUE;
        }
        addConstraint(createNegatedORExpression(declarationArray, state));
    }
    
}
