import { JavaObject, cast_java_lang_Object } from '../../../java/lang/JavaObject';
import { LinkedCollection, cast_de_nrw_schule_svws_core_adt_collection_LinkedCollection } from '../../../core/adt/collection/LinkedCollection';
import { Clause, cast_de_nrw_schule_svws_core_kursblockung_satsolver_Clause } from '../../../core/kursblockung/satsolver/Clause';
import { JavaString, cast_java_lang_String } from '../../../java/lang/JavaString';
import { System, cast_java_lang_System } from '../../../java/lang/System';

export class Variable extends JavaObject {

	readonly nr : number;

	readonly statSatFree : Array<Array<number>>;

	readonly clauses : LinkedCollection<Clause>;

	readonly neighbours : LinkedCollection<Variable>;

	index : number = 0;

	negation : Variable | null = null;


	/**
	 * Konstruktor. Erzeugt eine neue Variable mit einer bestimmten Variablen-Nummer
	 * (ungleich 0).
	 * 
	 * @param pNr Die Nummer der Variablen (ungleich 0).
	 */
	public constructor(pNr : number) {
		super();
		this.nr = pNr;
		this.statSatFree = [...Array(4)].map(e => Array(4).fill(0));
		this.clauses = new LinkedCollection();
		this.neighbours = new LinkedCollection();
		this.index = -3;
		this.negation = null;
	}

	public toString() : String {
		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.
	 */
	public isUnsat() : boolean {
		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.
	 */
	public isBetterThan(b : Variable) : boolean {
		let statB : Array<Array<number>> = 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.
	 */
	public debug() : void {
		console.log(JSON.stringify("DEBUGGING VAR " + this.nr));
		for (let r : number = 0; r < this.statSatFree.length; r++){
			for (let c : number = 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 : number = 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() : number {
		let sum : number = 0;
		for (let free : number = 0; free < 4; free++){
			sum += this.statSatFree[0][free];
		}
		return sum;
	}

	isTranspiledInstanceOf(name : string): boolean {
		return ['de.nrw.schule.svws.core.kursblockung.satsolver.Variable'].includes(name);
	}

}

export function cast_de_nrw_schule_svws_core_kursblockung_satsolver_Variable(obj : unknown) : Variable {
	return obj as Variable;
}