package lite;

import java.util.LinkedList;

import sbdd.BDDInterface;
import sbdd.SBDDFactoryInterface;
import verifier.Backtrack;
import verifier.LogicSolver;

public class ITLSolver extends LogicSolver 
	implements Next,BDDInterface {
	
	public int hash=-1;     // hash value cache
	public int order=-1;    // BDD variable order for this subterm
	
	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
		return null;
	}

	@Override
	public String toString() {
		return null;
	}

	public ITLSolver next(ITLSatisfier sat, lite.Continuation next, ITLSolver value) throws Backtrack {
		return null;
	}


	public void setValue(boolean solver) {
		
	}

	public boolean isMacro() {
		return false;
	}
	
	public LinkedList<? extends ITLSolver> arguments() {
		return null;
	}

	public ITLSolver predicate() {
		return null;
	}

	public ITLSolver eval(LinkedList<ITLSolver> args) {
		return this;
	}

	public boolean isTermMacro() {
		return false;
	}

	public boolean isModal() {
		return false;
	}
	
	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
		return (BDDSolver) sf.falseNode();
	}

	public boolean value() {
		return value;
	}

	
}