package lite;

import parser.TokenID;
import sbdd.SBDDFactoryInterface;

public class ChopSolver extends ITLSolver {

	protected ITLSolver former;
	private ITLSolver later;

	/*
	 *    Interval Temporal Logic Chop Operator
	 *    
	 *    former      & later
	 *    
	 *    former        later
	 *   |-------------|---------------|
	 *   
	 *   case 1  outer empty
	 *   former (t/f)
	 *   later  (t/f)
	 *   ||
	 *   no next:
	 *   
	 *   case 2  inner empty (outer ~ empty)
	 *   former (t/f)
	 *   later  (t/f/@later)
	 *   ||----------------------------|
	 *   next:   @later
	 *       
	 *   case 3  inner more
	 *   former (t/f/@former)
	 *       later
	 *   |--|--------------------------|
	 *   next:   @former&later
	 *   
	 */
	
	public ChopSolver(ITLSolver former, ITLSolver later) {
		this.former = former;
		this.later = later;
	}

	public String toString() {
		return "("+former+" & "+later+")";
	}
	
	public ITLSolver sat(ITLSatisfier sat, Next next) throws Backtrack {
		// make choice point on empty, first try empty case
		return sat.empty.sat(sat, new ChopSolver1(next));
	}


	class ChopSolver1 implements Next {
		Next next;
		ChopSolver1(Next next) {
			this.next = next;
		}
		// check later part on Outer empty case (same as AndSolver )
		public ITLSolver next(ITLSatisfier sat,ITLSolver value) throws Backtrack {
			if (value!=null) { // Outer empty case
				return former.sat(sat, new ChopSolver2(next));
			} else {
				sat.empty.setValue(true);
				// Try inner empty case ( former is going to check on empty interval )
				return former.sat(sat, new ChopSolver3(next));
			}
		}
	}

	class ChopSolver2 implements Next {

		Next next;
		ChopSolver2(Next next) {
			this.next = next;
		}
		// check later part on Outer empty case (same as AndSolver )

		public ITLSolver next(ITLSatisfier sat,ITLSolver value) throws Backtrack {
			if (value==null) return next.next(sat,value);
			else return later.sat(sat, next);
		}
	}

	class ChopSolver3 implements Next {

		Next next;
		ChopSolver3(Next next) {
			this.next = next;
		}
		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			try {
				sat.empty.setValue(false);
				if (value==null) {
					// former is falied on empty, try more
					return former.sat(sat,  new ChopSolver4(next));
				} else {
					// former is true on empty try later part on outer interval
					// outerEmpty is false now (we have already tried true case), so if later contains empty, it will fail.
					return later.sat(sat, new ChopSolver5(next));
				}
			} catch (Backtrack e) {
				sat.empty.setValue(true);
				throw e;
			}
		}
	}
	
	class ChopSolver4 implements Next {
		// try former on more (single choice case)

		Next next;
		ChopSolver4(Next next) {
			this.next = next;
		}
		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			try {
				if (value==null) {
					// all failed
					return next.next(sat,value);
				} else {
					// former is true with @value, return @(value&later)
					// optimize required to avoid creating same node
					return next.next(sat,sat.lf.chopNode(value,later));
				}
				} catch (Backtrack e) {
					sat.empty.setValue(false);
					throw e;
				}
		}
	}

	class ChopSolver5 implements Next {

		Next next;
		ChopSolver5(Next next) {
			this.next = next;
		}
		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			if (value==null) {  // former is true on empty but later is failed on more
				// try again only on more case
				return former.sat(sat,  new ChopSolver4(next));
			} else {
				// try innerMore case with this next term
				return former.sat(sat,  new ChopSolver6(next,value));
			}
		}
	}
	
	class ChopSolver6 implements Next {
		ITLSolver later1;
		Next next;
		ChopSolver6(Next next,ITLSolver value) { later1 = value;this.next = next; }
		
		public ITLSolver next(ITLSatisfier sat, ITLSolver value) throws Backtrack {
			try {
				if (value==null) {  // former is fail on more inerval
					return next.next(sat,later1);
				} else {
					// we don't have to execute later case now, do it on next clock
					ITLSolver former1 = sat.lf.chopNode(value,later);
					// return disjunction with other choice
					ITLSolver v = sat.lf.orNode(later1,former1);
					if (v==sat.false_) v = null;
					return next.next(sat,v);
				}
				} catch (Backtrack e) {
					sat.empty.setValue(false);
					throw e;
				}
		}
	}

	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
		return sf.chopNode(former.toSBDD(sf), later.toSBDD(sf)).toSBDD(sf);
	}


	public boolean isModal() {
		return true;
	}
	
	public int hashCode() {
		if (hash!=-1) return hash;
		return hash = BDDSolver.NODEHASH(TokenID.Chop.hash,former.hashCode(),later.hashCode());
	}

	public boolean equals(Object o) {
		if (o.getClass()==this.getClass()) {
			ChopSolver v = (ChopSolver)o;
			return former.equals(v.former)&& later.equals(v.later);
		}
		return false;
	}
}