5 public class ConstraintDependence {
11 Termination termination;
13 ConstraintDependence(State state, Termination t) {
16 constnodes=new HashSet();
18 constonode=new Hashtable();
19 nodetonode=new Hashtable();
23 public Set computeOrdering() {
24 HashSet allnodes=new HashSet();
25 allnodes.addAll(constnodes);
26 allnodes.addAll(nodes);
27 boolean acyclic=GraphNode.DFS.depthFirstSearch(allnodes);
29 throw new Error("Cylic dependency between constraints.");
31 TreeSet topologicalsort = new TreeSet(new Comparator() {
32 public boolean equals(Object obj) { return false; }
33 public int compare(Object o1, Object o2) {
34 GraphNode g1 = (GraphNode) o1;
35 GraphNode g2 = (GraphNode) o2;
36 return g1.getFinishingTime() - g2.getFinishingTime();
40 topologicalsort.addAll(constnodes);
41 return topologicalsort;
44 public void addNode(GraphNode gn) {
45 GraphNode gn2=new GraphNode(gn.getLabel(),gn.getTextLabel(),gn);
47 nodetonode.put(gn,gn2);
50 public void associateWithConstraint(GraphNode gn, Constraint c) {
51 if (!nodetonode.containsKey(gn)) {
54 GraphNode ggn=(GraphNode)nodetonode.get(gn);
55 GraphNode gc=(GraphNode)constonode.get(c);
56 GraphNode.Edge e=new GraphNode.Edge("associated",ggn);
60 public void requiresConstraint(GraphNode gn, Constraint c) {
61 if (!nodetonode.containsKey(gn)) {
64 GraphNode ggn=(GraphNode)nodetonode.get(gn);
65 GraphNode gc=(GraphNode)constonode.get(c);
66 GraphNode.Edge e=new GraphNode.Edge("requires",gc);
70 public void traversedependences(Termination termination) {
71 constructconjunctionnodes(termination);
72 constructconjunctionedges(termination);
73 Set removedset=termination.removedset;
75 for(int i=0;i<state.vConstraints.size();i++) {
76 Constraint c=(Constraint)state.vConstraints.get(i);
77 Set conjset=(Set)termination.conjunctionmap.get(c);
78 HashSet exploredset=new HashSet();
80 for(Iterator it=conjset.iterator();it.hasNext();) {
81 GraphNode gn=(GraphNode)it.next();
82 recursedependence(c,termination,exploredset,gn);
87 void recursedependence(Constraint c,Termination termination, HashSet exploredset, GraphNode gn) {
88 Set removedset=termination.removedset;
89 Set conjunctionset=termination.conjunctions;
91 if (removedset.contains(gn))
94 associateWithConstraint(gn,c);
95 for(Iterator it=gn.edges();it.hasNext();) {
96 GraphNode.Edge e=(GraphNode.Edge) it.next();
97 GraphNode gn2=e.getTarget();
98 if (!(exploredset.contains(gn2)||
99 conjunctionset.contains(gn2)))
100 recursedependence(c,termination,exploredset,gn2);
104 /** Constructs a node for each Constraint */
105 private void constructnodes() {
106 for(int i=0;i<state.vConstraints.size();i++) {
107 Constraint c=(Constraint)state.vConstraints.get(i);
108 GraphNode gn=new GraphNode(c.toString(),c);
109 constonode.put(c,gn);
114 private void constructconjunctionnodes(Termination termination) {
115 /*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
116 GraphNode conjnode=(GraphNode)it.next();
117 TermNode tn=(TermNode)conjnode.getOwner();
118 Conjunction conj=tn.getConjunction();
121 Set removedset=termination.removedset;
123 for(int i=0;i<state.vConstraints.size();i++) {
124 Constraint c=(Constraint)state.vConstraints.get(i);
125 Set conjset=(Set)termination.conjunctionmap.get(c);
126 for(Iterator it=conjset.iterator();it.hasNext();) {
127 GraphNode gn=(GraphNode)it.next();
128 if (!removedset.contains(gn))
129 associateWithConstraint(gn,c);
134 private void constructconjunctionedges(Termination termination) {
135 Set removedset=termination.removedset;
136 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
137 GraphNode conjnode=(GraphNode)it.next();
138 if (removedset.contains(conjnode))
141 TermNode tn=(TermNode)conjnode.getOwner();
142 Conjunction conj=tn.getConjunction();
143 for(int i=0;i<conj.size();i++) {
144 DNFPredicate dpred=conj.get(i);
145 Predicate pred=dpred.getPredicate();
147 if (pred instanceof InclusionPredicate) {
148 InclusionPredicate ip=(InclusionPredicate)pred;
150 } else if (pred instanceof ExprPredicate) {
151 ExprPredicate ep=(ExprPredicate)pred;
153 } else throw new Error("Unrecognized Predicate");
154 Set functions=expr.getfunctions();
157 for(Iterator fit=functions.iterator();fit.hasNext();) {
158 Function f=(Function)fit.next();
159 if (rulesensurefunction(state,f,false))
160 continue; //no constraint needed to ensure
162 Set s=providesfunction(state,f);
164 System.out.println("Warning: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
167 Constraint c=(Constraint)s.iterator().next(); //Take the first one
168 requiresConstraint(conjnode,c);
174 /** This method determines whether the model definition rules
175 * ensure that the relation and evaluation domain descriped by f
176 * is either a function (if isPartial=false) or a partial function
177 * (if isPartial=true). */
179 static private boolean rulesensurefunction(State state,Function f, boolean isPartial) {
180 boolean foundrule=false;
181 for(int i=0;i<state.vRules.size();i++) {
182 Rule r=(Rule)state.vRules.get(i);
183 if (r.getInclusion().getTargetDescriptors().contains(f.getRelation())) {
184 RelationInclusion ri=(RelationInclusion)r.getInclusion();
185 Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
186 SetDescriptor sd=e.getSet();
189 if (state.setanalysis.noIntersection(f.getSet(),sd))
190 continue; /* This rule doesn't effect the function */
191 if (foundrule) /* two different rules are a problem */
193 if (!((e instanceof VarExpr)&&(r.numQuantifiers()==1)))
195 VarExpr ve=(VarExpr)e;
196 Quantifier q=r.getQuantifier(0);
197 if (!(q instanceof SetQuantifier))
199 SetQuantifier sq=(SetQuantifier)q;
200 if (ve.getVar()!=sq.getVar())
203 if (!sq.getSet().isSubset(f.getSet()))
205 if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
206 ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
209 Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
210 if (isPartial||e2.isSafe())
219 static private Set providesfunction(State state, Function f) {
220 return providesfunction(state,f,false);
223 static private Set providesfunction(State state, Function f, boolean isPartial) {
224 HashSet set=new HashSet();
225 for(int i=0;i<state.vConstraints.size();i++) {
226 Constraint c=(Constraint)state.vConstraints.get(i);
227 boolean goodconstraint=true;
228 DNFConstraint dnfconst=c.dnfconstraint;
229 for(int j=0;j<dnfconst.size();j++) {
230 Conjunction conj=dnfconst.get(j);
231 boolean conjprovides=false;
232 for(int k=0;k<conj.size();k++) {
233 DNFPredicate dpred=conj.get(k);
234 if (!dpred.isNegated()&&
235 (dpred.getPredicate() instanceof ExprPredicate)&&
236 ((ExprPredicate)dpred.getPredicate()).getType()==ExprPredicate.SIZE) {
237 ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
238 if (ep.isRightInt()&&
240 (ep.getOp()==Opcode.EQ||(ep.getOp()==Opcode.LE&&isPartial))&&
241 ep.inverted()==f.isInverse()&&
242 ep.getDescriptor()==f.getRelation()) {
243 ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
244 VarDescriptor vd=se.getVar();
245 if (c.numQuantifiers()==1) {
246 for(int l=0;l<c.numQuantifiers();l++) {
247 Quantifier q=c.getQuantifier(l);
248 if (q instanceof SetQuantifier&&
249 ((SetQuantifier)q).getVar()==vd) {
250 SetDescriptor sd=((SetQuantifier)q).getSet();
251 if (sd.isSubset(f.getSet()))
261 goodconstraint=false;
272 /** This method determines whether the model definition rules
273 * ensure that the relation r (or inverse relation if inverse is
274 * true) evaluated on the domain sd is either a function (if
275 * isPartial=false) or a partial function (if isPartial=true). */
277 static public boolean rulesensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse, boolean isPartial) {
278 return rulesensurefunction(state, new Function(r,sd,inverse,null),isPartial);
281 /** This method determines whether the model constraints ensure
282 * that the relation r (or inverse relation if inverse is true)
283 * evaluated on the domain sd is either a function (if
284 * isPartial=false) or a partial function (if isPartial=true). */
286 static public boolean constraintsensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse,boolean isPartial) {
287 Set constraints=providesfunction(state, new Function(r,sd,inverse,null),isPartial);
288 return (!constraints.isEmpty());
291 public static class Function {
292 private RelationDescriptor rd;
293 private SetDescriptor sd;
294 private boolean inverse;
297 public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
298 this.inverse=inverse;
304 public Expr getExpr() {
308 public SetDescriptor getSet() {
312 public RelationDescriptor getRelation() {
316 public boolean isInverse() {