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

import static org.logicng.formulas.FType.AND;
import static org.logicng.formulas.FType.FALSE;
import static org.logicng.formulas.FType.LITERAL;
import static org.logicng.formulas.FType.NOT;
import static org.logicng.formulas.FType.OR;
import static org.logicng.formulas.FType.TRUE;
import static org.logicng.formulas.cache.PredicateCacheEntry.IS_CNF;
import static org.logicng.formulas.cache.TransformationCacheEntry.FACTORIZED_CNF;

import org.logicng.cardinalityconstraints.CCConfig;
import org.logicng.configurations.Configuration;
import org.logicng.configurations.ConfigurationType;
import org.logicng.datastructures.Tristate;
import org.logicng.explanations.mus.MUSConfig;
import org.logicng.formulas.cache.CacheEntry;
import org.logicng.formulas.printer.FormulaStringRepresentation;
import org.logicng.functions.SubNodeFunction;
import org.logicng.pseudobooleans.PBConfig;
import org.logicng.pseudobooleans.PBEncoder;
import org.logicng.solvers.maxsat.algorithms.MaxSATConfig;
import org.logicng.solvers.sat.GlucoseConfig;
import org.logicng.solvers.sat.MiniSatConfig;
import org.logicng.transformations.FormulaFactoryImporter;
import org.logicng.transformations.cnf.CNFConfig;
import org.logicng.transformations.cnf.CNFEncoder;
import org.logicng.transformations.simplification.AdvancedSimplifierConfig;
import org.logicng.util.FormulaRandomizerConfig;
import org.logicng.util.Pair;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.EnumMap;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.Set;

/**
 * The formula factory for LogicNG.
 * <p>
 * New formulas can only be generated by a formula factory.  It is implemented s.t. it is guaranteed that equivalent
 * formulas (in terms of associativity and commutativity) are hold exactly once in memory.
 * <p>
 * A formula factory is NOT thread-safe.  If you generate formulas from more than one thread you either need to synchronize the formula factory
 * yourself or you use a formula factory for each single thread.
 * @version 2.5.0
 * @since 1.0
 */
public class FormulaFactory {

    public static final String CC_PREFIX = "@RESERVED_CC_";
    public static final String PB_PREFIX = "@RESERVED_PB_";
    public static final String CNF_PREFIX = "@RESERVED_CNF_";

    private final String name;

    private final CFalse cFalse;
    private final CTrue cTrue;
    private final FormulaStringRepresentation stringRepresentation;
    private final FormulaFactoryConfig.FormulaMergeStrategy formulaMergeStrategy;
    private final boolean simplifyComplementaryOperands;
    private final Map<ConfigurationType, Configuration> configurations;
    private final String ccPrefix;
    private final String pbPrefix;
    private final String cnfPrefix;
    private final SubNodeFunction subformulaFunction;
    private final PBEncoder pbEncoder;
    private final CNFEncoder cnfEncoder;
    Map<String, Variable> posLiterals;
    Map<String, Literal> negLiterals;
    Set<Variable> generatedVariables;
    Map<Formula, Not> nots;
    Map<Pair<Formula, Formula>, Implication> implications;
    Map<LinkedHashSet<? extends Formula>, Equivalence> equivalences;
    Map<LinkedHashSet<? extends Formula>, And> ands2;
    Map<LinkedHashSet<? extends Formula>, And> ands3;
    Map<LinkedHashSet<? extends Formula>, And> ands4;
    Map<LinkedHashSet<? extends Formula>, And> andsN;
    Map<LinkedHashSet<? extends Formula>, Or> ors2;
    Map<LinkedHashSet<? extends Formula>, Or> ors3;
    Map<LinkedHashSet<? extends Formula>, Or> ors4;
    Map<LinkedHashSet<? extends Formula>, Or> orsN;
    Map<PBOperands, PBConstraint> pbConstraints;
    Map<CCOperands, CardinalityConstraint> cardinalityConstraints;
    int ccCounter;
    int pbCounter;
    int cnfCounter;
    Map<Formula, Map<CacheEntry, Formula>> transformationCache;
    Map<Formula, Map<CacheEntry, Tristate>> predicateCache;
    Map<Formula, Map<CacheEntry, Object>> functionCache;
    Map<PBConstraint, List<Formula>> pbEncodingCache;
    private boolean cnfCheck;
    private FormulaFactoryImporter importer;

