package lite;

import java.util.LinkedList;

import logicNode.parser.TokenID;

import sbdd.SBDDFactoryInterface;
import verifier.Backtrack;

public class ExistsSolver extends ITLSolver {

	ITLSolver node;
	VariableSolver var;
	LinkedList<Boolean> oldVarList;
	ITLSolver residue;

	public ExistsSolver(VariableSolver var, ITLSolver node) {
		this.node = node;
		this.var = var;
		oldVarList = new LinkedList<Boolean>();
	}
	
	
	public String toString() {
		return "exists("+var+",("+node+"))";
	}

	@Override
	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
		boolean old = var.value;
		makeLocal(sat);
		var.setValue(true);
		try {
			return node.sat(sat, new Continuation(sat,next,this));
		} catch (Backtrack e) {
			restoreLocal(sat);
			var.setValue(old);
			throw sat.backtrack;
		}
	}


	private void restoreLocal(ITLSatisfier sat) {
		if (oldVarList.size()>0) {
			var.value = oldVarList.getLast();
			oldVarList.removeLast();
		} else {
			sat.deleteChoicePoint(var);
		}
	}

	private void makeLocal(ITLSatisfier sat) {
		if (sat.hasChoicePoint(var)) {
			oldVarList.add(var.value);
		} else {
			sat.addChoicePoint(var);
		}
	}

	private ITLSolver restoreLocal(ITLSatisfier sat,boolean now,ITLSolver value,Continuation next) throws Backtrack {
		restoreLocal(sat);
		try {
			return next.sat(value);
		} catch (Backtrack e) {
			makeLocal(sat);
			var.setValue(now);
			throw sat.backtrack;
		}
	}
	
	@Override
	public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
		if (value==null) {
			var.setValue(false);
			return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3()));
		} else if (value==sat.true_) {
			return restoreLocal(sat,var.value,value,next);
		} else {
			var.setValue(false);
			residue = value;
			return node.sat(sat, new Continuation(sat,next,
					new ExistsSolver2()));
		}
	}

	class ExistsSolver2 implements Next {
		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
			if (value==null) {
				value = sat.lf.existsNode(var,residue);
			} else if (value==sat.true_) {
			} else {
				value = sat.lf.orNode(residue,value);
				if (value==sat.true_)  {
				} else {
					value = sat.lf.existsNode(var,value);
				}
			}
			return restoreLocal(sat,var.value,value,next);
		}
	}
	
	class ExistsSolver3 implements Next {

		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
			if (value==null) {
			} else if (value==sat.true_) {
			} else {
				value = sat.lf.existsNode(var, value);
			}
			return restoreLocal(sat,var.value,value,next);
		}
	}
	
	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
		return sf.existsNode(var, node.toSBDD(sf)).toSBDD(sf);
	}

	

	public boolean isModal() {
		return true;
	}
	

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

	public boolean equals(Object o) {
		if (o.hashCode()!=hashCode()) return false;
		if (o.getClass()==this.getClass()) {
			ExistsSolver v = (ExistsSolver)o;
			// should ignore local variable name
			return var.equals(v.var)&& node.equals(v.node);
		}
		return false;
	}
}