package de.uni_hildesheim.sse.trans.convert;

import java.util.List;

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.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;

/**
 * Converts a Boolean {@link Project} into CNF form.
 * @author El-Sharkawy
 *
 */
public class CNFConverter {
    private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(CNFConverter.class, Main.ID);
    
    /**
     * Converts a Boolean {@link Project} into CNF form.
     * @param project A Boolean {@link Project} containing only constraints with AND, OR, and NOT operations.
     * @param converter A Strategy which is able to convert boolean formulas into CNF form.
     */
    public static void convert(Project project, ICNFConvertStrategy converter) {
        // Store complete content of project (imports are not used in this project).
        DeclarationFinder declfinder = new DeclarationFinder(project, FilterType.ALL, null);
        ConstraintFinder constFinder = new ConstraintFinder(project);
        
        // Clear old content
        project.clear();
        
        // 1. Re-add Declarations
        List<AbstractVariable> declarations = declfinder.getVariableDeclarations(VisibilityType.ALL);
        for (int i = 0, n = declarations.size(); i < n; i++) {
            project.add(declarations.get(i));
        }
        declfinder = null;
        declarations = null;
        
        // 2. Convert the constraints
        List<Constraint> constraints = constFinder.getConstraints();
        
        int lastNum = 0;
        long ms = 0;
        long timeLast = System.currentTimeMillis();
        
        for (int i = 0, n = constraints.size(); i < n; i++) {
            Constraint constraint = constraints.get(i);
            DisjunctionChecker checker = new DisjunctionChecker(constraint);
            if (checker.isDisjunctionTerm()) {
                project.add(constraint);
            } else {
                converter.convert(constraint);
            }
            
            ms += System.currentTimeMillis() - timeLast;
            timeLast = System.currentTimeMillis();
            while (ms > 5000) {
                ms -= 5000;
                LOGGER.info("Progress: " + i + "/" + constraints.size()
                        + " (" + (i - lastNum) + " in last 5 seconds)");
                lastNum = i;
            }
            
            /*
             *  Release constraint to deallocate memory.
             *  set(index, null) avoids Array.copy
             */
            constraints.set(i, null);
        }
    }
    
}