    /**
     * Constructor for a new formula factory.
     * @param config the configuration for this formula factory
     */
    public FormulaFactory(final FormulaFactoryConfig config) {
        this.name = config.name;
        this.stringRepresentation = config.stringRepresentation.get();
        this.formulaMergeStrategy = config.formulaMergeStrategy;
        this.simplifyComplementaryOperands = config.simplifyComplementaryOperands;
        this.configurations = initDefaultConfigs();
        this.cFalse = new CFalse(this);
        this.cTrue = new CTrue(this);
        this.clear();
        this.cnfEncoder = new CNFEncoder(this);
        this.subformulaFunction = SubNodeFunction.get();
        if (!this.name.isEmpty()) {
            this.ccPrefix = CC_PREFIX + this.name + "_";
            this.pbPrefix = PB_PREFIX + this.name + "_";
            this.cnfPrefix = CNF_PREFIX + this.name + "_";
        } else {
            this.ccPrefix = CC_PREFIX;
            this.pbPrefix = PB_PREFIX;
            this.cnfPrefix = CNF_PREFIX;
        }
        this.pbEncoder = new PBEncoder(this);
    }

    /**
     * Constructor for a new formula factory with the default configuration.
     */
    public FormulaFactory() {
        this(FormulaFactoryConfig.builder().build());
    }

    /**
     * Init all configurations with the default configurations.
     */
    private static Map<ConfigurationType, Configuration> initDefaultConfigs() {
        final Map<ConfigurationType, Configuration> configMap = new EnumMap<>(ConfigurationType.class);
        configMap.put(ConfigurationType.CNF, CNFConfig.builder().build());
        configMap.put(ConfigurationType.CC_ENCODER, CCConfig.builder().build());
        configMap.put(ConfigurationType.PB_ENCODER, PBConfig.builder().build());
        configMap.put(ConfigurationType.MINISAT, MiniSatConfig.builder().build());
        configMap.put(ConfigurationType.GLUCOSE, GlucoseConfig.builder().build());
        configMap.put(ConfigurationType.MAXSAT, MaxSATConfig.builder().build());
        configMap.put(ConfigurationType.MUS, MUSConfig.builder().build());
        configMap.put(ConfigurationType.ADVANCED_SIMPLIFIER, AdvancedSimplifierConfig.builder().build());
        configMap.put(ConfigurationType.FORMULA_RANDOMIZER, FormulaRandomizerConfig.builder().build());
        return configMap;
    }

    /**
     * Returns {@code true} if a given list of formulas contains the negation of a given formula,
     * {@code false} otherwise.  Always returns {@code false} if the formula factory is configured
     * to allow contradictions and tautologies.
     * @param formulas the list of formulas
     * @param formula  the formula
     * @return {@code true} if a given list of formulas contains a given formula, {@code false} otherwise
     */
    private boolean containsComplement(final LinkedHashSet<Formula> formulas, final Formula formula) {
        if (!this.simplifyComplementaryOperands) {
            return false;
        }
        final Formula negatedFormula = negateOrNull(formula);
        return negatedFormula != null && formulas.contains(negatedFormula);
    }

    /**
     * Returns the negated formula if the negation exists in the cache, otherwise {@code null} is returned.
     * @param formula the formula
     * @return the negated formula if the negation exists in the cache, otherwise {@code null}
     */
    private Formula negateOrNull(final Formula formula) {
        if (formula.type() == FALSE || formula.type() == TRUE || formula.type == NOT) {
            return formula.negate();
        } else if (formula.type() == LITERAL) {
            final Literal lit = (Literal) formula;
            final String name = lit.name();
            return lit.phase() ? this.negLiterals.get(name) : this.posLiterals.get(name);
        } else {
            return this.nots.get(formula);
        }
    }

