package parser;

import lite.ITLNodeFactory;
import lite.ITLSolver;

public class LogicNodeParserTest {
	
	static MacroNodeParser<ITLSolver> parser;
	
	public static void main(String arg[]) {
		LogicNodeParser<ITLSolver> p;
		ITLSolver n;
		LogicNodeFactoryInterface<ITLSolver> lf = new ITLNodeFactory(); 
		if (true) {
		p = new LogicNodeParser<ITLSolver>("a,(b;~c)",lf);
		n = p.parse();
		if (n!=null) System.out.print(n); System.out.println(".");
		}
		
		p = new LogicNodeParser<ITLSolver>("exists(x,(a,x))",lf);
		n = p.parse();
		if (n!=null) System.out.print(n); System.out.println(".");
		
		parser = (MacroNodeParser<ITLSolver>) p;
		n = parser.parse();
		if (n!=null) System.out.print(n); System.out.println(".");
		
		sat("~exists(x,(x,b))");
		
		parser.define("forall(x,body)", "~exists(x,(~body))");
		sat("forall(a,(a,~a))");
		
		parser.define("P->Q","(not (P);Q))",300);             // imply
		sat("p->q");
		parser.define("not R","~R",50);
		sat("p->q");
		
		parser.define("P and Q", "(P,Q)",200);
		
		sat("p , q , r");
		sat("p and q and r");
		sat("p -> q and r");
		sat("p and q and r -> s");				
		sat("p and q -> r -> s");		
		sat("p -> q -> r and s");
		sat("p -> q and r and s");
	}
	
	public static void sat(String s) {
		ITLSolver n = parser.parse(s);
		if (n!=null) System.out.print(n); System.out.println(".");
	}
}