///////////////////////////////////////////////////////////////////////////
//                   __                _      _   ________               //
//                  / /   ____  ____ _(_)____/ | / / ____/               //
//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
//                           /____/                                      //
//                                                                       //
//               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 org.logicng.datastructures.Assignment;
import org.logicng.datastructures.Substitution;
import org.logicng.datastructures.Tristate;
import org.logicng.formulas.cache.CacheEntry;
import org.logicng.functions.LiteralsFunction;
import org.logicng.functions.NumberOfAtomsFunction;
import org.logicng.functions.NumberOfNodesFunction;
import org.logicng.functions.VariablesFunction;
import org.logicng.knowledgecompilation.bdds.BDD;
import org.logicng.knowledgecompilation.bdds.BDDFactory;
import org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel;
import org.logicng.knowledgecompilation.bdds.orderings.VariableOrdering;
import org.logicng.knowledgecompilation.bdds.orderings.VariableOrderingProvider;
import org.logicng.predicates.CNFPredicate;
import org.logicng.predicates.DNFPredicate;
import org.logicng.predicates.NNFPredicate;
import org.logicng.predicates.satisfiability.ContradictionPredicate;
import org.logicng.predicates.satisfiability.SATPredicate;
import org.logicng.predicates.satisfiability.TautologyPredicate;
import org.logicng.transformations.NNFTransformation;

import java.util.SortedSet;
import java.util.stream.Stream;

/**
 * Super class for formulas.
 * @version 2.4.0
 * @since 1.0
 */
public abstract class Formula implements Iterable<Formula> {

    protected final FType type;
    protected final FormulaFactory f;

    /**
     * Constructs a new formula.
     * @param type the type of the formula
     * @param f    the factory which created this formula
     */
    protected Formula(final FType type, final FormulaFactory f) {
        this.type = type;
        this.f = f;
    }

    /**
     * Returns the type of this formula.
     * @return the type of this formula
     */
    public FType type() {
        return this.type;
    }

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

    /**
     * Returns the number of atomic formulas of this formula.  An atomic formula is a predicate (constants and literals)
     * or a pseudo-Boolean constraint.
     * @return the number of atomic formulas of this formula.
     */
    public long numberOfAtoms() {
        return NumberOfAtomsFunction.get().apply(this, true);
    }

    /**
     * Returns the number of nodes of this formula.
     * @return the number of nodes of this formula.
     */
    public long numberOfNodes() {
        return NumberOfNodesFunction.get().apply(this, true);
    }

    /**
     * Returns the number of operands of this formula.
     * @return the number of operands of this formula
     */
    public abstract int numberOfOperands();

    /**
     * Returns the number of internal nodes of this formula.
     * @return the number of internal nodes of this formula.
     */
    public long numberOfInternalNodes() {
        return this.f.numberOfNodes(this);
    }

    /**
     * Returns whether this formula is a constant formula ("True" or "False").
     * @return {@code true} if this formula is a constant formula, {@code false} otherwise
     */
    public abstract boolean isConstantFormula();

    /**
     * Returns whether this formula is an atomic formula (constant, literal, pseudo Boolean constraint), or not.
     * @return {@code true} if this formula is an atomic formula, {@code false} otherwise
     */
    public abstract boolean isAtomicFormula();

    /**
     * Returns all variables occurring in this formula.  Returns an unmodifiable set, so do not try to change the variable
     * set manually.
     * @return all variables occurring in this formula
     */
    public SortedSet<Variable> variables() {
        return VariablesFunction.get().apply(this, true);
    }

    /**
     * Returns all literals occurring in this formula.  Returns an unmodifiable set, so do not try to change the literal
     * set manually.
     * @return all literals occurring in this formula
     */
    public SortedSet<Literal> literals() {
        return LiteralsFunction.get().apply(this, true);
    }

    /**
     * Returns {@code true} if a given variable name is found in this formula, {@code false} otherwise.
     * @param variable the variable to search for
     * @return {@code true} if a given variable is found in this formula
     */
    public boolean containsVariable(final String variable) {
        return this.containsVariable(this.f.variable(variable));
    }

    /**
     * Returns {@code true} if a given variable name is found in this formula, {@code false} otherwise.
     * @param variable the variable to search for
     * @return {@code true} if a given variable is found in this formula
     */
    public abstract boolean containsVariable(final Variable variable);

