package sbdd;

import java.util.Comparator;
import java.util.LinkedList;
import java.util.TreeSet;

public class BDDDiagnosis {

	/*
	 * Search over generated SBDDEntry for satisfiability.
	 * find example or counter example.
	 * 
	 * For each tested SBDDEntry, Reachable set of SBDDEntry is necessary.
	 * It is stored in TreeSet in generated order.
	 */
	
	private BDDSatisfier sat;
	private SBDDEntry true_;
	private SBDDEntry empty_;
	private SBDDEntry false_;
	
	public TreeSet<SBDDEntry> reachable;
	public TreeSet<SBDDEntry> trueSet;
	public TreeSet<SBDDEntry> falseSet;
	private SBDDEntry last;

	public BDDDiagnosis(BDDSatisfier sat) {
		this.sat = sat;
		this.true_ = sat.getEntry(sat.true_);
		this.false_ = sat.getEntry(sat.false_);
		this.empty_ = sat.getEntry(sat.empty);
	}

	public void execute(SBDDEntry e,int length) {
		LinkedList<SBDDEntry> trace = findTrueEntry(e,length);
		show(trace);
	}
	
	public void counterExample(SBDDEntry e,int length) {
		LinkedList<SBDDEntry> trace = findFalseEntry(e,length);
		show(trace);
	}
	
	public void execute(int length) {
		LinkedList<SBDDEntry> trace = findTrueEntry(last,length);
		show(trace);
	}
	
	public void counterExample(int length) {
		LinkedList<SBDDEntry> trace = findFalseEntry(last,length);
		show(trace);
	}

	/*
	 * Show found trace. 
	 */
	private void show(LinkedList<SBDDEntry> trace) {
		if (trace.isEmpty()) return; 
		SBDDEntry last = trace.getLast();
		int i = 0;
		for(SBDDEntry e: trace) {
			if (e!=last) { 
				System.out.print(i+":"+e.id+":\t");
				// show choice point generated on the fly
				System.out.println(	sat.findNext(e,trace.get(++i)));
			}
		}
	}
	
	public void showState(SBDDEntry entry) {
		System.out.println("All Edges: "+sat.edge);
		System.out.println("Number of BDD: "+sat.sf.hash.size());
		System.out.println("Number of Subterm: "+(SBDDSet.subterms-SBDDSet.INITIAL_SUBTERMS));
		makeReachableEntry(entry);
		System.out.println("Reachable state: "+reachable.size());
		specialCase();
	}

	private LinkedList<SBDDEntry> findTrueEntry(SBDDEntry e, int length) {
		SBDDEntry dest = true_;
		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
		trace.addLast(dest);
		makeReachableEntry(e);
		if (specialCase()) return trace;
		dest = trueSet.first();
		return findMore(e,dest,length,trace);
	}

	private LinkedList<SBDDEntry> findFalseEntry(SBDDEntry e, int length) {
		SBDDEntry dest = false_;
		LinkedList<SBDDEntry> trace = new LinkedList<SBDDEntry>();
		trace.addLast(dest);
		makeReachableEntry(e);
		if (specialCase()) return trace;
		dest = falseSet.first();
		return findMore(e,dest,length,trace);
	}

	private boolean specialCase() {
		if (falseSet.isEmpty()) {
			System.out.println("valid."); return true;
		}
		if (trueSet.isEmpty()) {
			System.out.println("unsatisfiable."); return true;
		}
		return false;
	}
	
	/*
	 * find trace from an start entry to a destination. Reachable set have to
	 * be generated from the start entry.
	 */
	public LinkedList<SBDDEntry> findEntry(SBDDEntry e, SBDDEntry dest, int length, LinkedList<SBDDEntry> trace) {
		SBDDEntry small = dest;
		if (reachable.contains(dest)) {
			while(firstPrevious(small)!=e) {
				trace.addFirst(small);
			}
			trace.addFirst(e);
		}
		return trace;
	}

	/*
	 * find lengthy trace from an start entry to a destination. Reachable 
	 * set have to be generated from the start entry.
	 */
	public LinkedList<SBDDEntry> findMore(SBDDEntry e, SBDDEntry dest, int length, LinkedList<SBDDEntry> trace) {
		SBDDEntry small = dest;
		if (reachable.contains(dest)) {
			try {
				findTrace(trace,e,small,length);
			} catch (Result e1) {
				// found
				return trace;
			}
		}
		// not found
		return trace;
	}

	class sbddComparator implements Comparator<SBDDEntry>  {
		public int compare(SBDDEntry arg0, SBDDEntry arg1) {
			return arg0.id-arg1.id;
		}
	}

	public void makeReachableEntry(SBDDEntry e) {
		if (last==e) return; else last = e;
		reachable = new TreeSet<SBDDEntry>(new sbddComparator());
		trueSet   = new TreeSet<SBDDEntry>(new sbddComparator());
		falseSet  = new TreeSet<SBDDEntry>(new sbddComparator());
		if (e==null) return;
		//LinkedList<Iterable<SBDDEntry>> stack = new LinkedList<Iterable<SBDDEntry>>();
		Iterable<SBDDEntry> current = e.nexts(); 
		//stack.add(current);
		if(e.falsifiable) falseSet.add(e); 
		if(e.satisfiable) trueSet.add(e);
		reachable.add(e);
		addReachable(current);
	}


	/*
	 * Put new set of next states in reachable state set. SBDDEntry.nexts does not
	 * contains true/false.
	 */
	private void addReachable(Iterable<SBDDEntry> current) {
		if (current==null) return ;
		for(SBDDEntry s: current) {
			if (s==empty_) trueSet.add(s);
			if (reachable.add(s)) {
				// this is a new one
				if(s.falsifiable) falseSet.add(s); 
				if(s.satisfiable) trueSet.add(s);
				addReachable(s.nexts());
			}
		}
	}

	public SBDDEntry firstPrevious(SBDDEntry e) {
		// we assume reachable is sorted in generated order
		// it returns always younger entry
		for(SBDDEntry p: reachable) {
			if (p.nexts!=null&&p.nexts.contains(e)) {
				return e;
			}
		}
		return null;
	}
	
	class Result extends Exception {
		private static final long serialVersionUID = 1L;
	}

	private void findTrace(LinkedList<SBDDEntry> trace, SBDDEntry start,SBDDEntry e, int length) throws Result {
		// if (length<0) return;
		trace.addFirst(e);
		if (e==start) throw new Result();
		for(SBDDEntry p: reachable) {   // linear serach ?! should we create reverse index?
			if (trace.contains(p)) continue; 
			if (p.nexts!=null && p.nexts.contains(e)) {
				if (p==start)
					if (length<=0) throw new Result();
				findTrace(trace,start,p,length-1);
			}
		}
		trace.removeFirst(); // have to be e
	}
}