From 1f69c464c78b106f89d84c1c5f3209fb1e48ed12 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Thu, 18 Dec 2003 19:23:26 +0000
Subject: [PATCH] Updates

---
 .../MCC/IR/ComparisonPredicate.java           |   4 +
 Repair/RepairCompiler/MCC/IR/Conjunction.java |  43 +++++++
 Repair/RepairCompiler/MCC/IR/Constraint.java  |   4 +-
 .../RepairCompiler/MCC/IR/DNFConstraint.java  |  76 +++++++++++
 Repair/RepairCompiler/MCC/IR/DNFExpr.java     |  19 +++
 .../RepairCompiler/MCC/IR/DNFPredicate.java   |  21 ++++
 Repair/RepairCompiler/MCC/IR/DNFRule.java     |  76 +++++++++++
 .../MCC/IR/DependencyBuilder.java             |   2 +-
 Repair/RepairCompiler/MCC/IR/Expr.java        |   4 +
 .../RepairCompiler/MCC/IR/ExprPredicate.java  |   5 +-
 .../RepairCompiler/MCC/IR/ImplicitSchema.java | 119 ++++++++++++++++++
 .../MCC/IR/InclusionPredicate.java            |  15 ++-
 .../RepairCompiler/MCC/IR/LogicStatement.java |  16 ++-
 Repair/RepairCompiler/MCC/IR/OpExpr.java      |  17 +++
 Repair/RepairCompiler/MCC/IR/Optimizer.java   |   1 -
 Repair/RepairCompiler/MCC/IR/Predicate.java   |   4 +
 .../MCC/IR/RuleConjunction.java               |  43 +++++++
 .../MCC/IR/SemanticChecker.java               |   5 +-
 Repair/RepairCompiler/MCC/IR/SetAnalysis.java |  76 +++++++++++
 .../MCC/IR/SizeofPredicate.java               |  23 ++++
 Repair/RepairCompiler/MCC/IR/Termination.java |  93 ++++++++++++++
 21 files changed, 657 insertions(+), 9 deletions(-)
 create mode 100755 Repair/RepairCompiler/MCC/IR/Conjunction.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/DNFConstraint.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/DNFExpr.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/DNFPredicate.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/DNFRule.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/RuleConjunction.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/SetAnalysis.java
 create mode 100755 Repair/RepairCompiler/MCC/IR/Termination.java

diff --git a/Repair/RepairCompiler/MCC/IR/ComparisonPredicate.java b/Repair/RepairCompiler/MCC/IR/ComparisonPredicate.java
index 54b64ad..63390e9 100755
--- a/Repair/RepairCompiler/MCC/IR/ComparisonPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/ComparisonPredicate.java
@@ -34,6 +34,10 @@ public class ComparisonPredicate extends Predicate {
         return v;
     }
 
