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) {
		if (predicate.toString() == "length") {
			Node n = lf.emptyNode();
			int length = Integer.parseInt(args.get(0).toString());
			for(int i =0;i<length;i++) {
				n = lf.nextNode(n);
			}
			return (Node)n;
		} else if (predicate.toString() == "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 (predicate.toString() == "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 (predicate.toString() == "def") {
			parser.define(args.get(0).toString(),args.get(1).toString());
			return lf.trueNode();
		} else if (predicate.toString() == "verbose") {
			if (Integer.parseInt(args.get(0).toString())==0) {
				sat.verbose = false;
			} else {
				sat.verbose = true;
			}
			return lf.trueNode();
		} else if (predicate.toString() == "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;
	}

}