Added new file.

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 2fe4aeff43261ed0be2fbba1a5e51e10aa19272c..a4c1ba3cc33d42c709b7c609853369427ec50f7d 100755 (executable)
--- 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 d8888490324097dc8f1ee304b01af91fd2cee2a4..3cb9b03c24c0cf5c78ee78760e7dbaa6b38ccf2b 100755 (executable)
--- 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 32bf470223d68b039b033fa73e5feb034d9618f2..0588c0f8c24189ac52ab7ca16693b41bf1074b96 100755 (executable)
--- 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 ca558922afaa3005484391da9bc49ed808cfafa6..e5ebf677eecd812700d09aa34afef4e3d8ee8967 100755 (executable)
--- 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 (executable)
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 5b741c1e26a52a1aeae1b24c9e1e256e814cdbf4..3cf53b9e4b2dc437e1af61cf2e6b4f58223ca86c 100755 (executable)
--- 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) {