    /**
     * Evaluates this formula with a given assignment.  A literal not covered by the assignment evaluates
     * to {@code false} if it is positive, otherwise it evaluates to {@code true}.
     * @param assignment the given assignment
     * @return the result of the evaluation, {@code true} or {@code false}
     */
    public abstract boolean evaluate(final Assignment assignment);

    /**
     * Restricts this formula with a given assignment.
     * @param assignment the given assignment
     * @return a new restricted formula
     */
    public abstract Formula restrict(final Assignment assignment);

    /**
     * Returns {@code true} if this formula contains a given node, {@code false} otherwise.
     * <p>
     * In particular, a {@code Literal} node {@code ~a} does NOT contain the node {@code a}.
     * @param formula the node
     * @return {@code true} if this formula contains a given node
     */
    public abstract boolean containsNode(final Formula formula);

    /**
     * Returns {@code true} if this formula is in NNF, otherwise {@code false}
     * @return {@code true} if this formula is in NNF, otherwise {@code false}
     * @see NNFPredicate the NNF predicate
     */
    public boolean isNNF() {
        return this.holds(NNFPredicate.get());
    }

    /**
     * Returns {@code true} if this formula is in DNF, otherwise {@code false}
     * @return {@code true} if this formula is in DNF, otherwise {@code false}
     * @see DNFPredicate the DNF predicate
     */
    public boolean isDNF() {
        return this.holds(DNFPredicate.get());
    }

    /**
     * Returns {@code true} if this formula is in CNF, otherwise {@code false}
     * @return {@code true} if this formula is in CNF, otherwise {@code false}
     * @see CNFPredicate the CNF predicate
     */
    public boolean isCNF() {
        return this.holds(CNFPredicate.get());
    }

    /**
     * Performs a simultaneous substitution on this formula given a single mapping from variable to formula.
     * @param variable the variable
     * @param formula  the formula
     * @return a new substituted formula
     */
    public Formula substitute(final Variable variable, final Formula formula) {
        final Substitution subst = new Substitution();
        subst.addMapping(variable, formula);
        return this.substitute(subst);
    }

    /**
     * Performs a given substitution on this formula.
     * @param substitution the substitution
     * @return a new substituted formula
     */
    public abstract Formula substitute(final Substitution substitution);

    /**
     * Returns a negated copy of this formula.
     * @return a negated copy of this formula
     */
    public abstract Formula negate();

    /**
     * Returns a copy of this formula which is in NNF.
     * @return a copy of this formula which is in NNF
     */
    public Formula nnf() {
        return transform(NNFTransformation.get(), true);
    }

    /**
     * Returns a copy of this formula which is in CNF.  The algorithm which is used for the default CNF transformation
     * can be configured in the {@link FormulaFactory}.
     * <p>
     * Be aware that the default algorithm for the CNF transformation may result in a CNF containing additional auxiliary
     * variables with prefix {@value FormulaFactory#CNF_PREFIX}.  Also, the result may not be a semantically equivalent CNF
     * but an equisatisfiable CNF.
     * <p>
     * If the introduction of auxiliary variables is unwanted, you can choose one of the algorithms
     * {@link org.logicng.transformations.cnf.CNFConfig.Algorithm#FACTORIZATION} and
     * {@link org.logicng.transformations.cnf.CNFConfig.Algorithm#BDD}.  Both algorithms provide CNF conversions without
     * the introduction of auxiliary variables and the result is a semantically equivalent CNF.
     * <p>
     * Since CNF is the input for the SAT or MaxSAT solvers, it has a special treatment here.  For other conversions, use
     * the according formula functions.
     * @return a copy of this formula which is in CNF
     */
    public Formula cnf() {
        return this.f.cnfEncoder().encode(this);
    }

    /**
     * Returns whether this formula is satisfiable.
     * A new SAT solver is used to check the satisfiability. This is a convenience method for the
     * predicate {@link org.logicng.predicates.satisfiability.SATPredicate}. If you want to
     * have more influence on the solver (e.g. which solver type or configuration) you must create and
     * use a {@link org.logicng.solvers.SATSolver} on your own.
     * @return {@code true} when this formula is satisfiable, {@code false} otherwise
     */
    public boolean isSatisfiable() {
        return this.holds(new SATPredicate(this.f));
    }

