From d1dce81bfd31633476980542b3b301b5340d3f0d Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Wed, 28 Jul 2004 22:11:10 +0000
Subject: [PATCH] Added new file.

---
 .../MCC/IR/AbstractInterferes.java            | 35 ++++++++-------
 .../RepairCompiler/MCC/IR/AbstractRepair.java |  4 +-
 Repair/RepairCompiler/MCC/IR/ExactSize.java   | 13 +++---
 .../RepairCompiler/MCC/IR/RelationExpr.java   |  4 +-
 Repair/RepairCompiler/MCC/IR/SizeObject.java  | 43 +++++++++++++++++++
 Repair/RepairCompiler/MCC/IR/Termination.java | 16 +++----
 6 files changed, 82 insertions(+), 33 deletions(-)
 create mode 100755 Repair/RepairCompiler/MCC/IR/SizeObject.java

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 2fe4aef..a4c1ba3 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -9,8 +9,9 @@ class AbstractInterferes {
     }
 
     /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
-     * Rule r */
-    static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
+     * Rule r. */
+
+    static public boolean interfereswithrule(AbstractRepair ar, Rule r, boolean satisfy) {
 	boolean mayadd=false;
 	boolean mayremove=false;
 	switch (ar.getType()) {
@@ -60,7 +61,7 @@ class AbstractInterferes {
 
     /** Does performing the AbstractRepair ar falsify the predicate dp */
 
-    public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
+    public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
 	if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
 	    ((ar.getDescriptor() instanceof SetDescriptor)||
 	     !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
@@ -149,8 +150,6 @@ class AbstractInterferes {
 		    return false;
 	    }
 
-
-
 	    /* Translate the opcodes */
 	    op1=Opcode.translateOpcode(neg1,op1);
 	    op2=Opcode.translateOpcode(neg2,op2);
@@ -288,10 +287,10 @@ class AbstractInterferes {
 	return true;
     }
 
-    /** Does the increase (or decrease) in scope of a model defintion rule represented by sn
-     * falsify the predicate dp */
+    /** Does the increase (or decrease) in scope of a model defintion
+     * rule represented by sn falsify the predicate dp. */
 
-    public boolean interferes(ScopeNode sn, DNFPredicate dp) {
+    public boolean scopeinterfereswithpredicate(ScopeNode sn, DNFPredicate dp) {
 	if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
 	    Rule r=sn.getRule();
 	    Set target=r.getInclusion().getTargetDescriptors();
@@ -326,10 +325,10 @@ class AbstractInterferes {
 	return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
     }
 
-    /** Does increasing (or decreasing if satisfy=false) the size of the set or relation des
-     * falsify the predicate dp */
+    /** Does increasing (or decreasing if satisfy=false) the size of
+     * the set or relation des falsify the predicate dp. */
 
-    public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
+    private boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 	if ((des!=dp.getPredicate().getDescriptor()) &&
 	    ((des instanceof SetDescriptor)||
 	     !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
@@ -391,7 +390,13 @@ class AbstractInterferes {
 	return true;
     }
 
-    static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
+    /** This method test whether satisfying (or falsifying depending
+     * on the flag satisfy) a rule that adds an object(or tuple) to
+     * the set(or relation) descriptor may increase (or decrease
+     * depending on the flag satisfyrule) the scope of a constraint or
+     * model defintion rule r.  */
+
+    static private boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 	for(int i=0;i<r.numQuantifiers();i++) {
 	    Quantifier q=r.getQuantifier(i);
 	    if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
@@ -405,17 +410,17 @@ class AbstractInterferes {
 	return false;
     }
 
-    static public boolean interferes(AbstractRepair ar, Quantifiers q) {
+    static public boolean interferesquantifier(AbstractRepair ar, Quantifiers q) {
 	if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
 	    return interferesquantifier(ar.getDescriptor(),true,q,true);
 	return false;
     }
 
-    static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
+    static public boolean interfereswithquantifier(Descriptor des, boolean satisfy, Quantifiers q) {
 	return interferesquantifier(des, satisfy, q,true);
     }
 
-    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+    static public boolean interfereswithrule(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 	if (interferesquantifier(des,satisfy,r,satisfyrule))
 	    return true;
 	/* Scan DNF form */
diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
index d888849..3cb9b03 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
@@ -78,7 +78,7 @@ class AbstractRepair {
 		case ExprPredicate.COMPARISON:
 		    {
 			RelationExpr re=((RelationExpr)((OpExpr)ep.expr).left);
-			return ep.expr.getSet();
+			return re.expr.getSet();
 		    }
 		default:
 		    throw new Error("");
@@ -128,7 +128,7 @@ class AbstractRepair {
 		case ExprPredicate.COMPARISON:
 		    {
 			RelationExpr re=((RelationExpr)((OpExpr)ep.expr).left);
-			return ep.expr.getSet();
+			return re.expr.getSet();
 		    }
 		default:
 		    throw new Error("");
diff --git a/Repair/RepairCompiler/MCC/IR/ExactSize.java b/Repair/RepairCompiler/MCC/IR/ExactSize.java
index 32bf470..0588c0f 100755
--- a/Repair/RepairCompiler/MCC/IR/ExactSize.java
+++ b/Repair/RepairCompiler/MCC/IR/ExactSize.java
@@ -16,13 +16,15 @@ class ExactSize {
     }
     
     public int getsize(SetDescriptor sd) {
-	if (sizemap.containsKey(sd))
-	    return ((Integer)sizemap.get(sd)).intValue();
+	SizeObject so=new SizeObject(sd);
+	if (sizemap.containsKey(so))
+	    return ((Integer)sizemap.get(so)).intValue();
 	else
 	    return -1;
     }
     public Constraint getConstraint(SetDescriptor sd) {
-	return (Constraint)constraintmap.get(sd);
+	SizeObject so=new SizeObject(sd);
+	return (Constraint)constraintmap.get(so);
     }
 
     private void computesizes() {
@@ -69,8 +71,9 @@ class ExactSize {
 		}
 		if (matches) {
 		    System.out.println("Set "+sd.toString()+" has size "+oldsize);
-		    sizemap.put(sd,new Integer(oldsize));
-		    constraintmap.put(sd,c);
+		    SizeObject so=new SizeObject(sd);
+		    sizemap.put(so,new Integer(oldsize));
+		    constraintmap.put(so,c);
 		}
 	    }
 	}
diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
index ca55892..e5ebf67 100755
--- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
@@ -20,9 +20,9 @@ public class RelationExpr extends Expr {
 
     public SetDescriptor getSet() {
 	if (inverse)
-	    return relation.domain;
+	    return relation.getDomain();
 	else
-	    return relation.range;
+	    return relation.getRange();
     }
 
     public RelationExpr(Expr expr, RelationDescriptor relation, boolean inverse) {
diff --git a/Repair/RepairCompiler/MCC/IR/SizeObject.java b/Repair/RepairCompiler/MCC/IR/SizeObject.java
new file mode 100755
index 0000000..0bd7b8d
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/SizeObject.java
@@ -0,0 +1,43 @@
+package MCC.IR;
+
+class SizeObject {
+    Descriptor setorrelation;
+    boolean isRelation;
+    SetDescriptor set;
+    boolean isInverted;
+
+    public SizeObject(SetDescriptor sd) {
+	this.setorrelation=sd;
+	this.isRelation=false;
+    }
+
+    public SizeObject(RelationDescriptor rd, SetDescriptor sd,boolean inverted) {
+	this.isRelation=true;
+	this.setorrelation=rd;
+	this.set=sd;
+	this.isInverted=inverted;
+    }
+
+    public int hashCode() {
+	int hashcode=setorrelation.hashCode();
+	if (set!=null)
+	    hashcode^=set.hashCode();
+	return hashcode;
+    }
+    public boolean equals(java.lang.Object o) {
+	if (!(o instanceof SizeObject))
+	    return false;
+	SizeObject so=(SizeObject)o;
+	if (so.setorrelation!=setorrelation)
+	    return false;
+	if (so.isRelation!=isRelation)
+	    throw new Error("");
+	if (isRelation) {
+	    if (so.set!=set)
+		return false;
+	    if (so.isInverted!=isInverted)
+		return false;
+	}
+	return true;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 5b741c1..3cf53b9 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -280,8 +280,8 @@ public class Termination {
 
 		for(int i=0;i<conj.size();i++) {
 		    DNFPredicate dp=conj.get(i);
-		    if (AbstractInterferes.interferes(ar,cons)||
-			abstractinterferes.interferes(ar,dp)) {
+		    if (AbstractInterferes.interferesquantifier(ar,cons)||
+			abstractinterferes.interfereswithpredicate(ar,dp)) {
 			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 			gn.addEdge(e);
 			break;
@@ -292,7 +292,7 @@ public class Termination {
 		GraphNode gn2=(GraphNode)scopeiterator.next();
 		TermNode tn2=(TermNode)gn2.getOwner();
 		ScopeNode sn2=tn2.getScope();
-		if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
+		if (AbstractInterferes.interfereswithrule(ar,sn2.getRule(),sn2.getSatisfy())) {
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 		    gn.addEdge(e);
 		}
@@ -345,8 +345,8 @@ public class Termination {
 		Constraint constr=tn2.getConstraint();
 		for(int i=0;i<conj.size();i++) {
 		    DNFPredicate dp=conj.get(i);
-		    if (abstractinterferes.interferes(sn,dp)||
-			AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
+		    if (abstractinterferes.scopeinterfereswithpredicate(sn,dp)||
+			AbstractInterferes.interfereswithquantifier(sn.getDescriptor(),sn.getSatisfy(),constr)) {
 			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 			GraphNode gnconseq=(GraphNode)consequence.get(sn);
 			gnconseq.addEdge(e);
@@ -358,13 +358,13 @@ public class Termination {
 	    /* Now see if this could effect other model defintion rules */
 	    for(int i=0;i<state.vRules.size();i++) {
 		Rule r=(Rule) state.vRules.get(i);
-		if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
+		if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
 		    GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 		    GraphNode gnconseq=(GraphNode)consequence.get(sn);
 		    gnconseq.addEdge(e);
 		}
-		if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
+		if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 		    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 		    GraphNode gnconseq=(GraphNode)consequence.get(sn);
@@ -938,7 +938,6 @@ public class Termination {
 		}
 	    }
 	}
-
     }
 
     boolean debugmsg(String st) {
@@ -1190,7 +1189,6 @@ public class Termination {
 		} else {
 		    return false;
 		}
-		
 	    } else if (q instanceof SetQuantifier) {
 		SetQuantifier sq=(SetQuantifier)q;
 		if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
-- 
2.34.1