"use strict";
Object.defineProperty(exports, "__esModule", { value: true });
exports.cast_de_nrw_schule_svws_core_kursblockung_satsolver_Variable = exports.Variable = void 0;
const JavaObject_1 = require("../../../java/lang/JavaObject");
const LinkedCollection_1 = require("../../../core/adt/collection/LinkedCollection");
class Variable extends JavaObject_1.JavaObject {
    nr;
    statSatFree;
    clauses;
    neighbours;
    index = 0;
    negation = null;
    /**
     * Konstruktor. Erzeugt eine neue Variable mit einer bestimmten Variablen-Nummer
     * (ungleich 0).
     *
     * @param pNr Die Nummer der Variablen (ungleich 0).
     */
    constructor(pNr) {
        super();
        this.nr = pNr;
        this.statSatFree = [...Array(4)].map(e => Array(4).fill(0));
        this.clauses = new LinkedCollection_1.LinkedCollection();
        this.neighbours = new LinkedCollection_1.LinkedCollection();
        this.index = -3;
        this.negation = null;
    }
    toString() {
        return "" + this.nr;
    }
    /**
     * Überprüft, ob diese Variable noch auf TRUE gesetzt werden kann.
     *
     * @return TRUE, falls man diese Variable und einen logischen Widerspruch
     *         erfüllen kann.
     */
    isUnsat() {
        if (this.statSatFree[0][0] > 0) {
            console.log(JSON.stringify("FEHLER: Dieser Fall darf gar nicht passieren."));
            return true;
        }
        if ((this.negation !== null) && (this.negation.statSatFree[0][1] > 0)) {
            return true;
        }
        return false;
    }
    /**
     * Vergleicht die Statistik zweier Variablen und bestimmt, für welche man sich
     * entscheiden sollte.
     *
     * @param b Die Variable, mit der verglichen werden soll.
     *
     * @return TRUE, wenn diese Instanz besser als "b" ist.
     */
    isBetterThan(b) {
        let statB = b.statSatFree;
        if (this.statSatFree[0][0] > statB[0][0])
            return true;
        if (this.statSatFree[0][0] < statB[0][0])
            return false;
        if (this.statSatFree[0][1] > statB[0][1])
            return true;
        if (this.statSatFree[0][1] < statB[0][1])
            return false;
        if (this.statSatFree[0][2] > statB[0][2])
            return true;
        if (this.statSatFree[0][2] < statB[0][2])
            return false;
        if (this.statSatFree[0][3] > statB[0][3])
            return true;
        if (this.statSatFree[0][3] < statB[0][3])
            return false;
        return Math.random() < 0.5;
    }
    /**
     * Debug-Ausgabe. Nur für Testzwecke.
     */
    debug() {
        console.log(JSON.stringify("DEBUGGING VAR " + this.nr));
        for (let r = 0; r < this.statSatFree.length; r++) {
            for (let c = 0; c < this.statSatFree[r].length; c++) {
                console.log(JSON.stringify(" " + this.statSatFree[r][c]));
            }
            console.log(JSON.stringify("    "));
            if (this.negation !== null) {
                for (let c = 0; c < this.negation.statSatFree[r].length; c++) {
                    console.log(JSON.stringify(" " + this.negation.statSatFree[r][c]));
                }
            }
            console.log();
        }
    }
    /**
     * Liefert die Anzahl an noch nicht erfüllten Klauseln.
     *
     * @return Die Anzahl an noch nicht erfüllten Klauseln.
     */
    getClauseOccurences() {
        let sum = 0;
        for (let free = 0; free < 4; free++) {
            sum += this.statSatFree[0][free];
        }
        return sum;
    }
    isTranspiledInstanceOf(name) {
        return ['de.nrw.schule.svws.core.kursblockung.satsolver.Variable'].includes(name);
    }
}
exports.Variable = Variable;
function cast_de_nrw_schule_svws_core_kursblockung_satsolver_Variable(obj) {
    return obj;
}
exports.cast_de_nrw_schule_svws_core_kursblockung_satsolver_Variable = cast_de_nrw_schule_svws_core_kursblockung_satsolver_Variable;
//# sourceMappingURL=Variable.js.map