package sbdd;


import lite.BDDSolver;
import lite.ITLNodeParser;
import lite.ITLSolver;

public class SBDDTest {


	ITLNodeParser<ITLSolver> p;
	BDDSatisfier sat;
	SBDDFactory sf;
    
	public static void main(String arg[]) {

		SBDDTest test = new SBDDTest();
		
		//test.bddTest();
		//test.satTest();
		test.verifyTest();
	}
	
	SBDDTest() {
		sat = new BDDSatisfier();
		p = sat.p;
		sf = sat.sf;
	}
	
	public void bddTest() {
		bddTest("a,b,c,a");
		bddTest("a;b;c;b");
		bddTest("(a,b);(~a,b)");
		bddTest("a?b:c");
		bddTest("(true&b)?((true&empty);((true&a)?(true&empty):c)):false");
		bddTest("a?((true&empty);(b?(true&empty):c)):false");
		bddTest("a?(x;(b?x:c)):false");
		bddTest("A?(x;(B?x:C)):false");
		bddTest("A,x");
		bddTest("x,A");
	}
	
	public void bddTest(String exp) {
	    BDDSolver b;
		ITLSolver s = p.parse(exp);
		b = s.toSBDD(sf);
		System.out.println(b);
	}
	
	public void satTest() {

		sat.showAllNext("p&q");
		sat.showAllNext("true&q");
		sat.showAllNext("~(true& ~q)");
		sat.showAllNext("proj(length(3),<>(p))");
		

	}
	
	public void verifyTest() {
		// sat.showVerify("((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6)))))");

		if (false) {
		sat.showVerify("skip");
		sat.showVerify(" '<>'p");
		sat.showVerify("<>(p) = <>(p)");
		sat.showVerify("~(@(q))");
		sat.showVerify("p&q");
		// sat.showVerify("true&q");
		sat.showVerify("<>(q)");
		sat.showVerify("proj(length(3),<>(p))");
		sat.showVerify("~(true& ~q)");
		// sat.showVerify("@(@(@(empty)))");
		sat.showVerify("fin(p)=([](<>(p)))");
		sat.showVerify("fin(p)");
		sat.showVerify("all(x,@y)");
		sat.showVerify("exists(x,@@x = ~x)");
		sat.showVerify("all(x,@@x)");
		sat.showVerify("even(p)");
		sat.showVerify("Q, keep( @Q = ~Q)");
		}
		//sat.showVerify("share([a,b,c])");
		//sat.showVerify("less(3)");
		//sat.showVerify("*(a)");

		//sat.showVerify("a?(x;(b?x:c)):false");
		sat.showVerify("+(a & b)");
		//System.out.println(sat.state);
		sat.showVerify("ex(10,p)");
		sat.p.parseCommand.sat.verbose=false;
		sat.p.parse("include('data/example').");
		// System.out.println(p.parseCommand.sat.state);
	}

		
}