package sbdd;



import parser.TokenID;
import lite.BDDSolver;
import lite.ITLNodeFactory;
import lite.ITLSolver;


public class SBDDFactory implements SBDDFactoryInterface {

	public static final ITLSolver trueSolver   = new BDDSolver(ITLNodeFactory.trueSolver,BDDID.True,TokenID.True.hash);
	public static final ITLSolver falseSolver  = new BDDSolver(ITLNodeFactory.falseSolver,BDDID.False,TokenID.False.hash);
	public static final ITLSolver emptySolver  = new BDDSolver(ITLNodeFactory.emptySolver,trueSolver,falseSolver,BDDID.BDD);
	public SBDDSet hash;
	ITLNodeFactory itlf;
	
	SBDDFactory() {
		init();
	}
	
	void init() {
		hash = new SBDDSet(this);
		itlf = new ITLNodeFactory();

		hash.put(falseSolver);
		hash.put(trueSolver);
		hash.put(emptySolver);
	}
	

	public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2) {
		if (solver==solver2) return solver;
		ITLSolver v =  new BDDSolver(lvar,solver,solver2,BDDID.BDD);
		return hash.put(v); 
	}

	public ITLSolver chopNode(ITLSolver solver, ITLSolver solver2) {
		BDDSolver former = solver.toSBDD(this);
		BDDSolver later = solver2.toSBDD(this);
		if (former==emptySolver) return hash.put(later); 
		if (later==emptySolver) return hash.put(former); 
		ITLSolver v =  itlf.chopNode(solver.toSBDD(this),solver2.toSBDD(this));
		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Chop);
		return hash.put(b);
	}

	public ITLSolver emptyNode() {
		return emptySolver;
	}

	public ITLSolver existsNode(ITLSolver solver, ITLSolver solver2) {
		ITLSolver v =  itlf.existsNode(solver,solver2);
		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Exists);
		return hash.put(b);
	}

	public ITLSolver falseNode() {
		return falseSolver;
	}

	public ITLSolver nextNode(ITLSolver solver) {
		ITLSolver v =  itlf.nextNode(solver);
		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Next);
		return hash.put(b);
	}

	public ITLSolver projectionNode(ITLSolver solver, ITLSolver solver2) {
		ITLSolver v =  itlf.projectionNode(solver,solver2);
		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Projection);
		return hash.put(b);
	}

	public ITLSolver trueNode() {
		return trueSolver;
	}

	public ITLSolver variableNode(String name, boolean value) {
		ITLSolver v =  new BDDSolver(itlf.variableNode(name, value),trueSolver,falseSolver,BDDID.Variable);
		return hash.put(v); 
	}


	public ITLSolver andNode(ITLSolver left, ITLSolver right) {

		BDDSolver lb = left.toSBDD(this);
		BDDSolver rb = right.toSBDD(this);
		if (lb==falseSolver||rb==falseSolver)
			return falseSolver;
		if (lb==trueSolver)
			return rb;
		lb =  (BDDSolver) lb.and(this, rb);
		return hash.put(lb);
	}


	public ITLSolver notNode(ITLSolver node) {
		BDDSolver nb = node.toSBDD(this);
		if (nb==falseSolver) return trueSolver;
		if (nb==trueSolver)	 return falseSolver;
		nb = (BDDSolver) nb.not(this);
		return hash.put(nb);
	}


	public ITLSolver orNode(ITLSolver left, ITLSolver right) {
		BDDSolver lb = left.toSBDD(this);
		BDDSolver rb = right.toSBDD(this);
		if (lb==trueSolver||rb==trueSolver)
			return trueSolver;
		if (lb==falseSolver)
			return rb;
		lb = (BDDSolver) lb.or(this, rb);
		return hash.put(lb);
	}


	public SBDDSet set() {
		return hash;
	}



}