///////////////////////////////////////////////////////////////////////////
//                   __                _      _   ________               //
//                  / /   ____  ____ _(_)____/ | / / ____/               //
//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
//                           /____/                                      //
//                                                                       //
//               The Next Generation Logic Library                       //
//                                                                       //
///////////////////////////////////////////////////////////////////////////
//                                                                       //
//  Copyright 2015-20xx Christoph Zengler                                //
//                                                                       //
//  Licensed under the Apache License, Version 2.0 (the "License");      //
//  you may not use this file except in compliance with the License.     //
//  You may obtain a copy of the License at                              //
//                                                                       //
//  http://www.apache.org/licenses/LICENSE-2.0                           //
//                                                                       //
//  Unless required by applicable law or agreed to in writing, software  //
//  distributed under the License is distributed on an "AS IS" BASIS,    //
//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or      //
//  implied.  See the License for the specific language governing        //
//  permissions and limitations under the License.                       //
//                                                                       //
///////////////////////////////////////////////////////////////////////////

package org.logicng.transformations.qmc;

import org.logicng.datastructures.Tristate;
import org.logicng.formulas.Formula;

import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.SortedSet;
import java.util.TreeSet;
import java.util.Vector;

/**
 * A term table in the Quine–McCluskey algorithm.  The term table is used
 * for the line and column dominance checks.
 * @version 2.0.0
 * @since 1.4.0
 */
public class TermTable {

    protected final Vector<Formula> columnHeaders;
    protected final Vector<Term> lineHeaders;
    protected final Vector<Vector<Boolean>> matrixLines;
    protected final Vector<Vector<Boolean>> matrixColumns;

    /**
     * Constructs a prime term table from a given list of terms.
     * @param terms the terms
     */
    TermTable(final LinkedHashSet<Term> terms) {
        this.lineHeaders = new Vector<>(terms.size());
        this.columnHeaders = initializeColumnHeaders(terms);
        this.matrixLines = new Vector<>(terms.size());
        this.matrixColumns = new Vector<>(this.columnHeaders.size());
        final Vector<Boolean> matrixLineTemplate = new Vector<>(this.columnHeaders.size());
        for (int i = 0; i < this.columnHeaders.size(); i++) {
            matrixLineTemplate.add(false);
        }
        final Vector<Boolean> matrixColumnTemplate = new Vector<>(terms.size());
        for (int i = 0; i < terms.size(); i++) {
            matrixColumnTemplate.add(false);
        }
        for (int i = 0; i < this.columnHeaders.size(); i++) {
            this.matrixColumns.add(new Vector<>(matrixColumnTemplate));
        }
        int count = 0;
        for (final Term term : terms) {
            this.lineHeaders.add(term);
            final Vector<Boolean> matrixLine = new Vector<>(matrixLineTemplate);
            this.matrixLines.add(matrixLine);
            for (final Formula minterm : term.minterms()) {
                final int index = this.columnHeaders.indexOf(minterm);
                matrixLine.setElementAt(true, index);
                this.matrixColumns.get(index).setElementAt(true, count);
            }
            count++;
        }
    }

    /**
     * Initialize the column headers with the minterms
     * @param terms the terms
     * @return the column headers
     */
    protected Vector<Formula> initializeColumnHeaders(final LinkedHashSet<Term> terms) {
        final LinkedHashSet<Formula> header = new LinkedHashSet<>();
        for (final Term term : terms) {
            header.addAll(term.minterms());
        }
        return new Vector<>(header);
    }

    /**
     * Simplifies this table by using column and line dominance.
     */
    void simplifyTableByDominance() {
        boolean changed;
        do {
            final boolean eliminatedColumns = eliminateColumnDominance();
            final boolean eliminatedLines = eliminateLineDominance();
            changed = eliminatedColumns || eliminatedLines;
        } while (changed);
    }

    /**
     * Performs elimination of columns by dominance.
     * @return {@code true} if an elimination was performed, {@code false} otherwise
     */
    protected boolean eliminateColumnDominance() {
        final SortedSet<Integer> toEliminate = new TreeSet<>();
        for (int i = 0; i < this.matrixColumns.size(); i++) {
            for (int j = i + 1; j < this.matrixColumns.size(); j++) {
                if (isSubsetOf(this.matrixColumns.get(i), this.matrixColumns.get(j))) {
                    toEliminate.add(j);
                } else if (isSubsetOf(this.matrixColumns.get(j), this.matrixColumns.get(i))) {
                    toEliminate.add(i);
                }
            }
        }
        int count = 0;
        for (final Integer toDelete : toEliminate) {
            deleteColumn(toDelete - count++);
        }
        return !toEliminate.isEmpty();
    }

