package lite;

import sbdd.SBDDFactoryInterface;


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+")";
	}



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

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

	class AndSolver1 implements Next {
		Next next;
		public AndSolver1(Next next) {
			this.next = next;
		}
		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			if (value==null) {
				return next.next(sat,null);
			} else if (value==sat.true_) {
				return right.sat(sat, next);
			} else {
				return right.sat(sat, new AndSolver2(next,value));
			}
		}
	}
	@Override
	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
		return left.sat(sat,new AndSolver1(next));
	}

	
}