package lite;

import sbdd.BDDID;
import sbdd.SBDDFactoryInterface;

public class BDDSolver extends ITLSolver {
	
	/*
	 * var?high:low
	 */
	public ITLSolver var;
	public BDDSolver high; // true
	public BDDSolver low;  // flase
	public BDDID id;
	
	public BDDSolver(ITLSolver var, BDDSolver high, BDDSolver low) {
		this.var = var;
		this.high = high;
		this.low  = low;
		id = BDDID.Variable;
	}

	public BDDSolver(BDDID id, int hash) {
		// primitives
		this.id = id;
		this.hash = hash;
	}

	public BDDSolver(ITLSolver v, BDDSolver high, BDDSolver low, BDDID id) {
		// for modal node with id
		this(v,high,low);
		this.id = id;
	}

	public BDDSolver(ITLSolver v, BDDID id, int hash) {
		this(v,null,null);
		this.id = id;
		this.hash = hash;
	}

	public String toString() {
		if (var==null) {
			if (id!=null) return id.toString();
			else return "null";
		}
		if (id==BDDID.BDD) {
			if (high.id==BDDID.True) {
				if (low.id==BDDID.False) return var.toString();
				return "("+var+";"+low+")";
			} else if (high.id==BDDID.False&&low.id==BDDID.True)
				return "~("+var+")";
			else if (low.id==BDDID.False) {
				return "("+var+","+high+")";
			}
			return "("+var+"?"+high+":"+low+")";
		}
		return var.toString();
	}
	
	public boolean value() {
		return var.value()? high.value() : low.value();
	}


	class BDDSolver2 implements Next {
		ITLSolver cond; Next next;
		public BDDSolver2(Next next,ITLSolver value) {
			cond = value;this.next = next;
		}

		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			return low.sat(sat, new BDDSolver3(next,cond,value));
		}
	}

	class BDDSolver3 implements Next {
		ITLSolver cond, high; Next next;
		public BDDSolver3(Next next,ITLSolver cond, ITLSolver value) {
			this.cond = cond;
			high = value;
			this.next = next;
		}

		public ITLSolver next(ITLSatisfier sat, ITLSolver low) throws Backtrack {
			if (low==sat.true_ && high==sat.true_) 
				return next.next(sat,low);
			if (low==null && high==null) 
				return next.next(sat,null);
			if (low == high) {
				return next.next(sat,low);
			} else {
				// lf.bddNode(cond,high,low) won't work
				if (low==null)  low = sat.lf.falseNode();
				if (high==null) high = sat.lf.falseNode();
				// if (cond==null) cond = sat.lf.falseNode();
				ITLSolver value1 = sat.lf.orNode(
						sat.lf.andNode(cond, high),
						sat.lf.andNode(sat.lf.notNode(cond), low));
				if (value1==sat.false_) value1 = null;
				return next.next(sat,value1);
			}
		}
	}


	public BDDSolver and(SBDDFactoryInterface sf,BDDSolver right) {
		switch(id) {
		case True: return right;
		case False: return sf.falseNode();
		}

		int order = order(var,right.var);
		if (order==0) 
			return sf.bddNode(var,high.and(sf,right.high),low.and(sf,right.low));
		else if (order>0) 
			return right.and(sf,this);
		else
			return sf.bddNode(var,high.and(sf,right),low.and(sf,right));
	}

	public BDDSolver or(SBDDFactoryInterface sf,BDDSolver right) {
		switch(id) {
		case True: return sf.trueNode();
		case False: return right;
		}
		int order = order(var,right.var);
		if (order==0) 
			return sf.bddNode(var,high.or(sf,right.high),low.or(sf,right.low));
		else if (order>0) 
			return right.or(sf,this);
		else
			return sf.bddNode(var,high.or(sf,right),low.or(sf,right));
	}


	public BDDSolver not(SBDDFactoryInterface sf) {
		switch(id) {
		case True: return sf.falseNode();
		case False: return sf.trueNode();
		}
		return  sf.bddNode(var,high.toSBDD(sf).not(sf),low.toSBDD(sf).not(sf));
	}

	int order(ITLSolver a,ITLSolver b) {
		/*
		// should use hash? or more intelligent order
		return a.toString().compareTo(b.toString());
		*/
		return a.order-b.order;
	}
	
	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
		return this;
	}
	

    static final int PAIR(int a, int b) {
        return ((a + b) * (a + b + 1) / 2 + a);
    }
    static final int TRIPLE(int a, int b, int c) {
        return (PAIR(c, PAIR(a, b)));
    }

    static final int NODEHASH(int lvl, int l, int h) {
        return Math.abs(TRIPLE(lvl, l, h));
    }
	
	public int hashCode() {
		if (hash!=-1) return hash;
		return hash = NODEHASH(var.hashCode(),low.hashCode(),high.hashCode());
	}

	public boolean equals(Object o) {
		// if (o==this) return true;
		// if (o.hashCode()!=hashCode()) return false;
		if (o.getClass()==this.getClass()) {
			BDDSolver v = (BDDSolver)o;
			switch(id) {
			case True: case False: case Empty:
				return id == v.id; 
			default:
				return var.equals(v.var)&&low.equals(v.low)&&high.equals(v.high);
			}
		}
		return false;
	}

	public BDDSolver high() {
		return high;
	}

	public BDDSolver low() {
		return low;
	}

	public ITLSolver var() {
		return var;
	}

	class BDDSolver1 implements Next {
		Next next;
		public BDDSolver1(Next next) {
			this.next = next;
		}

		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			if (value==null) {
				return low.sat(sat, next);
			} else if (value==sat.true_) {
				return high.sat(sat, next);
			} else {
				return high.sat(sat, new BDDSolver2(next,value));
			}
		}
	}
	
	@Override
	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
		if (id!=BDDID.Variable&&id!=BDDID.BDD) {
			return var.sat(sat,next);
		}
		return var.sat(sat, new BDDSolver1(next));
	}
}