view src/lite/ITLCommander.java @ 67:4ced2af1ff09 bdd-order

BDD Order fix
author kono
date Sun, 13 Jan 2008 19:48:42 +0900
parents 48db54d3129b
children 416e4d272e79
line wrap: on
line source

package lite;

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;

	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) {
		this.lf = lf;
		this.parser = parser;
	}

	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") {
			if (sat==null) sat = new BDDSatisfier();
			// System.out.println(args.get(0)+":"+args.get(1));
			System.out.println(args.get(0));
			sat.verify(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") {
			if (Integer.parseInt(args.get(0).toString())==0) {
				sat.verbose = false;
			} else {
				sat.verbose = true;
			}
			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;
	}

}