/*  __    __  __  __    __  ___
 * \  \  /  /    \  \  /  /  __/
 *  \  \/  /  /\  \  \/  /  /
 *   \____/__/  \__\____/__/
 *
 * Copyright 2014-2017 Vavr, http://vavr.io
 *
 * 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 ch.usi.inf.sdm.sdm04.util;

import ch.usi.si.codelounge.jsicko.Contract;

import java.util.Arrays;
import java.util.BitSet;
import java.util.function.Supplier;
import java.util.stream.IntStream;

import static ch.usi.si.codelounge.jsicko.Contract.old;


@SuppressWarnings("unused") // methods used by jSicko
public interface FluentBitSetContracts extends FluentBitSetContractsContracts, Contract {

    @Pure
    boolean intersects(final FluentBitSet set);

    @Pure
    int cardinality();

    @Pure
    BitSet bitSet();

    @Pure
    int length();

    @Pure
    boolean get(final int bitIndex);

    @Pure
    default boolean test_cardinality(final FluentBitSet returns, final boolean oldShouldBeGreater) {
        return old(this).cardinality() == this.cardinality() ||
                oldShouldBeGreater == old(this).cardinality() > this.cardinality();
    }

    @Pure
    @Requires("cardinality_positive")
    default boolean test_lesser_cardinality(final FluentBitSet returns, final long cardinality) {
        return returns.cardinality() == (old(this).cardinality() - cardinality);
    }

    @Pure
    default boolean test_length(final FluentBitSet returns, final Supplier<Integer> paramLength) {
        return old(this).length() >= this.length() || paramLength.get() >= this.length();
    }

    @Pure
    default boolean and_fbs(final FluentBitSet returns, final FluentBitSet set) {
        return test_cardinality(returns, true) && test_length(returns, set::length);
    }

    @Pure
    default boolean or_fbs(final FluentBitSet returns, final FluentBitSet set) {
        return test_cardinality(returns, false) && test_length(returns, set::length);
    }
    @Pure
    default boolean xor_fbs(final FluentBitSet returns, final BitSet set) {
        int card1 = old(this).cardinality();
        int card2 = set.cardinality();
        //System.err.println("card1: "+card1);
        //System.err.println("card2: "+card2);
        //System.err.println("this.card: "+this.cardinality());
        final boolean bool;
        // example 1 test: (1st bit stream).card()=(1st bit stream).card() = 8, this.card()=0, this.len() = 8
        if(card1+card2>this.length()){
            bool = (card1 + card2 -this.length()) >=this.cardinality();// (8+8 - 8)>=0
            return (bool) && test_length(returns, set::length);
        }
        else{
            // example 2 test: (1st bit stream).card()= 0, (1st bit stream).card() = 8, this.card()=8, this.len() = 8
             return (card1+card2) >=this.cardinality(); // (8+0)>=8
        }
    }
    @Pure
    default boolean set_not_negative_input(final int ...bitIndexArray) {
        return Arrays.stream(bitIndexArray).allMatch(p -> p >= 0 || p <(this).length() );
    }
    @Pure
    default boolean set_(final FluentBitSet returns, final int ...bitIndexArray) {
        int len = bitIndexArray.length;
        for(final int i: bitIndexArray){
            if(i<0 || i>=returns.length()){
                len--;
            }
        }
        //System.err.println("array: "+ Arrays.toString(bitIndexArray));
        //System.err.println("len array: "+len);
        return (old(this).cardinality()+len) >= this.cardinality();

    }

    @Pure
    default boolean and_not_fbs(final FluentBitSet returns, final FluentBitSet set) {
        final FluentBitSet notSet = new FluentBitSet(set.bitSet()).flip(0, set.length());
        return test_cardinality(returns, true) && test_length(returns, notSet::length);
    }

    @Pure
    default boolean and_not_bs(final FluentBitSet returns, final BitSet set) {
        final FluentBitSet notSet = new FluentBitSet(set).flip(0, set.length());
        return test_cardinality(returns, true) && test_length(returns, notSet::length);
    }

    @Pure
    default boolean and_bs(final FluentBitSet returns, final BitSet set) {
        return test_cardinality(returns, true) && test_length(returns, set::length);
    }

    @Pure
    default boolean or_bs_array(final FluentBitSet returns, final FluentBitSet... set) {
        final FluentBitSet results = new FluentBitSet(old(this).bitSet());

        for (final FluentBitSet s : set) {
            results.or(s);
            if (!or_bs(results, s.bitSet())) {
                return false;
            }
        }

        return results.equals(returns);
    }

    @Pure
    default boolean or_bs(final FluentBitSet returns, final BitSet set) {
        return test_cardinality(returns, false) && test_length(returns, set::length);
    }


    @Pure
    default boolean clear_void(final FluentBitSet returns) {
        return cardinality() == 0;
    }

    @Pure
    default boolean clear_int(final FluentBitSet returns, final int bitIndex) {
        return test_lesser_cardinality(returns, old(this).get(bitIndex) ? 1 : 0);
    }

    @Pure
    default boolean clear_int_int(final FluentBitSet returns, final int fromIndex, final int toIndex) {
        return test_lesser_cardinality(returns, IntStream.range(fromIndex, toIndex)
                .filter(old(this)::get)
                .count());
    }

    @Pure
    default boolean is_empty(final boolean returns) {
        return returns == (cardinality() == 0) && returns == (length() == 0);
    }

    @Pure
    default boolean get_int(final int bitIndex) {
        return bitIndex >= 0;
    }

    @Pure
    default boolean valid_indexes(final int ...bitIndexArray) {
        return IntStream.of(bitIndexArray).allMatch(this::get_int);
    }

    @Pure
    default boolean get_int_range_pre(final int fromIndex, final int toIndex) {
        return 0 <= fromIndex && fromIndex <= toIndex;
    }

    @Pure
    default boolean get_int_range(final FluentBitSet returns, final int fromIndex, final int toIndex) {
        return IntStream.range(fromIndex, toIndex).allMatch(i -> this.get(i) == returns.get(i - fromIndex));
    }

    @Pure
    default boolean flip_int(final FluentBitSet returns, final int bitIndex) {
        return returns.get(bitIndex) != old(this).get(bitIndex);
    }

    @Pure
    default boolean flip_int_range(final FluentBitSet returns, final int fromIndex, final int toIndex) {
        return IntStream.range(fromIndex, toIndex).allMatch(i -> this.flip_int(returns, i));
    }

    @Pure
    default boolean intersects_bs(final boolean returns, final BitSet set) {
        return returns == set.intersects(this.bitSet());
    }

    @Pure
    default boolean intersects_fbs(final boolean returns, final FluentBitSet set) {
        return intersects_bs(returns, set.bitSet());
    }
    @Pure
    default boolean nice_range_next_previous_SetBit_post(int returns, final int fromIndex) {



         //  we return an index that is in the range [0, len),
        return (-1<= returns  && returns<this.length());// -1 if we do not find it or findIndex is out of bound
    }
    @Pure
    default boolean nice_range_next_previous_ClearBit_post(int returns, final int fromIndex) {
        if(fromIndex>=-1){ //if fromIndex is equal to -1 or greater, than the result will be -1(if index not found) or the index itself
            return (-1<= returns);
        }
        else{
            return false; // an exception is thrown
        }
    }
}