package lite;


import sbdd.SBDDFactoryInterface;
import verifier.Backtrack;
import verifier.ChoicePointList;

public class ITLSatisfier implements Next {

	/**
	 * 
	 */
	public ChoicePointList<ITLSolver> cp;
	public ITLSolver true_;
	public ITLSolver false_;
	public SBDDFactoryInterface lf;

	public Backtrack backtrack;
	public ITLSolver empty;
	public boolean verbose = true;

	
	public ITLSatisfier() {
		backtrack = new Backtrack();
		true_   = ITLNodeFactory.trueSolver;
		false_  = ITLNodeFactory.falseSolver;
		cp = new ChoicePointList<ITLSolver>();
	}
	
	public ITLSatisfier(ITLSolver p) {
		this();
		lf = new ITLNodeFactory();
		this.empty = p; // have to be the same in the parser
	}


	public ITLSolver satisfiable(ITLSolver n) {
		try {
			return n.sat(this, new Continuation(this,null,this));
		} catch (Backtrack e) {
			// no more choice
			return null; // unsatisfiable
		}
	}
	
	public void develop(ITLSolver n, Next next) {
		try {
			n.sat(this,new Continuation(this,null,next));
		} catch (Backtrack e) {
			return; // all end
		}
	}

	public ITLSolver next(ITLSatisfier sat, 
			Continuation next, ITLSolver value) throws Backtrack {
		if (value==null) {
			// try other choice on 
			throw backtrack;
		}
		return value;  // satisfiable
	}

	public ITLSolver true_() {
		return true_;
	}

	
	public ChoicePointList<ITLSolver> choicePoint() {
		return cp;
	}



}