    /**
     * Removes all formulas from the factory cache.
     */
    public void clear() {
        this.posLiterals = new HashMap<>();
        this.negLiterals = new HashMap<>();
        this.generatedVariables = new HashSet<>();
        this.nots = new HashMap<>();
        this.implications = new HashMap<>();
        this.equivalences = new HashMap<>();
        this.ands2 = new HashMap<>();
        this.ands3 = new HashMap<>();
        this.ands4 = new HashMap<>();
        this.andsN = new HashMap<>();
        this.ors2 = new HashMap<>();
        this.ors3 = new HashMap<>();
        this.ors4 = new HashMap<>();
        this.orsN = new HashMap<>();
        this.pbConstraints = new HashMap<>();
        this.cardinalityConstraints = new HashMap<>();
        this.ccCounter = 0;
        this.pbCounter = 0;
        this.cnfCounter = 0;
        this.transformationCache = new HashMap<>();
        this.predicateCache = new HashMap<>();
        this.functionCache = new HashMap<>();
        this.pbEncodingCache = new HashMap<>();
    }

    /**
     * Returns the name of this formula factory.
     * @return the name of this formula factory
     */
    public String name() {
        return this.name;
    }

    /**
     * Returns the configuration for a given configuration type or {@code null} if there isn't any.
     * @param cType the configuration type
     * @return the configuration for a given configuration type
     */
    public Configuration configurationFor(final ConfigurationType cType) {
        return this.configurations.get(cType);
    }

    /**
     * Puts a new configuration into the configuration database.  If there is already a configuration present for this
     * type, it will be overwritten.
     * <p>
     * Note that is not allowed to pass configurations of type {@link ConfigurationType#FORMULA_FACTORY}. Such
     * configurations can only be passed to the constructor and never be changed thereafter.
     * @param configuration the configuration
     * @throws IllegalArgumentException if a configuration of type {@link ConfigurationType#FORMULA_FACTORY} was passed
     */
    public void putConfiguration(final Configuration configuration) {
        if (configuration.type() == ConfigurationType.FORMULA_FACTORY) {
            throw new IllegalArgumentException("Configurations for the formula factory itself can only be passed in the constructor.");
        }
        this.configurations.put(configuration.type(), configuration);
    }

    /**
     * Returns a function to compute the sub-formulas.
     * @return a function to compute the sub-formulas
     */
    public SubNodeFunction subformulaFunction() {
        return this.subformulaFunction;
    }

    /**
     * Returns the default pseudo-Boolean encoder of this formula factory.
     * @return the default pseudo-Boolean encoder of this formula factory
     */
    public PBEncoder pbEncoder() {
        return this.pbEncoder;
    }

    /**
     * Returns the default CNF encoder of this formula factory.
     * @return the default CNF encoder of this formula factory
     */
    public CNFEncoder cnfEncoder() {
        return this.cnfEncoder;
    }

    /**
     * Creates a new binary operator with a given type and two operands.
     * @param type  the type of the formula
     * @param left  the left-hand side operand
     * @param right the right-hand side operand
     * @return the newly generated formula
     * @throws IllegalArgumentException if a wrong formula type is passed
     */
    public Formula binaryOperator(final FType type, final Formula left, final Formula right) {
        switch (type) {
            case IMPL:
                return this.implication(left, right);
            case EQUIV:
                return this.equivalence(left, right);
            default:
                throw new IllegalArgumentException("Cannot create a binary formula with operator: " + type);
        }
    }

