// SPDX-FileCopyrightText: 2020 Roberto Posenato <roberto.posenato@univr.it>
//
// SPDX-License-Identifier: LGPL-3.0-or-later

package it.univr.di.labeledvalue;

import it.unimi.dsi.fastutil.ints.Int2ObjectArrayMap;
import it.unimi.dsi.fastutil.ints.IntArraySet;
import it.unimi.dsi.fastutil.ints.IntSet;
import it.unimi.dsi.fastutil.objects.*;
import it.unimi.dsi.fastutil.objects.Object2IntMap.Entry;
import it.univr.di.Debug;

import javax.annotation.Nonnull;
import java.io.Serial;
import java.util.Arrays;
import java.util.Objects;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 * Simple implementation of {@link it.univr.di.labeledvalue.LabeledIntMap} interface.
 * <p>
 * An experimental result on 2024-10-16 showed that using the base, there is a small improvement in the performance.
 * <table border="1">
 * <caption>Execution time (ms) for some operations w.r.t the core data structure of the class (Object2IntMap).</caption>
 * <tr>
 * <th>Operation</th>
 * <th>Using Object2IntOpenHashMap (ms)</th>
 * <th>Using Object2IntArrayMap (ms)</th>
 * </tr>
 * <tr>
 * <td>Creating a map of 26 elements, adding 60 elements (some entries are simplified)</td>
 * <td>0.222982625</td>
 * <td>0.08684075</td>
 * </tr>
 * <tr>
 * <td>Finding the min value</td>
 * <td>0.002990083</td>
 * <td>0.003209583</td>
 * </tr>
 * <tr>
 * <td>Retrieve the value of label abd¿f</td>
 * <td>3.9083E-5</td>
 * <td>6.6917E-5</td>
 * </tr>
 * <tr>
 * <td>Simplification after insertion of (c,11) and (¬c,11)</td>
 * <td>0.056917</td>
 * <td>0.020042</td>
 * </tr>
 * </table>
 * <b>All code for performance tests is in the ` LabeledIntTreeMapTest ` class (not publicly available).</b>
 *
 * @author Roberto Posenato
 * @version $Rev$
 * @see LabeledIntMap
 */
@SuppressWarnings({"SizeReplaceableByIsEmpty", "UnusedReturnValue"})
public class LabeledIntTreeMap extends AbstractLabeledIntMap {

	/**
	 * A read-only view of an object
	 *
	 * @author posenato
	 */
	public static class LabeledIntTreeMapView extends LabeledIntTreeMap implements LabeledIntMapView {
		/**
		 *
		 */
		@Serial
		private static final long serialVersionUID = 1L;

		/**
		 * @param inputMap input
		 */
		public LabeledIntTreeMapView(LabeledIntTreeMap inputMap) {
			mainInt2SetMap = inputMap.mainInt2SetMap;
			base = inputMap.base;
			count = inputMap.count;
		}

		/**
		 * Object Read-only. It does nothing.
		 */
		@Override
		public void putForcibly(@Nonnull Label l, int i) {
		}
	}

	/**
	 * empty base;
	 */
	static private final char[] emptyBase = new char[0];
	/**
	 * logger
	 */
	static private final Logger LOG = Logger.getLogger("LabeledIntTreeMap");
	/**
	 *
	 */
	@Serial
	static private final long serialVersionUID = 2L;

	/**
	 * @return an Object2IntMap object
	 */
	private static Int2ObjectArrayMap<Object2IntMap<Label>> makeInt2ObjectMap() {
		return new Int2ObjectArrayMap<>();
	}

	/**
	 * @return an Object2IntMap object
	 */
	private static Object2IntMap<Label> makeObject2IntMap() {
		// Object2IntRBTreeMap is better than Object2IntArrayMap when the set is larger than 5000 elements!
//		return new Object2IntArrayMap<>();
		return new Object2IntOpenHashMap<>();
//		return new Object2IntRBTreeMap(); //don't use because it loses time to order
//		return new Object2IntAVLTreeMap<>(); //don't use because it loses time to order
	}

