package lite;

import sbdd.BDDID;
import sbdd.SBDDFactoryInterface;
import verifier.Backtrack;

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(ITLSolver var, ITLSolver high, ITLSolver low) {
		this.var = var;
		this.high = (BDDSolver) high;
		this.low  = (BDDSolver) low;
		id = BDDID.Variable;
	}

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

	public BDDSolver(ITLSolver v, ITLSolver high, ITLSolver 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();
	}


	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
		if (id!=BDDID.Variable&&id!=BDDID.BDD) {
			return var.sat(sat,next);
		}
		return var.sat(sat, new Continuation(sat,next,this));
	}

	@Override
	public ITLSolver next(ITLSatisfier sat,Continuation next, 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 Continuation(sat,next,
					new BDDSolver2(value)));
		}
	}

	class BDDSolver2 implements Next {
		ITLSolver cond;
		public BDDSolver2(ITLSolver value) {
			cond = value;
		}

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

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

		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver low) throws Backtrack {
			if (low==sat.true_ && high==sat.true_) 
				return next.sat(low);
			if (low==null && high==null) 
				return next.sat(null);
			if (low == high) {
				return 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 value = sat.lf.orNode(
						sat.lf.andNode(cond, high),
						sat.lf.andNode(sat.lf.notNode(cond), low));
				if (value==sat.false_) value = null;
				return next.sat(value);
			}
		}
	}


	public ITLSolver 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 ITLSolver 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 ITLSolver 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());
	}
	
	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;
	}
}