    /**
     * Performs elimination of lines by dominance.
     * @return {@code true} if an elimination was performed, {@code false} otherwise
     */
    protected boolean eliminateLineDominance() {
        final SortedSet<Integer> toEliminate = new TreeSet<>();
        for (int i = 0; i < this.matrixLines.size(); i++) {
            for (int j = i + 1; j < this.matrixLines.size(); j++) {
                if (isSubsetOf(this.matrixLines.get(i), this.matrixLines.get(j))) {
                    toEliminate.add(i);
                } else if (isSubsetOf(this.matrixLines.get(j), this.matrixLines.get(i))) {
                    toEliminate.add(j);
                }
            }
        }
        int count = 0;
        for (final Integer toDelete : toEliminate) {
            deleteLine(toDelete - count++);
        }
        return !toEliminate.isEmpty();
    }

    /**
     * Returns whether vec1 is a subset of vec2.
     * @param vec1 the first vector
     * @param vec2 the second vector
     * @return {@code true} if vec1 is a subset of vec2, {@code false} otherwise
     */
    static boolean isSubsetOf(final Vector<Boolean> vec1, final Vector<Boolean> vec2) {
        for (int i = 0; i < vec1.size(); i++) {
            if (vec1.get(i) && !vec2.get(i)) {
                return false;
            }
        }
        return true;
    }

    /**
     * Deletes a column at a given index.
     * @param colIndex the index
     */
    protected void deleteColumn(final int colIndex) {
        this.columnHeaders.removeElementAt(colIndex);
        this.matrixColumns.removeElementAt(colIndex);
        for (final Vector<Boolean> line : this.matrixLines) {
            line.removeElementAt(colIndex);
        }
    }

    /**
     * Deletes a line at a given index.
     * @param lineIndex the index
     */
    protected void deleteLine(final int lineIndex) {
        this.lineHeaders.removeElementAt(lineIndex);
        this.matrixLines.removeElementAt(lineIndex);
        for (final Vector<Boolean> column : this.matrixColumns) {
            column.removeElementAt(lineIndex);
        }
    }

    /**
     * Returns the lines of this table.
     * @return the lines of this table
     */
    Vector<Vector<Boolean>> lines() {
        return this.matrixLines;
    }

    /**
     * Returns the columns of this table.
     * @return the columns of this table
     */
    Vector<Vector<Boolean>> columns() {
        return this.matrixColumns;
    }

    /**
     * Returns the column headers of this table.
     * @return the column headers of this table
     */
    Vector<Formula> columnHeaders() {
        return this.columnHeaders;
    }

    /**
     * Returns the line headers of this table.
     * @return the line headers of this table
     */
    Vector<Term> lineHeaders() {
        return this.lineHeaders;
    }

    @Override
    public String toString() {
        final Vector<String> lineHeaderStrings = new Vector<>();
        for (final Term header : this.lineHeaders) {
            lineHeaderStrings.add(formatBits(header.bits()));
        }
        final int lineHeaderSize = lineHeaderStrings.firstElement().length();
        final StringBuilder sb = new StringBuilder();
        for (int i = 0; i < lineHeaderSize; i++) {
            sb.append(" ");
        }
        sb.append(" | ");
        final LinkedHashMap<String, String> legend = new LinkedHashMap<>();
        int columnSize = 0;
        for (int i = 0; i < this.columnHeaders.size(); i++) {
            final String key = "m" + i;
            legend.put(key, this.columnHeaders.get(i).toString());
            if (key.length() > columnSize) {
                columnSize = key.length();
            }
        }
        for (final String s : legend.keySet()) {
            sb.append(String.format("%s | ", padRight(s, columnSize)));
        }
        sb.append(String.format("%n"));

        for (int i = 0; i < this.matrixLines.size(); i++) {
            sb.append(String.format("%s | %s%n", lineHeaderStrings.get(i), formatMatrixLine(this.matrixLines.get(i), columnSize)));
        }
        return sb.toString();
    }

    protected String formatMatrixLine(final Vector<Boolean> booleans, final int size) {
        final StringBuilder sb = new StringBuilder();
        for (final Boolean entry : booleans) {
            sb.append(padRight((entry ? "X" : " "), size)).append(" | ");
        }
        return sb.toString();
    }

    protected String formatBits(final Tristate[] bits) {
        final StringBuilder sb = new StringBuilder();
        sb.append("[");
        for (int i = 0; i < bits.length; i++) {
            if (bits[i] == Tristate.TRUE) {
                sb.append("1");
            } else if (bits[i] == Tristate.FALSE) {
                sb.append("0");
            } else {
                sb.append("-");
            }
            if (i < bits.length - 1) {
                sb.append(", ");
            }
        }
        sb.append("]");
        return sb.toString();
    }

    private static String padRight(final String s, final int n) {
        return String.format("%1$-" + n + "s", s);
    }
}
