package org.spbu.bdd.core;

import java.util.Arrays;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.ListIterator;
import java.util.Set;

import org.spbu.bdd.core.impl.BddBackendBitvector;

public class Bdd<T> {	
	
	public interface BinOp<T1, T2, T> {
		T apply(T1 op1, T2 op2);
	}
	
	static class NotEquals<T1, T2> implements BinOp<T1, T2, Boolean> {
		public Boolean apply(T1 op1, T2 op2) {
			return ! op1.equals(op2);
		}
	}
	
	static class And implements BinOp<Boolean, Boolean, Boolean> {
		public Boolean apply(Boolean op1, Boolean op2) {
			return op1 && op2;
		}
	}
	
	public static interface Filter<T> {
		// canBeInSolution(filter.getStopVal()) should always be "false"
		boolean canBeInSolution(T value, int index);
		// to reinit data structures possibly used in canBeInSolution
		void checkFinished();
		// this value is used to terminate evaluation along a path
		// of vars * vals. If stopVal appears as an operand of a BinOp
		// this BinOp returns stopVal. This is done through Bdd.apply
		T getStopVal();
		boolean isSolution(LinkedList<T> lst);
	}
	
	static class CondNE<T> implements BinOp<T, T, T> {
		public T apply(T op1, T op2) {
			return !(op1.equals(op2)) ? op1 : (T)filter.getStopVal();
			//if (op2.equals((T)filter.getStopVal())) return op2;
			//else return (!op1.equals(op2)) ? op1 : (T)filter.getStopVal();
		}
	}
	/*
	static class LeafAndListToList<T> implements BinOp<T, LinkedList<T>, LinkedList<? extends Object>> {
		public LinkedList<? extends Object> apply(T leaf, LinkedList<T> lst) {
			if (leaf.equals(badVal_) || lst.getFirst().equals(badVal_))
				return badList_; 
			LinkedList<T> res = new LinkedList(lst);
			res.addFirst(leaf);
			return res;
		}	
	}
	*/

	public interface UnOp<T1, T> {
		T apply(T1 op);
	}
	
	
	static class LeafToList<T> implements UnOp<T, LinkedList<T>> {
		public LinkedList<T> apply(T op) {
			LinkedList<T> res = new LinkedList();
			res.addFirst(op);
			return res;
		}	
	}
	/*
	public class Path<T> {
		public int[] vars;
		public boolean[] vals;
		public T val; 
		
		public Path(int[] vars, boolean[] vals, T val) {
			this.vars=vars;
			this.vals=vals;
			this.val=val;
		}
	}
	*/
	
	static IBddBackend bddBackend;
	static int nextVar = 1;
	static Filter filter;
	
	// resCache stores solutions, and nulls for lists for which
	// canBeInSolution returns false
	static Cache<LinkedList<?>> resCache;
	// opCache stores results of "apply" and "ite"
	static Cache<INode> opCache;
	private static INode stopTerminal;
	public static <T> void Init(int maxNonterminals,
			int maxTerminals,
			Filter fltr,
			int opsToCache,
			int resToCache){
		bddBackend = new BddBackendBitvector();
		((BddBackendBitvector)bddBackend).init(maxNonterminals, maxTerminals);
		filter = fltr;
		stopTerminal = insertTerminal(filter.getStopVal());
		opCache = new Cache(opsToCache);
		resCache = new Cache(resToCache);
	}		
	
	private static INode insertNonterminal(int var, INode one, INode zero) {
		return bddBackend.insertNonterminal(var, one, zero);
	}
	
	private static <E> ITerminal<E> insertTerminal(E value) {
		return bddBackend.insertTerminal(value);
	}
			

	private INode root;
	
	protected Bdd(INode n) {
		root = n;
	}
		
	
	
	
	@Override
	public int hashCode() {
		return root.hashCode();
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		Bdd other = (Bdd) obj;
		if (root != other.root)
			return false;
		return true;
	}

	
	public static <E> Bdd<E> makeConst(E value) {
		return new Bdd(insertTerminal(value));
	}
	
	public static <E> Bdd<E> makeNode(int var, E valueOne, E valueZero, boolean inversed) {
		ITerminal<E> one = insertTerminal(valueOne);
		ITerminal<E> zero = insertTerminal(valueZero);
		INode n = (!inversed)?insertNonterminal(var, one, zero) : insertNonterminal(var, zero, one);
		return new Bdd<E>(n);
	}

	public static int getNextVar() {
		return nextVar;
	}

	public boolean isConst() {
		return root.isTerm();
	}