	/**
	 * A set of propositions forming a base for the labels of the map.
	 */
	char[] base;
	/**
	 * Design choice: the set of labeled values of this map is organized as a collection of sets, each containing labels of the same length. This allows the label minimization task to be performed more systematically and efficiently. The efficiency has been proved by comparing this implementation with one in which the map has been realized with a standard map, and the minimization task determines the same length labels every time it needs them.
	 */
	Int2ObjectArrayMap<Object2IntMap<Label>> mainInt2SetMap;


	/**
	 * Constructor to clone the structure. For optimization issues, this method clones only the LabeledIntTreeMap object.
	 *
	 * @param lvm      the LabeledValueTreeMap to clone. If LVM is null, this will be an empty map.
	 * @param optimize true for having the label as short as possible, false otherwise. For example, the set {(0, ¬C), (1, C)} is represented as {(0, ⊡), (1, C)} if this parameter is true.
	 */
	LabeledIntTreeMap(final LabeledIntMap lvm, final boolean optimize) {
		this(optimize);
		if (lvm == null) {
			return;
		}
		// this.base = ((LabeledIntTreeMap) lvm).base; It is wrong to set the base before because the following puts can add base values as last values!
		// The base has to be determined during the put!
		for (final Entry<Label> entry : lvm.entrySet()) {
			put(entry.getKey(), entry.getIntValue());
		}
	}

	/**
	 * Constructor to clone the structure. For optimization issues, this method clones only the LabeledIntTreeMap object.
	 *
	 * @param lvm the LabeledValueTreeMap to clone. If LVM is null, this will be an empty map.
	 */
	LabeledIntTreeMap(final LabeledIntMap lvm) {
		this(lvm, true);
	}


	/**
	 * Necessary constructor for the factory. The internal structure is built and empty.
	 *
	 * @param optimize true for having the label as short as possible, false otherwise. For example, the set {(0, ¬C), (1, C)} is represented as {(0, ⊡), (1, C)} if this parameter is true.
	 */
	LabeledIntTreeMap(final boolean optimize) {
		mainInt2SetMap = makeInt2ObjectMap();
		base = emptyBase;
		count = 0;
		this.optimize = optimize;
	}

	/**
	 * Necessary constructor for the factory. The internal structure is built and empty.
	 */
	LabeledIntTreeMap() {
		this(true);
	}


	@Override
	public boolean alreadyRepresents(Label newLabel, int newValue) {
		final int valuePresented = get(newLabel);
		if (valuePresented > newValue) {
			return false;
		}
		if (valuePresented != Constants.INT_NULL) {
			return true;
		}
		/*
		 * Check if there is already a value in the map that represents the new value.
		 */
		final int newLabelSize = newLabel.size();

		for (final int labelLength : mainInt2SetMap.keySet()) {
			if (labelLength > newLabelSize) {
				continue;
			}
			for (final Entry<Label> entry : mainInt2SetMap.get(labelLength).object2IntEntrySet()) {
				final Label l1 = entry.getKey();
				final int v1 = entry.getIntValue();

				if (newLabel.subsumes(l1) && newValue >= v1) {
					return true;
				}
			}
		}
		return (isBaseAbleToRepresent(newLabel, newValue));
	}

	@Override
	public void clear() {
		mainInt2SetMap.clear();
		base = emptyBase;
		count = 0;
	}

	/**
	 * {@inheritDoc}
	 * <br>
	 * Up to 1000 items in the map, it is better to use this method instead of {@link #keySet()} and {@link #get(Label)} .<br>
	 * With 1000 or more items, it is better to use {@link #keySet()} approach.
	 */
	public ObjectSet<Entry<Label>> entrySet() {
		final ObjectSet<Entry<Label>> coll = new ObjectArraySet<>();
		for (final Object2IntMap<Label> mapI : mainInt2SetMap.values()) {
			coll.addAll(mapI.object2IntEntrySet());//Remember that object2IntEntrySet() is a view, so the added entries are the ones of the map.
		}
		return coll;
	}

	@Override
	public int get(final Label l) {
		if (l == null) {
			return Constants.INT_NULL;
		}
		final Object2IntMap<Label> map1 = mainInt2SetMap.get(l.size());
		if (map1 == null) {
			return Constants.INT_NULL;
		}
		return map1.getInt(l);
	}