    /**
     * Returns whether this formula is a tautology, hence always true.
     * A new SAT solver is used to check the tautology. This is a convenience method for the
     * predicate {@link org.logicng.predicates.satisfiability.TautologyPredicate}. If you want to
     * have more influence on the solver (e.g. which solver type or configuration) you must create and
     * use a {@link org.logicng.solvers.SATSolver} on your own.
     * @return {@code true} when this formula is a tautology, {@code false} otherwise
     */
    public boolean isTautology() {
        return this.holds(new TautologyPredicate(this.f));
    }

    /**
     * Returns whether this formula is a contradiction, hence always false.
     * A new SAT solver is used to check the contradiction. This is a convenience method for the
     * predicate {@link org.logicng.predicates.satisfiability.ContradictionPredicate}. If you want to
     * have more influence on the solver (e.g. which solver type or configuration) you must create and
     * use a {@link org.logicng.solvers.SATSolver} on your own.
     * @return {@code true} when this formula is a contradiction, {@code false} otherwise
     */
    public boolean isContradiction() {
        return this.holds(new ContradictionPredicate(this.f));
    }

    /**
     * Returns whether this formula implies the given other formula, i.e. `this =&gt; other` is a tautology.
     * A new SAT solver is used to check this tautology. This is a convenience method. If you want to
     * have more influence on the solver (e.g. which solver type or configuration) you must create and
     * use a {@link org.logicng.solvers.SATSolver} on your own.
     * @param other the formula which should be checked if it is implied by this formula
     * @return {@code true} when this formula implies the given other formula, {@code false} otherwise
     */
    public boolean implies(final Formula other) {
        return this.f.implication(this, other).holds(new TautologyPredicate(this.f));
    }

    /**
     * Returns whether this formula is implied by the given other formula, i.e. `other =&gt; this` is a tautology.
     * A new SAT solver is used to check this tautology. This is a convenience method. If you want to
     * have more influence on the solver (e.g. which solver type or configuration) you must create and
     * use a {@link org.logicng.solvers.SATSolver} on your own.
     * @param other the formula which should be checked if it implies this formula
     * @return {@code true} when this formula is implied by the given other formula, {@code false} otherwise
     */
    public boolean isImpliedBy(final Formula other) {
        return this.f.implication(other, this).holds(new TautologyPredicate(this.f));
    }

    /**
     * Returns whether this formula is equivalent to the given other formula, i.e. `other &lt;=&gt; this` is a tautology.
     * A new SAT solver is used to check this tautology. This is a convenience method. If you want to
     * have more influence on the solver (e.g. which solver type or configuration) you must create and
     * use a {@link org.logicng.solvers.SATSolver} on your own.
     * @param other the formula which should be checked if it is equivalent with this formula
     * @return {@code true} when this formula is equivalent to the given other formula, {@code false} otherwise
     */
    public boolean isEquivalentTo(final Formula other) {
        return this.f.equivalence(this, other).holds(new TautologyPredicate(this.f));
    }

    /**
     * Generates a BDD from this formula with a given variable ordering.  This is done by generating a new BDD factory,
     * generating the variable order for this formula, and building a new BDD.  If more sophisticated operations should
     * be performed on the BDD or more than one formula should be constructed on the BDD, an own instance of
     * {@link BDDFactory} should be created and used.
     * @param variableOrdering the variable ordering
     * @return the BDD for this formula with the given ordering
     */
    public BDD bdd(final VariableOrdering variableOrdering) {
        final Formula formula = this.nnf();
        final int varNum = formula.variables().size();
        final BDDKernel kernel;
        if (variableOrdering == null) {
            kernel = new BDDKernel(this.f, varNum, varNum * 30, varNum * 20);
        } else {
            final VariableOrderingProvider provider = variableOrdering.provider();
            kernel = new BDDKernel(this.f, provider.getOrder(formula), varNum * 30, varNum * 20);
        }
        return BDDFactory.build(formula, kernel, null);
    }

    /**
     * Generates a BDD from this formula with no given variable ordering.  This is done by generating a new BDD factory
     * and building a new BDD.  If more sophisticated operations should be performed on the BDD or more than one
     * formula should be constructed on the BDD, an own instance of * {@link BDDFactory} should be created and used.
     * @return the BDD for this formula
     */
    public BDD bdd() {
        return bdd(null);
    }

