package lite;

import sbdd.SBDDFactory;
import verifier.Backtrack;

public class ProjectionSolver extends ITLSolver {

	ITLSolver clock,interval;
	ITLSolver clock1;

	/*
	 *      On interval's every clock, clock is true on clock's sub clock.
	 *      on empty interval, clock is ignored even if false.
	 *      
	 *           c         i
	 *      proj(length(3),length(4))
	 *       
     *      c     c     c     c  
	 *      |-|-|-|-|-|-|-|-|-|-|-|-|
	 *      |-----|-----|-----|-----|
	 *      i
	 *      
	 *      case 1
	 *      i is true on empty
	 *      ||
	 *      i
	 *      
	 *      case 2
	 *      one inner clock execution
	 *      
     *        @c  c     c     c  
	 *        |-|-|-|-|-|-|-|-|-|-|-|
	 *        ----|-----|-----|-----|
	 *        @i
	 *      
	 *      next:  @c & proj(c,@i)
	 *      
	 */

	public ProjectionSolver(ITLSolver clock, ITLSolver interval) {
		this.clock = clock;
		this.interval = interval;
	}

	public String toString() {
		return "proj("+clock+","+interval+")";
	}

	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
		// try empty case
		return sat.empty.sat(sat, new Continuation(sat,next,this));
	}

	@Override
	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
		if (value!=null) { // empty case, only check interval
			return interval.sat(sat, next);
		} else {
			// execute 1 clock on clock and interval. Try clock first.
			return clock.sat(sat, new Continuation(sat,next, new ProjectionSolver2()));
		}
	}

	class ProjectionSolver2 implements Next {
		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
			if (value==null) {
				// clock is falied, return null
				return next.sat(value);
			} else {
				// try interval keeping @clock
				clock1 = value;
				return interval.sat(sat, new Continuation(sat,next, new ProjectionSolver3()));
			}
		}
	}
	
	class ProjectionSolver3 implements Next {
		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
			if (value==null) {  // interval is failed, return null
				return next.sat(value);
			} else {
				// return    @clock & proj(clock,@interval)
				ITLSolver projection1 =sat.lf.projectionNode(clock,value);
				return next.sat(sat.lf.chopNode(clock1,projection1));
			}
		}
	}

	public BDDSolver toSBDD(SBDDFactory sf) {
		return sf.projectionNode(clock.toSBDD(sf),interval.toSBDD(sf));
	}

	public BDDSolver high() {
		return (BDDSolver)clock;
	}

	public BDDSolver low() {
		return (BDDSolver)interval;
	}

	public ITLSolver var() {
		return SBDDFactory.projSolver;
	}
}