Fix some of Dan's bugs (code generation for relation quantifiers misstyped), didn...
authorbdemsky <bdemsky>
Fri, 23 Jan 2004 03:58:49 +0000 (03:58 +0000)
committerbdemsky <bdemsky>
Fri, 23 Jan 2004 03:58:49 +0000 (03:58 +0000)
23 files changed:
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
Repair/RepairCompiler/MCC/IR/CastExpr.java
Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
Repair/RepairCompiler/MCC/IR/Constraint.java
Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
Repair/RepairCompiler/MCC/IR/Expr.java
Repair/RepairCompiler/MCC/IR/ForQuantifier.java
Repair/RepairCompiler/MCC/IR/GraphNode.java
Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
Repair/RepairCompiler/MCC/IR/LogicStatement.java
Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
Repair/RepairCompiler/MCC/IR/OpExpr.java
Repair/RepairCompiler/MCC/IR/Quantifier.java
Repair/RepairCompiler/MCC/IR/RelationInclusion.java
Repair/RepairCompiler/MCC/IR/RelationQuantifier.java
Repair/RepairCompiler/MCC/IR/Rule.java
Repair/RepairCompiler/MCC/IR/SetDescriptor.java
Repair/RepairCompiler/MCC/IR/SetInclusion.java
Repair/RepairCompiler/MCC/IR/TermNode.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/State.java
Repair/RepairCompiler/MCC/link.model

