code: ///////////////////////////////////////////////////////////////////////////
  //                   __                _      _   ________               //
  //                  / /   ____  ____ _(_)____/ | / / ____/               //
  //                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
  //                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
  //               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
  //                           /____/                                      //
  //                                                                       //
  //               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);
      }
  }
  