package com.naveensundarg.shadow.prover.representations.formula;

import com.naveensundarg.shadow.prover.representations.value.Value;
import com.naveensundarg.shadow.prover.representations.value.Variable;
import com.naveensundarg.shadow.prover.utils.Sets;

import java.util.Map;
import java.util.Set;
import java.util.function.UnaryOperator;

/**
 * Created by naveensundarg on 4/10/16.
 */
public final class BiConditional extends Formula {

    private final Formula left;
    private final Formula right;
    private final Set<Formula> subFormulae;
    private final Set<Variable> variables;
    private final Set<Value> values;
    private final Set<Variable> boundVariables;



    private final int weight;
    public BiConditional(Formula left, Formula right){

        this.left = left;
        this.right = right;

        this.subFormulae = Sets.union(left.subFormulae(), right.subFormulae());

        this.variables = Sets.union(left.variablesPresent(), right.variablesPresent());
        this.values = Sets.union(left.valuesPresent(), right.valuesPresent());
        this.boundVariables = Sets.union(left.boundVariablesPresent(), right.boundVariablesPresent());

        this.weight = 1 + 2 * (1 + left.getWeight() + right.getWeight());
    }

    public Formula getLeft() {
        return left;
    }

    public Formula getRight() {
        return right;
    }


    @Override
    public String toString() {
        return "(iff " + left + " " + right + ")";
    }

    @Override
    public String toSnarkString() {
        return "(iff " + left.toString() + " " + right.toSnarkString() + ")";
    }



    @Override
    public Formula generalize(Map<Value, Variable> substitution) {
        return new BiConditional(left.generalize(substitution), right.generalize(substitution));

    }
    @Override
    public boolean equals(Object o) {
        if (this == o) return true;
        if (o == null || getClass() != o.getClass()) return false;

        BiConditional that = (BiConditional) o;

        if (!left.equals(that.left)) return false;
        return right.equals(that.right);

    }

    @Override
    public int hashCode() {
        int result = safeHashCode(left);
        result = 31 * result + safeHashCode(right);
        return result;
    }

    @Override
    public Set<Formula> subFormulae() {
        return subFormulae;
    }

    @Override
    public Set<Variable> variablesPresent() {
        return variables;
    }

    @Override
    public Set<Value> valuesPresent() {
        return values;
    }

    @Override
    public Formula apply(Map<Variable, Value> substitution) {
        return new BiConditional(left.apply(substitution), right.apply(substitution));
    }

    @Override
    public Formula shadow(int level) {
        return new BiConditional(left.shadow(level), right.shadow(level));
    }

    @Override
    public Formula applyOperation(UnaryOperator<Formula> operator) {
        return new BiConditional(left.applyOperation(operator), right.applyOperation(operator));
    }

    @Override
    public int getLevel() {
        return Math.max(left.getLevel(), right.getLevel());
    }

    @Override
    public int getWeight() {
        return weight;
    }

    @Override
    public Formula replaceSubFormula(Formula oldFormula, Formula newFormula) {
        if(oldFormula.equals(this)){

            return newFormula;
        }

        if(!subFormulae().contains(oldFormula)){

            return this;
        }


        return new BiConditional(left.replaceSubFormula(oldFormula, newFormula), right.replaceSubFormula(oldFormula, newFormula));
    }

    @Override
    public Set<Variable> boundVariablesPresent() {
        return boundVariables;
    }
}
