1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.Collection;
7 import java.util.Iterator;
8 import java.util.LinkedList;
9 import java.util.List;
10 import java.io.BufferedWriter;
11 import java.io.FileWriter;
12 import java.io.IOException;
13 import java.io.PrintStream;
14 import java.math.BigInteger;
15 import jwutil.graphs.GlobalPathNumbering;
16 import jwutil.graphs.PathNumbering;
17 import jwutil.graphs.SCCPathNumbering;
18 import jwutil.io.SystemProperties;
19 import jwutil.util.Assert;
20 import net.sf.javabdd.BDD;
21 import net.sf.javabdd.BDDDomain;
22
23 /***
24 * This class represents a special kind of rule used for numbering paths.
25 *
26 * The form of the rule is as follows:
27 *
28 * pathNum(a,b,x,y) :- A(a,b),B(b,c),C(c,d),D(d,e). number
29 *
30 * The subgoal relations (A, B, C, and D) define the edges of the graph.
31 * The first two variables of the head relation define the edge you want
32 * to number, and the next two variables are filled in with the number
33 * of the source and destination, respectively.
34 *
35 * @author jwhaley
36 * @version $Id: NumberingRule.java 585 2005-06-10 18:04:11Z joewhaley $
37 */
38 public class NumberingRule extends InferenceRule {
39
40 /***
41 * Trace flag.
42 */
43 boolean TRACE = false;
44
45 /***
46 * Trace output stream.
47 */
48 PrintStream out;
49
50 /***
51 * Graph of relation.
52 */
53 RelationGraph rg;
54
55 /***
56 * Path numbering.
57 */
58 PathNumbering pn;
59
60 /***
61 * Time spent on computing this rule.
62 */
63 long totalTime;
64
65 /***
66 * Flag to control the dumping of the numbering of the graph in dot format.
67 */
68 static boolean DUMP_DOTGRAPH = !SystemProperties.getProperty("dumpnumberinggraph", "no").equals("no");
69
70 String numberingType = SystemProperties.getProperty("numberingtype", "scc");
71
72 /***
73 * Construct a new NumberingRule.
74 * Not to be called externally.
75 *
76 * @param s
77 * @param ir
78 */
79 NumberingRule(Solver s, InferenceRule ir) {
80 super(s, ir.top, ir.bottom, ir.id);
81 Assert._assert(ir.top.size() > 1);
82 out = s.out;
83 }
84
85
86
87
88 void initialize() {
89 if (TRACE) out.println("Initializing numbering rule: " + this);
90 RuleTerm root = (RuleTerm) top.get(0);
91 Variable rootVar;
92 if (root.variables.size() == 1) {
93 rootVar = (Variable) root.variables.get(0);
94 } else {
95 List rootVars = new LinkedList(root.variables);
96 calculateNecessaryVariables();
97 rootVars.retainAll(necessaryVariables);
98 Assert._assert(rootVars.size() == 1);
99 rootVar = (Variable) rootVars.get(0);
100 }
101 if (TRACE) out.println("Root variable: " + rootVar);
102 List edges = top.subList(1, top.size());
103 rg = new RelationGraph(root, rootVar, edges);
104 }
105
106
107
108
109 public Collection
110 throw new InternalError("Cannot split a numbering rule!");
111 }
112
113 public Variable checkUnnecessaryVariables() {
114 return null;
115 }
116
117
118
119
120
121
122 public boolean update() {
123 if (pn != null) {
124 Assert.UNREACHABLE("Can't put numbering in a cycle.");
125 return false;
126 }
127 if (solver.NOISY) solver.out.println("Applying numbering rule:\n " + this);
128 long time = System.currentTimeMillis();
129 if (numberingType.equals("scc"))
130 pn = new SCCPathNumbering();
131 else if (numberingType.equals("global"))
132 pn = new GlobalPathNumbering();
133 else
134 Assert.UNREACHABLE("Unknown numbering type "+numberingType);
135 BigInteger num = pn.countPaths(rg);
136 if (solver.NOISY) solver.out.println("Done counting paths ("+(System.currentTimeMillis()-time)+" ms, number of paths = "+num+" ("+num.bitLength()+" bits)");
137 Iterator i = bottom.variables.iterator();
138 Variable v1, v2;
139 v1 = (Variable) i.next();
140 v2 = (Variable) i.next();
141 if (TRACE) out.println("Finding relations with (" + v1 + "," + v2 + ")");
142
143 for (i = rg.edges.iterator(); i.hasNext();) {
144 RuleTerm rt = (RuleTerm) i.next();
145 if (rt.variables.get(0) == v1 && rt.variables.get(1) == v2) {
146 if (TRACE) out.println("Match: " + rt);
147
148 BDDRelation bddr = (BDDRelation) bottom.relation;
149 Iterator k = bddr.domains.iterator();
150 BDDDomain d0, d1, d2, d3;
151 d0 = (BDDDomain) k.next();
152 d1 = (BDDDomain) k.next();
153 if (TRACE) out.println("Domains for edge: " + d0 + " -> " + d1);
154 d2 = (BDDDomain) k.next();
155 d3 = (BDDDomain) k.next();
156 if (TRACE) out.println("Domains for numbering: " + d2 + " -> " + d3);
157 Assert._assert(d0 != d1);
158 Assert._assert(d2 != d3);
159 for (TupleIterator j = rt.relation.iterator(); j.hasNext();) {
160 BigInteger[] t = j.nextTuple();
161 Object source = RelationGraph.makeGraphNode(v1, t[0]);
162 Object target = RelationGraph.makeGraphNode(v2, t[1]);
163 PathNumbering.Range r0 = pn.getRange(source);
164 PathNumbering.Range r1 = pn.getEdge(source, target);
165 if (TRACE) out.println("Edge: " + source + " -> " + target + "\t" + r0 + " -> " + r1);
166 if (r0 == null) {
167 if (TRACE) out.println("Unreachable edge!");
168 Assert._assert(r1 == null);
169 continue;
170 }
171 Assert._assert(r1 != null);
172
173 BDD result = buildMap(d2, PathNumbering.toBigInt(r0.low), PathNumbering.toBigInt(r0.high), d3, PathNumbering.toBigInt(r1.low),
174 PathNumbering.toBigInt(r1.high));
175 result.andWith(d0.ithVar(t[0]));
176 result.andWith(d1.ithVar(t[1]));
177 bddr.relation.orWith(result);
178 }
179 }
180 }
181 time = System.currentTimeMillis() - time;
182 if (solver.NOISY) out.println("Time spent: " + time + " ms");
183 totalTime += time;
184 if (DUMP_DOTGRAPH) {
185 BufferedWriter dos = null;
186 try {
187 dos = new BufferedWriter(new FileWriter(solver.basedir + bottom.relation.name + ".dot"));
188 pn.dotGraph(dos, rg.getRoots(), rg.getNavigator());
189 } catch (IOException x) {
190 solver.err.println("Error while dumping dot graph.");
191 x.printStackTrace();
192 } finally {
193 if (dos != null) try {
194 dos.close();
195 } catch (IOException x) {
196 }
197 }
198 }
199 ((BDDRelation) bottom.relation).updateNegated();
200 return true;
201 }
202
203 /***
204 * Utility function to build a map from a range in one BDD domain to a range in another
205 *
206 * @param d1 first domain
207 * @param startD1 start of range in d1, inclusive
208 * @param endD1 end of range in d1, inclusive
209 * @param d2 second domain
210 * @param startD2 start of range in d2, inclusive
211 * @param endD2 end of range in d2, inclusive
212 * @return BDD representation of map
213 */
214 static BDD buildMap(BDDDomain d1, BigInteger startD1, BigInteger endD1, BDDDomain d2, BigInteger startD2, BigInteger endD2) {
215 BDD r;
216 BigInteger sizeD1 = endD1.subtract(startD1);
217 BigInteger sizeD2 = endD2.subtract(startD2);
218 if (sizeD1.signum() == -1) {
219 r = d2.varRange(startD2.longValue(), endD2.longValue());
220 r.andWith(d1.ithVar(0));
221 } else if (sizeD2.signum() == -1) {
222 r = d1.varRange(startD1.longValue(), endD1.longValue());
223 r.andWith(d2.ithVar(0));
224 } else {
225 int bits;
226 if (endD1.compareTo(endD2) != -1) {
227 bits = endD1.bitLength();
228 } else {
229 bits = endD2.bitLength();
230 }
231 long val = startD2.subtract(startD1).longValue();
232 r = d1.buildAdd(d2, bits, val);
233 if (sizeD2.compareTo(sizeD1) != -1) {
234
235 r.andWith(d1.varRange(startD1.longValue(), endD1.longValue()));
236 } else {
237
238 r.andWith(d2.varRange(startD2.longValue(), endD2.longValue()));
239 }
240 }
241 return r;
242 }
243
244
245
246
247
248
249 public void reportStats() {
250 out.println("Rule " + this);
251 out.println(" Time: " + totalTime + " ms");
252 }
253 }