Fixed some analysis problems...

[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 ae1ac7a1c088b44c72cf94c603fa29c692f31f0e..d6dc251382ff1a89bb786aab0759d52beb656d44 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -159,7 +159,7 @@ public class ConstraintDependence {
                    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("Warning: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
                        continue;
@@ -216,7 +216,11 @@ 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);
@@ -233,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();
@@ -274,6 +278,16 @@ public class ConstraintDependence {
        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;