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;
import logicNode.parser.ExecutorInterface;

public class BDDSatisfier extends ITLSatisfier implements ExecutorInterface<ITLSolver> {


	public ITLNodeParser<ITLSolver> p;
	public SBDDFactory sf;

	public  LinkedList<SBDDEntry> queue;
	public  SBDDSet state;
	public SBDDEntry currentState;
	

	private boolean satisfiable;
	private boolean falsfiable;
	public SBDDEntry last;


	/**
	 * 
	 */
	private static final long serialVersionUID = 1L;
	
		
	public void init() {
		lf = new ITLNodeFactory();
		p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf);
		// p.setExecutor(this);
		sf = new SBDDFactory();
		// empty = ITLNodeFactory.emptySolver;
		// empty = SBDDFactory.emptySolver;
		empty = lf.emptyNode();
	}
	
	public BDDSatisfier() {
		init();
		lf = new SBDDFactory();
		true_ = SBDDFactory.trueSolver;
		false_ = SBDDFactory.falseSolver;
		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 {
			if (value!=null) {
				SBDDEntry e = state.getEntry(value);
				if (e.expanded) {
					System.out.print((e.key==sat.true_)?"t":".");
				} else 	{
					queue.add(e); e.expanded = true;
					System.out.print(e.id+" ");
				} 
			} else {
				System.out.print("f");
			}
			throw sat.backtrack;
		}
	}
	
	class AllNextVerbose implements Next {

		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
			String s = "null";
			System.out.print(" "+sat.choicePoint()+" -> ");
			if (value!=null) {
				if (value==true_) {
					satisfiable = true; s="true";
				} else {
					SBDDEntry e = state.getEntry(value);
					currentState.addNext(e);
					s = value.toString(); s = Integer.toString(e.id)+":"+s;
					if (e.expanded) {
						// skip
					} else 	{
						queue.add(e); e.expanded = true;
						s = "!"+s;
					} 
				}
			} else {
				falsfiable = true;
			}
			System.out.println(s);
			throw sat.backtrack;
		}
	}

	public void verify(ITLSolver n) {
		falsfiable = false;
		satisfiable = false;
		queue = new LinkedList<SBDDEntry>();
		Next allNext = verbose? new AllNextVerbose() : new AllNext();
		SBDDEntry b = state.getEntry(n);
		last = b;
		if (b.expanded) {
			// already checked
			System.out.println("   already checked.");
			return;
		}
		queue.add(b); b.expanded = true;
		for(SBDDEntry e;(e = queue.poll())!=null; ) {
			System.out.println(e.id+":"+(verbose?e.key+"->":"")); 
			currentState = e;
			develop(e.key, allNext);
			if (!verbose) System.out.println();
		}
		if (verbose) {
			if (!falsfiable) {
				System.out.println("valid");
			}
			if (!satisfiable) {
				System.out.println("unsatisfiable");
			}
		}
	}
	
}