package lite;

import parser.TokenID;
import sbdd.SBDDFactoryInterface;

public class NextSolver extends ITLSolver {

	ITLSolver node;
	public NextSolver(ITLSolver node) {
		this.node = node;
	}
		
	public String toString() {
		return "next("+node+")";
	}

	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
		return sf.nextNode(node.toSBDD(sf)).toSBDD(sf);
	}
	public boolean isModal() {
		return true;
	}
	

	public int hashCode() {
		if (hash!=-1) return hash;
		return hash = BDDSolver.NODEHASH(TokenID.Next.hash,node.hashCode(),0);
	}

	public boolean equals(Object o) {
		if (o.hashCode()!=hashCode()) return false;
		if (o.getClass()==this.getClass()) {
			NextSolver v = (NextSolver)o;
			return node.equals(v.node);
		}
		return false;
	}

	class NextSolver1 implements Next {
		Next next;
		NextSolver1(Next next) { this.next = next; }
		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			if (value==null) {
				return next.next(sat,node); // not empty case
			} else
				return next.next(sat,sat.true_); 
		}
	}

	@Override
	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
		return sat.empty.sat(sat, new NextSolver1(next));
	}
}