From e2af60de1736531dfe9f5ce4b5192e2d343434b8 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Mon, 2 Aug 2004 21:42:44 +0000
Subject: [PATCH] Updates to allow discovering of partial functions

---
 Repair/RepairCompiler/MCC/Compiler.java       |  1 +
 Repair/RepairCompiler/MCC/IR/CastExpr.java    |  4 +++
 .../MCC/IR/ConstraintDependence.java          | 25 +++++++++++++++----
 Repair/RepairCompiler/MCC/IR/ExactSize.java   |  2 +-
 .../RepairCompiler/MCC/IR/ImplicitSchema.java | 23 ++++++++++++++++-
 Repair/RepairCompiler/MCC/State.java          |  2 ++
 6 files changed, 50 insertions(+), 7 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index a1f8bf6..fc4f738 100755
--- 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 23e194f..263460f 100755
--- 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 0e718c2..cd3eb99 100755
--- 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 b5b9851..1b665fc 100755
--- 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 6947c03..85bd076 100755
--- 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 a12d675..d30e7cc 100755
--- 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;
-- 
2.34.1