package org.spbu.bdd.core.impl;

import java.io.IOException;
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.ListIterator;

import org.spbu.bdd.core.IBddBackend;
import org.spbu.bdd.core.INode;
import org.spbu.bdd.core.INonterminal;
import org.spbu.bdd.core.ITerminal;

import static org.spbu.bdd.util.ByteUtil.*;

public class BddBackendBitvector implements IBddBackend {
	
	int maxNonterminals;
	int maxTerminals;
	
	byte[] ntMain;  // array of blocks [ 2 byte(var) + 3 byte(one-index) + 3 byte(zero-index) + 4bit (one-index-tail) + 4bit (zero-index-tail)]
	ITerminal<?>[] terminals;
	
	int nTerms;
	int nNterms;
	
	public BddBackendBitvector() {		
	}
	
	public void init(int maxnonterminals, int maxterminals) {
		this.maxNonterminals = maxnonterminals;
		this.maxTerminals = maxterminals;		
		ntMain = new byte[maxnonterminals * 9];		
		terminals = new ITerminal[maxterminals];
		nTerms = 0;
		nNterms = 0;
	}
	
	public INode getNode(int index) {
		if (index < 0) return terminals[-index - 1];
		else {
			int idx = index * 9;
			int var = twoBytesToInt(ntMain[idx], ntMain[idx + 1]);
			if (var == 0) return null;			
			int one = threeBytesAndHalfToInt(
					ntMain[idx + 2], ntMain[idx + 3], ntMain[idx + 4], 
					halfByteToInt(ntMain[idx+8], true));
			int zero = threeBytesAndHalfToInt(
					ntMain[idx + 5], ntMain[idx + 6], ntMain[idx + 7], 
					halfByteToInt(ntMain[idx+8], false));
			return new NonterminalImpl(var, BitvectorConst.realIndex(one), BitvectorConst.realIndex(zero), this, index);
		}
	}
	
	public INode insertNonterminal(int var, INode one, INode zero) {				
		NodeImpl _one = (NodeImpl)one;
		NodeImpl _zero = (NodeImpl)zero;
		if (_one.getIndex() == _zero.getIndex()) return one;
		
		NonterminalImpl nt = new NonterminalImpl(var, _one.getIndex(), _zero.getIndex(), this);
		
		int n = maxNonterminals;
		int nth = nt.hashCode();
		int h1 = nth % n;
		if (h1 < 0) h1 = n + h1;
		int h2 = (nth*13 + 37) % n;
		if (h2 < 0) h2 = n + h2;
		if (h2 == 0) h2 = 1;
		// bug here!! might cycle forever for some h1, h2, n
		// possible solution - force n be prime
		for (INonterminal t = (INonterminal)getNode(h1); t!= null; h1 = (h1 + h2) % n, t = (INonterminal)getNode(h1)) {
			if (nt.equals(t)) return t;
		}
		nt.setIndex(h1);
		nNterms++;
		if (nNterms >= maxNonterminals*0.75) throw new RuntimeException("Limit of nonterminals reached");
		putNterm(nt);
		return nt;
	}

	public <E> ITerminal<E> insertTerminal(E value) {		
		int n = maxTerminals;
		TerminalImpl<E> tt = new TerminalImpl(value);
		int tth = tt.hashCode();
		int h1 = tth % n;
		if (h1 < 0) h1 = n + h1;
		int h2 = (tth*13 + 37) % n;
		if (h2 < 0) h2 = n + h2;
		if (h2 == 0) h2 = 1;
		// bug here!! might cycle forever for some h1, h2, n
		// possible solution - force n be prime
		for (ITerminal<?> t = terminals[h1]; t!= null; h1 = (h1 + h2) % n, t = terminals[h1]) {			
			if (tt.equals(t)) return (ITerminal<E>)t;
		}
		
		tt.setIndex(-h1 - 1);
		nTerms ++;
		if (nTerms >= maxTerminals*0.75)
			throw new RuntimeException("Limit of terminals reached");
		terminals[h1] = tt;
		return tt;
	}
	
	
	private void putNterm(NonterminalImpl nt) {
		int idx = nt.getIndex()* 9;		
		intToTwoBytes(nt.var(), ntMain, idx);
		int remHi = intToThreeBytesAndHalf(BitvectorConst.fakeIndex(nt.oneIndex()), ntMain, idx+2);
		int remLo = intToThreeBytesAndHalf(BitvectorConst.fakeIndex(nt.zeroIndex()), ntMain, idx+5);
		ntMain[idx+8] = twoHalvesToByte(remHi, remLo);
	}
}