	@Override
	public int getMaxValue() {
		int max = Constants.INT_NEG_INFINITE;
		for (final Object2IntMap<Label> mapI : mainInt2SetMap.values()) {
			for (final int j : mapI.values()) {
				if (max < j) {
					max = j;
				}
			}
		}
		return (max == Constants.INT_NEG_INFINITE) ? Constants.INT_NULL : max;
	}

	@Override
	public int getMinValue() {
		int min = Constants.INT_POS_INFINITE;
		for (final Object2IntMap<Label> mapI : mainInt2SetMap.values()) {
			for (final int j : mapI.values()) {
				if (min > j) {
					min = j;
				}
			}
		}
		return (min == Constants.INT_POS_INFINITE) ? Constants.INT_NULL : min;
	}

	@Override
	public int getMinValueSubsumedBy(final Label l) {
		if (l == null) {
			return Constants.INT_NULL;
		}
		int min = get(l);
		if (min == Constants.INT_NULL) {
			//The label does not exist, try all subsumed labels
			min = get(Label.emptyLabel);
			if (min == Constants.INT_NULL) {
				min = Constants.INT_POS_INFINITE;
			}
			int v1;
			Label l1;
			final int n = l.size();
			for (int i = 0; i < n; i++) {
				final Object2IntMap<Label> map = mainInt2SetMap.get(i);
				if (map == null) {
					continue;
				}
				for (final Entry<Label> e : map.object2IntEntrySet()) {
					l1 = e.getKey();
					if (l.subsumes(l1)) {
						v1 = e.getIntValue();
						if (min > v1) {
							min = v1;
						}
					}
				}
			}
		}
		return (min == Constants.INT_POS_INFINITE) ? Constants.INT_NULL : min;
	}

	@Override
	public ObjectSet<Label> keySet() {
		final ObjectSet<Label> coll = new ObjectArraySet<>();
		for (final Object2IntMap<Label> mapI : mainInt2SetMap.values()) {
			coll.addAll(mapI.keySet());
		}
		return coll;
	}

	@Override
	public LabeledIntTreeMap newInstance() {
		return new LabeledIntTreeMap(true);
	}

	@Override
	public LabeledIntTreeMap newInstance(boolean optimize) {
		return new LabeledIntTreeMap(optimize);
	}

	@Override
	public LabeledIntTreeMap newInstance(LabeledIntMap lim) {
		return new LabeledIntTreeMap(lim, true);
	}

	@Override
	public LabeledIntTreeMap newInstance(LabeledIntMap lim, boolean optimize) {
		return new LabeledIntTreeMap(lim, optimize);
	}

	/**
	 * {@inheritDoc}
	 * <br>
	 * <br>
	 * <b>IMPORTANT!</b><br>
	 * This implementation tries to eliminate all redundant labels. Moreover, the code is sometimes redundant, but simple to check!
	 */
	@Override
	public boolean put(final Label newLabel, int newValue) {
		if ((newLabel == null) || (newValue == Constants.INT_NULL) || alreadyRepresents(newLabel, newValue)) {
			return false;
		}
		/*
		 * Step 1.
		 * The value is not yet represented.
		 * It must be added.
		 * In the following, all values already present and implied by the new one are removed before being added.
		 * Then, the new value is added in step 2.
		 */
		removeAllValuesGreaterThan(newLabel, newValue);

		/*
		 * Step 2.
		 * Insert the new value and check if it is possible to simplify with some other labels with the same value and only one different literal.
		 */
		final Object2IntMap<Label> a = makeObject2IntMap();
		a.defaultReturnValue(Constants.INT_NULL);
		a.put(newLabel, newValue);
		return insertAndSimplify(a, newLabel.size());
	}

	/**
	 * @param l a {@link it.univr.di.labeledvalue.Label} object.
	 * @param i the new value. If it is Constants#INT_NULL, the method does nothing.
	 */
	public void putForcibly(@Nonnull final Label l, final int i) {
		if (i == Constants.INT_NULL) {
			return;
		}
		Object2IntMap<Label> map1 = mainInt2SetMap.get(l.size());
		if (map1 == null) {
			map1 = makeObject2IntMap();
			map1.defaultReturnValue(Constants.INT_NULL);
			mainInt2SetMap.put(l.size(), map1);
		}
		final int old = map1.put(l, i);
		if (old == Constants.INT_NULL) {
			count++;//'i' is a new value
		}
	}

