Added needed comments, reorganized some code...

diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index 078574978a030a6433f239cb89a7dee08dc419ad..23e194f3b02b7ad716860566fee90a5ae0d71db9 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -31,10 +31,6 @@ public class CastExpr extends Expr {
        return expr.findInvariants(vars);
     }
 
        return expr.findInvariants(vars);
     }
 

-    public void findmatch(Descriptor d, Set s) {
-       expr.findmatch(d,s);
-    }
-

     public CastExpr(TypeDescriptor type, Expr expr) {
         this.type = type;
         this.expr = expr;
     public CastExpr(TypeDescriptor type, Expr expr) {
         this.type = type;
         this.expr = expr;


@@ -54,6 +50,10 @@ public class CastExpr extends Expr {
        else return ((this.type==((CastExpr)e).type)&&expr.equals(remap,((CastExpr)e).expr));
     }
 
        else return ((this.type==((CastExpr)e).type)&&expr.equals(remap,((CastExpr)e).expr));
     }
 

+    public void findmatch(Descriptor d, Set s) {
+       expr.findmatch(d,s);
+    }
+

     public Set useDescriptor(Descriptor d) {
        return expr.useDescriptor(d);
     }
     public Set useDescriptor(Descriptor d) {
        return expr.useDescriptor(d);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index e82284198cd9d0b94e7d473a1646a5c518547d9a..4f6c333b01ea850589294aa9f5a6a55ea1d1a0d6 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -8,25 +8,122 @@ public class ConcreteInterferes {
        this.termination=t;
     }
 
        this.termination=t;
     }
 

+    /** Returns true if the data structure updates performed by mun
+     * may increase (or decrease if satisfy=false) the scope of the
+     * model definition rule r. */

 
 

-    static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
+    public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+       
+       // A rule that adds something to a set can't be falsified by
+       // an update that is only performed if the set is empty
+       if (!initialinterferes(mun,r,satisfy)) 
+           return false;
+
+       for(int i=0;i<mun.numUpdates();i++) {
+           UpdateNode un=mun.getUpdate(i);
+           for (int j=0;j<un.numUpdates();j++) {
+               Updates update=un.getUpdate(j);
+               //Abstract updates don't have concrete interference1
+               if (update.isAbstract()) 
+                   continue;
+               
+               DNFRule drule=satisfy?r.getDNFNegGuardExpr():r.getDNFGuardExpr();
+               Descriptor updated_des=update.getDescriptor();
+               assert updated_des!=null;
+
+               // See if the update interferes with the inclusion
+               // condition for the rule
+               if (r.getInclusion().usesDescriptor(updated_des)) {
+                   boolean ok=false;
+
+                   /* If the update is for this rule, and the effect
+                       is the intended effect, and the update only
+                       effects one binding, then the abstract repair
+                       node already models the action of this
+                       update. */
+
+                   if ((un.getRule()==r)&& 
+                       (((mun.op==MultUpdateNode.ADD)&&satisfy)
+                        ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+                        ||(mun.op==MultUpdateNode.MODIFY))) {
+                       Inclusion inclusion=r.getInclusion();
+                       if (inclusion instanceof RelationInclusion) {
+                           RelationInclusion ri=(RelationInclusion)inclusion;
+                           if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
+                               (!testdisjoint(update,r,ri.getRightExpr())))
+                               ok=true;
+                       } else if (inclusion instanceof SetInclusion) {
+                           SetInclusion si=(SetInclusion)inclusion;
+                           if (!testdisjoint(update,r,si.getExpr()))
+                               ok=true;
+                       } else throw new Error();
+                   }
+
+
+                   if (!ok) {
+                       if (satisfy) {
+                           /** Check to see if the update definitely falsifies r, thus
+                            * can't accidentally satisfy it r. */
+                           if (interferesinclusion(un, update, r)) 
+                               return true;
+                       } else
+                           return true; /* Interferes with inclusion condition */
+                   }
+               }
+               
+               for(int k=0;k<drule.size();k++) {
+                   RuleConjunction rconj=drule.get(k);
+                   for(int l=0;l<rconj.size();l++) {
+                       DNFExpr dexpr=rconj.get(l);
+                       /* See if update interferes w/ dexpr */
+                       if ((un.getRule()==r)&&
+                           (((mun.op==MultUpdateNode.ADD)&&satisfy)
+                            ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+                            ||(mun.op==MultUpdateNode.MODIFY))) {
+                           if (!testdisjoint(update,r,dexpr.getExpr()))
+                               continue; /* Update is specific to
+                                             given binding of the
+                                             rule, and effect is the
+                                             intended one, so we're
+                                             okay */
+                       }
+                       if (interferes(update,dexpr))
+                           return true;
+                   }
+               }           
+           }
+       }
+       return false;
+    }
+
+    /** This method tries to show that if the Update update from the
+     *  UpdateNode un changes the value of the inclusion constraint
+     * that it falsifies the guard of model definition rule. */
+    
+    static private boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {

        Descriptor updated_des=update.getDescriptor();
        Inclusion inclusion=r.getInclusion();
        if (inclusion instanceof RelationInclusion) {
            RelationInclusion ri=(RelationInclusion)inclusion;
        Descriptor updated_des=update.getDescriptor();
        Inclusion inclusion=r.getInclusion();
        if (inclusion instanceof RelationInclusion) {
            RelationInclusion ri=(RelationInclusion)inclusion;

-           if (ri.getLeftExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getLeftExpr()))
+           if (ri.getLeftExpr().usesDescriptor(updated_des)
+               &&searchinterfere(un,update,r,ri.getLeftExpr()))

                return true;
                return true;

-           if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
+           if (ri.getRightExpr().usesDescriptor(updated_des)
+               &&searchinterfere(un,update,r,ri.getRightExpr()))

                return true;
        } else if (inclusion instanceof SetInclusion) {
            SetInclusion si=(SetInclusion)inclusion;
                return true;
        } else if (inclusion instanceof SetInclusion) {
            SetInclusion si=(SetInclusion)inclusion;

-           if (si.getExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,si.getExpr()))
+           if (si.getExpr().usesDescriptor(updated_des)
+               &&searchinterfere(un,update,r,si.getExpr()))

                return true;
        } else throw new Error();
        return false;
     }
 
                return true;
        } else throw new Error();
        return false;
     }
 

