package sbdd;

import java.util.LinkedList;


import verifier.Backtrack;
import lite.BDDSolver;
import lite.Continuation;
import lite.ITLNodeFactory;
import lite.ITLNodeFactoryInterface;
import lite.ITLNodeParser;
import lite.ITLSatisfier;
import lite.ITLSolver;
import lite.Next;

public class BDDSatisfier extends ITLSatisfier {


	public ITLNodeParser<ITLSolver> p;
	public SBDDFactory sf;

	public  LinkedList<SBDDEntry> queue;
	public  SBDDSet state;

	/**
	 * 
	 */
	private static final long serialVersionUID = 1L;
	
		
	public void init() {
		lf = new ITLNodeFactory();
		p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf);
		sf = new SBDDFactory();
		// empty = ITLNodeFactory.emptySolver;
		// empty = SBDDFactory.emptySolver;
		empty = lf.emptyNode();
	}
	
	public BDDSatisfier() {
		init();
		lf = new SBDDFactory();
		true_ = SBDDFactory.trueSolver;
		state = sf.set();
		state.getEntry(SBDDFactory.trueSolver).expanded = true;
		state.getEntry(SBDDFactory.falseSolver).expanded = true;
		state.getEntry(SBDDFactory.emptySolver).expanded = true;
	}

	public void showAllNext(String s) {
		ITLSolver n = p.parse(s);
		BDDSolver b = n.toSBDD(sf);
		System.out.println(b);
		develop(b, new Print());
		// System.out.println(sf.hash);
		System.out.println();
	}
	
	class Print implements Next {
		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
			System.out.println("  "+sat.choicePoint()+" -> "+value);
			throw sat.backtrack;
		}
	}
	

	public void showVerify(String s) {
		ITLSolver n = p.parse(s);
		BDDSolver b = n.toSBDD(sf);
		System.out.println(s);
		verify(b);
		// System.out.println(sf.hash);
		System.out.println();
	}
	
	
	class AllNext implements Next {
		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
			System.out.print(" "+sat.choicePoint()+" -> "+value);
			if (value!=null) {
				SBDDEntry e = state.getEntry(value);
				if (e.expanded) {
						// skip
				} else 	{
					queue.add(e);
					System.out.print("!");
				} 
			}
			System.out.println();
			throw sat.backtrack;
		}
	}

	public void verify(ITLSolver n) {
		queue = new LinkedList<SBDDEntry>();
		AllNext allNext = new AllNext();
		SBDDEntry b = state.getEntry(n);
		this.clear(); // if not empty something wrong
		if (b.expanded) {
			// already checked
			System.out.println("   already checked.");
			return;
		}
		queue.add(b);
		for(SBDDEntry e;(e = queue.poll())!=null; ) {
			if (e.expanded) continue;
			e.expanded = true;
			System.out.println(e.key+"->");
			develop(e.key, allNext);
		}
	}
		
	
}