Mercurial > hg > Applications > JavaLite
view src/lite/ITLSolverTest.java @ 100:bf35bebd55ab
restore generic (not necearry...)
author | kono |
---|---|
date | Sat, 19 Jan 2008 10:31:19 +0900 |
parents | 5bd5c58edfd0 |
children | 30e74062f06c |
line wrap: on
line source
package lite; import verifier.Backtrack; 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, Continuation next, ITLSolver value) throws Backtrack { System.out.println(" "+sat.choicePoint()+" -> "+value); throw sat.backtrack; } } }