Code to improve search by pruning certain types of repair..
authorbdemsky <bdemsky>
Tue, 11 May 2004 21:14:26 +0000 (21:14 +0000)
committerbdemsky <bdemsky>
Tue, 11 May 2004 21:14:26 +0000 (21:14 +0000)
Repair/RepairCompiler/MCC/CLI.java
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/DotExpr.java
Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
Repair/RepairCompiler/MCC/IR/SemanticChecker.java
Repair/RepairCompiler/MCC/IR/TermNode.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/IR/VarExpr.java

index a8b2bce..11f479a 100755 (executable)
@@ -11,7 +11,7 @@ import java.util.StringTokenizer;
  * files.
  *
  * @author  le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.4 2004/05/10 21:54:40 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.5 2004/05/11 21:14:24 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -106,6 +106,8 @@ public class CLI {
                 Compiler.REPAIR=false;
            } else if (args[i].equals("-aggressivesearch")) {
                 Compiler.AGGRESSIVESEARCH=true;
+           } else if (args[i].equals("-prunequantifiernodes")) {
+                Compiler.PRUNEQUANTIFIERS=true;
             } else if (args[i].equals("-verbose") || args[i].equals("-v")) {
                 context = 0;
                 verbose++;
index df09791..9ecf6a6 100755 (executable)
@@ -20,6 +20,7 @@ public class Compiler {
     /* Set this flag to false to turn repairs off */
     public static boolean REPAIR=true;
     public static boolean AGGRESSIVESEARCH=false;
+    public static boolean PRUNEQUANTIFIERS=false;
 
     public static void main(String[] args) {
         State state = null;
index b0a49a3..adc8721 100755 (executable)
@@ -9,7 +9,7 @@ public class DotExpr extends Expr {
     String field;
     Expr index;
     
-    static boolean DOMEMCHECKS=true;
+    static boolean DOMEMCHECKS=false;
     static boolean DOTYPECHECKS=false;
     static boolean DONULL=false;
 
index 6b6a715..a44f431 100755 (executable)
@@ -134,8 +134,21 @@ public class GraphAnalysis {
                    if (!foundupdate)
                        allgood=false;
                }
-               if (allgood)
+               if (allgood) {
                    couldremove.remove(gn);
+                   if (Compiler.PRUNEQUANTIFIERS) {
+                       TermNode tn=(TermNode)gn.getOwner();
+                       Constraint constr=tn.getConstraint();
+                       for(Iterator consit=((Set)termination.conjunctionmap.get(constr)).iterator();consit.hasNext();) {
+                           GraphNode gn4=(GraphNode)consit.next();
+                           TermNode tn4=(TermNode)gn4.getOwner();
+                           if (tn4.getquantifiernode()) {
+                               mustremove.add(gn4); /* This node is history */
+                               System.out.println("Eliminating: "+gn4.getTextLabel());
+                           }
+                       }
+                   }
+               }
            }
 
 
index 4fda86c..c99715d 100755 (executable)
@@ -10,9 +10,17 @@ public class InclusionPredicate extends Predicate {
     public TypeDescriptor typecheck(SemanticAnalyzer sa) {
        TypeDescriptor t=expr.typecheck(sa);
        TypeDescriptor ts=setexpr.typecheck(sa);
-       if (t!=ts)
+       if (t instanceof StructureTypeDescriptor) {
+           while(((StructureTypeDescriptor)t).getSuperType()!=null)
+               t=((StructureTypeDescriptor)t).getSuperType();
+       }
+       if (ts instanceof StructureTypeDescriptor) {
+           while(((StructureTypeDescriptor)ts).getSuperType()!=null)
+               ts=((StructureTypeDescriptor)ts).getSuperType();
+       }
+       if (t!=ts) {
            return null;
-       
+       }
        return ReservedTypeDescriptor.INT;
     }
 
index c3d2c5d..c35feaf 100755 (executable)
@@ -404,6 +404,7 @@ public class SemanticChecker {
             TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
 
             if (constype == null) {
+               System.out.println("Failed attempting to type constraint");
                 ok = false;
             } else if (constype != ReservedTypeDescriptor.INT) {
                 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
@@ -439,6 +440,7 @@ public class SemanticChecker {
                 assert qn.getLabel().equals("quantifier");
                 Quantifier quantifier = parse_quantifier(qn);
                 if (quantifier == null) {
+                   System.out.println("Failed parsing quantifier");
                     ok = false;
                 } else {
                     constraint.addQuantifier(quantifier);
@@ -450,6 +452,7 @@ public class SemanticChecker {
         LogicStatement logicexpr = parse_body(pn.getChild("body"));
 
         if (logicexpr == null) {
+           System.out.println("Failed parsing logical expression");
             ok = false;
         } else {
             constraint.setLogicStatement(logicexpr);
index 337c569..bd46b6b 100755 (executable)
@@ -14,6 +14,16 @@ class TermNode {
     AbstractRepair repair;
     ScopeNode scope;
     MultUpdateNode update;
+    boolean quantifiernode=false;
+
+    public void setquantifiernode() {
+       quantifiernode=true;
+    }
+    
+    public boolean getquantifiernode() {
+       return quantifiernode;
+    }
+
 
     public int getType() {
        return type;
index 4698b51..7727567 100755 (executable)
@@ -143,8 +143,6 @@ public class Termination {
                    conjunctionmap.put(c,new HashSet());
                ((Set)conjunctionmap.get(c)).add(gn);
                conjtonodemap.put(dnf.get(j),gn);
-
-
            }
            // Construct quantifier "conjunction" nodes
            for(int j=0;j<c.numQuantifiers();j++) {
@@ -156,6 +154,7 @@ public class Termination {
                    DNFConstraint dconst=new DNFConstraint(ip);
                    dconst=dconst.not();
                    TermNode tn=new TermNode(c,dconst.get(0));
+                   tn.setquantifiernode();
                    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
                                               "Conj ("+i+","+j+") "+dconst.get(0).name()
                                               ,tn);
@@ -172,6 +171,7 @@ public class Termination {
                    DNFConstraint dconst=new DNFConstraint(ip);
                    dconst=dconst.not();
                    TermNode tn=new TermNode(c,dconst.get(0));
+                   tn.setquantifiernode();
                    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
                                               "Conj ("+i+","+j+") "+dconst.get(0).name()
                                               ,tn);
index 2e59733..db9e443 100755 (executable)
@@ -3,7 +3,7 @@ package MCC.IR;
 import java.util.*;
 
 public class VarExpr extends Expr {
-    static boolean DOMEMCHECKS=true;
+    static boolean DOMEMCHECKS=false;
     static boolean DOTYPECHECKS=false;
     static boolean DONULL=false;