From 2bad0dfb94fcdfc04e3c5725177803e7158158b0 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Tue, 3 Aug 2004 19:43:51 +0000
Subject: [PATCH] ...

---
 Repair/RepairCompiler/MCC/IR/AbstractRepair.java  | 15 ++++++++++++++-
 .../MCC/IR/ConstraintDependence.java              | 14 ++++++++++++--
 Repair/RepairCompiler/MCC/IR/RepairGenerator.java |  3 +--
 3 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
index 153677f..1d32666 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
@@ -152,7 +152,7 @@ class AbstractRepair {
     }
 
 
-    /** Thie method tells whether the repair needs to remove objects *
+    /** This method tells whether the repair needs to remove objects *
      *  from the relation, or whether the model definition rules make
      *  the remove unnecessary.*/
 
@@ -162,6 +162,19 @@ class AbstractRepair {
 	return !ConstraintDependence.rulesensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted(), true);
     }
 
+    /** This method tells whether the repair needs to force the
+     *  relation to be function-like.  */
+    
+    public boolean mayNeedFunctionEnforcement(State state) {
+	assert type==MODIFYRELATION;
+	SetDescriptor sd=getPredicate().getPredicate().inverted()?getRangeSet():getDomainSet();	
+	if (ConstraintDependence.rulesensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted(), false))
+	    return false;
+	if (ConstraintDependence.constraintsensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted()))
+	    return false;
+	return true;
+    }
+    
     public AbstractRepair(DNFPredicate dp,int typ, Descriptor d, Sources s) {
 	torepair=dp;
 	type=typ;
diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index ae1ac7a..c36d913 100755
--- 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,7 @@ public class ConstraintDependence {
 	return foundrule;
     }
  
-    private Set providesfunction(Function f) {
+    static private Set providesfunction(State state, Function f) {
 	HashSet set=new HashSet();
 	for(int i=0;i<state.vConstraints.size();i++) {
 	    Constraint c=(Constraint)state.vConstraints.get(i);
@@ -274,6 +274,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) {
+	Set constraints=providesfunction(state, new Function(r,sd,inverse,null));
+	return (!constraints.isEmpty());
+    }
+
     public static class Function {
 	private RelationDescriptor rd;
 	private SetDescriptor sd;
diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 79b89a6..66f2e38 100755
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -791,7 +791,7 @@ public class RepairGenerator {
                 cr.outputline("if (maybe)");
                 cr.startblock();
                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \\n\");");
-                cr.outputline("exit(1);");
+		//cr.outputline("exit(1);");
                 cr.endblock();
 
                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
@@ -1088,7 +1088,6 @@ public class RepairGenerator {
 	    }
 	} else {
 	    /* Start with scheduling removal */
-	    
 	    if (ar.needsRemoves(state))
 		for(int i=0;i<state.vRules.size();i++) {
 		    Rule r=(Rule)state.vRules.get(i);
-- 
2.34.1