	/*
	public <T> T getConst() {
		return ((ITerminal<T>)root).getValue();
	}
	*/
	
	//makes a new (balanced, of log(n) height) bdd (with new vars) with leaves from a list
	public Bdd<T> insertNewList(List<T> lst) {
		int size = lst.size();
		int domlen = 0;
		// next for is like domlen=log(2,size) - we need this number of vars
		// to represent a "size" number of values
		for (int i=1; i<size; i*=2) domlen++;
		int[] varidx = new int[domlen];
		boolean[] varval = new boolean[domlen];
		
		for (int i=0; i<domlen; i++) varidx[i] = nextVar++;
		
		Bdd<T> res = this;
		for (T elem : lst) {
			res = res.insertElem(elem, varidx, varval);
			//varval is actually "i" in binary
			int k = varval.length-1;
			//imitation of depth-first traverse: left subtree (we just add 1 to i in binary)
			while (k>0 && varval[k]) varval[k--] = false;
			//...right subtree
			if (k>=0) varval[k] = true;
		}
		return res;
	}
	
	public Bdd<T> insertElem(T value, int[] varIndex, boolean[] varValue) {
		Bdd<Boolean> elem = makeConst(true);
		//alternatively maybe put makeNode(varIndex[0]...) here and start "for" from i=1?
		for (int i=0; i<varIndex.length; i++) {
			elem = elem.and(makeNode(varIndex[i], true, false, varValue[i]));
		}
		/* after this we have a bdd with "true" at one desired leaf
		 * at the end of the route through varIndex vars along varValue path.
		 * All vars of "elem" are > all vars of "this", hence they'll be lower
		 * in the result
		 */
		return Bdd.ite(elem, makeConst(value), this);
	}

	//if this.leaf=bdd.leaf, return badval, else return this.leaf
	public Bdd<T> condNE(Bdd<T> bdd) {
		return Bdd.apply(this, bdd, BinaryOps.CNE.getBinOp());
	}

	public Bdd<Boolean> and(Bdd<Boolean> bdd) {
		return Bdd.apply(this, bdd, BinaryOps.AND.getBinOp());
	}
	
	/*
	private Bdd<Boolean> notEquals(Bdd<T> bdd) {
		return Bdd.apply(this, bdd, BinaryOps.NE.getBinOp());
	}
	
	public Bdd<LinkedList<T>> leafToList() {
		return Bdd.apply(this, UnaryOps.LTL.getUnOp());
	}

	public Bdd<LinkedList<T>> leavesToList(Bdd<LinkedList<T>> lstBdd) {
		return Bdd.apply(this, lstBdd, new LeafAndListToList());
	}
	*/

	//next two methods are to collect all the solutions
	public static <T> Set<LinkedList<T>> getResult(Bdd<T>[] bdds) {
		Set<LinkedList<T>> res = new HashSet(20000);
		int size = bdds.length;
		INode[] nodes = new INode[size];
		for (int i=0; i<size; i++) nodes[i] = bdds[i].root;
		_getResult(nodes, res);
		return res;
	}
	
	/*
	 * traverse all BDDs in parallel, collect all results from leaves
	 * using filter.canBeInSolution(val) to stop in advance
	 * and using filter.isSolution(lst) to filter bad solutions
	 */
	
	// for correct work with ITerminal<somearray>
	// check that Cache.idx uses deepHashCode! 
	private static <T> void _getResult(INode[] nodes, Set<LinkedList<T>> res) {
		LinkedList<T> lst;
		if (resCache.contains(nodes)) {
			lst=(LinkedList<T>) resCache.get(nodes);
			if (lst!=null)
				res.add(lst);
			return;
		}
		boolean allTerms = true;
		int var = Integer.MIN_VALUE;
		int size = nodes.length;
		for (int i=size-1; i>=0; i--) //for (int i=0; i<size; i++)
			if (!nodes[i].isTerm()) {
				allTerms = false;
				var = Math.max(var, ((INonterminal)nodes[i]).var());				
			}
			else if (!filter.canBeInSolution(((ITerminal<T>)nodes[i]).getValue(),i)) {
				resCache.put(nodes, null);
				return;
			}
		filter.checkFinished();
		if (allTerms) {
			lst = new LinkedList();
			for (INode node : nodes)
				lst.addLast(((ITerminal<T>)node).getValue());
			if (filter.isSolution(lst)) {
				res.add(lst);
				resCache.put(nodes, lst);
			}
			else
				resCache.put(nodes, null);
		}
		else {
			INode[] zeroNodes = new INode[size];
			for (int i=0; i<size; i++) {
				zeroNodes[i] = optZero(var, nodes[i]);
				nodes[i] = optOne(var, nodes[i]);
			}
			_getResult(nodes, res);
			_getResult(zeroNodes, res);
			// do NOT put here any resCache! We are collecting ALL
			// the solutions
		}
		return;
	}

