From a3c5c1cd64c83a127b8d89293794a67c5f530dbe Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Sun, 7 Nov 2004 01:19:30 +0000
Subject: [PATCH] Some embarrassing erros.  The DNF conversion for negation
 wasn't working quite right.  Printing negation a little more clearly.  Fixed
 a problem with the termination analysis (it was too conservative).

---
 .../RepairCompiler/MCC/IR/DNFConstraint.java  | 21 +++++--
 Repair/RepairCompiler/MCC/IR/DNFRule.java     | 21 +++++--
 .../RepairCompiler/MCC/IR/GraphAnalysis.java  | 57 +++++++++++--------
 .../RepairCompiler/MCC/IR/LogicStatement.java |  2 +-
 Repair/RepairCompiler/MCC/IR/OpExpr.java      |  7 ++-
 .../MCC/IR/SemanticChecker.java               |  2 +-
 6 files changed, 75 insertions(+), 35 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
index 018df2f..55770f5 100755
--- a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
@@ -9,6 +9,11 @@ public class DNFConstraint {
 	conjunctions.add(new Conjunction(new DNFPredicate(false,p)));
     }
 
+    public DNFConstraint(DNFPredicate dp) {
+	conjunctions=new Vector();
+	conjunctions.add(new Conjunction(dp));
+    }
+
     public DNFConstraint(Conjunction conj) {
 	conjunctions=new Vector();
 	conjunctions.add(conj);
@@ -17,7 +22,7 @@ public class DNFConstraint {
     public DNFConstraint(Vector conj) {
 	conjunctions=conj;
     }
-    
+
     DNFConstraint() {
 	conjunctions=new Vector();
     }
@@ -62,15 +67,23 @@ public class DNFConstraint {
 
     public DNFConstraint not() {
 	DNFConstraint copy=copy();
+        DNFConstraint notconst=null;
 	for (int i=0;i<size();i++) {
 	    Conjunction conj=copy.get(i);
+            DNFConstraint newconst=null;
 	    for (int j=0;j<conj.size();j++) {
 		DNFPredicate dp=conj.get(j);
 		dp.negatePred();
+                if (newconst==null)
+                   newconst=new DNFConstraint(dp);
+                else
+                   newconst=newconst.or(new DNFConstraint(dp));
 	    }
+            if (notconst==null)
+               notconst=newconst;
+            else
+               notconst=notconst.and(newconst);
 	}
-	return copy;
+	return notconst;
    }
 }
-
-
diff --git a/Repair/RepairCompiler/MCC/IR/DNFRule.java b/Repair/RepairCompiler/MCC/IR/DNFRule.java
index 345a588..26fb1f8 100755
--- a/Repair/RepairCompiler/MCC/IR/DNFRule.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFRule.java
@@ -9,6 +9,11 @@ public class DNFRule {
 	ruleconjunctions.add(new RuleConjunction(new DNFExpr(false,e)));
     }
 
+    public DNFRule(DNFExpr de) {
+	ruleconjunctions=new Vector();
+	ruleconjunctions.add(new RuleConjunction(de));
+    }
+
     public DNFRule(RuleConjunction conj) {
 	ruleconjunctions=new Vector();
 	ruleconjunctions.add(conj);
@@ -17,7 +22,7 @@ public class DNFRule {
     public DNFRule(Vector conj) {
 	ruleconjunctions=conj;
     }
-    
+
     DNFRule() {
 	ruleconjunctions=new Vector();
     }
@@ -62,15 +67,23 @@ public class DNFRule {
 
     public DNFRule not() {
 	DNFRule copy=copy();
+        DNFRule notrule=null;
 	for (int i=0;i<size();i++) {
 	    RuleConjunction conj=copy.get(i);
+            DNFRule newrule=null;
 	    for (int j=0;j<conj.size();j++) {
 		DNFExpr dp=conj.get(j);
 		dp.negatePred();
+                if (newrule==null)
+                   newrule=new DNFRule(dp);
+                else
+                   newrule=newrule.or(new DNFRule(dp));
 	    }
+            if (notrule==null)
+               notrule=newrule;
+            else
+               notrule=notrule.and(newrule);
 	}
-	return copy;
+	return notrule;
    }
 }
-
-
diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 16a51f7..0d516d3 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -35,7 +35,7 @@ public class GraphAnalysis {
 			 &&termination.conjunctions.contains(gn2))||
 			cantremovetrans.contains(gn2))
 			cantremovetrans.add(gn3);
-		    
+
 		    if (termination.abstractrepair.contains(gn3)||
 			termination.conjunctions.contains(gn3)||
 			termination.updatenodes.contains(gn3)) {
@@ -55,7 +55,7 @@ public class GraphAnalysis {
 		if (!goodoption) {
 		    if (termination.scopenodes.contains(gn2))
 			return false;
-		}		    
+		}
 	    }
 	}
 	if (needcyclecheck) {
@@ -116,6 +116,8 @@ public class GraphAnalysis {
 		GraphNode gn=(GraphNode) it.next();
 		if (mustremove.contains(gn)||cantremove.contains(gn))
 		    continue;
+		if (!safetransclosure(gn, mustremove,cantremove, cantremove))
+                    continue;
 
 		boolean allgood=true;
 		for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
@@ -124,7 +126,7 @@ public class GraphAnalysis {
 		    assert tn2.getType()==TermNode.ABSTRACT;
 		    boolean foundupdate=false;
 		    for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
-			GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();		    
+			GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
 			if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
 			    TermNode tn3=(TermNode)gn3.getOwner();
 			    if (tn3.getType()==TermNode.UPDATE)
@@ -153,7 +155,7 @@ public class GraphAnalysis {
 
 
 	    /* Look for constraints which can only be satisfied one way */
-	    
+
 	    Vector constraints=termination.state.vConstraints;
 	    for(int i=0;i<constraints.size();i++) {
 		Constraint c=(Constraint)constraints.get(i);
@@ -226,7 +228,7 @@ public class GraphAnalysis {
 			change=true;
 		}
 	    }
-	    
+
 	    if (Compiler.AGGRESSIVESEARCH) {
 		/* Aggressively remove compensation nodes */
 		for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
@@ -321,7 +323,7 @@ public class GraphAnalysis {
 		    AbstractRepair ar=tn2.getAbstract();
 		    boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
 		    int numadd=0;int numremove=0;
-		    
+
 		    for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 			GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 			GraphNode gn3=e2.getTarget();
@@ -392,11 +394,11 @@ public class GraphAnalysis {
 			GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 			GraphNode gn2=e.getTarget();
 			TermNode tn2=(TermNode)gn2.getOwner();
-			
+
 			if ((tn2.getType()==TermNode.CONSEQUENCE)&&
 			    !mustremove.contains(gn2))
 			    count++;
-			    
+
 
 			if (tn2.getType()!=TermNode.UPDATE)
 			    continue;
@@ -405,7 +407,7 @@ public class GraphAnalysis {
 			boolean containsgn2=cantremove.contains(gn2);
 			cantremove.add(gn);
 			cantremove.add(gn2);
-			
+
 			Set cycle=GraphNode.findcycles(cantremove);
 			if (cycle.contains(gn2)) {
 			    if (!mustremove.contains(gn2)) {
@@ -421,7 +423,7 @@ public class GraphAnalysis {
 			if (!containsgn2)
 			    cantremove.remove(gn2);
 		    }
-		
+
 		    if (count==1) {
 			for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 			    GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
@@ -440,7 +442,7 @@ public class GraphAnalysis {
 	    }
 	    couldremove.removeAll(mustremove);
 	    couldremove.removeAll(cantremove);
-	    
+
 	    Vector couldremovevector=new Vector();
 	    couldremovevector.addAll(couldremove);
 	    Vector combination=new Vector();
@@ -460,7 +462,7 @@ public class GraphAnalysis {
 		e.printStackTrace();
 		System.exit(-1);
 	    }
-	    
+
 	    System.out.println("Searching set of "+couldremove.size()+" nodes.");
 	    System.out.println("Eliminated must "+mustremove.size()+" nodes");
 	    System.out.println("Eliminated cant "+cantremove.size()+" nodes");
@@ -479,22 +481,31 @@ public class GraphAnalysis {
 		GraphNode gn=(GraphNode)it.next();
 		System.out.println(gn.getTextLabel());
 	    }
-	    
-	    
+
+	    System.out.println("==================================================");
 	    while(true) {
 		if (illegal(combination,couldremovevector))
 		    break;
 		Set combinationset=buildset(combination,couldremovevector);
+                System.out.println("---------------------------");
+                for(Iterator it=combinationset.iterator();it.hasNext();) {
+                    System.out.println(((GraphNode)it.next()).getTextLabel());
+                }
+                System.out.println("---------------------------");
 		checkmodify(combinationset);
 		combinationset.addAll(mustremove);
 		if (combinationset!=null) {
-		    System.out.println("Checkabstract="+checkAbstract(combinationset));
-		    System.out.println("Checkrepairs="+checkRepairs(combinationset));
-		    System.out.println("Checkall="+checkAll(combinationset));
-		    
-		    if (checkAbstract(combinationset)==0&&
-			checkRepairs(combinationset)==0&&
-			checkAll(combinationset)==0) {
+                    int checkabstract=checkAbstract(combinationset);
+                    int checkrep=checkRepairs(combinationset);
+                    int checkall=checkAll(combinationset);
+
+		    System.out.println("Checkabstract="+checkabstract);
+		    System.out.println("Checkrepairs="+checkrep);
+		    System.out.println("Checkall="+checkall);
+
+		    if (checkabstract==0&&
+			checkrep==0&&
+			checkall==0) {
 			return combinationset;
 		    }
 		}
@@ -522,7 +533,7 @@ public class GraphAnalysis {
 		    if (!removednodes.contains(gn2)&&
 			tn2.getType()==TermNode.UPDATE) {
 			MultUpdateNode mun=tn2.getUpdate();
-			
+
 			if (mun.getType()==MultUpdateNode.ADD)
 			    numadd++;
 			if (mun.getType()==MultUpdateNode.REMOVE)
@@ -709,7 +720,7 @@ public class GraphAnalysis {
 	tset.addAll(termination.consequencenodes);
 	abstractnodes.retainAll(tset);
 	Set cycles=GraphNode.findcycles(abstractnodes);
-	
+
 	for(Iterator it=cycles.iterator();it.hasNext();) {
 	    GraphNode gn=(GraphNode)it.next();
 	    System.out.println("NODE: "+gn.getTextLabel());
diff --git a/Repair/RepairCompiler/MCC/IR/LogicStatement.java b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
index b750ffd..0569137 100755
--- a/Repair/RepairCompiler/MCC/IR/LogicStatement.java
+++ b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
@@ -10,7 +10,7 @@ public class LogicStatement {
 
     public String name() {
 	if (op==NOT)
-	    return "!"+left.name();
+	    return "!("+left.name()+")";
 	String name=left.name();
 	name+=" "+op.toString()+" ";
 	if (right!=null)
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index c5f6b27..e9cde37 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -191,8 +191,10 @@ public class OpExpr extends Expr {
 	if (opcode==Opcode.RND)
 	    return "Round("+left.name()+")";
 	String name=left.name()+opcode.toString();
-	if (right!=null)
+	if (right!=null) {
 	    name+=right.name();
+            name="("+name+")";
+        }
 	return name;
     }
 
@@ -411,8 +413,9 @@ public class OpExpr extends Expr {
     public void prettyPrint(PrettyPrinter pp) {
         pp.output("(");
         if (opcode == Opcode.NOT) {
-	    pp.output("!");
+	    pp.output("!(");
             left.prettyPrint(pp);
+	    pp.output(")");
 	} else if (opcode == Opcode.NOP) {
             left.prettyPrint(pp);
 	} else if (opcode == Opcode.RND) {
diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index b7f3479..108a883 100755
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -381,6 +381,7 @@ public class SemanticChecker {
         if (!precheck(pn, "constraints")) {
             return false;
         }
+        //System.out.println(pn.PPrint(2,true));
 
         boolean ok = true;
         ParseNodeVector constraints = pn.getChildren();
@@ -594,7 +595,6 @@ public class SemanticChecker {
         } else if (pn.getChild("not") != null) {
             /* NOT body */
             LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
-
             if (left == null) {
                 return null;
             }
-- 
2.34.1