8 private Hashtable sizemap;
9 private Hashtable constraintmap;
10 private SetAnalysis setanalysis;
12 public ExactSize(State state) {
14 this.sizemap=new Hashtable();
15 this.constraintmap=new Hashtable();
16 this.setanalysis=state.setanalysis;
20 public int getsize(SetDescriptor sd) {
21 SizeObject so=new SizeObject(sd);
22 if (sizemap.containsKey(so))
23 return ((Integer)sizemap.get(so)).intValue();
27 public Constraint getConstraint(SetDescriptor sd) {
28 SizeObject so=new SizeObject(sd);
29 return (Constraint)constraintmap.get(so);
32 public int getsize(RelationDescriptor rd, SetDescriptor sd, boolean inverted) {
33 Iterator it=setanalysis.getSuperset(sd).iterator();
35 SizeObject so=new SizeObject(rd,sd,inverted);
36 if (sizemap.containsKey(so))
37 return ((Integer)sizemap.get(so)).intValue();
40 sd=(SetDescriptor)it.next();
45 public Constraint getConstraint(RelationDescriptor rd, SetDescriptor sd, boolean inverted) {
46 Iterator it=setanalysis.getSuperset(sd).iterator();
48 SizeObject so=new SizeObject(rd,sd,inverted);
49 if (constraintmap.containsKey(so))
50 return ((Constraint)constraintmap.get(so));
53 sd=(SetDescriptor)it.next();
58 private void computesizes() {
59 for(Iterator it=state.stSets.descriptors();it.hasNext();) {
60 SetDescriptor sd=(SetDescriptor)it.next();
61 for(int i=0;i<state.vConstraints.size();i++) {
62 Constraint c=(Constraint)state.vConstraints.get(i);
63 if (c.numQuantifiers()!=0)
65 DNFConstraint dconst=c.dnfconstraint;
68 for(int j=0;j<dconst.size();j++) {
69 Conjunction conj=dconst.get(j);
70 boolean goodmatch=false;
71 for(int k=0;k<conj.size();k++) {
72 DNFPredicate dpred=conj.get(k);
73 if (!dpred.isNegated()) {
74 Predicate p=dpred.getPredicate();
75 if (p instanceof ExprPredicate) {
76 ExprPredicate ep=(ExprPredicate)p;
77 if (ep.getType()==ExprPredicate.SIZE&&
78 ep.getOp()==Opcode.EQ&&
79 ep.getDescriptor()==sd&&
82 oldsize=ep.rightSize();
86 if (oldsize==ep.rightSize()) {
97 break; //this constraint won't work
101 System.out.println("Set "+sd.toString()+" has size "+oldsize);
102 SizeObject so=new SizeObject(sd);
103 sizemap.put(so,new Integer(oldsize));
104 constraintmap.put(so,c);
109 for(Iterator it=state.stRelations.descriptors();it.hasNext();) {
110 RelationDescriptor rd=(RelationDescriptor)it.next();
111 for(int i=0;i<state.vConstraints.size();i++) {
112 Constraint c=(Constraint)state.vConstraints.get(i);
113 if (c.numQuantifiers()!=1||!(c.getQuantifier(0) instanceof SetQuantifier))
115 SetQuantifier q=(SetQuantifier) c.getQuantifier(0);
117 DNFConstraint dconst=c.dnfconstraint;
119 boolean matches=true;
120 boolean inverted=false;
121 for(int j=0;j<dconst.size();j++) {
122 Conjunction conj=dconst.get(j);
123 boolean goodmatch=false;
124 for(int k=0;k<conj.size();k++) {
125 DNFPredicate dpred=conj.get(k);
126 if (!dpred.isNegated()) {
127 Predicate p=dpred.getPredicate();
128 if (p instanceof ExprPredicate) {
129 ExprPredicate ep=(ExprPredicate)p;
130 if (ep.getType()==ExprPredicate.SIZE&&
131 ep.getOp()==Opcode.EQ&&
132 ep.getDescriptor()==rd&&
134 ((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).getSetExpr()).getVar()==q.getVar()) {
136 oldsize=ep.rightSize();
138 inverted=ep.inverted();
141 if (oldsize==ep.rightSize()&&inverted==ep.inverted()) {
152 break; //this constraint won't work
156 System.out.println("Set "+rd.toString()+" has size "+oldsize);
157 SizeObject so=new SizeObject(rd,q.getSet(),inverted);
158 sizemap.put(so,new Integer(oldsize));
159 constraintmap.put(so,c);