    /**
     * Transforms this formula with a given formula transformator and caches the result.
     * @param transformation the formula transformator
     * @return the transformed formula
     */
    public Formula transform(final FormulaTransformation transformation) {
        return transformation.apply(this, true);
    }

    /**
     * Transforms this formula with a given formula transformator.
     * @param transformation the formula transformator
     * @param cache          indicates whether the result (and associated predicates) should be cached in this formula's cache.
     * @return the transformed formula
     */
    public Formula transform(final FormulaTransformation transformation, final boolean cache) {
        return transformation.apply(this, cache);
    }

    /**
     * Evaluates a given predicate on this formula, caches the result, and returns {@code true} if the predicate holds,
     * {@code false} otherwise.
     * @param predicate the predicate
     * @return {@code true} if the predicate holds, {@code false} otherwise
     */
    public boolean holds(final FormulaPredicate predicate) {
        return predicate.test(this, true);
    }

    /**
     * Evaluates a given predicate on this formula and returns {@code true} if the predicate holds, {@code false} otherwise.
     * @param predicate the predicate
     * @param cache     indicates whether the result should be cached in this formula's cache
     * @return {@code true} if the predicate holds, {@code false} otherwise
     */
    public boolean holds(final FormulaPredicate predicate, final boolean cache) {
        return predicate.test(this, cache);
    }

    /**
     * Applies a given function on this formula and returns the result.
     * @param function the function
     * @param cache    indicates whether the result should be cached in this formula's cache
     * @param <T>      the result type of the function
     * @return the result of the function application
     */
    public <T> T apply(final FormulaFunction<T> function, final boolean cache) {
        return function.apply(this, cache);
    }

    /**
     * Applies a given function on this formula, caches and returns the result.
     * @param function the function
     * @param <T>      the result type of the function
     * @return the result of the function application
     */
    public <T> T apply(final FormulaFunction<T> function) {
        return function.apply(this, true);
    }

    /**
     * Returns an entry of the transformation cache of this formula.
     * @param key the cache key
     * @return the cache value or {@code null} if the key is not found
     */
    public Formula transformationCacheEntry(final CacheEntry key) {
        return this.f.transformationCacheEntry(this, key);
    }

    /**
     * Sets an entry in the transformation cache of this formula
     * @param key   the cache key
     * @param value the cache value
     */
    public void setTransformationCacheEntry(final CacheEntry key, final Formula value) {
        this.f.setTransformationCacheEntry(this, key, value);
    }

    /**
     * Returns an entry of the predicate cache of this formula.
     * @param key the cache key
     * @return the cache value (which is {@code UNDEF} if nothing is present)
     */
    public Tristate predicateCacheEntry(final CacheEntry key) {
        return this.f.predicateCacheEntry(this, key);
    }

    /**
     * Sets an entry in the predicate cache of this formula
     * @param key   the cache key
     * @param value the cache value
     */
    public void setPredicateCacheEntry(final CacheEntry key, final boolean value) {
        this.f.setPredicateCacheEntry(this, key, value);
    }

    /**
     * Sets an entry in the predicate cache of this formula
     * @param key   the cache key
     * @param value the cache value
     */
    public void setPredicateCacheEntry(final CacheEntry key, final Tristate value) {
        this.f.setPredicateCacheEntry(this, key, value);
    }

    /**
     * Returns an entry of the function cache of this formula.
     * @param key the cache key
     * @return the cache value or {@code null} if the key is not found
     */
    public Object functionCacheEntry(final CacheEntry key) {
        return this.f.functionCacheEntry(this, key);
    }

    /**
     * Sets an entry in the function cache of this formula
     * @param key   the cache key
     * @param value the cache value
     */
    public void setFunctionCacheEntry(final CacheEntry key, final Object value) {
        this.f.setFunctionCacheEntry(this, key, value);
    }

    /**
     * Clears the transformation and function cache of the formula.
     */
    public void clearCaches() {
        this.f.clearCaches(this);
    }

    /**
     * Returns a stream of this formula's operands.
     * <p>
     * Most times streams have worse performance then iterating over the formula per iterator.
     * Since internally formulas store their operands, a costly call to {@code Arrays.stream()}
     * is necessary.  So if performance matters - avoid using streams.
     * @return the stream
     */
    public abstract Stream<Formula> stream();

    @Override
    public String toString() {
        return this.f.string(this);
    }
}
