package lite;

import sbdd.SBDDFactory;
import verifier.Backtrack;


public class AndSolver extends ITLSolver {

	ITLSolver left;
	ITLSolver right;
	
	public AndSolver(ITLSolver _left,ITLSolver _right) {
		left = _left;
		right = _right;
	}
	
	public String toString() {
		return "("+left+" and "+right+")";
	}


	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
		return left.sat(sat, new Continuation(sat,next,this));
	}

	@Override
	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
		if (value==null) {
			return next.sat(null);
		} else if (value==ITLSatisfier.true_) {
			return right.sat(sat, next);
		} else {
			return right.sat(sat, new Continuation(sat,next,
					new AndSolver2(value)));
		}
	}

	class AndSolver2 implements Next {
		ITLSolver residue;
		public AndSolver2(ITLSolver value) {
			residue = value;
		}

		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
			if (value==null) {
				return next.sat(null);
			} else if (value==ITLSatisfier.true_) {
				return next.sat(residue);
			} else {
				return next.sat(sat.lf.andNode(residue,value));
			}
		}
	}

	public BDDSolver toSBDD(SBDDFactory sf) {
		return left.toSBDD(sf).and(sf, right.toSBDD(sf));
	}

	
}