+    public int[] getRepairs(boolean negated) {
+	return new int[] {AbstractRepair.MODIFYRELATION};
+    }
+
     public void generate(CodeWriter writer, VarDescriptor vd) {
         // get (first) value for quantifer.relation ... then do comparison with expr... 
         // can this be maybe? i guess if quantifer.relation is empty
diff --git a/Repair/RepairCompiler/MCC/IR/Conjunction.java b/Repair/RepairCompiler/MCC/IR/Conjunction.java
new file mode 100755
index 0000000..82e115f
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/Conjunction.java
@@ -0,0 +1,43 @@
+package MCC.IR;
+import java.util.*;
+
+public class Conjunction {
+
+    Vector predicates;
+    public Conjunction(DNFPredicate pred) {
+	predicates=new Vector();
+	predicates.add(pred);
+    }
+    Conjunction(Vector preds){
+	predicates=preds       ;
+    }
+
+    int size() {
+	return predicates.size();
+    }
+    
+    DNFPredicate get(int i) {
+	return (DNFPredicate) predicates.get(i);
+    }
+
+    void add(DNFPredicate dp) {
+	predicates.add(dp);
+    }
+
+    public Conjunction append(Conjunction c) {
+	Conjunction copy=copy();
+	for(int i=0;i<c.size();i++) {
+	    copy.add(new DNFPredicate(c.get(i)));
+	}
+	return copy;
+    }
+
+    public Conjunction copy() {
+	Vector vector=new Vector();
+	for (int i=0;i<size();i++) {
+	    DNFPredicate dp=get(i);
+	    vector.add(new DNFPredicate(dp));
+	}
+	return new Conjunction(vector);
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/Constraint.java b/Repair/RepairCompiler/MCC/IR/Constraint.java
index 852313a..97a2c24 100755
--- a/Repair/RepairCompiler/MCC/IR/Constraint.java
+++ b/Repair/RepairCompiler/MCC/IR/Constraint.java
@@ -11,7 +11,7 @@ public class Constraint {
     SymbolTable st = new SymbolTable();
     Vector quantifiers = new Vector(); 
     LogicStatement logicstatement = null;
-
+    DNFConstraint dnfconstraint;
     int num;
 
     public Constraint() {
@@ -37,6 +37,8 @@ public class Constraint {
 
     public void setLogicStatement(LogicStatement ls) {
         logicstatement = ls;
+	// Construct DNF form for analysis
+	dnfconstraint=logicstatement.constructDNF();
     }
 
     public LogicStatement getLogicStatement() {
diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
new file mode 100755
index 0000000..1f3849f
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
@@ -0,0 +1,76 @@
+package MCC.IR;
+import java.util.*;
+
+public class DNFConstraint {
+   Vector conjunctions;
+
+    public DNFConstraint(Predicate p) {
+	conjunctions=new Vector();
+	conjunctions.add(new Conjunction(new DNFPredicate(true,p)));
+    }
+
+    public DNFConstraint(Conjunction conj) {
+	conjunctions=new Vector();
+	conjunctions.add(conj);
+    }
+
+    public DNFConstraint(Vector conj) {
+	conjunctions=conj;
+    }
+    
+    DNFConstraint() {
+	conjunctions=new Vector();
+    }
+
+    int size() {
+	return conjunctions.size();
+    }
+
+    Conjunction get(int i) {
+	return (Conjunction)conjunctions.get(i);
+    }
+
+    void add(Conjunction c) {
+	conjunctions.add(c);
+    }
+
+    public DNFConstraint copy() {
+	Vector vector=new Vector();
+	for (int i=0;i<size();i++) {
+	    vector.add(get(i).copy());
+	}
+	return new DNFConstraint(vector);
+    }
+
+    public DNFConstraint and(DNFConstraint c) {
+	DNFConstraint newdnf=new DNFConstraint();
+	for(int i=0;i<size();i++) {
+	    for(int j=0;j<c.size();j++) {
+		newdnf.add(get(i).append(c.get(j))); //Cross product
+	    }
+	}
+	return newdnf;
+    }
+
+    public DNFConstraint or(DNFConstraint c) {
+	DNFConstraint copy=copy();
+	for(int i=0;i<c.size();i++) {
+	    copy.add(c.get(i).copy()); //Add in other conjunctions
+	}
+	return copy;
+    }
+
+    public DNFConstraint not() {
+	DNFConstraint copy=copy();
+	for (int i=0;i<size();i++) {
+	    Conjunction conj=get(i);
+	    for (int j=0;j<conj.size();j++) {
+		DNFPredicate dp=conj.get(j);
+		dp.negatePred();
+	    }
+	}
+	return copy;
+   }
+}
+
+
diff --git a/Repair/RepairCompiler/MCC/IR/DNFExpr.java b/Repair/RepairCompiler/MCC/IR/DNFExpr.java
new file mode 100755
index 0000000..ce039db
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/DNFExpr.java
@@ -0,0 +1,19 @@
+package MCC.IR;
+
+public class DNFExpr {
+    boolean negate;
+    Expr predicate;
+
+    public DNFExpr(DNFExpr dp) {
+	this.negate=dp.negate;
+	this.predicate=dp.predicate;
+    }
+
+    public DNFExpr(boolean negate,Expr predicate) {
+	this.negate=negate;
+	this.predicate=predicate;
+    }
+    void negatePred() {
+	negate=!negate;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/DNFPredicate.java b/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
new file mode 100755
index 0000000..2328bfc
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
@@ -0,0 +1,21 @@
+package MCC.IR;
+
+public class DNFPredicate {
+    boolean negate;
+    Predicate predicate;
+
+    public DNFPredicate(DNFPredicate dp) {
+	this.negate=dp.negate;
+	this.predicate=dp.predicate;
+    }
+    Predicate getPredicate() {
+	return predicate;
+    }
+    public DNFPredicate(boolean negate,Predicate predicate) {
+	this.negate=negate;
+	this.predicate=predicate;
+    }
+    void negatePred() {
+	negate=!negate;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/DNFRule.java b/Repair/RepairCompiler/MCC/IR/DNFRule.java
new file mode 100755
index 0000000..942f7f6
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/DNFRule.java
@@ -0,0 +1,76 @@
+package MCC.IR;
+import java.util.*;
+
+public class DNFRule {
+   Vector ruleconjunctions;
+
+    public DNFRule(Expr e) {
+	ruleconjunctions=new Vector();
+	ruleconjunctions.add(new RuleConjunction(new DNFExpr(true,e)));
+    }
+
+    public DNFRule(RuleConjunction conj) {
+	ruleconjunctions=new Vector();
+	ruleconjunctions.add(conj);
+    }
+
+    public DNFRule(Vector conj) {
+	ruleconjunctions=conj;
+    }
+    
+    DNFRule() {
+	ruleconjunctions=new Vector();
+    }
+
+    int size() {
+	return ruleconjunctions.size();
+    }
+
+    RuleConjunction get(int i) {
+	return (RuleConjunction)ruleconjunctions.get(i);
+    }
+
+    void add(RuleConjunction c) {
+	ruleconjunctions.add(c);
+    }
+
+    public DNFRule copy() {
+	Vector vector=new Vector();
+	for (int i=0;i<size();i++) {
+	    vector.add(get(i).copy());
+	}
+	return new DNFRule(vector);
+    }
+
+    public DNFRule and(DNFRule c) {
+	DNFRule newdnf=new DNFRule();
+	for(int i=0;i<size();i++) {
+	    for(int j=0;j<c.size();j++) {
+		newdnf.add(get(i).append(c.get(j))); //Cross product
+	    }
+	}
+	return newdnf;
+    }
+
+    public DNFRule or(DNFRule c) {
+	DNFRule copy=copy();
+	for(int i=0;i<c.size();i++) {
+	    copy.add(c.get(i).copy()); //Add in other conjunctions
+	}
+	return copy;
+    }
+
+    public DNFRule not() {
+	DNFRule copy=copy();
+	for (int i=0;i<size();i++) {
+	    RuleConjunction conj=get(i);
+	    for (int j=0;j<conj.size();j++) {
+		DNFExpr dp=conj.get(j);
+		dp.negatePred();
+	    }
+	}
+	return copy;
+   }
+}
+
+
diff --git a/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java b/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
index babdd0e..c913a26 100755
--- a/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
+++ b/Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
@@ -79,7 +79,7 @@ public class DependencyBuilder {
                         otherrulenode.addEdge(new GraphNode.Edge(d.getSymbol(), rulenode));
                     }
                 }
-            }           
+            }
         }
 
         /* build constraint->rule dependencies */
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 1e7fd14..cd82227 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -25,4 +25,8 @@ public abstract class Expr {
         throw new IRException("unsupported");
     }
 
+    public DNFRule constructDNF() {
+	return new DNFRule(this);
+    }
+
 }
diff --git a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
index 4508867..3242de1 100755
--- a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
@@ -25,6 +25,9 @@ public class ExprPredicate extends Predicate {
     public void generate(CodeWriter writer, VarDescriptor dest) {
         expr.generate(writer, dest);
     }
-            
+
+    public int[] getRepairs(boolean negated) {
+	return new int[] {};
+    }
 }
     
diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
new file mode 100755
index 0000000..adea1ff
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -0,0 +1,119 @@
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+public class ImplicitSchema {
+    State state;
+    SetAnalysis setanalysis;
+    public ImplicitSchema(State state) {
+	this.state=state;
+	this.setanalysis=new SetAnalysis(state);
+    }
+
+    public void update() {
+	updaterules();
+	updateconstraints();
+	updaterelationconstraints();
+    }
+
+    void updaterelationconstraints() {
+	Vector reldescriptors=state.stRelations.getAllDescriptors();
+	for(int i=0;i<reldescriptors.size();i++) {
+	    RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
+	    Constraint c=new Constraint();
+	    
+	    /* Construct quantifier */
+	    RelationQuantifier rq=new RelationQuantifier();
+	    String varname1=new String("partitionvar1");
+	    String varname2=new String("partitionvar2");
+	    VarDescriptor var1=new VarDescriptor(varname1);
+	    VarDescriptor var2=new VarDescriptor(varname2);
+	    c.getSymbolTable().add(var1);
+	    c.getSymbolTable().add(var2);
+	    var1.setType(rd.getDomain().getType());
+	    var2.setType(rd.getRange().getType());
+	    rq.setTuple(var1,var2);
+	    rq.setRelation(rd);
+	    c.addQuantifier(rq);
+
+	    VarExpr ve1=new VarExpr(varname1);
+	    SetExpr se1=new SetExpr(rd.getDomain());
+	    LogicStatement incpred1=new InclusionPredicate(ve1,se1);
+
+	    VarExpr ve2=new VarExpr(varname2);
+	    SetExpr se2=new SetExpr(rd.getRange());
+	    LogicStatement incpred2=new InclusionPredicate(ve2,se2);
+	    c.setLogicStatement(new LogicStatement(LogicStatement.AND,incpred1,incpred2));
+	    state.vConstraints.add(c);
+	}
+    }
+
+    void updateconstraints() {
+	Vector setdescriptors=state.stSets.getAllDescriptors();
+	for(int i=0;i<setdescriptors.size();i++) {
+	    SetDescriptor sd=(SetDescriptor) setdescriptors.get(i);
+	    if(sd.isPartition()) {
+		Constraint c=new Constraint();
+
+		/* Construct quantifier */
+		SetQuantifier sq=new SetQuantifier();
+		String varname=new String("partitionvar");
+		VarDescriptor var=new VarDescriptor(varname);
+		c.getSymbolTable().add(var);
+		var.setType(sd.getType());
+		sq.setVar(var);
+		sq.setSet(sd);
+		c.addQuantifier(sq);
+
+		/*Construct logic statement*/
+		LogicStatement ls=null;
+		for(int j=0;j<sd.getSubsets().size();j++) {
+		    LogicStatement conj=null;
+		    for(int k=0;k<sd.getSubsets().size();k++) {
+			VarExpr ve=new VarExpr(varname);
+			SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
+			LogicStatement incpred=new InclusionPredicate(ve,se);
+			if (j!=k) {
+			    incpred=new LogicStatement(LogicStatement.NOT ,incpred);
+			}
+			if (conj==null)
+			    conj=incpred;
+			else 
+			    conj=new LogicStatement(LogicStatement.AND, conj, incpred);
+		    }
+		    if (ls==null)
+			ls=conj;
+		    else 
+			ls=new LogicStatement(LogicStatement.OR, ls, conj);
+		}
+		c.setLogicStatement(ls);
+		state.vConstraints.add(c);
+	    }
+	}
+    }
+    
+    void updaterules() {
+	Vector oldrules=state.vRules;
+	Vector newrules=new Vector();
+	for(int i=0;i<oldrules.size();i++) {
+	    Rule r=(Rule)oldrules.get(i);
+	    if (r.inclusion instanceof SetInclusion) {
+		SetDescriptor sd=((SetInclusion)r.inclusion).getSet();
+		Set supersets=setanalysis.getSuperset(sd);
+		if (supersets!=null)
+		    for(Iterator superit=supersets.iterator();superit.hasNext();) {
+			SetDescriptor sd1=(SetDescriptor)superit.next();
+			Rule nr=new Rule();
+			nr.guard=r.guard;
+			nr.quantifiers=r.quantifiers;
+			nr.isstatic=r.isstatic;
+			nr.isdelay=r.isdelay;
+			nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
+			nr.st=r.st;
+			newrules.add(nr);
+		    }
+	    }
+	}
+	oldrules.addAll(newrules);
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
index fd4d8ff..26b9f4a 100755
--- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
@@ -40,6 +40,19 @@ public class InclusionPredicate extends Predicate {
         //set.addAll(expr.getInversedRelations());
         //return set;
     }
-            
+
+    public int[] getRepairs(boolean negated) {
+	if (setexpr instanceof ImageSetExpr) {
+	    if (negated)
+		return new int[] {AbstractRepair.REMOVEFROMRELATION};
+	    else
+		return new int[] {AbstractRepair.ADDTORELATION};
+	} else {
+	    if (negated)
+		return new int[] {AbstractRepair.REMOVEFROMSET};
+	    else
+		return new int[] {AbstractRepair.ADDTOSET};
+	}
+    }
 }
     
diff --git a/Repair/RepairCompiler/MCC/IR/LogicStatement.java b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
index 9c3a1ed..6667422 100755
--- a/Repair/RepairCompiler/MCC/IR/LogicStatement.java
+++ b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
@@ -12,7 +12,6 @@ public class LogicStatement {
         if (left == null) {
             throw new IRException();
         }
-
         Set set = left.getInversedRelations();
         if (right != null) {
             set.addAll(right.getInversedRelations());
@@ -20,6 +19,21 @@ public class LogicStatement {
         return set;
     }
     
+    public DNFConstraint constructDNF() {
+	if (op==AND) {
+	    DNFConstraint leftd=left.constructDNF();
+	    DNFConstraint rightd=right.constructDNF();
+	    return leftd.and(rightd);
+	} else if (op==OR) {
+	    DNFConstraint leftd=left.constructDNF();
+	    DNFConstraint rightd=right.constructDNF();
+	    return leftd.or(rightd);
+	} else if (op==NOT) {
+	    DNFConstraint leftd=left.constructDNF();
+	    return leftd.not();
+	} else throw new Error();
+    }
+
     public static class Operation {
         private final String name;
         private Operation(String opname) { name = opname; }
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 315c9fa..b576cbd 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -16,6 +16,23 @@ public class OpExpr extends Expr {
         assert (right == null && opcode == Opcode.NOT) || (right != null);
     }
 
+    public DNFRule constructDNF() {
+        if (opcode==Opcode.AND) {
+            DNFRule leftd=left.constructDNF();
+            DNFRule rightd=right.constructDNF();
+            return leftd.and(rightd);
+        } else if (opcode==Opcode.OR) {
+            DNFRule leftd=left.constructDNF();
+            DNFRule rightd=right.constructDNF();
+            return leftd.or(rightd);
+        } else if (opcode==Opcode.NOT) {
+            DNFRule leftd=left.constructDNF();
+            return leftd.not();
+        } else throw new Error();
+    }
+
+
+
     public Set getInversedRelations() {
         Set set = left.getInversedRelations();
         if (right != null) {
diff --git a/Repair/RepairCompiler/MCC/IR/Optimizer.java b/Repair/RepairCompiler/MCC/IR/Optimizer.java
index 9b739ff..ec465a4 100755
--- a/Repair/RepairCompiler/MCC/IR/Optimizer.java
+++ b/Repair/RepairCompiler/MCC/IR/Optimizer.java
@@ -6,7 +6,6 @@ import java.util.*;
 public class Optimizer {
 
     State state;
-
     public Optimizer(State s) {
         state = s;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/Predicate.java b/Repair/RepairCompiler/MCC/IR/Predicate.java
index 6c1539e..7ab2179 100755
--- a/Repair/RepairCompiler/MCC/IR/Predicate.java
+++ b/Repair/RepairCompiler/MCC/IR/Predicate.java
@@ -4,5 +4,9 @@ import java.util.*;
 
 public abstract class Predicate extends LogicStatement {
     protected Predicate() {}
+    public DNFConstraint constructDNF() {
+	return new DNFConstraint(this);
+    }
+    public int[] getRepairs(boolean negated) {}
 }
     
diff --git a/Repair/RepairCompiler/MCC/IR/RuleConjunction.java b/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
new file mode 100755
index 0000000..c1aa03b
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
@@ -0,0 +1,43 @@
+package MCC.IR;
+import java.util.*;
+
+public class RuleConjunction {
+
+    Vector predicates;
+    public RuleConjunction(DNFExpr pred) {
+	predicates=new Vector();
+	predicates.add(pred);
+    }
+    RuleConjunction(Vector preds){
+	predicates=preds       ;
+    }
+
+    int size() {
+	return predicates.size();
+    }
+    
+    DNFExpr get(int i) {
+	return (DNFExpr) predicates.get(i);
+    }
+
+    void add(DNFExpr dp) {
+	predicates.add(dp);
+    }
+
+    public RuleConjunction append(RuleConjunction c) {
+	RuleConjunction copy=copy();
+	for(int i=0;i<c.size();i++) {
+	    copy.add(new DNFExpr(c.get(i)));
+	}
+	return copy;
+    }
+
+    public RuleConjunction copy() {
+	Vector vector=new Vector();
+	for (int i=0;i<=size();i++) {
+	    DNFExpr dp=get(i);
+	    vector.add(new DNFExpr(dp));
+	}
+	return new RuleConjunction(vector);
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index ae6b665..265663c 100755
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -389,8 +389,8 @@ public class SemanticChecker {
         }
 
         /* do any post checks... (type constraints, etc?) */
-         
-        return ok;
+
+	return ok;
     }
 
     private boolean parse_constraint(ParseNode pn) {
@@ -527,7 +527,6 @@ public class SemanticChecker {
         } else {
             throw new IRException("not supported yet");
         }
-
     }
 
     private LogicStatement parse_body(ParseNode pn) {
diff --git a/Repair/RepairCompiler/MCC/IR/SetAnalysis.java b/Repair/RepairCompiler/MCC/IR/SetAnalysis.java
new file mode 100755
index 0000000..7717ca6
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/SetAnalysis.java
@@ -0,0 +1,76 @@
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+public class SetAnalysis {
+    State state;
+    Hashtable intersection;
+    Hashtable subset;
+    Hashtable superset;
+
+    public SetAnalysis(State state) {
+	this.state=state;
+	intersection=new Hashtable();
+	subset=new Hashtable();
+	superset=new Hashtable();
+	doanalysis();
+    }
+
+    public Set getSuperset(SetDescriptor set1) {
+	return (Set)superset.get(set1);
+    }
+
+    public boolean isSubset(SetDescriptor set1, SetDescriptor set2) {
+	return subset.contains(set1)&&((Set)subset.get(set1)).contains(set2);
+    }
+
+    public boolean noIntersection(SetDescriptor set1, SetDescriptor set2) {
+	return intersection.contains(set1)&&((Set)intersection.get(set1)).contains(set2);
+    }
+    
+    void doanalysis() {
+	SymbolTable sets=state.stSets;
+	Vector descriptors=sets.getAllDescriptors();
+	for(int i=0;i<descriptors.size();i++) {
+	    SetDescriptor sd=(SetDescriptor)descriptors.get(i);
+	    Stack st=new Stack();
+	    st.addAll(sd.getSubsets());
+	    while(!st.empty()) {
+		SetDescriptor subsetsd=(SetDescriptor)st.pop();
+		System.out.print(subsetsd.toString());
+
+		st.addAll(subsetsd.getSubsets());
+		if (!subset.contains(sd))
+		    subset.put(sd,new HashSet());
+		((HashSet)subset.get(sd)).addAll(subsetsd.getSubsets());
+		for(Iterator it=subsetsd.getSubsets().iterator();it.hasNext();) {
+		    SetDescriptor sd2=(SetDescriptor)it.next();
+		    if (!superset.contains(sd2))
+			superset.put(sd2,new HashSet());
+		    ((HashSet)superset.get(sd2)).add(sd);
+		}
+	    }
+	}
+	for(int i=0;i<descriptors.size();i++) {
+	    SetDescriptor sd=(SetDescriptor)descriptors.get(i);
+	    if (sd.isPartition()) {
+		Vector subst=sd.getSubsets();
+		for(Iterator it1=subst.iterator();it1.hasNext();) {
+		    SetDescriptor sd1=(SetDescriptor)it1.next();
+		    for(Iterator it2=subst.iterator();it2.hasNext();) {
+			SetDescriptor sd2=(SetDescriptor)it2.next();
+			if (sd1!=sd2) {
+			    for(Iterator it3=sd1.allSubsets().iterator();it3.hasNext();) {
+				SetDescriptor sd3=(SetDescriptor)it3.next();
+				
+				if (!intersection.contains(sd3))
+				    intersection.put(sd3,new HashSet());
+				((HashSet)intersection.get(sd3)).addAll(sd2.allSubsets());
+			    }
+			}
+		    }
+		}
+	    }
+	}
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/SizeofPredicate.java b/Repair/RepairCompiler/MCC/IR/SizeofPredicate.java
index fee9795..4d375ac 100755
--- a/Repair/RepairCompiler/MCC/IR/SizeofPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/SizeofPredicate.java
@@ -22,6 +22,29 @@ public class SizeofPredicate extends Predicate {
         this.cardinality = cardinality;
     }
 
+    public int[] getRepairs(boolean negated) {
+	if (setexpr instanceof ImageSetExpr) {
+	    if (opcode==Opcode.EQ)
+		return new int[] {AbstractRepair.ADDTORELATION,
+				      AbstractRepair.REMOVEFROMRELATION};
+	    if (((opcode==Opcode.GE)&&!negated)||
+		((opcode==Opcode.LE)&&negated))
+		return new int[]{AbstractRepair.ADDTORELATION};
+	    else
+		return new int[]{AbstractRepair.REMOVEFROMRELATION};
+	} else {
+	    if (opcode==Opcode.EQ)
+		return new int[] {AbstractRepair.ADDTOSET,
+				      AbstractRepair.REMOVEFROMSET};
+
+	    if (((opcode==Opcode.GE)&&!negated)||
+		((opcode==Opcode.LE)&&negated))
+		return new int[] {AbstractRepair.ADDTOSET};
+	    else 
+		return new int[] {AbstractRepair.REMOVEFROMSET};
+	}
+    }
+
     public Set getRequiredDescriptors() {
         assert setexpr != null;
         Set v = setexpr.getRequiredDescriptors();
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
new file mode 100755
index 0000000..14d144a
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -0,0 +1,93 @@
+package MCC.IR;
+import java.util.*;
+
+class Termination {
+    HashSet conjunctions;
+    Hashtable conjunctionmap;
+
+    HashSet abstractrepair;
+
+    State state;
+
+    public Termination(State state) {
+	this.state=state;
+	generateconjunctionnodes();
+	generaterepairnodes();
+    }
+    
+    void generateconjunctionnodes() {
+	Vector constraints=state.vConstraints;
+	for(int i=0;i<constraints.size();i++) {
+	    Constraint c=(Constraint)constraints.get(i);
+	    DNFConstraint dnf=c.dnfconstraint;
+	    for(int j=0;j<dnf.size();j++) {
+		TermNode tn=new TermNode(c,dnf.get(j));
+		GraphNode gn=new GraphNode("Conjunction"+i+","+j,tn);
+		conjunctions.add(gn);
+		conjunctionmap.put(c,gn);
+	    }
+	}
+    }
+
+    void generaterepairnodes() {
+	for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
+	    GraphNode gn=(GraphNode)conjiterator.next();
+	    TermNode tn=(TermNode)gn.getOwner();
+	    Conjunction conj=tn.getConjunction();
+	    for(int i=0;i<conj.size();i++) {
+		DNFPredicate dp=conj.get(i);
+		int[] array=dp.getPredicate().getRepairs();
+		for {int j=0;j<array.length;j++) {
+		    AbstractRepair ar=new AbstractRepair(dp,array[j]);
+		    TermNode tn=new TermNode(ar);
+		    GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn);
+		    Edge e=new Edge("abstract",gn2);
+		    gn.addEdge(e);
+		    abstractrepair.add(gn2);
+		}
+	    }
+	}
+    }
+}
+
+class AbstractRepair {
+    public final static int ADDTOSET=1;
+    public final static int REMOVEFROMSET=2;
+    public final static int ADDTORELATION=3;
+    public final static int REMOVEFROMRELATION=4;
+    public final static int MODIFYRELATION=5;
+
+    DNFPredicate torepair;
+    int type;
+
+    public AbstractRepair(DNFPredicate dp,int typ) {
+	torepair=dp;
+	type=typ;
+    }
+}
+
+class TermNode {
+    public final static int CONJUNCTION=1;
+    public final static int ABSTRACT=2;
+
+    Constraint constr;
+    Conjunction conj;
+    int type;
+    AbstractRepair repair;
+
+    public TermNode(Constraint constr, Conjunction conj) {
+	this.constr=constr;
+	this.conj=conj;
+	type=CONJUNCTION;
+    }
+
+    public TermNode(AbstractRepair ar) {
+	repair=ar;
+	type=ABSTRACT;
+    }
+
+    public Conjunction getConjunction() {
+	return conj;
+    }
+}
+
-- 
2.34.1