    /**
     * Creates a new implication.
     * @param leftIn  the left-hand side operand
     * @param rightIn the right-hand side operand
     * @return a new implication
     */
    public Formula implication(final Formula leftIn, final Formula rightIn) {
        final Formula left = importOrPanic(leftIn);
        final Formula right = importOrPanic(rightIn);
        if (left.type() == FALSE || right.type() == TRUE) {
            return this.verum();
        }
        if (left.type() == TRUE) {
            return right;
        }
        if (right.type() == FALSE) {
            return this.not(left);
        }
        if (left.equals(right)) {
            return this.verum();
        }
        final Pair<Formula, Formula> key = new Pair<>(left, right);
        Implication implication = this.implications.get(key);
        if (implication == null) {
            implication = new Implication(left, right, this);
            this.implications.put(key, implication);
        }
        return implication;
    }

    /**
     * Creates a new equivalence.
     * @param leftIn  the left-hand side operand
     * @param rightIn the right-hand side operand
     * @return a new equivalence
     */
    public Formula equivalence(final Formula leftIn, final Formula rightIn) {
        final Formula left = importOrPanic(leftIn);
        final Formula right = importOrPanic(rightIn);
        if (left.type() == TRUE) {
            return right;
        }
        if (right.type() == TRUE) {
            return left;
        }
        if (left.type() == FALSE) {
            return this.not(right);
        }
        if (right.type() == FALSE) {
            return this.not(left);
        }
        if (left.equals(right)) {
            return this.verum();
        }
        if (left.equals(negateOrNull(right))) {
            return this.falsum();
        }
        final LinkedHashSet<Formula> key = new LinkedHashSet<>(Arrays.asList(left, right));
        Equivalence equivalence = this.equivalences.get(key);
        if (equivalence == null) {
            equivalence = new Equivalence(left, right, this);
            this.equivalences.put(key, equivalence);
        }
        return equivalence;
    }

    /**
     * Returns a (singleton) object for the constant "True".
     * @return an object for the constant "True"
     */
    public CTrue verum() {
        return this.cTrue;
    }

    /**
     * Creates the negation of a given formula.
     * <p>
     * Constants, literals and negations are negated directly and returned.
     * For all other formulas a new {@code Not} object is returned.
     * @param formula the given formula
     * @return the negated formula
     */
    public Formula not(final Formula formula) {
        final Formula operand = importOrPanic(formula);
        if (operand.type() == LITERAL || operand.type() == FALSE || operand.type() == TRUE || operand.type() == NOT) {
            return operand.negate();
        }
        Not not = this.nots.get(operand);
        if (not == null) {
            not = new Not(operand, this);
            this.nots.put(operand, not);
        }
        return not;
    }

    /**
     * Returns a (singleton) object for the constant "False".
     * @return an object for the constant "False"
     */
    public CFalse falsum() {
        return this.cFalse;
    }

    /**
     * Returns the constant "True" or "False" depending on the given value.
     * @param value the given value
     * @return the constant
     */
    public Constant constant(final boolean value) {
        return value ? this.cTrue : this.cFalse;
    }

    /**
     * Creates a new n-ary operator with a given type and a list of operands.
     * @param type     the type of the formula
     * @param operands the list of operands
     * @return the newly generated formula
     * @throws IllegalArgumentException if a wrong formula type is passed
     */
    public Formula naryOperator(final FType type, final Collection<? extends Formula> operands) {
        return this.naryOperator(type, operands.toArray(new Formula[0]));
    }

    /**
     * Creates a new n-ary operator with a given type and a list of operands.
     * @param type     the type of the formula
     * @param operands the list of operands
     * @return the newly generated formula
     * @throws IllegalArgumentException if a wrong formula type is passed
     */
    public Formula naryOperator(final FType type, final Formula... operands) {
        switch (type) {
            case OR:
                return this.or(operands);
            case AND:
                return this.and(operands);
            default:
                throw new IllegalArgumentException("Cannot create an n-ary formula with operator: " + type);
        }
    }

    /**
     * Creates a new conjunction from an array of formulas.
     * @param operands the vector of formulas
     * @return a new conjunction
     */
    public Formula and(final Formula... operands) {
        final LinkedHashSet<Formula> ops = new LinkedHashSet<>(operands.length);
        Collections.addAll(ops, operands);
        return this.constructAnd(ops);
    }

