"use strict";
Object.defineProperty(exports, "__esModule", { value: true });
exports.cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver = exports.KursblockungAlgorithmusKSatSolver = void 0;
const SatSolver3_1 = require("../../core/kursblockung/satsolver/SatSolver3");
const HashMap_1 = require("../../java/util/HashMap");
const SatSolverWrapper_1 = require("../../core/kursblockung/satsolver/SatSolverWrapper");
const LinkedCollection_1 = require("../../core/adt/collection/LinkedCollection");
const System_1 = require("../../java/lang/System");
const SatSolverA_1 = require("../../core/kursblockung/satsolver/SatSolverA");
const NullPointerException_1 = require("../../java/lang/NullPointerException");
const KursblockungAlgorithmusK_1 = require("../../core/kursblockung/KursblockungAlgorithmusK");
class KursblockungAlgorithmusKSatSolver extends KursblockungAlgorithmusK_1.KursblockungAlgorithmusK {
    kurseAlle;
    schuelerAlle;
    maxNichtWaehler = 0;
    /**
     * Im Konstruktor kann die Klasse die jeweiligen Datenstrukturen aufbauen. Kurse
     * dürfen in diese Methode noch nicht auf Schienen verteilt werden.
     *
     * @param logger Logger für Benutzerhinweise, Warnungen und Fehler.
     * @param dynDat Die dynamischen Blockungsdaten.
     */
    constructor(logger, dynDat) {
        super(logger, dynDat);
        this.kurseAlle = dynDat.gibKurseAlle();
        this.schuelerAlle = this.dynDaten.gibSchuelerArray(false);
        this.maxNichtWaehler = 10;
    }
    berechne(pMaxTimeMillis) {
        if (this.dynDaten.gibKurseDieFreiSindAnzahl() === 0) {
            return;
        }
        let timeStart = System_1.System.currentTimeMillis();
        this.dynDaten.aktionSchuelerAusAllenKursenEntfernen();
        this.dynDaten.aktionKurseFreieZufaelligVerteilen();
        this.dynDaten.aktionZustandSpeichernK();
        let difNichtWaehler = 1;
        while (System_1.System.currentTimeMillis() - timeStart < pMaxTimeMillis) {
            let result = this.berechneSchritt(pMaxTimeMillis);
            if (result === SatSolverA_1.SatSolverA.RESULT_UNKNOWN) {
                return;
            }
            if (result === SatSolverA_1.SatSolverA.RESULT_SATISFIABLE) {
                this.maxNichtWaehler = Math.max(this.maxNichtWaehler - difNichtWaehler, 0);
                continue;
            }
            this.maxNichtWaehler++;
            difNichtWaehler = 0;
        }
    }
    /**
     * Erzeugt eine Formel in konjuntiver Normalform (CNF) und übergibt sie dem
     * SAT-Solver. Der Solver versucht die Formel innerhalb des Zeitlimits zu lösen.
     * Falls er es nicht schafft, dann wurde zuvor eine zufällige Kursverteilung
     * definiert. #
     *
     * @param pMaxTimeMillis Die maximale Blockungszeit in Millisekunde.
     *
     * @return Liefert eines der drei möglichen Ergebnisse
     *         {@link SatSolverA#RESULT_SATISFIABLE oder SatSolverI#RESULT_UNKNOWN
     *         oder SatSolverI#RESULT_UNSATISFIABLE. }
     */
    berechneSchritt(pMaxTimeMillis) {
        let ssw = new SatSolverWrapper_1.SatSolverWrapper(new SatSolver3_1.SatSolver3());
        let nSchienen = this.dynDaten.gibSchienenAnzahl();
        let mapKursSchiene = new HashMap_1.HashMap();
        for (let kurs of this.kurseAlle) {
            let schienen = Array(nSchienen).fill(0);
            for (let s = 0; s < nSchienen; s++) {
                schienen[s] = kurs.gibIstSchieneFixiert(s) ? ssw.getVarTRUE() : kurs.gibIstSchieneGesperrt(s) ? ssw.getVarFALSE() : ssw.createNewVar();
            }
            mapKursSchiene.put(kurs, schienen);
        }
        let mapSchuelerFachartNichtwahl = new HashMap_1.HashMap();
        let mapSchuelerIstInKurs = new HashMap_1.HashMap();
        let listNichtwahlen = new LinkedCollection_1.LinkedCollection();
        for (let schueler of this.schuelerAlle) {
            mapSchuelerFachartNichtwahl.put(schueler, new HashMap_1.HashMap());
            mapSchuelerIstInKurs.put(schueler, new HashMap_1.HashMap());
            for (let fachart of schueler.gibFacharten()) {
                let varNichtwahlen = ssw.createNewVar();
                let mapFachartNichtwahl = mapSchuelerFachartNichtwahl.get(schueler);
                if (mapFachartNichtwahl === null)
                    throw new NullPointerException_1.NullPointerException();
                mapFachartNichtwahl.put(fachart, varNichtwahlen);
                listNichtwahlen.add(varNichtwahlen);
                for (let kurs of fachart.gibKurse()) {
                    let varKurs = ssw.createNewVar();
                    let mapIstInKurs = mapSchuelerIstInKurs.get(schueler);
                    if (mapIstInKurs === null)
                        throw new NullPointerException_1.NullPointerException();
                    mapIstInKurs.put(kurs, varKurs);
                }
            }
        }
        for (let kurs of this.kurseAlle) {
            let list = new LinkedCollection_1.LinkedCollection();
            let schienen = mapKursSchiene.get(kurs);
            if (schienen === null)
                throw new NullPointerException_1.NullPointerException();
            for (let s = 0; s < nSchienen; s++) {
                list.add(schienen[s]);
            }
            let amount = kurs.gibSchienenAnzahl();
            ssw.c_exactly_GENERIC(list, amount);
        }
        for (let schueler of this.schuelerAlle) {
            for (let fachart of schueler.gibFacharten()) {
                let list = new LinkedCollection_1.LinkedCollection();
                for (let kurs of fachart.gibKurse()) {
                    let mapIstInKurs = mapSchuelerIstInKurs.get(schueler);
                    if (mapIstInKurs === null)
                        throw new NullPointerException_1.NullPointerException();
                    let varKurs = mapIstInKurs.get(kurs);
                    if (varKurs === null)
                        throw new NullPointerException_1.NullPointerException();
                    list.add(varKurs);
                }
                ssw.c_exactly_GENERIC(list, 1);
            }
        }
        for (let schueler of this.schuelerAlle) {
            let mapIstInKurs = mapSchuelerIstInKurs.get(schueler);
            if (mapIstInKurs === null)
                throw new NullPointerException_1.NullPointerException();
            for (let fachart1 of schueler.gibFacharten()) {
                for (let fachart2 of schueler.gibFacharten()) {
                    if (fachart1.gibNr() < fachart2.gibNr()) {
                        for (let kurs1 of fachart1.gibKurse()) {
                            for (let kurs2 of fachart2.gibKurse()) {
                                let var1 = mapIstInKurs.get(kurs1);
                                let var2 = mapIstInKurs.get(kurs2);
                                if ((var1 === null) || (var2 === null))
                                    throw new NullPointerException_1.NullPointerException();
                                let x = ssw.c_new_var_AND(var1.valueOf(), var2.valueOf());
                                for (let s = 0; s < nSchienen; s++) {
                                    let schienenKurs1 = mapKursSchiene.get(kurs1);
                                    let schienenKurs2 = mapKursSchiene.get(kurs2);
                                    if ((schienenKurs1 === null) || (schienenKurs2 === null))
                                        throw new NullPointerException_1.NullPointerException();
                                    let var3 = schienenKurs1[s];
                                    let var4 = schienenKurs2[s];
                                    ssw.c_3(-x, -var3, -var4);
                                }
                            }
                        }
                    }
                }
            }
        }
        console.log(JSON.stringify("V=" + ssw.getVarCount() + ", C=" + ssw.getClauseCount()));
        let satresult = ssw.solve(pMaxTimeMillis);
        if (satresult !== SatSolverA_1.SatSolverA.RESULT_SATISFIABLE) {
            return satresult;
        }
        this.dynDaten.aktionSchuelerAusAllenKursenEntfernen();
        for (let kurs of this.kurseAlle) {
            let schienen = new LinkedCollection_1.LinkedCollection();
            for (let s = 0; s < nSchienen; s++) {
                let schienenKurs = mapKursSchiene.get(kurs);
                if (schienenKurs === null)
                    throw new NullPointerException_1.NullPointerException();
                if (ssw.isVarTrue(schienenKurs[s])) {
                    schienen.add(s);
                }
            }
            kurs.aktionVerteileAufSchienen(schienen);
        }
        return satresult;
    }
    isTranspiledInstanceOf(name) {
        return ['de.nrw.schule.svws.core.kursblockung.KursblockungAlgorithmusKSatSolver', 'de.nrw.schule.svws.core.kursblockung.KursblockungAlgorithmusK'].includes(name);
    }
}
exports.KursblockungAlgorithmusKSatSolver = KursblockungAlgorithmusKSatSolver;
function cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver(obj) {
    return obj;
}
exports.cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver = cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver;
//# sourceMappingURL=KursblockungAlgorithmusKSatSolver.js.map