Mercurial > hg > Applications > JavaLite
view src/lite/ITLCommander.java @ 71:01356168f25f
*** empty log message ***
author | kono |
---|---|
date | Tue, 15 Jan 2008 15:25:06 +0900 |
parents | 416e4d272e79 |
children | 034c573af8ea |
line wrap: on
line source
package lite; import java.util.HashMap; import java.util.LinkedList; import sbdd.BDDSatisfier; import logicNode.parser.Command; public class ITLCommander<Node extends ITLSolver> implements Command<Node> { private ITLNodeFactoryInterface<Node> lf; private ITLNodeParser<Node> parser; public BDDSatisfier sat; private HashMap<Integer,Node> examples; public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) { this.lf = lf; this.parser = parser; this.examples = new HashMap<Integer,Node>(); } public Node exec(Node predicate, Node value, LinkedList<Node> args) { // All names used here have to be reserved. Otherwise, parser generated name becomes // different string at run time, as a result, name=="less" will fail even if name contains "less". // If we reseve it, paredicateNode.varaibleNode.name contains pregenerated String which is // equivalent to used here. Of course name.equal("less") works fine, but it is time consuming. // Although it is practically allowed but I cannot accept. // We can also define Command as internal interface class in ITLNodeParser. In this case // reserve operation is not required, like "length" macro. String name = predicate.toString(); if (name=="less") { Node n = lf.falseNode(); int length = Integer.parseInt(args.get(0).toString()); for(int i =0;i<length;i++) { n = lf.orNode(lf.emptyNode(),lf.nextNode(n)); } return (Node)n; } else if (name == "ex"|| name=="do") { checkSat(); if (args.size()<1) { parser.error("ex(1) or ex(<>p) or ex(10,[]p)"); return lf.trueNode(); } Node n = args.get(0); int index = -1; if (n.getClass()==NumberSolver.class) { index = Integer.parseInt(n.toString()); } if (args.size()==1) { // System.out.println(args.get(0)+":"+args.get(1)); if (index>=0) { n = examples.get(index); if (n==null) { parser.error("Unknown registered example"); return lf.trueNode(); } } System.out.println(n); sat.verify(n); return lf.trueNode(); } else if (args.size()==2 && index>=0){ examples.put(index, args.get(1)); return lf.trueNode(); } } else if (name == "def") { parser.define(args.get(0).toString(),args.get(1).toString()); return lf.trueNode(); } else if (name == "verbose") { // verbose(true) / verbose(off) Node n= null; checkSat(); try { int i = Integer.parseInt((n=args.get(0)).toString()); sat.verbose = (i==0)? false:true; } catch (NumberFormatException e) { sat.verbose = (n==lf.trueNode())?true:false; } return lf.trueNode(); } else if (name == "include") { String file = args.getFirst().toString(); parser.parseFile(file); return lf.trueNode(); } System.out.println("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args); return value; } private void checkSat() { if (sat==null) sat = new BDDSatisfier(); } }