"use strict";
Object.defineProperty(exports, "__esModule", { value: true });
exports.cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolverWrapper = exports.SatSolverWrapper = void 0;
const JavaObject_1 = require("../../../java/lang/JavaObject");
const SatSolverA_1 = require("../../../core/kursblockung/satsolver/SatSolverA");
const LinkedCollection_1 = require("../../../core/adt/collection/LinkedCollection");
class SatSolverWrapper extends SatSolverA_1.SatSolverA {
    _solver;
    varFALSE;
    varTRUE;
    /**
     * Erstellt eine Ebene über dem {@link SatSolverA}, um verschiedene Bedingungen/Constraints als Klauseln zu
     * codieren.
     *
     * @param solver Der Solver, der intern verwendet wird.
     */
    constructor(solver) {
        super();
        this._solver = solver;
        this.varTRUE = this._solver.createNewVar();
        this.varFALSE = -this.varTRUE;
        this.c_1(this.varTRUE);
    }
    createNewVar() {
        return this._solver.createNewVar();
    }
    addClause(pVars) {
        this._solver.addClause(pVars);
    }
    isVarTrue(pVar) {
        return this._solver.isVarTrue(pVar);
    }
    solve(maxTimeMillis) {
        return this._solver.solve(maxTimeMillis);
    }
    getVarCount() {
        return this._solver.getVarCount();
    }
    getClauseCount() {
        return this._solver.getClauseCount();
    }
    /**
     * Liefert ein Array der Länge n mit neu erzeugten Variablennummern.
     *
     * @param n Die Länge des Arrays.
     *
     * @return Ein Array der Länge n mit neu erzeugten Variablennummern.
     */
    createNewVars(n) {
        let temp = Array(n).fill(0);
        for (let i = 0; i < temp.length; i++) {
            temp[i] = this._solver.createNewVar();
        }
        return temp;
    }
    /**
     * Liefert eine Variable, die zuvor auf FALSE forciert wurde.
     *
     * @return Eine Variable, die zuvor auf FALSE forciert wurde.
     */
    getVarFALSE() {
        return this.varFALSE;
    }
    /**
     * Liefert eine Variable, die zuvor auf TRUE forciert wurde.
     *
     * @return Eine Variable, die zuvor auf TRUE forciert wurde.
     */
    getVarTRUE() {
        return this.varTRUE;
    }
    /**
     * Fügt eine Klausel der Größe 1 hinzu. Forciert damit die übergebene Variable auf TRUE.
     *
     * @param x Die Variable wird auf TRUE gesetzt.
     */
    c_1(x) {
        this._solver.addClause([x]);
    }
    /**
     * Fügt eine Klausel der Größe 2 hinzu. Forciert damit, dass mindestens eine der beiden Variablen TRUE ist,
     * letzlich @code{x + y >= 1}.
     *
     * @param x Die Variable x der Klausel (x OR y).
     * @param y Die Variable y der Klausel (x OR y).
     */
    c_2(x, y) {
        this._solver.addClause([x, y]);
    }
    /**
     * Fügt eine Klausel der Größe 3 hinzu. Forciert damit, dass mindestens eine der drei Variablen TRUE ist,
     * letzlich @code{x + y + z >= 1}.
     *
     * @param x Die Variable x der Klausel (x OR y OR z).
     * @param y Die Variable y der Klausel (x OR y OR z).
     * @param z Die Variable z der Klausel (x OR y OR z).
     */
    c_3(x, y, z) {
        this._solver.addClause([x, y, z]);
    }
    /**
     * Forciert, dass nicht beide Variablen TRUE sind, letzlich @code{x + y ≤ 1}.
     *
     * @param x Die Variable x der Klausel (-x OR -y).
     * @param y Die Variable y der Klausel (-x OR -y).
     */
    c_not_both(x, y) {
        this.c_2(-x, -y);
    }
    /**
     * Liefert die Variable z für die {@code z = x AND y} gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     *
     * @return Die Variable z für die {@code z = x AND y} gilt.
     */
    c_new_var_AND(x, y) {
        let c = this._solver.createNewVar();
        this.c_2(x, -c);
        this.c_2(y, -c);
        this.c_3(-x, -y, c);
        return c;
    }
    /**
     * Implementation for method overloads of 'c_exactly_GENERIC'
     */
    c_exactly_GENERIC(__param0, __param1) {
        if (((typeof __param0 !== "undefined") && Array.isArray(__param0)) && ((typeof __param1 !== "undefined") && typeof __param1 === "number")) {
            let pArray = __param0;
            let amount = __param1;
            this.c_exactly_GENERIC(SatSolverWrapper.toList(pArray), amount);
        }
        else if (((typeof __param0 !== "undefined") && ((__param0 instanceof JavaObject_1.JavaObject) && (__param0.isTranspiledInstanceOf('de.nrw.schule.svws.core.adt.collection.LinkedCollection'))) || (__param0 === null)) && ((typeof __param1 !== "undefined") && typeof __param1 === "number")) {
            let list = (0, LinkedCollection_1.cast_de_nrw_schule_svws_core_adt_collection_LinkedCollection)(__param0);
            let amount = __param1;
            list = new LinkedCollection_1.LinkedCollection(list);
            if (amount > list.size()) {
                console.log(JSON.stringify("FEHLER: c_exactly_GENERIC --> amount > list.size()"));
            }
            if (amount === 0) {
                for (let x of list) {
                    this.c_1(-x);
                }
                return;
            }
            if (amount === list.size()) {
                for (let x of list) {
                    this.c_1(+x);
                }
                return;
            }
            if (amount === 1) {
                if (list.size() === 1) {
                    this.c_1(list.getFirst().valueOf());
                    return;
                }
                if (list.size() === 2) {
                    this.c_unequal(list.getFirst().valueOf(), list.getLast().valueOf());
                    return;
                }
                this.c_exactly_one(list);
                return;
            }
            this.c_exactly_NETWORK(list, amount);
        }
        else
            throw new Error('invalid method overload');
    }
    /**
     * Forciert, dass höchstens {@code maximum} Variablen der Variablenliste den Wert TRUE haben.
     *
     * @param list    Die Variablenliste.
     * @param maximum Die maximale Anzahl an TRUEs in der Variablenliste.
     */
    c_at_most_GENERIC(list, maximum) {
        list = new LinkedCollection_1.LinkedCollection(list);
        if (maximum >= list.size()) {
            return;
        }
        if (maximum === 0) {
            for (let x of list) {
                this.c_1(-x);
            }
            return;
        }
        if (maximum === 1) {
            this.c_at_most_one_tree(list);
            return;
        }
        this.c_at_most_NETWORK(list, maximum);
    }
    /**
     * Forciert, dass genau eine Variable der Liste TRUE ist. Falls die Liste leer ist, führt das zur direkten
     * Unlösbarkeit der Formel.
     *
     * @param list Genau eine der Variablen der Liste muss TRUE sein.
     */
    c_exactly_one(list) {
        this.c_1(this.c_at_most_one_tree(list));
    }
    /**
     * Forciert, dass {@code z = x OR y} gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     * @param z Variable der obigen Gleichung.
     */
    c_z_equals_x_or_y(x, y, z) {
        this.c_2(-x, z);
        this.c_2(-y, z);
        this.c_3(x, y, -z);
    }
    /**
     * Liefert die Variable z für die {@code z = x OR y} gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     *
     * @return Die Variable z für die {@code z = x OR y} gilt.
     */
    c_new_var_OR(x, y) {
        let z = this._solver.createNewVar();
        this.c_2(-x, z);
        this.c_2(-y, z);
        this.c_3(x, y, -z);
        return z;
    }
    /**
     * Forciert, dass in der Liste maximal eine Variable TRUE ist. Die Ergebnisvariable ist eine OR-Verknüpfung
     * aller Variablen der Liste.
     *
     * @param list Forciert, dass maximal eine Variable der Liste TRUE ist.
     *
     * @return Die Ergebnisvariable ist eine OR-Verknüpfung aller Variablen der Liste.
     */
    c_at_most_one_tree(list) {
        list = new LinkedCollection_1.LinkedCollection(list);
        if (list.isEmpty()) {
            list.add(this.varFALSE);
        }
        while (list.size() >= 2) {
            let a = list.removeFirst().valueOf();
            let b = list.removeFirst().valueOf();
            let c = this._solver.createNewVar();
            this.c_not_both(a, b);
            this.c_z_equals_x_or_y(a, b, c);
            list.add(c);
        }
        return list.removeFirst().valueOf();
    }
    c_exactly_NETWORK(list, amount) {
        this.c_bitonic_sort(list);
        let i = 0;
        let iter = list.iterator();
        while (iter.hasNext()) {
            let value = iter.next();
            if (i < amount) {
                this.c_1(+value.valueOf());
            }
            else {
                this.c_1(-value.valueOf());
            }
            i++;
        }
    }
    c_at_most_NETWORK(list, maximum) {
        this.c_bitonic_sort(list);
        let i = 0;
        let iter = list.iterator();
        while (iter.hasNext()) {
            let value = iter.next();
            if (i < maximum)
                i++;
            else
                this.c_1(-value.valueOf());
        }
    }
    c_bitonic_sort(list) {
        this.c_fill_False_until_power_two(list);
        this.c_bitonic_sort_power_two(list);
    }
    c_fill_False_until_power_two(list) {
        let size = 1;
        while (size < list.size()) {
            size *= 2;
        }
        while (list.size() < size) {
            list.addLast(this.varFALSE);
        }
    }
    c_bitonic_sort_power_two(list) {
        for (let window = 2; window <= list.size(); window *= 2) {
            this.c_bitonic_sort_spiral(list, window);
            for (let difference = Math.trunc(window / 2); difference >= 2; difference /= 2) {
                this.c_bitonic_sort_difference(list, difference);
            }
        }
    }
    c_bitonic_sort_spiral(list, size) {
        for (let i = 0; i < list.size(); i += size) {
            for (let i1 = i, i2 = i + size - 1; i1 < i2; i1++, i2--) {
                this.c_bitonic_comparator(list, i1, i2);
            }
        }
    }
    c_bitonic_sort_difference(list, size) {
        let half = Math.trunc(size / 2);
        for (let i = 0; i < list.size(); i += size) {
            for (let j = 0; j < half; j++) {
                this.c_bitonic_comparator(list, i + j, i + j + half);
            }
        }
    }
    c_bitonic_comparator(result, i1, i2) {
        if (i1 >= i2) {
            console.log(JSON.stringify("c_bitonic_comparator: " + i1 + "," + i2 + " <-- ERROR!!!"));
        }
        let a = result.get(i1).valueOf();
        let b = result.get(i2).valueOf();
        result.set(i1, this.c_new_var_OR(a, b));
        result.set(i2, this.c_new_var_AND(a, b));
    }
    static toList(pArray) {
        let list = new LinkedCollection_1.LinkedCollection();
        for (let x of pArray) {
            list.addLast(x);
        }
        return list;
    }
    c_unequal(x, y) {
        this.c_equal(x, -y);
    }
    c_equal(x, y) {
        this.c_2(-x, +y);
        this.c_2(+x, -y);
    }
    isTranspiledInstanceOf(name) {
        return ['de.nrw.schule.svws.core.kursblockung.satsolver.SatSolverA', 'de.nrw.schule.svws.core.kursblockung.satsolver.SatSolverWrapper'].includes(name);
    }
}
exports.SatSolverWrapper = SatSolverWrapper;
function cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolverWrapper(obj) {
    return obj;
}
exports.cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolverWrapper = cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolverWrapper;
//# sourceMappingURL=SatSolverWrapper.js.map