    /**
     * Creates a new conjunction from a collection of formulas.
     * <p>
     * Note: The LinkedHashSet is used to eliminate duplicate sub-formulas and to respect the commutativity of operands.
     * @param operands the array of formulas
     * @return a new conjunction
     */
    public Formula and(final Collection<? extends Formula> operands) {
        final LinkedHashSet<Formula> ops = new LinkedHashSet<>(operands);
        return this.constructAnd(ops);
    }

    /**
     * Checks if the given formula was created by this formula factory. If this is the case,
     * the formula is returned. Otherwise, depending on the {@link #formulaMergeStrategy}
     * the formula is either imported or an exception is thrown.
     * @param formula the formula to check
     * @return the (possibly imported) formula
     * @throws UnsupportedOperationException if the formula was created by another factory
     *                                       and the formula merge strategy is
     *                                       {@link FormulaFactoryConfig.FormulaMergeStrategy#PANIC}.
     */
    private Formula importOrPanic(final Formula formula) {
        if (formula.factory() == this) {
            return formula;
        }
        switch (this.formulaMergeStrategy) {
            case IMPORT:
                return importFormula(formula);
            case PANIC:
                throw new UnsupportedOperationException("Found an operand with a different formula factory.");
            default:
                throw new IllegalStateException("Unknown formula merge strategy: " + this.formulaMergeStrategy);
        }
    }

    /**
     * Checks if the given formulas were created by this formula factory. If this is the case,
     * the same list is returned. Otherwise, depending on the {@link #formulaMergeStrategy}
     * the formulas are either imported or an exception is thrown.
     * @param formulas the formulas to check
     * @return the (possibly imported) formulas
     * @throws UnsupportedOperationException if one of the formulas was created by another factory
     *                                       and the formula merge strategy is
     *                                       {@link FormulaFactoryConfig.FormulaMergeStrategy#PANIC}.
     */
    private LinkedHashSet<? extends Formula> importOrPanic(final LinkedHashSet<? extends Formula> formulas) {
        boolean foundAnotherFormulaFactory = false;
        for (final Formula formula : formulas) {
            if (formula.factory() != this) {
                foundAnotherFormulaFactory = true;
                break;
            }
        }
        if (!foundAnotherFormulaFactory) {
            return formulas;
        }
        switch (this.formulaMergeStrategy) {
            case IMPORT:
                final LinkedHashSet<Formula> result = new LinkedHashSet<>();
                for (final Formula formula : formulas) {
                    result.add(formula.factory() != this ? importFormula(formula) : formula);
                }
                return result;
            case PANIC:
                throw new UnsupportedOperationException("Found an operand with a different formula factory.");
            default:
                throw new IllegalStateException("Unknown formula merge strategy: " + this.formulaMergeStrategy);
        }
    }

    /**
     * Checks if the given literals were created by this formula factory. If this is the case,
     * the same array is returned. Otherwise, depending on the {@link #formulaMergeStrategy}
     * the formulas are either imported or an exception is thrown.
     * @param literals the literals to check
     * @return the (possibly imported) literals
     * @throws UnsupportedOperationException if one of the literals was created by another factory
     *                                       and the formula merge strategy is
     *                                       {@link FormulaFactoryConfig.FormulaMergeStrategy#PANIC}.
     */
    private Literal[] importOrPanic(final Literal[] literals) {
        boolean foundAnotherFormulaFactory = false;
        for (final Literal lit : literals) {
            if (lit.factory() != this) {
                foundAnotherFormulaFactory = true;
                break;
            }
        }
        if (!foundAnotherFormulaFactory) {
            return literals;
        }
        switch (this.formulaMergeStrategy) {
            case IMPORT:
                final Literal[] result = new Literal[literals.length];
                for (int i = 0; i < literals.length; i++) {
                    final Literal lit = literals[i];
                    result[i] = lit.factory() != this ? this.literal(lit.name(), lit.phase()) : lit;
                }
                return result;
            case PANIC:
                throw new UnsupportedOperationException("Found an operand with a different formula factory.");
            default:
                throw new IllegalStateException("Unknown formula merge strategy: " + this.formulaMergeStrategy);
        }
    }

