Added minimum size analysis.

[repair.git] / Repair / RepairCompiler / MCC / IR / ConstraintDependence.java

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index 7ae89cb7143fc41e9b47a875ecae9da2eec0c7bc..3deab4939293bcef58fdc030b007d028a7c5cdfe 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -19,7 +19,7 @@ public class ConstraintDependence {
        nodetonode=new Hashtable();
        constructnodes();
     }
-    
+
     public Set computeOrdering() {
        HashSet allnodes=new HashSet();
        allnodes.addAll(constnodes);
@@ -36,7 +36,7 @@ public class ConstraintDependence {
                     return g1.getFinishingTime() - g2.getFinishingTime();
                 }
             });
-       
+
         topologicalsort.addAll(constnodes);
        return topologicalsort;
     }
@@ -110,7 +110,7 @@ public class ConstraintDependence {
            constnodes.add(gn);
        }
     }
-    
+
     private void constructconjunctionnodes(Termination termination) {
        /*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
          GraphNode conjnode=(GraphNode)it.next();
@@ -137,7 +137,7 @@ public class ConstraintDependence {
            GraphNode conjnode=(GraphNode)it.next();
            if (removedset.contains(conjnode))
                continue;
-           
+
            TermNode tn=(TermNode)conjnode.getOwner();
            Conjunction conj=tn.getConjunction();
            for(int i=0;i<conj.size();i++) {
@@ -156,13 +156,13 @@ public class ConstraintDependence {
                    continue;
                for(Iterator fit=functions.iterator();fit.hasNext();) {
                    Function f=(Function)fit.next();
-                   if (rulesensurefunction(f))
+                   if (rulesensurefunction(state,f,false))
                        continue; //no constraint needed to ensure
 
-                   Set s=providesfunction(f);
+                   Set s=providesfunction(state,f);
                    if (s.size()==0) {
-                       System.out.println("Error: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
-                       System.exit(-1);
+                       System.out.println("Warning: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
+                       continue;
                    }
                    Constraint c=(Constraint)s.iterator().next(); //Take the first one
                    requiresConstraint(conjnode,c);
@@ -171,7 +171,12 @@ public class ConstraintDependence {
        }
     }
 
-    private boolean rulesensurefunction(Function f) {
+    /** This method determines whether the model definition rules
+     * ensure that the relation and evaluation domain descriped by f
+     * is either a function (if isPartial=false) or a partial function
+     * (if isPartial=true). */
+
+    static private boolean rulesensurefunction(State state,Function f, boolean isPartial) {
        boolean foundrule=false;
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule)state.vRules.get(i);
@@ -179,7 +184,9 @@ public class ConstraintDependence {
                RelationInclusion ri=(RelationInclusion)r.getInclusion();
                Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
                SetDescriptor sd=e.getSet();
-               if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
+               if (sd==null)
+                   return false;
+               if (state.setanalysis.noIntersection(f.getSet(),sd))
                    continue; /* This rule doesn't effect the function */
                if (foundrule) /* two different rules are a problem */
                    return false;
@@ -192,13 +199,15 @@ public class ConstraintDependence {
                SetQuantifier sq=(SetQuantifier)q;
                if (ve.getVar()!=sq.getVar())
                    return false;
-               if (!sq.getSet().isSubset(f.getSet()))
-                   return false;
-               if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
-                     ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
-                   return false;
+               if (!isPartial) {
+                   if (!sq.getSet().isSubset(f.getSet()))
+                       return false;
+                   if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+                          ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
+                       return false;
+               }
                Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
-               if (e2.isSafe())
+               if (isPartial||e2.isSafe())
                    foundrule=true;
                else
                    return false;
@@ -206,8 +215,12 @@ public class ConstraintDependence {
        }
        return foundrule;
     }
- 
-    private Set providesfunction(Function f) {
+
+    static private Set providesfunction(State state, Function f) {
+       return providesfunction(state,f,false);
+    }
+
+    static private Set providesfunction(State state, Function f, boolean isPartial) {
        HashSet set=new HashSet();
        for(int i=0;i<state.vConstraints.size();i++) {
            Constraint c=(Constraint)state.vConstraints.get(i);
@@ -224,7 +237,7 @@ public class ConstraintDependence {
                        ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
                        if (ep.isRightInt()&&
                            ep.rightSize()==1&&
-                           ep.getOp()==Opcode.EQ&&
+                           (ep.getOp()==Opcode.EQ||(ep.getOp()==Opcode.LE&&isPartial))&&
                            ep.inverted()==f.isInverse()&&
                            ep.getDescriptor()==f.getRelation()) {
                            ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
@@ -255,15 +268,41 @@ public class ConstraintDependence {
        return set;
     }
 
+
+    /** This method determines whether the model definition rules
+     * ensure that the relation r (or inverse relation if inverse is
+     * true) evaluated on the domain sd is either a function (if
+     * isPartial=false) or a partial function (if isPartial=true). */
+
+    static public boolean rulesensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse, boolean isPartial) {
+       return rulesensurefunction(state, new Function(r,sd,inverse,null),isPartial);
+    }
+
+    /** This method determines whether the model constraints ensure
+     * that the relation r (or inverse relation if inverse is true)
+     * evaluated on the domain sd is either a function (if
+     * isPartial=false) or a partial function (if isPartial=true). */
+
+    static public boolean constraintsensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse,boolean isPartial) {
+       Set constraints=providesfunction(state, new Function(r,sd,inverse,null),isPartial);
+       return (!constraints.isEmpty());
+    }
+
     public static class Function {
        private RelationDescriptor rd;
        private SetDescriptor sd;
        private boolean inverse;
+       private Expr expr;
 
-       public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse) {
+       public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
            this.inverse=inverse;
            this.sd=sd;
            this.rd=r;
+           this.expr=e;
+       }
+
+       public Expr getExpr() {
+           return expr;
        }
 
        public SetDescriptor getSet() {