	/**
	 * {@inheritDoc}
	 * <p>
	 * Warning!<br>
	 * Use this method not during a map scan by {@link #entrySet()}!
	 */
	@Override
	public int remove(@Nonnull final Label l) {
		final Object2IntMap<Label> map1 = mainInt2SetMap.get(l.size());
		if (map1 == null) {
			return Constants.INT_NULL;
		}
		final int oldValue = map1.removeInt(l);
		if (map1.size() == 0) {
			mainInt2SetMap.remove(l.size());
		}
		if (oldValue != Constants.INT_NULL) {// && this.optimize)
			// The base could have been changed.
			// To keep things simple, for now, it is better to rebuild everything instead of trying to rebuild a possibly damaged base.
			count--;
			if (checkValidityOfTheBaseAfterRemoving(l)) {
				final LabeledIntTreeMap newMap = new LabeledIntTreeMap(this, optimize);
				mainInt2SetMap = newMap.mainInt2SetMap;
				base = newMap.base;
			}
		}
		return oldValue;
	}

	@SuppressWarnings("ClassReferencesSubclass")
	@Override
	public LabeledIntTreeMapView unmodifiable() {
		return new LabeledIntTreeMapView(this);
	}

	@Override
	public IntSet values() {
		final IntArraySet coll = new IntArraySet();
		for (final Object2IntMap<Label> mapI : mainInt2SetMap.values()) {
			for (final Entry<Label> i : mapI.object2IntEntrySet()) {
				coll.add(i.getIntValue());
			}
		}
		return coll;
	}

	/**
	 * If the removed label {@code l} is a component of the base, then the base is reset.
	 * <p>
	 * An experiment result on 2016-01-13 showed that using the base, there is a small improvement in the performance.
	 *
	 * @param l the input label
	 *
	 * @return true if {@code l} is a component of the base, false otherwise.
	 */
	private boolean checkValidityOfTheBaseAfterRemoving(final Label l) {
		final int lSize = l.size();
		if ((base.length == 0) || (lSize == 0) || (lSize != base.length) || l.containsUnknown()) {
			return false;
		}

		// l and base have the same length.
		for (final char c : base) {
			if (!l.contains(c)) {
				return false;
			}
		}
		// l is a component of the base, and it was removed.
		base = emptyBase;
		return true;
	}