    /**
     * Creates a new conjunction.
     * @param operandsIn the formulas
     * @return a new conjunction
     */
    private Formula constructAnd(final LinkedHashSet<? extends Formula> operandsIn) {
        final LinkedHashSet<? extends Formula> operands = importOrPanic(operandsIn);
        And tempAnd = null;
        Map<LinkedHashSet<? extends Formula>, And> opAndMap = this.andsN;
        if (operands.size() > 1) {
            switch (operands.size()) {
                case 2:
                    opAndMap = this.ands2;
                    break;
                case 3:
                    opAndMap = this.ands3;
                    break;
                case 4:
                    opAndMap = this.ands4;
                    break;
                default:
                    break;
            }
            tempAnd = opAndMap.get(operands);
        }
        if (tempAnd != null) {
            return tempAnd;
        }
        final LinkedHashSet<? extends Formula> condensedOperands = operands.size() < 2
                ? operands
                : this.condenseOperandsAnd(operands);
        if (condensedOperands == null) {
            return this.falsum();
        }
        if (condensedOperands.isEmpty()) {
            return this.verum();
        }
        if (condensedOperands.size() == 1) {
            return condensedOperands.iterator().next();
        }
        final And and;
        Map<LinkedHashSet<? extends Formula>, And> condAndMap = this.andsN;
        switch (condensedOperands.size()) {
            case 2:
                condAndMap = this.ands2;
                break;
            case 3:
                condAndMap = this.ands3;
                break;
            case 4:
                condAndMap = this.ands4;
                break;
            default:
                break;
        }
        and = condAndMap.get(condensedOperands);
        if (and == null) {
            tempAnd = new And(condensedOperands, this);
            setCnfCaches(tempAnd, this.cnfCheck);
            opAndMap.put(operands, tempAnd);
            condAndMap.put(condensedOperands, tempAnd);
            return tempAnd;
        }
        opAndMap.put(operands, and);
        return and;
    }

    /**
     * Creates a new CNF from an array of clauses.
     * <p>
     * ATTENTION: it is assumed that the operands are really clauses - this is not checked for performance reasons.
     * Also, no reduction of operands is performed - this method should only be used if you are sure that the CNF is free
     * of redundant clauses.
     * @param clauses the array of clauses
     * @return a new CNF
     */
    public Formula cnf(final Formula... clauses) {
        final LinkedHashSet<Formula> ops = new LinkedHashSet<>(clauses.length);
        Collections.addAll(ops, clauses);
        return this.constructCNF(ops);
    }

    /**
     * Creates a new CNF from a collection of clauses.
     * <p>
     * ATTENTION: it is assumed that the operands are really clauses - this is not checked for performance reasons.
     * Also, no reduction of operands is performed - this method should only be used if you are sure that the CNF is free
     * of redundant clauses.
     * @param clauses the collection of clauses
     * @return a new CNF
     */
    public Formula cnf(final Collection<? extends Formula> clauses) {
        final LinkedHashSet<? extends Formula> ops = new LinkedHashSet<>(clauses);
        return this.constructCNF(ops);
    }