index df39d0f..ad98137 100755 (executable)
@@ -17,7 +17,7 @@ import MCC.IR.*;
  */
 
 public class Compiler {
-    public static boolean REPAIR=true;
+    public static boolean REPAIR=false;
     
     public static void main(String[] args) {
         State state = null;
@@ -54,11 +54,13 @@ public class Compiler {
            success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
            success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
 
+           /* Check partition constraints */
+           (new ImplicitSchema(state)).update();
+
            if (REPAIR) {
-               (new ImplicitSchema(state)).update();
                Termination t=new Termination(state);
            }
-            
+            state.printall();
             (new DependencyBuilder(state)).calculate();
             
             try {
index 569485c..4217361 100755 (executable)
@@ -50,7 +50,24 @@ class AbstractInterferes {
                    return false;
            } 
        }
-       /* This if handles all the c comparisons in the paper */
+
+       if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+           (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+           (dp.getPredicate() instanceof ExprPredicate)&&
+           (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+           boolean neg2=dp.isNegated();
+           Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+               (neg2&&(op2==Opcode.NE)&&(size2==0))||
+               (!neg2&&(op2==Opcode.GE))||
+               (!neg2&&(op2==Opcode.GT))||
+               (neg2&&(op2==Opcode.LE))||
+               (neg2&&(op2==Opcode.LT)))
+               return false;
+       }
+
+       /* This handles all the c comparisons in the paper */
        if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
            (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
            (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
@@ -63,8 +80,8 @@ class AbstractInterferes {
            boolean neg2=dp.isNegated();
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
            int size2=((ExprPredicate)dp.getPredicate()).leftsize();
-           if ((neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
-               (!neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
+           if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
+               (neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
                int size1a=0;
                if (neg1) {
                    if((op1==Opcode.EQ)||(op1==Opcode.GE))
@@ -91,8 +108,37 @@ class AbstractInterferes {
                    (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
                    (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
                    return false;
-           } 
+           }
+       }
+
+       if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+           (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+           (dp.getPredicate() instanceof ExprPredicate)&&
+           (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+           boolean neg2=dp.isNegated();
+           Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+               (neg2&&(op2==Opcode.NE)&&(size2==0))||
+               (neg2&&(op2==Opcode.GE))||
+               (neg2&&(op2==Opcode.GT))||
+               (!neg2&&(op2==Opcode.LE))||
+               (!neg2&&(op2==Opcode.LT)))
+               return false;
+           
        }
+       if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+           (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+           (dp.getPredicate() instanceof InclusionPredicate)&&
+           (dp.isNegated()==false))
+           return false; /* Could only satisfy this predicate */
+
+       if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+           (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+           (dp.getPredicate() instanceof InclusionPredicate)&&
+           (dp.isNegated()==true))
+           return false; /* Could only satisfy this predicate */
+         
        return true;
     }
 
@@ -113,6 +159,8 @@ class AbstractInterferes {
            {
                if ((!neg2&&(op2==Opcode.GE))||
                    (!neg2&&(op2==Opcode.GT))||
+                   (neg2&&(op2==Opcode.EQ)&&(size2==0))||
+                   (!neg2&&(op2==Opcode.NE)&&(size2==0))||
                    (neg2&&(op2==Opcode.LE))||
                    (neg2&&(op2==Opcode.LT)))
                    return false;
@@ -129,15 +177,29 @@ class AbstractInterferes {
            {
                if ((neg2&&(op2==Opcode.GE))||
                    (neg2&&(op2==Opcode.GT))||
+                   (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+                   (neg2&&(op2==Opcode.NE)&&(size2==0))||
                    (!neg2&&(op2==Opcode.LE))||
                    (!neg2&&(op2==Opcode.LT)))
                    return false;
            } 
        }
+       if ((des==dp.getPredicate().getDescriptor())&&
+           satisfy&&
+           (dp.getPredicate() instanceof InclusionPredicate)&&
+           (dp.isNegated()==false))
+           return false; /* Could only satisfy this predicate */
+
+       if ((des==dp.getPredicate().getDescriptor())&&
+           (!satisfy)&&
+           (dp.getPredicate() instanceof InclusionPredicate)&&
+           (dp.isNegated()==true))
+           return false; /* Could only satisfy this predicate */
+
        return true;
     }
 
-    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+    static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
        for(int i=0;i<r.numQuantifiers();i++) {
            Quantifier q=r.getQuantifier(i);
            if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
@@ -148,6 +210,22 @@ class AbstractInterferes {
                    return true;
            } else throw new Error("Unrecognized Quantifier");
        }
+       return false;
+    }
+
+    static public boolean interferes(AbstractRepair ar, Quantifiers q) {
+       if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
+           return interferesquantifier(ar.getDescriptor(),true,q,true);
+       return false;
+    }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
+       return interferesquantifier(des, satisfy, q,true);
+    }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+       if (interferesquantifier(des,satisfy,r,satisfyrule))
+           return true;
        /* Scan DNF form */
        DNFRule drule=r.getDNFGuardExpr();
        for(int i=0;i<drule.size();i++) {
index 5b12c6d..4ccc637 100755 (executable)
@@ -12,6 +12,12 @@ public class CastExpr extends Expr {
         this.expr = expr;
     }
 
+    public String name() {
+       String str="";
+       str="(("+type.toString()+")"+expr.name()+")";
+       return str;
+    }
+
     public boolean equals(Map remap, Expr e) {
        if (e==null)
            return false;
index aeaf4c9..9419563 100755 (executable)
@@ -21,7 +21,7 @@ class ConcreteInterferes {
                        RuleConjunction rconj=drule.get(k);
                        for(int l=0;l<rconj.size();l++) {
                            DNFExpr dexpr=rconj.get(l);
-                           /* See if update interfers w/ dexpr */
+                           /* See if update interferes w/ dexpr */
                            
                            if (!dexpr.getExpr().usesDescriptor(updated_des))
                                continue; /* No use of the descriptor */
index 97a2c24..f3fdcec 100755 (executable)
@@ -2,7 +2,7 @@ package MCC.IR;
 
 import java.util.*;
 
-public class Constraint {
+public class Constraint implements Quantifiers {
     
     private static int count = 1;
 
@@ -19,10 +19,27 @@ public class Constraint {
         label = new String("c" + count++);
     }
 
+    public String toString() {
+       String name="";
+       for(int i=0;i<numQuantifiers();i++) {
+           name+=getQuantifier(i).toString()+",";
+       }
+       name+=logicstatement.name();
+       return name;
+    }
+
     public int getNum() {
         return num;
     }
 
+    public int numQuantifiers() {
+       return quantifiers.size();
+    }
+
+    public Quantifier getQuantifier(int i) {
+       return (Quantifier) quantifiers.get(i);
+    }
+
     public String getLabel() {
         return label;
     }
@@ -59,7 +76,7 @@ public class Constraint {
 
         for (int i = 0; i < quantifiers.size(); i++) {            
             Quantifier q = (Quantifier) quantifiers.elementAt(i);
-            topdescriptors.addAll(q.getRequiredDescriptors());                
+            topdescriptors.addAll(q.getRequiredDescriptors());
         }
 
         return SetDescriptor.expand(topdescriptors);
index c913a26..9ad6460 100755 (executable)
@@ -14,8 +14,7 @@ public class DependencyBuilder {
     }
 
     public void calculate() {
-                     
-        /* reinitialize (clear) nodes */
+       /* reinitialize (clear) nodes */
         constraintnodes = new Hashtable();
         rulenodes = new Hashtable();
 
@@ -109,8 +108,8 @@ public class DependencyBuilder {
                         edge.setDotNodeParameters("style=dotted");
                         otherrulenode.addEdge(edge);
                     }
-                }               
-            }           
+                }
+            }
         }
 
         /* store results in state */
index 4e9d283..6be665b 100755 (executable)
@@ -20,6 +20,7 @@ public abstract class Expr {
     }
 
     public String name() {
+       System.out.println(this.getClass().getName());
        return "?";
     }
 
index 5739d63..86cf50a 100755 (executable)
@@ -32,7 +32,7 @@ public class ForQuantifier extends Quantifier {
     }
 
     public String toString() {
-        return "for quantifier " + var.getSymbol() + " = " + lower + " to " + upper;
+        return "for quantifier " + var.getSymbol() + " = " + lower.name() + " to " + upper.name();
     }
 
     public void generate_open(CodeWriter writer) {
index fde26ad..da50a5a 100755 (executable)
@@ -83,6 +83,22 @@ public class GraphNode {
         return owner;
     }
 
+    public static void computeclosure(Set nodes) {
+       Stack tovisit=new Stack();
+       tovisit.addAll(nodes);
+       while(!tovisit.isEmpty()) {
+           GraphNode gn=(GraphNode)tovisit.pop();
+           for(Iterator it=gn.edges();it.hasNext();) {
+               Edge edge=(Edge)it.next();
+               GraphNode target=edge.getTarget();
+               if (!nodes.contains(target)) {
+                   nodes.add(target);
+                   tovisit.push(target);
+               }
+           }
+       }
+    }
+
     public void setDotNodeParameters(String param) {
         if (param == null) {
             throw new NullPointerException();
@@ -195,8 +211,10 @@ public class GraphNode {
                 while (edges.hasNext()) {
                     Edge edge = (Edge) edges.next();
                     GraphNode node = edge.getTarget();
-                    String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
-                    output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+                   if (nodes.contains(node)) {
+                       String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
+                       output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
+                   }
                 }
             }
         }
index 8d61947..1be0068 100755 (executable)
@@ -11,38 +11,230 @@ public class ImplicitSchema {
     }
 
     public void update() {
-       updaterules();
+       //      updaterules();
        updateconstraints();
        updaterelationconstraints();
     }
 
+    boolean needDomain(RelationDescriptor rd) {
+       return needDR(rd, true);
+    }
+
+    boolean needDR(RelationDescriptor rd,boolean isdomain) {
+       Vector rules=state.vRules;
+       SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+       for(int i=0;i<rules.size();i++) {
+           Rule r=(Rule)rules.get(i);
+           if ((r.numQuantifiers()==1)&&
+               (r.getQuantifier(0) instanceof RelationQuantifier)&&
+               (((RelationQuantifier)r.getQuantifier(0)).getRelation()==rd)&&
+               r.getInclusion().getTargetDescriptors().contains(sd)) {
+               SetInclusion rinc=(SetInclusion)r.getInclusion();
+               RelationQuantifier rq=(RelationQuantifier)r.getQuantifier(0);
+               VarDescriptor vd=isdomain?rq.x:rq.y;
+               if ((rinc.getExpr() instanceof VarExpr)&&
+                   (((VarExpr)rinc.getExpr()).getVar()==vd)&&
+                   (r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+                   (((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
+                   return false;
+           }
+       }
+
+
+       for(int i=0;i<rules.size();i++) {
+           Rule r=(Rule)rules.get(i);
+           Inclusion inc=r.getInclusion();
+           if (inc.getTargetDescriptors().contains(rd)) {
+               /* Need to check this rule */
+               boolean good=false;
+               RelationInclusion rinc=(RelationInclusion)inc;
+               Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
+               if (expr instanceof VarExpr) {
+                   VarDescriptor vd=((VarExpr)expr).getVar();
+                   assert vd!=null;
+                   for (int j=0;j<r.numQuantifiers();j++) {
+                       Quantifier q=r.getQuantifier(j);
+                       if ((q instanceof SetQuantifier)&&
+                           (((SetQuantifier)q).getVar()==vd)&&
+                           (sd.allSubsets().contains(((SetQuantifier)q).getSet()))) {
+                           good=true;
+                           break;
+                       }
+                       if ((q instanceof RelationQuantifier)&&
+                           (
+                           ((((RelationQuantifier)q).x==vd)&&
+                           (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getDomain())))
+                           ||
+                           ((((RelationQuantifier)q).y==vd)&&
+                           (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getRange())))
+                           )) {
+                           good=true;
+                           break;
+                       }
+                       
+                   }
+                   if (good)
+                       continue; /* Proved for this case */
+               }
+               for(int j=0;j<rules.size();j++) {
+                   Rule r2=(Rule)rules.get(j);
+                   Inclusion inc2=r2.getInclusion();
+                   
+                   if (checkimplication(r,r2,isdomain)) {
+                       good=true;
+                       break;
+                   }
+               }
+               if (good)
+                   continue;
+
+               return true; /* Couldn't prove we didn't need */
+           }
+       }
+       return false;
+    }
+
+    boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
+       /* r1 is the relation */
+       /* See if this rule guarantees relation */
+       /* Steps:
+          1. match up quantifiers
+          2. check inclusion condition
+          3. see if guard expr of set rule is more general */
+
+       RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
+       RelationDescriptor rd=inc1.getRelation();
+       SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+       Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
+
+       Inclusion inc2=r2.getInclusion();
+       if (!(inc2 instanceof SetInclusion))
+           return false;
+       SetInclusion sinc2=(SetInclusion)inc2;
+       if (sinc2.getSet()!=sd)
+           return false;
+       if (r1.numQuantifiers()!=r2.numQuantifiers())
+           return false; 
+       /* Construct a mapping between quantifiers */
+       int[] mapping=new int[r2.numQuantifiers()];
+       HashMap map=new HashMap();
+       for(int i=0;i<r1.numQuantifiers();i++) {
+           Quantifier q1=r1.getQuantifier(i);
+           boolean foundmapping=false;
+           for (int j=0;j<r2.numQuantifiers();j++) {
+               if (mapping[j]==1)
+                   continue; /* Its already used */
+               Quantifier q2=r2.getQuantifier(j);
+               if (q1 instanceof SetQuantifier && q2 instanceof SetQuantifier&&
+                   ((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
+                   mapping[j]=1;
+                   map.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+                   foundmapping=true;
+                   break;
+               }
+               if (q1 instanceof RelationQuantifier && q2 instanceof RelationQuantifier &&
+                   ((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
+                   mapping[j]=1;
+                   map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
+                   map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
+                   foundmapping=true;
+                   break;
+               }
+           }
+           if (!foundmapping)
+               return false;
+       }
+       /* Built mapping */
+       Expr sexpr=sinc2.getExpr();
+       if (!expr.equals(map,sexpr))
+           return false;  /* This rule doesn't add the right thing */
+       DNFRule drule1=r1.getDNFGuardExpr();
+       DNFRule drule2=r2.getDNFGuardExpr();
+       for (int i=0;i<drule1.size();i++) {
+           RuleConjunction rconj1=drule1.get(i);
+           boolean foundmatch=false;
+           for (int j=0;j<drule2.size();j++) {
+               RuleConjunction rconj2=drule2.get(j);
+               /* Need to show than rconj2 is true if rconj1 is true */
+               if (implication(map,rconj1,rconj2)) {
+                   foundmatch=true;
+                   break;
+               }
+           }
+           if (!foundmatch)
+               return false;
+       }
+       return true;
+    }
+
+    boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2) {
+       for(int i=0;i<rc2.size();i++) {
+           /* Check that rc1 has all predicates that rc2 has */
+           DNFExpr de2=rc2.get(i);
+           boolean havematch=false;
+           for(int j=0;j<rc1.size();j++) {
+               DNFExpr de1=rc1.get(i);
+               if (de1.getNegation()!=de2.getNegation())
+                   continue;
+               if (de1.getExpr().equals(map,de2.getExpr())) {
+                   havematch=true;
+                   break;
+               }
+           }
+           if (!havematch)
+               return false;
+       }
+       return true;
+    }
+
+    boolean needRange(RelationDescriptor rd) {
+       return needDR(rd, false);
+    }
+
     void updaterelationconstraints() {
        Vector reldescriptors=state.stRelations.getAllDescriptors();
        for(int i=0;i<reldescriptors.size();i++) {
            RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
-           Constraint c=new Constraint();
-           
-           /* Construct quantifier */
-           RelationQuantifier rq=new RelationQuantifier();
-           String varname1=new String("relationvar1");
-           String varname2=new String("relationvar2");
-           VarDescriptor var1=new VarDescriptor(varname1);
-           VarDescriptor var2=new VarDescriptor(varname2);
-           c.getSymbolTable().add(var1);
-           c.getSymbolTable().add(var2);
-           var1.setType(rd.getDomain().getType());
-           var2.setType(rd.getRange().getType());
-           rq.setTuple(var1,var2);
-           rq.setRelation(rd);
-           c.addQuantifier(rq);
-           VarExpr ve1=new VarExpr(varname1);
-           SetExpr se1=new SetExpr(rd.getDomain());
-           LogicStatement incpred1=new InclusionPredicate(ve1,se1);
-           VarExpr ve2=new VarExpr(varname2);
-           SetExpr se2=new SetExpr(rd.getRange());
-           LogicStatement incpred2=new InclusionPredicate(ve2,se2);
-           c.setLogicStatement(new LogicStatement(LogicStatement.AND,incpred1,incpred2));
-           state.vConstraints.add(c);
+           if (needDomain(rd)||needRange(rd)) {
+               
+               Constraint c=new Constraint();
+               /* Construct quantifier */
+               LogicStatement ls=null;
+
+               RelationQuantifier rq=new RelationQuantifier();
+               String varname1=new String("relationvar1");
+               VarDescriptor var1=new VarDescriptor(varname1);
+               String varname2=new String("relationvar2");
+               VarDescriptor var2=new VarDescriptor(varname2);
+               rq.setTuple(var1,var2);
+               rq.setRelation(rd);
+               c.addQuantifier(rq);
+               c.getSymbolTable().add(var1);
+               c.getSymbolTable().add(var2);
+               var1.setType(rd.getDomain().getType());
+               var2.setType(rd.getRange().getType());
+
+               if (needDomain(rd)) {
+                   VarExpr ve1=new VarExpr(var1);
+                   SetExpr se1=new SetExpr(rd.getDomain());
+                   se1.td=rd.getDomain().getType();
+                   ls=new InclusionPredicate(ve1,se1);
+               }
+
+
+               if (needRange(rd)) {
+                   VarExpr ve2=new VarExpr(var2);
+                   SetExpr se2=new SetExpr(rd.getRange());
+                   se2.td=rd.getRange().getType();
+                   LogicStatement incpred2=new InclusionPredicate(ve2,se2);
+                   if (ls==null) ls=incpred2;
+                   else ls=new LogicStatement(LogicStatement.AND,ls,incpred2);
+               }
+               rd.addUsage(RelationDescriptor.IMAGE);
+
+               c.setLogicStatement(ls);
+               state.vConstraints.add(c);
+           }
        }
     }
 
@@ -67,8 +259,9 @@ public class ImplicitSchema {
                for(int j=0;j<sd.getSubsets().size();j++) {
                    LogicStatement conj=null;
                    for(int k=0;k<sd.getSubsets().size();k++) {
-                       VarExpr ve=new VarExpr(varname);
+                       VarExpr ve=new VarExpr(var);
                        SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
+                       se.td=sd.getType();
                        LogicStatement incpred=new InclusionPredicate(ve,se);
                        if (j!=k) {
                            incpred=new LogicStatement(LogicStatement.NOT ,incpred);
index aa093b4..5871004 100755 (executable)
@@ -9,8 +9,10 @@ public class LogicStatement {
     public static final Operation NOT = new Operation("NOT");
 
     public String name() {
+       if (op==NOT)
+           return "!"+left.name();
        String name=left.name();
-       name+=op.toString();
+       name+=" "+op.toString()+" ";
        if (right!=null)
            name+=right.name();
        return name;
index fdddbeb..033c8d6 100755 (executable)
@@ -4,9 +4,21 @@ import java.util.*;
 class MultUpdateNode {
     Vector updates;
     AbstractRepair abstractrepair;
-    public MultUpdateNode(AbstractRepair ar) {
+    ScopeNode scopenode;
+    int op;
+    static public final int ADD=0;
+    static public final int REMOVE=1;
+    static public final int MODIFY=2;
+
+    public MultUpdateNode(AbstractRepair ar, int op) {
        updates=new Vector();
        abstractrepair=ar;
+       this.op=op;
+    }
+
+    public MultUpdateNode(ScopeNode sn) {
+       updates=new Vector();
+       scopenode=sn;
     }
     void addUpdate(UpdateNode un) {
        updates.add(un);
index f903a33..8f6aa59 100755 (executable)
@@ -29,6 +29,9 @@ public class OpExpr extends Expr {
        return opcode;
     }
 
+
+
+
     public boolean equals(Map remap, Expr e) {
        if (e==null||!(e instanceof OpExpr))
            return false;
@@ -61,11 +64,13 @@ public class OpExpr extends Expr {
     public boolean usesDescriptor(Descriptor d) {
        if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
            opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
-           return right.usesDescriptor(d);
+           return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
+           //      return right.usesDescriptor(d);
        else
            return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
     }
     
+
     public int[] getRepairs(boolean negated) {
        if (left instanceof RelationExpr)
            return new int[] {AbstractRepair.MODIFYRELATION};
@@ -73,21 +78,33 @@ public class OpExpr extends Expr {
            boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
            if (isRelation) {
                if (opcode==Opcode.EQ)
-                   return new int[] {AbstractRepair.ADDTORELATION,
-                                         AbstractRepair.REMOVEFROMRELATION};
+                   if (((IntegerLiteralExpr)right).getValue()==0)
+                       return new int[] {AbstractRepair.REMOVEFROMRELATION};
+                   else
+                       return new int[] {AbstractRepair.ADDTORELATION,
+                                             AbstractRepair.REMOVEFROMRELATION};
                if (((opcode==Opcode.GE)&&!negated)||
-                   ((opcode==Opcode.LE)&&negated))
-                   return new int[]{AbstractRepair.ADDTORELATION};
+                   ((opcode==Opcode.LE)&&negated)) {
+                   if (((IntegerLiteralExpr)right).getValue()==0)
+                       return new int[0];
+                   else
+                       return new int[]{AbstractRepair.ADDTORELATION}; }
                else
                    return new int[]{AbstractRepair.REMOVEFROMRELATION};
            } else {
                if (opcode==Opcode.EQ)
-                   return new int[] {AbstractRepair.ADDTOSET,
-                                         AbstractRepair.REMOVEFROMSET};
+                   if (((IntegerLiteralExpr)right).getValue()==0)
+                       return new int[] {AbstractRepair.REMOVEFROMSET};                        
+                   else
+                       return new int[] {AbstractRepair.ADDTOSET,
+                                             AbstractRepair.REMOVEFROMSET};
                
                if (((opcode==Opcode.GE)&&!negated)||
-                   ((opcode==Opcode.LE)&&negated))
-                   return new int[] {AbstractRepair.ADDTOSET};
+                   ((opcode==Opcode.LE)&&negated)) {
+                   if (((IntegerLiteralExpr)right).getValue()==0)
+                       return new int[0];
+                   else
+                       return new int[] {AbstractRepair.ADDTOSET}; }
                else
                    return new int[] {AbstractRepair.REMOVEFROMSET};
            }
index 2f5c170..4b50b30 100755 (executable)
@@ -9,5 +9,4 @@ public abstract class Quantifier {
 
     public abstract int generate_worklistload(CodeWriter writer, int offset);
     public abstract int generate_workliststore(CodeWriter writer, int offset);
-
 }
index a2b40bc..d1b3a02 100755 (executable)
@@ -17,6 +17,11 @@ public class RelationInclusion extends Inclusion {
         this.relation = relation;
     }
 
+    public String toString() {
+       String str="<"+leftelementexpr.name()+","+rightelementexpr.name()+"> in "+relation.toString();
+       return str;
+    }
+
     public boolean usesDescriptor(Descriptor d) {
        if (d==relation)
            return true;
index 7281d2e..193e02c 100755 (executable)
@@ -13,6 +13,10 @@ public class RelationQuantifier extends Quantifier {
         relation = rd; 
     }
 
+    public RelationDescriptor getRelation() {
+       return relation;
+    }
+
     public void setTuple(VarDescriptor x, VarDescriptor y) {
         this.x = x;
         this.y = y;
@@ -31,9 +35,9 @@ public class RelationQuantifier extends Quantifier {
     public void generate_open(CodeWriter writer) {
         writer.outputline("for (SimpleIterator* " + x.getSafeSymbol() + "_iterator = " + relation.getSafeSymbol() + "_hash->iterator(); " + x.getSafeSymbol() + "_iterator->hasNext(); )");
         writer.startblock();
-        writer.outputline(y.getType().getSafeSymbol() + " " + y.getSafeSymbol() + " = (" + y.getType().getSafeSymbol() + ") " + x.getSafeSymbol() + "_iterator->next();");        
+        writer.outputline(y.getType().getGenerateType() + " " + y.getSafeSymbol() + " = (" + y.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->next();");        
         // #ATTN#: key is called second because next() forwards ptr and key does not! 
-        writer.outputline(x.getType().getSafeSymbol() + " " + x.getSafeSymbol() + " = (" + x.getType().getSafeSymbol() + ") " + x.getSafeSymbol() + "_iterator->key();");
+        writer.outputline(x.getType().getGenerateType() + " " + x.getSafeSymbol() + " = (" + x.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->key();");
     }
 
     public int generate_worklistload(CodeWriter writer, int offset) {        
index 12650d9..017e788 100755 (executable)
@@ -2,7 +2,7 @@ package MCC.IR;
 
 import java.util.*;
 
-public class Rule {
+public class Rule implements Quantifiers {
     
     static int count = 1;
 
@@ -23,6 +23,15 @@ public class Rule {
         label = new String("rule" + count++);
     }
     
+    public String toString() {
+       String name="";
+       for(int i=0;i<numQuantifiers();i++) {
+           name+=getQuantifier(i).toString()+",";
+       }
+       name+=guard.name()+"=>"+inclusion.toString();
+       return name;
+    }
+
     public int numQuantifiers() {
        return quantifiers.size();
     }
index 6bd62ed..2b42ac2 100755 (executable)
@@ -28,7 +28,8 @@ public class SetDescriptor extends Descriptor {
             
             if (descriptor instanceof SetDescriptor) {
                 expanded.addAll(((SetDescriptor) descriptor).allSubsets());
-            }
+            } else
+               expanded.add(descriptor); /* Still need the descriptor */
         }
 
         expanded.addAll(descriptors);
index cdf67b2..9d37572 100755 (executable)
@@ -13,6 +13,12 @@ public class SetInclusion extends Inclusion {
     static boolean worklist = false;
     public boolean dostore = true;
 
+    public String toString() {
+       String str="";
+       str+=elementexpr.name()+" in "+set;
+       return str;
+    }
+
     public SetInclusion(Expr elementexpr, SetDescriptor set) {
         this.elementexpr = elementexpr;
         this.set = set;
@@ -25,6 +31,10 @@ public class SetInclusion extends Inclusion {
            return elementexpr.usesDescriptor(d);
     }
 
+    public Expr getExpr() {
+       return elementexpr;
+    }
+
     public SetDescriptor getSet() {
         return set;
     }
index 9e3dbe8..7fadf32 100755 (executable)
@@ -55,6 +55,13 @@ class TermNode {
            return conj;
     }
 
+    public Constraint getConstraint() {
+       if (type!=CONJUNCTION)
+           throw new Error("Not Conjunction Node!");
+       else
+           return constr;
+    }
+
     public MultUpdateNode getUpdate() {
        if (type!=UPDATE)
            throw new Error("Not Update Node!");
index 0b01ab9..f9ae3bb 100755 (executable)
@@ -15,6 +15,8 @@ public class Termination {
     Hashtable scopesatisfy;
     Hashtable scopefalsify;
     Hashtable consequence;
+    Hashtable abstractadd;
+    Hashtable abstractremove;
 
     State state;
 
@@ -29,11 +31,15 @@ public class Termination {
        consequence=new Hashtable();
        updatenodes=new HashSet();
        consequencenodes=new HashSet();
+       abstractadd=new Hashtable();
+       abstractremove=new Hashtable();
+
 
        generateconjunctionnodes();
        generatescopenodes();
        generaterepairnodes();
        generatedatastructureupdatenodes();
+       generatecompensationnodes();
 
        generateabstractedges();
        generatescopeedges();
@@ -42,9 +48,10 @@ public class Termination {
        HashSet superset=new HashSet();
        superset.addAll(conjunctions);
        superset.addAll(abstractrepair);
-       superset.addAll(updatenodes);
-       superset.addAll(scopenodes);
-       superset.addAll(consequencenodes);
+       //superset.addAll(updatenodes);
+       //superset.addAll(scopenodes);
+       //superset.addAll(consequencenodes);
+       //GraphNode.computeclosure(superset);
        try {
            GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
        } catch (Exception e) {
@@ -101,9 +108,12 @@ public class Termination {
                GraphNode gn2=(GraphNode)conjiterator.next();
                TermNode tn2=(TermNode)gn2.getOwner();
                Conjunction conj=tn2.getConjunction();
+               Constraint cons=tn2.getConstraint();
+
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);
-                   if (AbstractInterferes.interferes(ar,dp)) {
+                   if (AbstractInterferes.interferes(ar,cons)||
+                       AbstractInterferes.interferes(ar,dp)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                        gn.addEdge(e);
                        break;
@@ -124,9 +134,11 @@ public class Termination {
                GraphNode gn2=(GraphNode)conjiterator.next();
                TermNode tn2=(TermNode)gn2.getOwner();
                Conjunction conj=tn2.getConjunction();
+               Constraint constr=tn2.getConstraint();
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);
-                   if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)) {
+                   if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)||
+                       AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                        GraphNode gnconseq=(GraphNode)consequence.get(sn);
                        gnconseq.addEdge(e);
@@ -154,8 +166,9 @@ public class Termination {
        }
     }
 
-
+    /* Generates the abstract repair nodes */
     void generaterepairnodes() {
+       /* Generate repairs of conjunctions */
        for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
            GraphNode gn=(GraphNode)conjiterator.next();
            TermNode tn=(TermNode)gn.getOwner();
@@ -174,6 +187,122 @@ public class Termination {
                }
            }
        }
+       /* Generate additional abstract repairs */
+       Vector setdescriptors=state.stSets.getAllDescriptors();
+       for(int i=0;i<setdescriptors.size();i++) {
+           SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
+
+           /* XXXXXXX: Not sure what to do here */
+           VarExpr ve=new VarExpr("DUMMY");
+           InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
+           
+           DNFPredicate tp=new DNFPredicate(false,ip);
+           AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
+           TermNode tn=new TermNode(ar);
+           GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
+           abstractrepair.add(gn);
+           abstractadd.put(sd,gn);
+           
+           DNFPredicate tp2=new DNFPredicate(true,ip);
+           AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
+           TermNode tn2=new TermNode(ar2);
+           GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
+           abstractrepair.add(gn2);
+           abstractremove.put(sd,gn2);
+       }
+
+       Vector relationdescriptors=state.stRelations.getAllDescriptors();
+       for(int i=0;i<relationdescriptors.size();i++) {
+           RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
+
+           /* XXXXXXX: Not sure what to do here */
+           VarDescriptor vd1=new VarDescriptor("DUMMY1");
+           VarExpr ve2=new VarExpr("DUMMY2");
+
+           InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
+           
+           DNFPredicate tp=new DNFPredicate(false,ip);
+           AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
+           TermNode tn=new TermNode(ar);
+           GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
+           abstractrepair.add(gn);
+           abstractadd.put(rd,gn);
+           
+           DNFPredicate tp2=new DNFPredicate(true,ip);
+           AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
+           TermNode tn2=new TermNode(ar2);
+           GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
+           abstractrepair.add(gn2);
+           abstractremove.put(rd,gn2);
+       }
+       
+    }
+
+    int compensationcount=0;
+    void generatecompensationnodes() {
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule) state.vRules.get(i);
+           Vector possiblerules=new Vector();
+           /* Construct bindings */
+           Vector bindings=new Vector();
+           constructbindings(bindings, r,true);
+           
+           for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
+               GraphNode gn=(GraphNode)scopesatisfy.get(r);
+               TermNode tn=(TermNode) gn.getOwner();
+               ScopeNode sn=tn.getScope();
+               MultUpdateNode mun=new MultUpdateNode(sn);
+               TermNode tn2=new TermNode(mun);
+               GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
+               UpdateNode un=new UpdateNode();
+               un.addBindings(bindings);
+               if (j<r.numQuantifiers()) {
+                   /* Remove quantifier */
+                   Quantifier q=r.getQuantifier(j);
+                   if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier)q;
+                       TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
+                       toe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(toe,true);
+                       un.addUpdate(u);
+                       if (abstractremove.containsKey(rq.relation)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           continue; /* Abstract repair doesn't exist */
+                       }
+                   } else if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier)q;
+                       ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+                       eoe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(eoe,true);
+                       un.addUpdate(u);
+                       if (abstractremove.containsKey(sq.set)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(sq.set);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           continue; /* Abstract repair doesn't exist */
+                       }
+                   } else {
+                       continue;
+                   }
+               } else {
+                   int c=j-r.numQuantifiers();
+                   if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
+                       continue;
+                   }
+               }
+
+               mun.addUpdate(un);
+
+               GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
+               compensationcount++;
+               gn.addEdge(e);
+               updatenodes.add(gn2);
+           }
+       }
     }
 
     void generatedatastructureupdatenodes() {
@@ -190,6 +319,10 @@ public class Termination {
            } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
                generateremovefromsetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+               /* Generate remove/add pairs */
+               generateremovefromsetrelation(gn,ar);
+               generateaddtosetrelation(gn,ar);
+               /* Generate atomic modify */
                generatemodifyrelation(gn,ar);
            }
        }
@@ -207,9 +340,14 @@ public class Termination {
                (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
                possiblerules.add(r);
        }
+       if (possiblerules.size()==0)
+           return;
        int[] count=new int[possiblerules.size()];
        while(remains(count,possiblerules)) {
-           MultUpdateNode mun=new MultUpdateNode(ar);
+           MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
+           TermNode tn=new TermNode(mun);
+           GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
+
            boolean goodflag=true;
            for(int i=0;i<possiblerules.size();i++) {
                Rule r=(Rule)possiblerules.get(i);
@@ -217,6 +355,7 @@ public class Termination {
                /* Construct bindings */
                Vector bindings=new Vector();
                constructbindings(bindings, r,true);
+               un.addBindings(bindings);
                if (count[i]<r.numQuantifiers()) {
                    /* Remove quantifier */
                    Quantifier q=r.getQuantifier(count[i]);
@@ -226,12 +365,26 @@ public class Termination {
                        toe.td=ReservedTypeDescriptor.INT;
                        Updates u=new Updates(toe,true);
                        un.addUpdate(u);
+                       if (abstractremove.containsKey(rq.relation)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           goodflag=false;break; /* Abstract repair doesn't exist */
+                       }
                    } else if (q instanceof SetQuantifier) {
                        SetQuantifier sq=(SetQuantifier)q;
                        ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
                        eoe.td=ReservedTypeDescriptor.INT;
                        Updates u=new Updates(eoe,true);
                        un.addUpdate(u);
+                       if (abstractremove.containsKey(sq.set)) {
+                           GraphNode agn=(GraphNode)abstractremove.get(sq.set);
+                           GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                           gn2.addEdge(e);
+                       } else {
+                           goodflag=false;break; /* Abstract repair doesn't exist */
+                       }
                    } else {goodflag=false;break;}
                } else {
                    int c=count[i]-r.numQuantifiers();
@@ -242,8 +395,6 @@ public class Termination {
                mun.addUpdate(un);
            }
            if (goodflag) {
-               TermNode tn=new TermNode(mun);
-               GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
                GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
                removefromcount++;
                gn.addEdge(e);
@@ -437,13 +588,14 @@ public class Termination {
                    RuleConjunction ruleconj=dnfrule.get(j);
                    /* Add in updates for quantifiers */
                    System.out.println("Attempting to generate add to set #4");
-                   if (processquantifers(un, r)&&debugdd()&&
+                   MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
+                   TermNode tn=new TermNode(mun);
+                   GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
+
+                   if (processquantifers(gn2,un, r)&&debugdd()&&
                        processconjunction(un,ruleconj)) {
                        System.out.println("Attempting to generate add to set #5");
-                       MultUpdateNode mun=new MultUpdateNode(ar);
                        mun.addUpdate(un);
-                       TermNode tn=new TermNode(mun);
-                       GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
                        GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
                        addtocount++;
                        gn.addEdge(e);
@@ -458,8 +610,7 @@ public class Termination {
        return true;
     }
 
-    boolean processquantifers(UpdateNode un, Rule r) {
-       boolean goodupdate=true;
+    boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
        Inclusion inc=r.getInclusion();
        for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
            Quantifier q=(Quantifier)iterator.next();
@@ -471,15 +622,30 @@ public class Termination {
                toe.td=ReservedTypeDescriptor.INT;
                Updates u=new Updates(toe,false);
                un.addUpdate(u);
+               if (abstractremove.containsKey(rq.relation)) {
+                   GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
+                   GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                   gn.addEdge(e);
+               } else {
+                   return false;
+               }
+
            } else if (q instanceof SetQuantifier) {
                SetQuantifier sq=(SetQuantifier)q;
                ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
                eoe.td=ReservedTypeDescriptor.INT;
                Updates u=new Updates(eoe,false);
                un.addUpdate(u);
-           } else {goodupdate=false; break;}
+               if (abstractremove.containsKey(sq.set)) {
+                   GraphNode agn=(GraphNode)abstractadd.get(sq.set);
+                   GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+                   gn.addEdge(e);
+               } else {
+                   return false;
+               }
+           } else return false;
        }
-       return goodupdate;
+       return true;
     }
 
     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
index ee1dfa0..9f907a9 100755 (executable)
@@ -49,4 +49,15 @@ public class State {
         ptSpace = null;
     }
 
+    void printall() {
+       for(int i=0;i<vRules.size();i++) {
+           Rule r=(Rule)vRules.get(i);
+           System.out.println(r.toString());
+       }
+       for(int i=0;i<vConstraints.size();i++) {
+           Constraint c=(Constraint)vConstraints.get(i);
+           System.out.println(c.toString());
+       }
+    }
+    
 }
index 18c9466..1953ef2 100755 (executable)
@@ -1,7 +1,6 @@
 [], literal(true) => head in Nodes;
 [forall node in Nodes], !(node.next=literal(0)) => node.next in Nodes;
 [forall node in Nodes], !(node.next=literal(0)) => <node, node.next> in nextnodes;
-[forall node in Nodes], !(node.prev=literal(0)) => node.prev in Nodes;
 [forall node in Nodes], !(node.prev=literal(0)) => <node, node.prev> in prevnodes;