	/**
	 * Tries to add all given labeled values into the current map:
	 * <ol>
	 * <li>Given a set of labeled values to insert (all labels have the same length)
	 * <li>For each of them, it compares all same-length labels already in the map with the current one, looking for one with the same value and only one opposite literal. (This allows the simplification of the two labels with a shorter one.) In case of a positive search, shorten the current label to insert.
	 * <li>For each of the labeled values to insert (possibly updated), it removes all labeled values in the map greater than it.
	 * At each round, it tries to add labeled values of the same size.
	 * </ol>
	 *
	 * @param inputMap            contains all the elements that have to be inserted.
	 * @param inputMapLabelLength length of labels contained in inputMap
	 *
	 * @return true if any element of inputMap has been inserted into the map.
	 */
	@SuppressWarnings("LocalCanBeFinal")
	private boolean insertAndSimplify(Object2IntMap<Label> inputMap, int inputMapLabelLength) {

		final ObjectArraySet<Label> toRemove = new ObjectArraySet<>();
		boolean add = false;

		while (inputMapLabelLength >= 0) {
			// All entries of inputMap should have the label of the same size.
			// `currentMapOfLabelsWithSizeEqGivenOne` contains all the labeled values with label size = inputMapSize;
			final Object2IntMap<Label> currentMapOfLabelsWithSizeEqGivenOne = mainInt2SetMap.get(inputMapLabelLength);
			final Object2IntMap<Label> toAdd = makeObject2IntMap();
			toAdd.defaultReturnValue(Constants.INT_NULL);
			toRemove.clear();

			if (currentMapOfLabelsWithSizeEqGivenOne != null) {
				for (final Entry<Label> inputEntry : inputMap.object2IntEntrySet()) {
					final Label inputLabel = inputEntry.getKey();
					final int inputValue = inputEntry.getIntValue();

					// check if there is any labeled value with the same value and only one opposite literal.
					// 2024-10-17 To remove an entry from a Map during a map scan, it is necessary to use iterator() and iterator.remove() because it is the only way to guarantee the correct semantics.
					ObjectIterator<Entry<Label>> iterator = currentMapOfLabelsWithSizeEqGivenOne.object2IntEntrySet().iterator();
					while (iterator.hasNext()) {
						Entry<Label> entry = iterator.next();
						Label l1 = entry.getKey();
						final int v1 = entry.getIntValue();

						final Literal lit;
						// Management of two labels that differ for only one literal (one contains the straight one while the other contains the negated one).
						// Such labels can be reduced in two different ways.
						// 1) The label with the maximum value is always replaced with a labeled value where the value is the same, but the label does not contain a different literal.
						// If both have the same value, the management is equivalent to 2) the first part.
						// The disadvantage of this management is that it is quite challenging to build a base.
						// 2) If they have the same value, then they can be replaced with one only labeled value (same value) where the label does not contain the different literal.
						// If they have different values, they are ignored and, in the following, they will constitute a base for the set.
						//
						// An experimental test showed that 1) management makes the algorithm ~30% faster.
						// On 2019-03-22, I discovered that it is more important to have labels with fewer literals,
						// so Management 1 is more important!
						if (this.optimize) {
							/*
							 * Management 1)
							 */
							if ((lit = l1.getUniqueDifferentLiteral(inputLabel)) != null) {
								final int max = Math.max(inputValue, v1);
								//We can simplify (newLabel, newValue) and (v1,l1)
								//We maintain the pair with lower value while we insert the one with greater value, removing from its label 'lit'
								final Label labelWOLiteral = l1.remove(lit.getName());

								if (max == inputValue && max == v1) {
									//both values are equal, remove both
									toRemove.add(inputLabel);
									toRemove.add(l1);
									iterator.remove();
									count--;
								} else {
									if (max == inputValue) {
										toRemove.add(inputLabel);
									} else {
										toRemove.add(l1);
										iterator.remove();
										count--;
									}
								}
								toAdd.put(labelWOLiteral, max);
							}
						} else {
							/*
							 * Management 2)
							 */
							if (inputValue == v1 && (lit = l1.getUniqueDifferentLiteral(inputLabel)) != null) {
								// // we can simplify (newLabel, newValue) and (v1,l1) removing them and putting in the map (v1/lit,l1)
								toRemove.add(inputLabel);
								toRemove.add(entry.getKey());
								if (Debug.ON) {
									if (LOG.isLoggable(Level.FINEST)) {
										LOG.log(Level.FINEST, "Label %s, combined with label %s induces a simplification. Firstly, (%s, %d) in removed.".formatted(l1, inputLabel, inputLabel, inputValue));
									}
								}
								l1 = l1.remove(lit.getName());
								if (l1.size() < 0) {
									throw new IllegalStateException("There is no literal to remove, there is a problem in the code!");
								}
								if (Debug.ON) {
									if (LOG.isLoggable(Level.FINEST)) {
										LOG.log(Level.FINEST, "Then, (%s, %d) is considering for adding at the end.".formatted(l1, v1));
									}
								}
								toAdd.put(l1, v1);
							}
						}
					}
				}
				if (currentMapOfLabelsWithSizeEqGivenOne.size() == 0) {
					mainInt2SetMap.remove(inputMapLabelLength);
				}
			}
			for (final Label l : toRemove) {
				if (Debug.ON) {
					if (LOG.isLoggable(Level.FINEST)) {
						LOG.log(Level.FINEST, "Label %s is removed from the `inputMap`.".formatted(l));
					}
				}
				inputMap.removeInt(l);//safe
			}
			// The `inputMap` has been updated. Now it contains all the elements that have to be inserted.
			for (final Entry<Label> entry : inputMap.object2IntEntrySet()) {
				removeAllValuesGreaterThan(entry.getKey(), entry.getIntValue());
				if (isBaseAbleToRepresent(entry)) {
					continue;
				}
				putForcibly(entry.getKey(), entry.getIntValue());
				add = true;
				if (makeABetterBase(entry)) {
					removeAllValuesGreaterThanBase();
				}
			}
			if (toAdd.size() != 0) {
				inputMap = toAdd;
				inputMapLabelLength--;
			} else {
				inputMapLabelLength = -1;
			}
		}
		return add;
	}