	//next two methods are to get one solution
	public static <T> LinkedList<T> getSolution(Bdd<T>[] bdds) {
		int size = bdds.length;
		INode[] nodes = new INode[size];
		for (int i=0; i<size; i++) nodes[i] = bdds[i].root;
		return _getSolution(nodes);
	}
	
	/*
	 * traverse all BDDs in parallel, collect all results from leaves
	 * using filter.canBeInSolution(val) to stop in advance
	 * and using filter.isSolution(lst) to filter bad solutions
	 */
	
	// for correct work with ITerminal<somearray>
	// check that Cache.idx uses deepHashCode!
	private static <T> LinkedList<T> _getSolution(INode[] nodes) {
		if (resCache.contains(nodes))
			return (LinkedList<T>)resCache.get(nodes);
		boolean allTerms = true;
		int var = Integer.MIN_VALUE;
		int size = nodes.length;
		for (int i=size-1; i>=0; i--)
			if (!nodes[i].isTerm()) {
				allTerms = false;
				var = Math.max(var, ((INonterminal)nodes[i]).var());				
			}
			else if (!filter.canBeInSolution(((ITerminal<T>)nodes[i]).getValue(),i)) {
				resCache.put(nodes, null);
				return null;
			}
		filter.checkFinished();
		LinkedList<T> lst;
		if (allTerms) {
			lst = new LinkedList();
			for (INode node : nodes)
				lst.addLast(((ITerminal<T>)node).getValue());
			if (!filter.isSolution(lst))
				lst = null;
			resCache.put(nodes, lst);
		}
		else {
			INode[] zeroNodes = new INode[size];
			for (int i=0; i<size; i++) {
				zeroNodes[i] = optZero(var, nodes[i]);
				nodes[i] = optOne(var, nodes[i]);
			}
			lst =_getSolution(zeroNodes);
			if (lst==null)
				lst = _getSolution(nodes);
		}
		// do NOT put here any resCache! We may be collecting ALL
		// the solutions after invoking getSolution
		return lst;
	}
	
	/* Keys for efficient hashCode use.
	 * Don't use generics, Lists or anything else here -
	 * it degrades performance.
	 */
	
	/*
	static class UnOpKey {
		INode n;
		UnOp op;

		private UnOpKey(INode n, UnOp op) {
			super();
			this.n = n;
			this.op = op;
		}

		@Override
		public int hashCode() {
			final int prime = 31;
			int result = 1;
			result = prime * result + ((n == null) ? 0 : n.hashCode());
			result = prime * result + ((op == null) ? 0 : op.hashCode());
			return result;
		}

		@Override
		public boolean equals(Object obj) {
			if (this == obj)
				return true;
			if (obj == null)
				return false;
			if (getClass() != obj.getClass())
				return false;
			UnOpKey other = (UnOpKey) obj;
			if (n == null) {
				if (other.n != null)
					return false;
			} else if (!n.equals(other.n))
				return false;
			if (op == null) {
				if (other.op != null)
					return false;
			} else if (!op.equals(other.op))
				return false;
			return true;
		}
	}
	*/

	static class BinOpKey {
		INode n1;
		INode n2;
		BinOp op;
		
		private BinOpKey(INode n1, INode n2, BinOp op) {
			super();
			this.n1 = n1;
			this.n2 = n2;
			this.op = op;
		}

		@Override
		public int hashCode() {
			final int prime = 31;
			int result = 1;
			result = prime * result + ((n1 == null) ? 0 : n1.hashCode());
			result = prime * result + ((n2 == null) ? 0 : n2.hashCode());
			result = prime * result + ((op == null) ? 0 : op.hashCode());
			return result;
		}

		@Override
		public boolean equals(Object obj) {
			if (this == obj)
				return true;
			if (obj == null)
				return false;
			if (getClass() != obj.getClass())
				return false;
			BinOpKey other = (BinOpKey) obj;
			if (n1 == null) {
				if (other.n1 != null)
					return false;
			} else if (!n1.equals(other.n1))
				return false;
			if (n2 == null) {
				if (other.n2 != null)
					return false;
			} else if (!n2.equals(other.n2))
				return false;
			if (op == null) {
				if (other.op != null)
					return false;
			} else if (!op.equals(other.op))
				return false;
			return true;
		}
	}
	
