package lite;

import verifier.Backtrack;

public class ITLSolverTest {

	static ITLNodeParser p;
	static ITLNodeScanner<ITLSolver> scan;
	
	private ITLSatisfier sat;
	private ITLNodeParser parser;
	
	public static void main(String arg[]) {
		ITLNodeFactoryInterface<ITLSolver> lf = new ITLNodeFactory();
		
		p = new ITLNodeParser(lf);
		
		System.out.println(p.parse("p , ~ q"));
		System.out.println(p.parse("p=q"));
		System.out.println(p.parse("p & q"));
		System.out.println(p.parse("p & @q"));
		System.out.println(p.parse("<>(p)"));
		System.out.println(p.parse("[](p)"));
		System.out.println(p.parse("empty & q"));
		System.out.println(p.parse("fin(p) = [](<>(p))"));
		System.out.println(p.parse("length(3)"));
		System.out.println(p.parse("[](more)"));

		sat("false");
		sat("true");
		
		sat("@p");
		sat("@p&q");
		sat("p& @(q)");
		sat("proj(@p,@q)");
		
		ITLSolverTest test = new ITLSolverTest();
		
		test.showAllNext("p&q");
		test.showAllNext("true&q");
		test.showAllNext("~(true& ~q)");
		test.showAllNext("proj(length(3),<>(p))");

	}
	
	ITLSolverTest() {
		ITLNodeFactoryInterface<ITLSolver> lf = new ITLNodeFactory();
		parser =new ITLNodeParser(lf);
		sat = new ITLSatisfier(parser.emptyNode);
	}

	
	public static void sat(String expr) {
		ITLSolver n,result;
		n = p.parse(expr);
		if (n!=null) {
			ITLSatisfier sat = new ITLSatisfier(p.emptyNode);

			System.out.print(n);

			if ((result=sat.satisfiable(n))!=null) {
				System.out.println(" is satisfiable on next="+result);
			} else {
				System.out.println(" is unsatisfiable.");
			}
		} else {
			System.out.println("can't parse '"+expr+"'.");
		}
	}

	public void showAllNext(String s) {
		ITLSolver n = p.parse(s);
		System.out.println(n);
		sat.develop(n, new Print());
		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;
		}
	}
}