/*******************************************************************************
 * Copyright (c) 2009 Elliott Baron
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *    Elliott Baron - initial API and implementation
 *******************************************************************************/
package org.eclipse.cdt.codan.extension;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import org.eclipse.cdt.core.dom.ast.IVariable;

public class ExecutionState {
	private List<ExecutionStateClause> clauses;
	private Map<IVariable, Boolean> truthAssignments;
	private boolean top;
	private boolean bottom;

	public ExecutionState() {
		truthAssignments = new HashMap<IVariable, Boolean>();
		clauses = new ArrayList<ExecutionStateClause>();
		top = true;
		bottom = false;
	}
	
	public void addClause(ExecutionStateClause clause) {
		// Cannot get out of bottom, do not add duplicate clauses
		if (!bottom && !clauses.contains(clause)) {
			top = false; // T AND x = x
			if (clauses.contains(clause.getNegation())) {
				clauses.clear();
				bottom = true; // x AND NOT x = F
			}
			else {
				clauses.add(clause);
			}
		}
	}
	
	public void removeClause(ExecutionStateClause node) {
		clauses.remove(node);
		if (clauses.size() == 0) {
			setTop();
		}
	}
	
	public void addTruthAssignment(IVariable var, boolean value) {
		truthAssignments.put(var, value);
	}
	
	public Map<IVariable, Boolean> getTruthAssignments() {
		return truthAssignments;
	}
	
	public void setTruthAssignments(Map<IVariable, Boolean> truthAssignments) {
		this.truthAssignments = truthAssignments;
	}
	
	public void bindTruthAssignments() {
		boolean unsatisfiable = false;
		List<ExecutionStateClause> clausesCopy = new ArrayList<ExecutionStateClause>(clauses);
		for (ExecutionStateClause c : clausesCopy) {
			Boolean truth = truthAssignments.get(c.getVariable());
			if (truth != null) {
				if (truth == c.isTrue()) { // does truth value of clause match truth assignment?
					removeClause(c);
				}
				else {
					unsatisfiable = true;
				}
			}
		}
		
		if (unsatisfiable) {
			setBottom();
		}
	}
	
	//FIXME
	public ExecutionState join(ExecutionState other) {
		// Add clauses from other, canceling out negating clauses
		for (ExecutionStateClause clause : other.getClauses()) {
			ExecutionStateClause negation = clause.getNegation();
			if (clauses.contains(negation)) {
				removeClause(negation);
				other.removeClause(clause);
			}
		}
		return this;
	}
	
	public ExecutionStateClause[] getClauses() {
		return clauses.toArray(new ExecutionStateClause[clauses.size()]);
	}
	
	public boolean isTop() {
		return top;
	}
	
	public boolean isBottom() {
		return bottom;
	}
	
	public void setTop() {
		top = true;
		bottom = false;
		clauses.clear();
	}
	
	public void setBottom() {
		bottom = true;
		top = false;
		clauses.clear();
	}
	
	@Override
	public String toString() {
		String ret;
		if (top) {
			ret = "[TOP]";
		}
		else if (bottom) {
			ret = "[BOTTOM]";
		}
		else {
			StringBuffer buf = new StringBuffer();
			if (clauses.size() > 0) {
				for (ExecutionStateClause c : clauses) {
					buf.append(c);
					buf.append(" AND ");
				}
				buf.delete(buf.length() - 5 /* " AND ".length() */, buf.length());
			}
			ret = buf.toString();
		}
		return ret;
	}

}