	static class ITEKey {
		INode n1, n2, n3;

		private ITEKey(INode n1, INode n2, INode n3) {
			super();
			this.n1 = n1;
			this.n2 = n2;
			this.n3 = n3;
		}

		@Override
		public int hashCode() {
			final int prime = 31;
			int result = 1;
			result = prime * result + ((n1 == null) ? 0 : n1.hashCode());
			result = prime * result + ((n2 == null) ? 0 : n2.hashCode());
			result = prime * result + ((n3 == null) ? 0 : n3.hashCode());
			return result;
		}

		@Override
		public boolean equals(Object obj) {
			if (this == obj)
				return true;
			if (obj == null)
				return false;
			if (getClass() != obj.getClass())
				return false;
			ITEKey other = (ITEKey) obj;
			if (n1 == null) {
				if (other.n1 != null)
					return false;
			} else if (!n1.equals(other.n1))
				return false;
			if (n2 == null) {
				if (other.n2 != null)
					return false;
			} else if (!n2.equals(other.n2))
				return false;
			if (n3 == null) {
				if (other.n3 != null)
					return false;
			} else if (!n3.equals(other.n3))
				return false;
			return true;
		}
	}
	

	// Functions for correct descending through BDD
	private static INode optOne(int var, INode n) {
		if (n.isTerm()) return n;
		INonterminal nt = (INonterminal)n;
		if (nt.var() == var) return nt.one();
		else return n;
	}
	
	
	private static INode optZero(int var, INode n) {
		if (n.isTerm()) return n;
		INonterminal nt = (INonterminal)n;
		if (nt.var() == var) return nt.zero();
		else return n;
	}
	
	
	private static int optVar(INode n) {
		if (n.isTerm()) return Integer.MAX_VALUE;
		INonterminal nt = (INonterminal)n;
		return nt.var();
	}
	
	
	private static int minVar(INode n1, INode n2) {
		return Math.min(optVar(n1), optVar(n2));
	}
	
	
	private static int minVar(INode n1, INode n2, INode n3) {
		return Math.min(Math.min(optVar(n1), optVar(n2)), optVar(n3));
	}
	
	/*
	// Function for applying something to leaves
	// Doesn't use filter.getStopVal() yet!
	public static <T1,T2> Bdd<T2> apply(Bdd<T1> bdd, UnOp<T1,T2> unOp) {
		return new Bdd(Bdd._apply(bdd.root, unOp));
	}
	
	private static INode _apply(INode n, UnOp unOp) {
		UnOpKey key = new UnOpKey(n, unOp);
		if (opCache.contains(key)) return opCache.get(key);
		
		INode res = null;
		if (n.isTerm()) {
			res = insertTerminal(unOp.apply(((ITerminal)n).getValue()));
		} else {
			INonterminal nt = (INonterminal)n;
			res = insertNonterminal(nt.var(),
					_apply(nt.one(), unOp), 
					_apply(nt.zero(), unOp)
					);		
		}
		
		opCache.put(key, res);
		return res;
	}
	*/
	
	public static <T1,T2,T3> Bdd<T3> apply(Bdd<T1> bdd, Bdd<T2> bdd2, BinOp<T1,T2,T3> binOp) {
		return new Bdd(Bdd._apply(bdd.root, bdd2.root, binOp));
	}
	
	//static int c=0;
	private static INode _apply(INode n1, INode n2, BinOp binOp) {
		//System.out.println("apply: "+(c++)+" "+n1.toString()+" | "+n2.toString());
		
		// degenerate cases, this order is the fastest
		BinOpKey key = new BinOpKey(n1, n2, binOp);
		if (opCache.contains(key))
			return opCache.get(key);
		if (n1.isTerm() && ((ITerminal)n1).getValue().equals(filter.getStopVal()))
			return stopTerminal;
		if (n2.isTerm() && ((ITerminal)n2).getValue().equals(filter.getStopVal()))
			return stopTerminal;

		// normal cases
		INode res = null;
		if (n1.isTerm() && n2.isTerm())
			res = insertTerminal(binOp.apply(((ITerminal)n1).getValue(),
											 ((ITerminal)n2).getValue()));
		else {
			int var = minVar(n1, n2);
			res = insertNonterminal(var,
					_apply(optOne(var, n1), optOne(var, n2), binOp), 
					_apply(optZero(var, n1), optZero(var, n2), binOp)
					);
		}
		opCache.put(key, res);
		return res;
	}
	