-    static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
+    /** This method finds all instances of a field or global that an
+     * update may modify, and builds a variable correspondance */
+
+    static private boolean searchinterfere(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {

        Descriptor updated_des=update.getDescriptor();
        if (updated_des instanceof FieldDescriptor) {
            /* Build variable correspondance */
        Descriptor updated_des=update.getDescriptor();
        if (updated_des instanceof FieldDescriptor) {
            /* Build variable correspondance */


@@ -64,7 +161,10 @@ public class ConcreteInterferes {
        return false;
     }
 
        return false;
     }
 

-    static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
+    /** This method tries to show that if dvd=uvd, then the update un
+     *  must falsify the rule r. */
+
+    static private boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {

        DNFRule negrule=r.getDNFNegGuardExpr();
        HashMap remap=new HashMap();
        remap.put(dvd,uvd);
        DNFRule negrule=r.getDNFNegGuardExpr();
        HashMap remap=new HashMap();
        remap.put(dvd,uvd);


@@ -96,8 +196,6 @@ public class ConcreteInterferes {
                    if (!varok)
                        continue;
 
                    if (!varok)
                        continue;
 

-
-

                    Opcode op=expr.getOpcode();
                    op=Opcode.translateOpcode(dexpr.getNegation(),op);
 
                    Opcode op=expr.getOpcode();
                    op=Opcode.translateOpcode(dexpr.getNegation(),op);
 


@@ -151,90 +249,25 @@ public class ConcreteInterferes {
        return true;
     }
 
        return true;
     }
 

-    /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
-     * the scope of the model definition rule r. */
-
-    public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
-       if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
-           return false;
-       for(int i=0;i<mun.numUpdates();i++) {
-           UpdateNode un=mun.getUpdate(i);
-           for (int j=0;j<un.numUpdates();j++) {
-               Updates update=un.getUpdate(j);
-               
-               DNFRule drule=r.getDNFGuardExpr();
-               if (satisfy)
-                   drule=r.getDNFNegGuardExpr();
-
-
-               if (!update.isAbstract()) {
-                   Descriptor updated_des=update.getDescriptor();
-                   assert updated_des!=null;
-                   /* Update is local to this rule, and the effect is intentional */
-                   /* If we're adding something, a side effect could be to falsify some other binding
-                      If we're removing something, there is no similar side effect */
+    /** This method checks whether the update effects only the
+     *  intended binding for the model definition rule. */

 
 

-                   /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
-                   if (r.getInclusion().usesDescriptor(updated_des)) {
-                       boolean ok=false;
-                       if ((un.getRule()==r)&&
-                           (((mun.op==MultUpdateNode.ADD)&&satisfy)
-                            ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
-                            ||(mun.op==MultUpdateNode.MODIFY))) {
-                           Inclusion inclusion=r.getInclusion();
-                           if (inclusion instanceof RelationInclusion) {
-                               RelationInclusion ri=(RelationInclusion)inclusion;
-                               if ((!interferes(update,r,ri.getLeftExpr()))&&
-                                   (!interferes(update,r,ri.getRightExpr())))
-                                   ok=true;
-                           } else if (inclusion instanceof SetInclusion) {
-                               SetInclusion si=(SetInclusion)inclusion;
-                               if (!interferes(update,r,si.getExpr()))
-                                   ok=true;
-                           } else throw new Error();
-                       }
-                       if (!ok) {
-                           if (satisfy) {
-                               if (interferesinclusion(un, update, r))
-                                   return true;
-                           } else
-                               return true; /* Interferes with inclusion condition */
-                       }
-                   }
-                   
-                   for(int k=0;k<drule.size();k++) {
-                       RuleConjunction rconj=drule.get(k);
-                       for(int l=0;l<rconj.size();l++) {
-                           DNFExpr dexpr=rconj.get(l);
-                           /* See if update interferes w/ dexpr */
-                           if ((un.getRule()==r)&&
-                               (((mun.op==MultUpdateNode.ADD)&&satisfy)
-                                ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
-                                ||(mun.op==MultUpdateNode.MODIFY))) {
-                               if (!interferes(update,r,dexpr.getExpr()))
-                                   continue; /* unique state - we're okay */
-                           }
-                           if (interferes(un,update, r,dexpr))
-                               return true;
-                       }
-                   }
-               }
-           }
-       }
-       return false;
-    }
-
-    private boolean interferes(Updates u, Rule r, Expr e) {
+    private boolean testdisjoint(Updates u, Rule r, Expr e) {
+       // find all exprs that may be be effected by update

        Set exprs=e.useDescriptor(u.getDescriptor());
        for(Iterator eit=exprs.iterator();eit.hasNext();) {
            Expr e2=(Expr)eit.next();
        Set exprs=e.useDescriptor(u.getDescriptor());
        for(Iterator eit=exprs.iterator();eit.hasNext();) {
            Expr e2=(Expr)eit.next();

-           if (mayinterfere(u,r,e2))
+           if (testdisjointness(u,r,e2))

                return true;
        }
        return false;
     }
 
                return true;
        }
        return false;
     }
 

-    private boolean mayinterfere(Updates u, Rule r, Expr e) {
+    /** This method tries to show that the modification only effects
+     * one binding of the model definition rule, and thus has no
+     * unintended side effects. */
+
+    private boolean testdisjointness(Updates u, Rule r, Expr e) {

        // Note: rule of u must be r
 
        Expr update_e=u.getLeftExpr();
        // Note: rule of u must be r
 
        Expr update_e=u.getLeftExpr();


@@ -244,6 +277,8 @@ public class ConcreteInterferes {
            return false; /* Can't accidentally interfere with other bindings if there aren't any! */
 
        boolean firstfield=true;
            return false; /* Can't accidentally interfere with other bindings if there aren't any! */
 
        boolean firstfield=true;

+       
+

        while(true) {
            if (update_e instanceof CastExpr)
                update_e=((CastExpr)update_e).getExpr();
        while(true) {
            if (update_e instanceof CastExpr)
                update_e=((CastExpr)update_e).getExpr();


@@ -285,9 +320,10 @@ public class ConcreteInterferes {
                return true;
            } else return true;
        }
                return true;
            } else return true;
        }

-

     }
 
     }
 

+    /** This method returns the quantifier that defines the quantifier
+     * variable vd. */

     static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
        for (int i=0;i<qs.numQuantifiers();i++) {
            Quantifier q=qs.getQuantifier(i);
     static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
        for (int i=0;i<qs.numQuantifiers();i++) {
            Quantifier q=qs.getQuantifier(i);


@@ -308,13 +344,14 @@ public class ConcreteInterferes {
        return null;
     }
     
        return null;
     }
     

+    
+    /** This function checks to see if an update is only performed if
+     * a given set is empty, and the algorithm is computing whether
+     * the update may falsify a rule that adds something to the set */
+

     static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
        AbstractRepair ar=mun.getRepair();
     static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
        AbstractRepair ar=mun.getRepair();

-       if (satisfy)
-           return true;
-       if (ar==null)
-           return true;
-       if (ar.getType()==AbstractRepair.ADDTOSET) {
+       if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET)) {

            if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
                return true;
            boolean negated=ar.getPredicate().isNegated();
            if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
                return true;
            boolean negated=ar.getPredicate().isNegated();


@@ -325,26 +362,25 @@ public class ConcreteInterferes {
            if (ep.getType()!=ExprPredicate.SIZE)
                return true;
            Opcode op=Opcode.translateOpcode(negated,ep.getOp());
            if (ep.getType()!=ExprPredicate.SIZE)
                return true;
            Opcode op=Opcode.translateOpcode(negated,ep.getOp());

-           
+   

            if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
                ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
                ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
                ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
                return false;
        }
            if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
                ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
                ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
                ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
                return false;
        }

-       

        return true;
        return true;

-
-       

     }
 
     }
 

-    static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
+    static private boolean interferes(Updates update, DNFExpr dexpr) {

        Descriptor descriptor=update.getDescriptor();
        Descriptor descriptor=update.getDescriptor();

+       /* If the DNFExpr expr doesn't use the updated descriptor,
+          there is no interference. */

        if (!dexpr.getExpr().usesDescriptor(descriptor))
            return false;
            
        if (!dexpr.getExpr().usesDescriptor(descriptor))
            return false;
            

-       /* We need to pair the variables */

        if (update.isExpr()) {
        if (update.isExpr()) {

+           /* We need to pair the variables */

            Set vars=update.getRightExpr().freeVars();
            Opcode op1=update.getOpcode();
            Expr lexpr1=update.getLeftExpr();
            Set vars=update.getRightExpr().freeVars();
            Opcode op1=update.getOpcode();
            Expr lexpr1=update.getLeftExpr();


@@ -353,8 +389,8 @@ public class ConcreteInterferes {
            if (vars!=null)
                for(Iterator it=vars.iterator();it.hasNext();) {
                    VarDescriptor vd=(VarDescriptor) it.next();
            if (vars!=null)
                for(Iterator it=vars.iterator();it.hasNext();) {
                    VarDescriptor vd=(VarDescriptor) it.next();

+                   /* VarDescriptor isn't a global */

                    if (!vd.isGlobal()) {
                    if (!vd.isGlobal()) {

-                       /* VarDescriptor isn't a global */

                        if (update.getVar()!=vd) {
                            good=false;
                            break;
                        if (update.getVar()!=vd) {
                            good=false;
                            break;


@@ -368,24 +404,21 @@ public class ConcreteInterferes {
                Opcode op2=expr.getOpcode();
                op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
 
                Opcode op2=expr.getOpcode();
                op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
 

-               good=true;
-               vars=rexpr2.freeVars();

                VarDescriptor leftdescriptor=null;
                VarDescriptor leftdescriptor=null;

-               if (lexpr2 instanceof VarExpr)
-                   leftdescriptor=((VarExpr)lexpr2).getVar();
-               else if (lexpr2 instanceof DotExpr) {
+               {

                    Expr e=lexpr2;
                    Expr e=lexpr2;

-                   do {
+                   while(!(e instanceof VarExpr)) {

                        for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
                        if (e instanceof VarExpr)
                            break;
                        if (e instanceof CastExpr)
                            e=((CastExpr)e).getExpr();
                        else throw new Error("Bad Expr Type:"+e.name());
                        for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
                        if (e instanceof VarExpr)
                            break;
                        if (e instanceof CastExpr)
                            e=((CastExpr)e).getExpr();
                        else throw new Error("Bad Expr Type:"+e.name());

-                   } while (true);
+                   }

                    leftdescriptor=((VarExpr)e).getVar();
                    leftdescriptor=((VarExpr)e).getVar();

-               } else throw new Error("Bad Expr");
-               
+               }
+
+               vars=rexpr2.freeVars();

                if (vars!=null)
                    for(Iterator it=vars.iterator();it.hasNext();) {
                        VarDescriptor vd=(VarDescriptor) it.next();
                if (vars!=null)
                    for(Iterator it=vars.iterator();it.hasNext();) {
                        VarDescriptor vd=(VarDescriptor) it.next();


@@ -397,6 +430,8 @@ public class ConcreteInterferes {
                            }
                        }
                    }
                            }
                        }
                    }

+
+

                if (good) {
                    HashMap remap=new HashMap();
                    remap.put(update.getVar(),leftdescriptor);
                if (good) {
                    HashMap remap=new HashMap();
                    remap.put(update.getVar(),leftdescriptor);

diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 9361d5e8af95602663d3c1a8d70c31fbf83cd6f6..029b22c98c59770f5456c61f674de0787536fd52 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -65,14 +65,6 @@ public class DotExpr extends Expr {
        return true;
     }
 
        return true;
     }
 

-    public void findmatch(Descriptor d, Set s) {
-       if (d==fd)
-           s.add(this);
-       left.findmatch(d,s);
-       if (intindex!=null)
-           intindex.findmatch(d,s);
-    }
-

     public Set freeVars() {
        Set lset=left.freeVars();
        Set iset=null;
     public Set freeVars() {
        Set lset=left.freeVars();
        Set iset=null;


@@ -108,6 +100,14 @@ public class DotExpr extends Expr {
        return name;
     }
     
        return name;
     }
     

+    public void findmatch(Descriptor d, Set s) {
+       if (d==fd)
+           s.add(this);
+       left.findmatch(d,s);
+       if (intindex!=null)
+           intindex.findmatch(d,s);
+    }
+

     public Set useDescriptor(Descriptor d) {
        HashSet newset=new HashSet();
        if (d==fd)
     public Set useDescriptor(Descriptor d) {
        HashSet newset=new HashSet();
        if (d==fd)

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 55aacfc30dc9ff1323f8ad2776facaba131504d6..dfa0c1433dda72f5bff7d60a1a17d466c86609bf 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -78,12 +78,6 @@ public class OpExpr extends Expr {
        return rightfunctions;
     }
 
        return rightfunctions;
     }
 

-    public void findmatch(Descriptor d, Set  s) {
-       left.findmatch(d,s);
-       if (right!=null)
-           right.findmatch(d,s);
-    }
-

     public static boolean isInt(Expr e) {
        if (e==null)
            return false;
     public static boolean isInt(Expr e) {
        if (e==null)
            return false;


@@ -239,6 +233,12 @@ public class OpExpr extends Expr {
        return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
     }
 
        return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
     }
 

+    public void findmatch(Descriptor d, Set  s) {
+       left.findmatch(d,s);
+       if (right!=null)
+           right.findmatch(d,s);
+    }
+

     public Set useDescriptor(Descriptor d) {
        HashSet newset=new HashSet();
        newset.addAll(left.useDescriptor(d));
     public Set useDescriptor(Descriptor d) {
        HashSet newset=new HashSet();
        newset.addAll(left.useDescriptor(d));

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 57cf6c9d171055f47842b5d14029703cdbd61ddd..9f00c5b04611ee51dd02ebb952c9268d65741049 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -1160,6 +1160,9 @@ public class Termination {
        return okay;
     }
 
        return okay;
     }
 

+    /** This method sees if when the quantifiers listed in set are
+     *  fixed, whether there can be more than one unique binding for
+     *  the constraint or model definition rule qs.*/

     public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
        for(int i=0;i<qs.numQuantifiers();i++) {
            Quantifier q=qs.getQuantifier(i);
     public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
        for(int i=0;i<qs.numQuantifiers();i++) {
            Quantifier q=qs.getQuantifier(i);