	/**
	 * Determines whether any component of the base can represent the value.<br> There are the following cases:
	 * <ol>
	 * <li>A component of the base can represent the labeled value {@code (l,v)} if {@code l} subsumes the component label and the {@code v} is
	 * greater than or equal to the component value.
	 * <li>If the entry has a value that is greater than any value of the base, then the base can represent it.
	 * </ol>
	 * <p>
	 * An experiment result on 2016-01-13 showed that using the base, there is a small improvement in the performance.
	 *
	 * @param inputLabel the input label
	 * @param inputValue the input value
	 *
	 * @return true if {@code inputValue} is greater than or equal to a base component value that is subsumed by {@code inputLabel}. False otherwise.
	 */
	private boolean isBaseAbleToRepresent(final Label inputLabel, final int inputValue) {
		if (Arrays.equals(base, emptyBase)) {
			return false;
		}

		final Object2IntMap<Label> map1 = mainInt2SetMap.get(base.length);
		for (final Label baseLabel : Objects.requireNonNull(Label.allComponentsOfBaseGenerator(base))) {
			final int baseValue = map1.getInt(baseLabel);

			if (baseValue == Constants.INT_NULL) {
				if (Debug.ON) {
					if (LOG.isLoggable(Level.SEVERE)) {
						LabeledIntTreeMap.LOG.severe("The base is not sound: base=" + Arrays.toString(base) + ". Map1=" + map1);
					}
				}
				base = emptyBase;
				return false;
				// throw new IllegalStateException("A base component has a null value. It is not possible.");
			}
			if (inputLabel.subsumes(baseLabel)) {
				if (inputLabel.size() == baseLabel.size()) {
					// inputLabel subsumes all the literals of baseLabel, and it has no more literals.
					// so, they are equal or unknown.
					return true;
				}
				// entry.setValue(baseValue);// case 6
				return inputValue >= baseValue;
			}
			if (inputLabel.isConsistentWith(baseLabel)) {
				if (inputValue < baseValue) {
					return false;
				}
			}
		}
		return true;
	}

	/**
	 * @param entry the entry
	 *
	 * @return true if {@code inputValue} is greater than or equal to a base component value that is subsumed by {@code inputLabel}. False otherwise.
	 *
	 * @see #isBaseAbleToRepresent(Label, int)
	 */
	private boolean isBaseAbleToRepresent(final Entry<Label> entry) {
		return isBaseAbleToRepresent(entry.getKey(), entry.getIntValue());
	}

	/**
	 * If entry (label, value) determines a new (better) base, the base is updated.<br> An experiment result on 2016-01-13 showed that using base there is a small improvement in the performance.
	 *
	 * @param entry the entry
	 *
	 * @return true if (label, value) determines a new (better) base. If true, the base is updated. False otherwise.
	 */
	private boolean makeABetterBase(final Entry<Label> entry) {
		if (entry.getIntValue() == Constants.INT_NULL) {
			return false;
		}

		final int n = entry.getKey().size();

		if (n == 0) {
			// The new labeled value (l,v) has a universal label; the base is not necessary!
			base = emptyBase;
			return true;
		}
		final Object2IntMap<Label> map1 = mainInt2SetMap.get(n);
		if (map1.size() < Math.pow(2.0, n)) // there are no enough elements!
		{
			return false;
		}
		final char[] baseCandidateColl = entry.getKey().getPropositions();
		for (final Label label1 : Objects.requireNonNull(Label.allComponentsOfBaseGenerator(baseCandidateColl))) {
			final int value = map1.getInt(label1);
			if (value == Constants.INT_NULL) {
				return false;
			}
		}
		base = baseCandidateColl;
		return true;
	}

