package net.ssehub.kernel_haven.util.logic;

import static net.ssehub.kernel_haven.util.null_checks.NullHelpers.notNull;

import java.util.ArrayDeque;
import java.util.HashSet;
import java.util.Queue;
import java.util.Set;
import java.util.function.Function;

import net.ssehub.kernel_haven.util.Logger;
import net.ssehub.kernel_haven.util.null_checks.NonNull;
import net.ssehub.kernel_haven.util.null_checks.Nullable;

/**
 * Queue to create balanced (and simplified) {@link Disjunction} terms. <br/>
 * Supported simplification optimizations:
 * <ul>
 * <li>Won't store any new formulas if it stores already an {@link True}</li>
 * <li>Won't store {@link Formula}s twice</li>
 * <li>Won't store a {@link False}</li>
 * </ul>
 * @author El-Sharkawy
 *
 */
public class DisjunctionQueue {
    
    private static final Logger LOGGER = Logger.get();
    
    private Queue<@NonNull Formula> queue = new ArrayDeque<>();
    private boolean isTrue = false;
    private Set<Formula> conditions = new HashSet<>();
    private boolean simplify;
    private Function<@NonNull Formula, @NonNull Formula> simplifier;
    
    /**
     * Allows to specify if the above mentioned simplification rules shall be applied, won't use a simplifier for
     * further simplifications of the result.
     * @param simplify Specification if the rules from the class comment shall be applied.
     * @see #DisjunctionQueue(boolean, Function)
     */
    public DisjunctionQueue(boolean simplify) {
        this(simplify, null);
    }
    
    /**
     * Will turn all simplifications on and use the specified <tt>simplifier</tt> to simplify the results of this
     * queue.
     * @param simplifier A function specifying how {@link Formula}s can be further simplified. Probably use:
     * <pre><code>f -> LogicUtils.simplify(f)</code></pre>
     * @see #DisjunctionQueue(boolean, Function)
     */
    public DisjunctionQueue(Function<@NonNull Formula, @NonNull Formula> simplifier) {
        this(true, simplifier);
    }
    
    /**
     * Allows specify a <tt>simplifier</tt> to be used on the final results as well as to specify if simplifications
     * should be applied at all.
     * @param simplify Specification if the rules from the class comment shall be applied.
     * @param simplifier A function specifying how {@link Formula}s can be further simplified (will be ignored if
     *     <tt>simplifier = false</tt>). Probably use:
     * <pre><code>f -> LogicUtils.simplify(f)</code></pre>
     */
    public DisjunctionQueue(boolean simplify, Function<@NonNull Formula, @NonNull Formula> simplifier) {
        this.simplify = simplify;
        this.simplifier = this.simplify ? simplifier : null;
    }
    
    /**
     * Adds a new formula to the queue.
     * @param condition The formula to add (<tt>null</tt> will be ignored).
     */
    public void add(@Nullable Formula condition) {
        if (null != condition) {
            if (simplify) {
                // Default case: Avoid doubled formulas and handle TRUE/FALSE literals
                if (!isTrue && !conditions.contains(condition) && !(condition instanceof False)) {
                    if (condition instanceof True) {
                        isTrue = true;
                    } else {
                        conditions.add(condition);
                        queue.add(condition);
                    }
                }
            } else {
                // No optimization
                queue.add(condition);
            }
        }
    }
    
    /**
     * Creates one disjunction term based on the elements passed to the queue. This will also clear all contents from
     * this queue.
     * @return The disjunction, maybe {@link True} if one of the passed elements was {@link True},
     *     never be <tt>null</tt>.
     * @see #getDisjunction(String)
     */
    public @NonNull Formula getDisjunction() {
        return getDisjunction(null);
    }
    
    /**
     * Creates one disjunction term based on the elements passed to the queue. This will also clear all contents from
     * this queue.
     * @param varName Optional: The name of the variable for which the disjunction is currently be created, this is only
     *     used to create an error log in case of an error.
     * @return The disjunction, maybe {@link True} if one of the passed elements was {@link True},
     *     never be <tt>null</tt>.
     */
    public @NonNull Formula getDisjunction(@Nullable String varName) {
        @NonNull Formula result;
        
        // Create disjunction of all elements
        if (isTrue || queue.isEmpty()) {
            result = True.INSTANCE;
        } else {
            // Try to create a balanced, flat tree
            while (queue.size() > 1) {
                queue.add(new Disjunction(queue.poll(), queue.poll()));
            }
            result = notNull(queue.poll()); // this can't be null, since queue.size()==1
            
            // Simplification if wished and if possible
            if (null != simplifier) {
                result = notNull(simplifier.apply(result));
            }
            
            // Check if all elements have been processed
            if (!queue.isEmpty()) {
                if (null != varName) {
                    LOGGER.logError("Error while creating disjunction for conditions of " + varName);
                } else {
                    LOGGER.logError("Error while creating disjunction.");
                }
            }
        }
        
        // Reset
        queue.clear();
        conditions.clear();
        isTrue = false;
        
        return result;
    }
}

@@ -791,23 +791,85 @@
    %0A    
-priva
+/**%0A     * The global singleton %7B@link Logger%7D.%0A     */%0A    protec
 te
+d
  static 
@@ -913,23 +913,233 @@
    %0A    
-private
+/**%0A     * Whether a %7B@link True%7D element was %7B@link #add(Formula)%7Ded.%0A     */%0A    protected boolean isTrue = false;%0A    %0A    /**%0A     * The queue containing the %7B@link #add(Formula)%7Ded formulas.%0A     */%0A    protected
  Queue%3C@
@@ -1191,39 +1191,8 @@
     
-private boolean isTrue = false;
 %0A   
@@ -3893,32 +3893,40 @@
   * this queue.%0A
+     * %0A
      * @return T
@@ -4000,32 +4000,32 @@
 s %7B@link True%7D,%0A
-
      *     never
@@ -4319,32 +4319,40 @@
   * this queue.%0A
+     * %0A
      * @param va
@@ -4737,25 +4737,16 @@
         
-@NonNull 
 Formula 
@@ -5762,16 +5762,234 @@
 / Reset%0A
+        reset();%0A        %0A        return result;%0A    %7D%0A    %0A    /**%0A     * Resets this %7B@link DisjunctionQueue%7D. After this, the queue is in the same state as if it was newly created.%0A     */%0A    public void reset() %7B%0A
         
@@ -6063,40 +6063,13 @@
     
+%7D%0A
     
-%0A        return result;%0A    %7D
 %0A%7D%0A

Make DisjunctionQueue more inheritable