1 files changed, 75 insertions, 14 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 6f4f496..208f9f0 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
@@ -11,29 +11,89 @@
 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 node) {
-		setTop(false);
-		setBottom(false);
-		clauses.add(node);
+	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(true);
-			setBottom(false);
+			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() {
@@ -48,12 +108,16 @@ public class ExecutionState {
 		return bottom;
 	}
 	
-	public void setTop(boolean top) {
-		this.top = top;
+	public void setTop() {
+		top = true;
+		bottom = false;
+		clauses.clear();
 	}
 	
-	public void setBottom(boolean bottom) {
-		this.bottom = bottom;
+	public void setBottom() {
+		bottom = true;
+		top = false;
+		clauses.clear();
 	}
 	
 	@Override
@@ -69,10 +133,7 @@ public class ExecutionState {
 			StringBuffer buf = new StringBuffer();
 			if (clauses.size() > 0) {
 				for (ExecutionStateClause c : clauses) {
-					if (!c.isTrue()) {
-						buf.append("NOT ");
-					}
-					buf.append(c.getNode().getRawSignature());
+					buf.append(c);
 					buf.append(" AND ");
 				}
 				buf.delete(buf.length() - 5 /* " AND ".length() */, buf.length());