Updates to allow discovering of partial functions

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index a1f8bf6ffef8b22d40eb3ba4d6c49c48fd872821..fc4f7382a5de0a4ba7363b20ffc3314818e6c9d1 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -62,6 +62,7 @@ public class Compiler {
        success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
        
        
+       state.setanalysis=new SetAnalysis(state);
        Termination termination=null;
        /* Check partition constraints */
        (new ImplicitSchema(state)).update();

diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index 23e194f3b02b7ad716860566fee90a5ae0d71db9..263460f5bc1667bef1152f9342da9c96fbe8a785 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -15,6 +15,10 @@ public class CastExpr extends Expr {
        return expr.isValue(td);
     }
 
+    public SetDescriptor getSet() {
+       return expr.getSet();
+    }
+
     public Set freeVars() {
        return expr.freeVars();
     }

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index 0e718c21665891017ff7b89404f924c52c4ba72d..cd3eb99f5a143608aa3eeb33a66f74792db5b98a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -156,7 +156,7 @@ 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);
@@ -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);
@@ -181,7 +186,7 @@ public class ConstraintDependence {
                SetDescriptor sd=e.getSet();
                if (sd==null)
                    return false;
-               if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
+               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;
@@ -196,8 +201,8 @@ public class ConstraintDependence {
                    return false;
                if (!sq.getSet().isSubset(f.getSet()))
                    return false;
-               if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
-                     ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
+               if (!(((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+                      ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))||isPartial)
                    return false;
                Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
                if (e2.isSafe())
@@ -257,6 +262,16 @@ 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);
+    }
+
     public static class Function {
        private RelationDescriptor rd;
        private SetDescriptor sd;

diff --git a/Repair/RepairCompiler/MCC/IR/ExactSize.java b/Repair/RepairCompiler/MCC/IR/ExactSize.java
index b5b98518d54b36bcc6c8b8e5123ad3ec1f8cbe86..1b665fce32aace3d8826702d310135c162c5cb3e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ExactSize.java
+++ b/Repair/RepairCompiler/MCC/IR/ExactSize.java
@@ -13,7 +13,7 @@ class ExactSize {
        this.state=state;
        this.sizemap=new Hashtable();
        this.constraintmap=new Hashtable();
-       this.setanalysis=new SetAnalysis(state);
+       this.setanalysis=state.setanalysis;
        computesizes();
     }
     

diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index 6947c038251c6e91e1553186a4ef6d475b1e06d7..85bd076dab1e383bbd69bea470bd85af407abfbb 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -9,7 +9,7 @@ public class ImplicitSchema {
     SetAnalysis setanalysis;
     public ImplicitSchema(State state) {
        this.state=state;
-       this.setanalysis=new SetAnalysis(state);
+       this.setanalysis=state.setanalysis;
     }
 
     public void update() {
@@ -346,6 +346,27 @@ public class ImplicitSchema {
                if (supersets!=null)
                    for(Iterator superit=supersets.iterator();superit.hasNext();) {
                        SetDescriptor sd1=(SetDescriptor)superit.next();
+                       Expr e=((SetInclusion)r.inclusion).getExpr();
+                       while(e instanceof CastExpr) {
+                           e=((CastExpr)e).getExpr();
+                       }
+                       if (e instanceof VarExpr) {
+                           VarDescriptor vde=((VarExpr)e).getVar();
+                           boolean ok=false;
+                           for (int j=0;j<r.numQuantifiers();j++) {
+                               Quantifier tmp=r.getQuantifier(j);
+                               if (tmp instanceof SetQuantifier&&
+                                   ((SetQuantifier)tmp).getVar()==vde)
+                                   ok=true; /* Need to make sure we don't have a relation quantifier. */
+                           }
+
+                           SetDescriptor currentset=e.getSet();
+                           if (ok&&currentset!=null&&currentset.isSubset(sd1))
+                               continue; /* This rule doesn't add item to
+                                            this set, as item is already
+                                            in this set. */
+                       }
+                       
                        Rule nr=new Rule();
                        nr.setGuardExpr(r.getGuardExpr());
                        nr.quantifiers=r.quantifiers;

diff --git a/Repair/RepairCompiler/MCC/State.java b/Repair/RepairCompiler/MCC/State.java
index a12d675903e15180b3f6ae79d7d0b0d06b3edd22..d30e7cc4af074909c953d8085b7148b0a36e5e59 100755 (executable)
--- a/Repair/RepairCompiler/MCC/State.java
+++ b/Repair/RepairCompiler/MCC/State.java
@@ -35,6 +35,8 @@ public class State {
     public Hashtable constraintnodes;    
     public Hashtable implicitrule;
     public Hashtable implicitruleinv;
+
+    public SetAnalysis setanalysis;
     State() {
         vConstraints = null;
         vRules = null;