Mercurial > hg > Applications > JavaLite
view src/lite/ITLSolverTest.java @ 107:30e74062f06c continuation-removal
*** empty log message ***
author | kono |
---|---|
date | Sun, 20 Jan 2008 18:22:55 +0900 |
parents | bf35bebd55ab |
children |
line wrap: on
line source
package lite; import parser.ITLNodeParser; import parser.ITLNodeScanner; public class ITLSolverTest { static ITLNodeParser<ITLSolver> p; static ITLNodeScanner<ITLSolver> scan; private ITLSatisfier sat; private ITLNodeParser<ITLSolver> parser; public static void main(String arg[]) { ITLNodeFactoryInterface<ITLSolver> lf = new ITLNodeFactory(); p = new ITLNodeParser<ITLSolver>(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<ITLSolver>(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, ITLSolver value) throws Backtrack { System.out.println(" "+sat.choicePoint()+" -> "+value); throw sat.backtrack; } } }