	/**
	 * Remove all labeled values that subsume {@code l} and have values greater or equal to {@code i}.
	 *
	 * @param givenLabel the input label
	 * @param givenValue the new value
	 *
	 * @return true if at least one element has been removed, false otherwise.
	 */
	private boolean removeAllValuesGreaterThan(final Label givenLabel, final int givenValue) {
		if (givenLabel == null || givenValue == Constants.INT_NULL) {
			return false;
		}
		boolean removed = false;
		final int inputLabelSize = givenLabel.size();
		//since this.mainInt2SetMap can change during the cycle, its aLabelSet must be stored at the start (see note below).
		final IntSet labelLengthSet = new IntArraySet(mainInt2SetMap.keySet());
		for (final int labelLength : labelLengthSet) {
			if (labelLength < inputLabelSize) {
				continue;
			}
			final Object2IntMap<Label> internalMap = mainInt2SetMap.get(labelLength);
			//BE CAREFUL!
			//Since it is necessary to remove (label and map), it is not possible to use internalMap.aLabelSet() directly because removing an element in the map changes the key set, and it is possible to lose the checking of some label (the following one after a deleted element).
			//Iterators are not rightly implemented as of 2019-03-30!
			//The last resource is to copy the labeled value set.
			//2024-10-17: It seems that the iterator now works!
//			final ObjectList<Label> labelsOfInternalMap = new ObjectArrayList<>(internalMap.aLabelSet());
//			for (final Label currentLabel : labelsOfInternalMap) {
//				final int currentValue = internalMap.getInt(currentLabel);
			final ObjectIterator<Entry<Label>> iterator = internalMap.object2IntEntrySet().iterator();
			while (iterator.hasNext()) {
				final Entry<Label> entry = iterator.next();
				final Label currentLabel = entry.getKey();
				final int currentValue = entry.getIntValue();

				if ((currentValue >= givenValue) && currentLabel.subsumes(givenLabel)) {
					if (Debug.ON) {
						if (LOG.isLoggable(Level.FINEST)) {
							LOG.log(Level.FINEST, "New label " + givenLabel + " induces a remove of (" + currentLabel + ", " + currentValue + ")");
						}
					}
//					internalMap.removeInt(currentLabel);
					iterator.remove();
					count--;
					removed = true;
					checkValidityOfTheBaseAfterRemoving(currentLabel);
				}
			}
			if (internalMap.size() == 0) {//remove from the mainInt2SetMap
				mainInt2SetMap.remove(labelLength);
			}
		}
		return removed;
	}

	/**
	 * Remove all labeled values with each value greater than all values of base components consistent with it. An experiment result on 2016-01-13 showed that using the base, there is a small improvement in the performance.
	 *
	 * @return true if at least one element has been removed, false otherwise.
	 */
	private boolean removeAllValuesGreaterThanBase() {
		if ((base == null) || (base.length == 0)) {
			return false;
		}
		final LabeledIntTreeMap newMap = new LabeledIntTreeMap(optimize);
		// build the list of labeled values that form the base
		final ObjectArrayList<Entry<Label>> baseComponent = new ObjectArrayList<>((int) Math.pow(2, base.length));
		for (final Label l : Objects.requireNonNull(Label.allComponentsOfBaseGenerator(base))) {
			baseComponent.add(new AbstractObject2IntMap.BasicEntry<>(l, get(l)));
		}
		Label l1, lb;
		int v1, vb;
		boolean toInsert;
		for (final Object2IntMap<Label> map1 : mainInt2SetMap.values()) {
			for (final Entry<Label> entry : map1.object2IntEntrySet()) {
				l1 = entry.getKey();
				v1 = entry.getIntValue();
				toInsert = false;

				for (final Entry<Label> baseEntry : baseComponent) {
					lb = baseEntry.getKey();
					vb = baseEntry.getIntValue();
					if (l1.equals(lb)) {
						toInsert = true; // a base component always has to be inserted!
						break;
					}
					if (l1.isConsistentWith(lb) && v1 < vb) {// isConsistent is necessary to manage cases like base =
						// {(b,3)(¬b,4)} l1={(a,1)}
						toInsert = true;
						break;
					}
				}
				if (toInsert) {
					newMap.putForcibly(l1, v1);
				}
			}
		}
		if (!newMap.equals(this)) {
			if (Debug.ON) {
				if (LOG.isLoggable(Level.FINEST)) {
					LOG.finest("Base changed: the old map " + this + " is substituted by " + newMap);
				}
			}
			mainInt2SetMap = newMap.mainInt2SetMap;
			count = newMap.count;
			return true;
		}
		return false;
	}

}