    /**
     * Creates a new CNF.
     * @param clausesIn the clauses
     * @return a new CNF
     */
    private Formula constructCNF(final LinkedHashSet<? extends Formula> clausesIn) {
        final LinkedHashSet<? extends Formula> clauses = importOrPanic(clausesIn);
        if (clauses.isEmpty()) {
            return this.verum();
        }
        if (clauses.size() == 1) {
            return clauses.iterator().next();
        }
        Map<LinkedHashSet<? extends Formula>, And> opAndMap = this.andsN;
        switch (clauses.size()) {
            case 2:
                opAndMap = this.ands2;
                break;
            case 3:
                opAndMap = this.ands3;
                break;
            case 4:
                opAndMap = this.ands4;
                break;
            default:
                break;
        }
        And tempAnd = opAndMap.get(clauses);
        if (tempAnd != null) {
            return tempAnd;
        }
        tempAnd = new And(clauses, this);
        setCnfCaches(tempAnd, true);
        opAndMap.put(clauses, tempAnd);
        return tempAnd;
    }

    /**
     * Creates a new disjunction from an array of formulas.
     * @param operands the list of formulas
     * @return a new disjunction
     */
    public Formula or(final Formula... operands) {
        final LinkedHashSet<Formula> ops = new LinkedHashSet<>(operands.length);
        Collections.addAll(ops, operands);
        return this.constructOr(ops);
    }

    /**
     * Creates a new disjunction from a collection of formulas.
     * <p>
     * Note: The LinkedHashSet is used to eliminate duplicate sub-formulas and to respect the commutativity of operands.
     * @param operands the collection of formulas
     * @return a new disjunction
     */
    public Formula or(final Collection<? extends Formula> operands) {
        final LinkedHashSet<Formula> ops = new LinkedHashSet<>(operands);
        return this.constructOr(ops);
    }

    /**
     * Creates a new disjunction.
     * @param operandsIn the formulas
     * @return a new disjunction
     */
    private Formula constructOr(final LinkedHashSet<? extends Formula> operandsIn) {
        final LinkedHashSet<? extends Formula> operands = importOrPanic(operandsIn);
        Or tempOr = null;
        Map<LinkedHashSet<? extends Formula>, Or> opOrMap = this.orsN;
        if (operands.size() > 1) {
            switch (operands.size()) {
                case 2:
                    opOrMap = this.ors2;
                    break;
                case 3:
                    opOrMap = this.ors3;
                    break;
                case 4:
                    opOrMap = this.ors4;
                    break;
                default:
                    break;
            }
            tempOr = opOrMap.get(operands);
        }
        if (tempOr != null) {
            return tempOr;
        }
        final LinkedHashSet<? extends Formula> condensedOperands = operands.size() < 2
                ? operands
                : this.condenseOperandsOr(operands);
        if (condensedOperands == null) {
            return this.verum();
        }
        if (condensedOperands.isEmpty()) {
            return this.falsum();
        }
        if (condensedOperands.size() == 1) {
            return condensedOperands.iterator().next();
        }
        final Or or;
        Map<LinkedHashSet<? extends Formula>, Or> condOrMap = this.orsN;
        switch (condensedOperands.size()) {
            case 2:
                condOrMap = this.ors2;
                break;
            case 3:
                condOrMap = this.ors3;
                break;
            case 4:
                condOrMap = this.ors4;
                break;
            default:
                break;
        }
        or = condOrMap.get(condensedOperands);
        if (or == null) {
            tempOr = new Or(condensedOperands, this);
            setCnfCaches(tempOr, this.cnfCheck);
            opOrMap.put(operands, tempOr);
            condOrMap.put(condensedOperands, tempOr);
            return tempOr;
        }
        opOrMap.put(operands, or);
        return or;
    }

    /**
     * Creates a new DNF from an array of terms (conjunctions of literals).
     * <p>
     * ATTENTION: it is assumed that the operands are really terms - this is not checked for performance reasons.
     * Also, no reduction of operands is performed - this method should only be used if you are sure that the DNF is free
     * of redundant terms.
     * @param terms the array of terms
     * @return a new DNF
     */
    public Formula dnf(final Formula... terms) {
        final LinkedHashSet<Formula> ops = new LinkedHashSet<>(terms.length);
        Collections.addAll(ops, terms);
        return this.constructDNF(ops);
    }

    /**
     * Creates a new DNF from a collection of terms (conjunctions of literals).
     * <p>
