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

import static java.util.Collections.emptySortedSet;
import static java.util.Collections.unmodifiableSortedSet;

import org.logicng.datastructures.Tristate;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Literal;
import org.logicng.formulas.Variable;

import java.util.Collections;
import java.util.Objects;
import java.util.SortedMap;
import java.util.SortedSet;
import java.util.TreeMap;
import java.util.TreeSet;

/**
 * This class represents a backbone.  A backbone of a formula is a set of literals (positive and/or negative) which
 * are present in their respective polarity in every model of the given formula.  Therefore, the literals must be set
 * accordingly in order for the formula to evaluate to true.
 * <p>
 * A backbone of a formula has up to three sets of variables
 * <ol>
 * <li>Positive backbone variables: Variables that occur positive in each model of the formula
 * <li>Negative backbone variables: Variables that occur negative in each model of the formula
 * <li>Optional variables: Variables that are neither in the positive nor in the negative backbone.
 * Therefore these variables can be assigned to true or false.
 * </ol>
 * All variable sets which were not computed are empty.
 * @version 2.3.1
 * @since 1.5.0
 */
public final class Backbone {

    private static final Backbone UNSAT_BACKBONE = new Backbone(false, null, null, null);

    private final boolean sat;
    private final SortedSet<Variable> positiveBackbone;
    private final SortedSet<Variable> negativeBackbone;
    private final SortedSet<Variable> optionalVariables;

    /**
     * Constructs a new backbone that contains the given backbone variables and the given optional variables.
     * @param sat               is the original formula satisfiable or not
     * @param positiveBackbone  positive backbone variables
     * @param negativeBackbone  negative backbone variables
     * @param optionalVariables optional variables
     */
    private Backbone(final boolean sat, final SortedSet<Variable> positiveBackbone, final SortedSet<Variable> negativeBackbone,
                     final SortedSet<Variable> optionalVariables) {
        this.sat = sat;
        this.positiveBackbone = positiveBackbone == null ? emptySortedSet() : positiveBackbone;
        this.negativeBackbone = negativeBackbone == null ? emptySortedSet() : negativeBackbone;
        this.optionalVariables = optionalVariables == null ? emptySortedSet() : optionalVariables;
    }

    /**
     * Returns a new backbone for a satisfiable formula.
     * @param positiveBackbone  positive backbone variables
     * @param negativeBackbone  negative backbone variables
     * @param optionalVariables optional variables
     * @return the backbone
     */
    public static Backbone satBackbone(final SortedSet<Variable> positiveBackbone, final SortedSet<Variable> negativeBackbone,
                                       final SortedSet<Variable> optionalVariables) {
        return new Backbone(true, positiveBackbone, negativeBackbone, optionalVariables);
    }

    /**
     * Returns a new empty backbone for an unsatisfiable formula.
     * @return the backbone
     */
    public static Backbone unsatBackbone() {
        return UNSAT_BACKBONE;
    }

    /**
     * Returns whether the original formula of this backbone was satisfiable or not.
     * @return whether the original formula of this backbone was satisfiable or not
     */
    public boolean isSat() {
        return this.sat;
    }

    /**
     * Returns the positive variables of the backbone.
     * @return the set of positive backbone variables
     */
    public SortedSet<Variable> getPositiveBackbone() {
        return unmodifiableSortedSet(this.positiveBackbone);
    }

    /**
     * Returns the negative variables of the backbone.
     * @return the set of negative backbone variables
     */
    public SortedSet<Variable> getNegativeBackbone() {
        return unmodifiableSortedSet(this.negativeBackbone);
    }

    /**
     * Returns the variables of the formula that are optional, i.e. not in the positive or negative backbone.
     * @return the set of non-backbone variables
     */
    public SortedSet<Variable> getOptionalVariables() {
        return unmodifiableSortedSet(this.optionalVariables);
    }

    /**
     * Returns all literals of the backbone.  Positive backbone variables have positive polarity, negative
     * backbone variables have negative polarity.
     * @return the set of both positive and negative backbone variables as literals
     */
    public SortedSet<Literal> getCompleteBackbone() {
        final SortedSet<Literal> completeBackbone = new TreeSet<Literal>(this.positiveBackbone);
        for (final Variable var : this.negativeBackbone) {
            completeBackbone.add(var.negate());
        }
        return Collections.unmodifiableSortedSet(completeBackbone);
    }

    /**
     * Returns the positive and negative backbone as a conjunction of literals.
     * @param f the formula factory needed for construction the backbone formula.
     * @return the backbone formula
     */
    public Formula toFormula(final FormulaFactory f) {
        return this.sat ? f.and(this.getCompleteBackbone()) : f.falsum();
    }

    /**
     * Returns the backbone as map from variables to tri-states. A positive variable is mapped to {@code Tristate.TRUE},
     * a negative variable to {@code Tristate.FALSE} and the optional variables to {@code Tristate.UNDEF}.
     * @return the mapping of the backbone
     */
    public SortedMap<Variable, Tristate> toMap() {
        final SortedMap<Variable, Tristate> map = new TreeMap<>();
        for (final Variable var : this.positiveBackbone) {
            map.put(var, Tristate.TRUE);
        }
        for (final Variable var : this.negativeBackbone) {
            map.put(var, Tristate.FALSE);
        }
        for (final Variable var : this.optionalVariables) {
            map.put(var, Tristate.UNDEF);
        }
        return Collections.unmodifiableSortedMap(map);
    }

    @Override
    public boolean equals(final Object other) {
        if (other == null) {
            return false;
        }
        if (this == other) {
            return true;
        }
        if (getClass() != other.getClass()) {
            return false;
        }
        final Backbone backbone = (Backbone) other;
        return this.sat == backbone.sat && Objects.equals(this.positiveBackbone, backbone.positiveBackbone) &&
                Objects.equals(this.negativeBackbone, backbone.negativeBackbone) &&
                Objects.equals(this.optionalVariables, backbone.optionalVariables);
    }

    @Override
    public int hashCode() {
        return Objects.hash(this.sat, this.positiveBackbone, this.negativeBackbone, this.optionalVariables);
    }

    @Override
    public String toString() {
        return "Backbone{" +
                "sat=" + this.sat +
                ", positiveBackbone=" + this.positiveBackbone +
                ", negativeBackbone=" + this.negativeBackbone +
                ", optionalVariables=" + this.optionalVariables +
                '}';
    }
}