	/* "ite" means If Then Else. If the sets of vars of all 3 bdds
	 * here are the same, then it works like this:
	 * For each route in cond, if its leaf is false,
	 * go through the same route in bdd1 and use its leaf
	 * else go through the same route in bdd2 and use its leaf.
	 * If the sets are not equal, we merge them as we did in "apply"
	 */
	// don't use filter.getStopVal() here!!
	public static <T> Bdd<T> ite(Bdd<Boolean> cond, Bdd<T> bdd1, Bdd<T> bdd2) {
		return new Bdd(Bdd._ite(cond.root, bdd1.root, bdd2.root));
	}
	
	private static INode _ite(INode cond, INode n1, INode n2) {
		ITEKey key = new ITEKey(cond, n1, n2);
		if (opCache.contains(key))
			return opCache.get(key);
		
		INode res;
		if (n1.isTerm() && n2.isTerm() && cond.isTerm())
			res = (((ITerminal<Boolean>)cond).getValue()) ? n1 : n2;
		else {
			int var = minVar(n1, n2, cond);
			res = insertNonterminal(var,
					_ite(optOne(var, cond), optOne(var, n1), optOne(var, n2)), 
					_ite(optZero(var, cond), optZero(var, n1), optZero(var, n2))
					);		
		}
		
		opCache.put(key, res);
		return res;
	}
	
	/*
	// assuming first var was 1
	public <T> Path<T> getPathNotTo(T badval) {
		int size = Bdd.getNextVar()-1;
		// why -1? because nextVar isn't assigned yet
		int[] vars = new int[size+1];
		boolean[] vals = new boolean[size+1];
		INode[] nodes = new INode[size+1]; //+1 - for terminal node
		int i = 0;
		nodes[0] = (INonterminal)root;
		
		do {
			// by this time we should have correct nodes[0..i]
			// and correct vals[0..size-1]
			// and correct vars[0..i-1]
			if (nodes[i].isTerm()) {
				T val = ((ITerminal<T>)nodes[i]).getValue();
				if (!val.equals(badval)) {
					// leaf is good, path is found
					int[] varsRes = new int[i];
					boolean[] valsRes = new boolean[i];
					// last several vars are unnecessary (they are from previous paths)
					for (int j = 0; j < i; j++) {
						varsRes[j] = vars[j];
						valsRes[j] = vals[j];
					}
					return new Path<T>(varsRes, valsRes, val);
				}
				else {
					// leaf is bad, make next path
					// setting vals[<last false>..size-1] to new path
					// bounds exception here => all vals=true and we've traversed the BDD
					try {
						while (vals[i]) vals[i--] = false;
					} catch (ArrayIndexOutOfBoundsException e) {
						return null;
					}
					if (i >= 0) vals[i] = true;
				}
			}
			else {
				// now that we know nodes[i] is Nonterminal ...
				INonterminal nt = (INonterminal)nodes[i]; 
				// ... we set vars[i] ...
				vars[i] = nt.var();
				// ... and nodes[i+1]
				if (vals[i++]) nodes[i] = nt.one();
				else nodes[i] = nt.zero();
			}
		} while (true);
	}
	
	// assuming p.vars has sorted vars and vars[0]==root.var()
	public <T> T walkPath(Path p) {
		if (root.isTerm()) return ((ITerminal<T>)root).getValue();
		INonterminal nt = (INonterminal)root;
		int size = p.vars.length;
		int i = 0;
		while (i < size-1) {
			if (nt.var() < p.vars[i]) return null; // path doesn't have current var
			if (p.vals[i]) nt = (INonterminal)nt.one();
			else nt = (INonterminal)nt.zero();
			while (i < size - 1 && nt.var() > p.vars[i]) i++;
		}
		if (p.vals[i] && nt.one().isTerm())
			return ((ITerminal<T>)(nt.one())).getValue();
		else if (!p.vals[i] && nt.zero().isTerm())
			return ((ITerminal<T>)(nt.zero())).getValue();
		else return null; // path was too short for this bdd and ended at a nonterminal
	}
	*/
	
	public String toString() {
		return toString(root, 0);
	}
	
	static String toString(INode n, int lev) {
		String res = "";
		for (int i=0; i<lev; i++) res += "  ";
		if (n.isTerm()) res += "<"+((ITerminal)n).getValue().toString()+">";
		else {
			INonterminal nt = (INonterminal)n;
			res += nt.var() + "\n"+toString(nt.one(), lev+1)+"\n"+toString(nt.zero(), lev+1);
		}
		return res;
	}
}
