1 files changed, 58 insertions, 42 deletions

diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
index 208f9f0..c19970e 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
@@ -10,26 +10,26 @@
  *******************************************************************************/
 package org.eclipse.cdt.codan.extension;
 
-import java.util.ArrayList;
 import java.util.HashMap;
-import java.util.List;
+import java.util.HashSet;
 import java.util.Map;
+import java.util.Set;
 
 import org.eclipse.cdt.core.dom.ast.IVariable;
 
 public class ExecutionState {
-	private List<ExecutionStateClause> clauses;
+	private Set<ExecutionStateClause> clauses;
 	private Map<IVariable, Boolean> truthAssignments;
 	private boolean top;
 	private boolean bottom;
 
 	public ExecutionState() {
 		truthAssignments = new HashMap<IVariable, Boolean>();
-		clauses = new ArrayList<ExecutionStateClause>();
+		clauses = new HashSet<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)) {
@@ -37,110 +37,126 @@ public class ExecutionState {
 			if (clauses.contains(clause.getNegation())) {
 				clauses.clear();
 				bottom = true; // x AND NOT x = F
-			}
-			else {
+			} 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);
+		Set<ExecutionStateClause> clausesCopy = new HashSet<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?
+				if (truth == c.isTrue()) { // does truth value of clause match
+											// truth assignment?
 					removeClause(c);
-				}
-				else {
+				} 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 static Set<ExecutionState> join(Set<ExecutionState> es) {
+		ESTruthTable tt = new ESTruthTable(es);
+		ESSimplifier simp = new ESSimplifier(tt);
+		return simp.getExecutionStateCover();
 	}
-	
-	public ExecutionStateClause[] getClauses() {
-		return clauses.toArray(new ExecutionStateClause[clauses.size()]);
+
+	public Set<ExecutionStateClause> getClauses() {
+		return clauses;
 	}
-	
+
 	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) {
+		} else if (bottom) {
 			ret = "[BOTTOM]";
-		}
-		else {
+		} 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());
+				buf.delete(buf.length() - 5 /* " AND ".length() */, buf
+						.length());
 			}
 			ret = buf.toString();
 		}
 		return ret;
 	}
 
+	public ExecutionState copy() {
+		ExecutionState ret = new ExecutionState();
+		for (ExecutionStateClause cl : clauses) {
+			ret.addClause(cl);
+		}
+		return ret;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof ExecutionState) {
+			ExecutionState other = (ExecutionState) obj;
+			return clauses.equals(other.getClauses())
+					&& truthAssignments.equals(other.getTruthAssignments())
+					&& top == other.isTop() && bottom == other.isBottom();
+		}
+		return false;
+	}
+	
+	@Override
+	public int hashCode() {
+		return clauses.hashCode() + truthAssignments.hashCode() + (top ? 1 : 0) + (bottom ? 1 : 0);
+	}
+
 }