+ return true;
+ }
+
+ /** This method constructs bindings for an update using rule
+ * r. The boolean flag isremoval indicates that the update
+ * performs a removal. The function returns true if it is able to
+ * generate a valid set of bindings and false otherwise. */
+
+ boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
+ boolean goodupdate=true;
+ Inclusion inc=r.getInclusion();
+ for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+ Quantifier q=(Quantifier)iterator.next();
+ if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
+ VarDescriptor vd=null;
+ SetDescriptor set=null;
+ if (q instanceof SetQuantifier) {
+ vd=((SetQuantifier)q).getVar();
+ set=((SetQuantifier)q).getSet();
+ } else {
+ vd=((ForQuantifier)q).getVar();
+ }
+ if(inc instanceof SetInclusion) {
+ SetInclusion si=(SetInclusion)inc;
+ if ((si.elementexpr instanceof VarExpr)&&
+ (((VarExpr)si.elementexpr).getVar()==vd)) {
+ /* Can solve for v */
+ Binding binding=new Binding(vd,0);
+ bindings.add(binding);
+ } else {
+ goodupdate=false;
+ }
+ } else if (inc instanceof RelationInclusion) {
+ RelationInclusion ri=(RelationInclusion)inc;
+ boolean f1=true;
+ boolean f2=true;
+ if ((ri.getLeftExpr() instanceof VarExpr)&&
+ (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+ /* Can solve for v */
+ Binding binding=new Binding(vd,0);
+ bindings.add(binding);
+ } else f1=false;
+ if ((ri.getRightExpr() instanceof VarExpr)&&
+ (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+ /* Can solve for v */
+ Binding binding=new Binding(vd,0);
+ bindings.add(binding);
+ } else f2=false;
+ if (!(f1||f2))
+ goodupdate=false;
+ } else throw new Error("Inclusion not recognized");
+ if (!goodupdate)
+ if (isremoval) {
+ /* Removals don't need bindings anymore
+ Binding binding=new Binding(vd);
+ bindings.add(binding);*/
+ goodupdate=true;
+ } else if (q instanceof SetQuantifier) {
+ /* Create new element to bind to */
+ // search if the set 'set' has a size
+ Binding binding=new Binding(vd,set,exactsize.getsize(set)==1);
+ bindings.add(binding);
+ goodupdate=true;
+
+ } else
+ goodupdate=false;
+ } else if (q instanceof RelationQuantifier) {
+ RelationQuantifier rq=(RelationQuantifier)q;
+ for(int k=0;k<2;k++) {
+ VarDescriptor vd=(k==0)?rq.x:rq.y;
+ if(inc instanceof SetInclusion) {
+ SetInclusion si=(SetInclusion)inc;
+ if ((si.elementexpr instanceof VarExpr)&&
+ (((VarExpr)si.elementexpr).getVar()==vd)) {
+ /* Can solve for v */
+ Binding binding=new Binding(vd,0);
+ bindings.add(binding);
+ } else
+ goodupdate=false;
+ } else if (inc instanceof RelationInclusion) {
+ RelationInclusion ri=(RelationInclusion)inc;
+ boolean f1=true;
+ boolean f2=true;
+ if ((ri.getLeftExpr() instanceof VarExpr)&&
+ (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+ /* Can solve for v */
+ Binding binding=new Binding(vd,0);
+ bindings.add(binding);
+ } else f1=false;
+ if ((ri.getRightExpr() instanceof VarExpr)&&
+ (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+ /* Can solve for v */
+ Binding binding=new Binding(vd,0);
+ bindings.add(binding);
+ } else f2=false;
+ if (!(f1||f2))
+ goodupdate=false;
+ } else throw new Error("Inclusion not recognized");
+ if (!goodupdate)
+ if (isremoval) {
+ /* Removals don't need bindings anymore
+ Binding binding=new Binding(vd);
+ bindings.add(binding);*/
+ goodupdate=true;
+ } else
+ break;
+ }
+ if (!goodupdate)
+ break;
+ } else throw new Error("Quantifier not recognized");
+ }
+ return goodupdate;
+ }
+
+ /** Adds updates that add an item to the appropriate set or
+ * relation quantified over by the model definition rule.. */
+
+ boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r) {
+ Inclusion inc=r.getInclusion();
+ for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+ Quantifier q=(Quantifier)iterator.next();
+ /* Add quantifier */
+ /* FIXME: Analysis to determine when this update is necessary */
+ 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,false);
+ un.addUpdate(u);
+ if (abstractadd.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;
+ if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
+ Binding b=un.getBinding(sq.var);
+ Constraint reqc=exactsize.getConstraint(b.getSet());
+ constraintdependence.requiresConstraint(gn,reqc);
+ continue; /* Don't need to ensure addition for search */
+ }
+
+ ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+ eoe.td=ReservedTypeDescriptor.INT;
+ Updates u=new Updates(eoe,false);
+ un.addUpdate(u);
+ if (abstractadd.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 true;
+ }
+
+ /** This method generates the necessary updates to satisfy the
+ * conjunction ruleconj. */
+
+ boolean processconjunction(UpdateNode un,RuleConjunction ruleconj){
+ boolean okay=true;
+ for(int k=0;k<ruleconj.size();k++) {
+ DNFExpr de=ruleconj.get(k);
+ Expr e=de.getExpr();
+ if (e instanceof OpExpr) {
+ OpExpr ex=(OpExpr)de.getExpr();
+ Opcode op=ex.getOpcode();
+ Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
+ un.addUpdate(up);
+ } else if (e instanceof ElementOfExpr) {
+ Updates up=new Updates(e,de.getNegation());
+ un.addUpdate(up);
+ } else if (e instanceof TupleOfExpr) {
+ Updates up=new Updates(e,de.getNegation());
+ un.addUpdate(up);
+ } else if (e instanceof BooleanLiteralExpr) {
+ boolean truth=((BooleanLiteralExpr)e).getValue();
+ if (de.getNegation())
+ truth=!truth;
+ if (!truth) {
+ okay=false;
+ break;
+ }
+ } else {
+ System.out.println(e.getClass().getName());
+ throw new Error("Unrecognized Expr");
+ }
+ }
+ return okay;
+ }
+
+ public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
+ for(int i=0;i<qs.numQuantifiers();i++) {
+ Quantifier q=qs.getQuantifier(i);
+ if (set.contains(q))
+ continue;
+ if (q instanceof SetQuantifier) {
+ SetDescriptor sd=((SetQuantifier)q).getSet();
+ if (maxsize.getsize(sd)<=1&&
+ maxsize.getsize(sd)>=0)
+ continue;
+ } else if (q instanceof RelationQuantifier) {
+ RelationDescriptor rd=((RelationQuantifier)q).getRelation();
+ if (maxsize.getsize(rd)<=1&&
+ maxsize.getsize(rd)>=0)
+ continue;
+ }
+ return false;
+ }
+ return true;
+ }
+
+ public boolean mutuallyexclusive(SetDescriptor sd1, SetDescriptor sd2) {
+ if (mutualexclusive(sd1,sd2)||
+ mutualexclusive(sd2,sd1))
+ return true;
+ else
+ return false;
+ }
+
+ private boolean mutualexclusive(SetDescriptor sd1, SetDescriptor sd2) {
+ Vector rules=state.vRules;
+ for(int i=0;i<rules.size();i++) {
+ Rule r=(Rule)rules.get(i);
+ if (r.getInclusion().getTargetDescriptors().contains(sd1)) {
+ /* Rule may add items to sd1 */
+ SetInclusion si=(SetInclusion)r.getInclusion();
+ Expr ve=si.getExpr();
+ DNFRule drule=r.getDNFGuardExpr();
+ for(int j=0;j<drule.size();j++) {
+ RuleConjunction rconj=drule.get(j);
+ boolean containsexclusion=false;
+ for (int k=0;k<rconj.size();k++) {
+ DNFExpr dexpr=rconj.get(k);
+ if (dexpr.getNegation()&&
+ dexpr.getExpr() instanceof ElementOfExpr&&
+ ((ElementOfExpr)dexpr.getExpr()).element.equals(null,ve)) {
+ SetDescriptor sd=((ElementOfExpr)dexpr.getExpr()).set;
+ if (sd.isSubset(sd2))
+ containsexclusion=true;
+ }
+ }
+ if (!containsexclusion)
+ return false;
+ }
+ }
+ }
+ return true;