00001
00005 package edu.mit.csail.sdg.squander.engine.kk;
00006
00007 import java.util.ArrayList;
00008 import java.util.Collection;
00009 import java.util.Collections;
00010 import java.util.Comparator;
00011 import java.util.HashMap;
00012 import java.util.HashSet;
00013 import java.util.Iterator;
00014 import java.util.LinkedHashMap;
00015 import java.util.LinkedList;
00016 import java.util.List;
00017 import java.util.Map;
00018 import java.util.Set;
00019 import java.util.Map.Entry;
00020
00021 import kodkod.ast.Relation;
00022 import kodkod.engine.Solution;
00023 import kodkod.instance.Bounds;
00024 import kodkod.instance.TupleFactory;
00025 import kodkod.instance.TupleSet;
00026 import kodkod.instance.Universe;
00027 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00028 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00029 import edu.mit.csail.sdg.squander.engine.ISquander;
00030 import edu.mit.csail.sdg.squander.engine.ISquanderResult.IEvaluator;
00031 import edu.mit.csail.sdg.squander.log.Log;
00032 import forge.program.ForgeDomain;
00033 import forge.program.ForgeExpression;
00034 import forge.program.ForgeLiteral;
00035 import forge.program.ForgeType;
00036 import forge.program.ForgeVariable;
00037 import forge.program.GlobalVariable;
00038 import forge.program.InstanceDomain;
00039 import forge.program.IntegerLiteral;
00040 import forge.program.LocalVariable;
00041 import forge.program.ForgeType.Unary;
00042 import forge.solve.ForgeAtom;
00043 import forge.solve.ForgeBounds;
00044 import forge.solve.ForgeConstant;
00045
00053 public class SquanderKodkodPartImpl extends SquanderKodkodImpl {
00054
00055
00056
00057
00058
00059 class KodkodIntEval extends KodkodEval {
00060
00061 private ForgeVariable var;
00062
00063 public KodkodIntEval(Iterator<Solution> solutions) {
00064 super(solutions);
00065 }
00066
00067 @Override
00068 public ObjTupleSet evaluate(ForgeVariable var) {
00069 this.var = var;
00070 return super.evaluateExpr(var);
00071 }
00072
00073 @Override
00074 public ObjTupleSet evaluateExpr(ForgeExpression expr) {
00075 throw new RuntimeException("No can do");
00076 }
00077
00078 @Override
00079 protected ObjTupleSet makeConst(TupleSet ts) {
00080 assert var.arity() == ts.arity();
00081 ObjTupleSet res = new ObjTupleSet(ts.arity());
00082 for (kodkod.instance.Tuple t : ts) {
00083 ObjTuple fTuple = new ObjTuple();
00084 for (int i = 0; i < t.arity(); i++) {
00085 Atom atom = (Atom) t.atom(i);
00086 ForgeType.Unary type = (Unary) var.type().projectType(i);
00087 ForgeLiteral lit = partitions.get(type).get(atom);
00088 assert lit != null;
00089 Object fAtom = fconv.lit2obj(lit);
00090 fTuple = ObjTuple.product(fTuple, fAtom);
00091 }
00092 if (fTuple.arity() != 0)
00093 res.add(fTuple);
00094 }
00095 return res;
00096 }
00097
00098 }
00099
00100
00101
00102
00103
00104
00105 protected static class Atom {
00106 int key;
00107
00108 Atom(int key) {
00109 this.key = key;
00110 }
00111
00112 @Override
00113 public int hashCode() {
00114 final int prime = 31;
00115 int result = 1;
00116 result = prime * result + key;
00117 return result;
00118 }
00119
00120 @Override
00121 public boolean equals(Object obj) {
00122 if (this == obj)
00123 return true;
00124 if (obj == null)
00125 return false;
00126 if (getClass() != obj.getClass())
00127 return false;
00128 Atom other = (Atom) obj;
00129 if (key != other.key)
00130 return false;
00131 return true;
00132 }
00133
00134 @Override
00135 public String toString() {
00136 return "a" + Integer.toString(key);
00137 }
00138
00139 }
00140
00141
00142
00143 protected Map<ForgeType.Unary, Map<Atom, ForgeLiteral>> partitions;
00144 protected Map<String, Atom> lit2atom;
00145
00146 public SquanderKodkodPartImpl() { }
00147
00148 private void sort(List<ForgeType.Unary> types) {
00149 Collections.sort(types, new Comparator<ForgeType.Unary>() {
00150 @Override
00151 public int compare(ForgeType.Unary o1, ForgeType.Unary o2) {
00152 int n1 = fconv.findLiteralsForType(o1).size();
00153 int n2 = fconv.findLiteralsForType(o2).size();
00154 return -(new Integer(n1).compareTo(n2));
00155 }
00156 });
00157 }
00158
00159 protected void partitionDomains() {
00160 List<ForgeType.Unary> types = new ArrayList<ForgeType.Unary>(forgeScene.usedTypes());
00161 sort(types);
00162
00163 partitions = new LinkedHashMap<ForgeType.Unary, Map<Atom, ForgeLiteral>>();
00164 lit2atom = new LinkedHashMap<String, Atom>();
00165
00166
00167 for (ForgeLiteral lit : fconv.findLiteralsForType(program.integerDomain())) {
00168 int value = ((IntegerLiteral) lit).value();
00169 ints.add(value);
00170 }
00171
00172 Map<ForgeDomain, Set<ForgeDomain>> deps = createDependencies(types);
00173 Iterator<Unary> it = types.iterator();
00174 Set<Atom> allAtoms = processFirst(it.next());
00175 while (it.hasNext()) {
00176 processNext(it.next(), deps, allAtoms);
00177 }
00178 }
00179
00180 private void processNext(ForgeType.Unary t, Map<ForgeDomain, Set<ForgeDomain>> deps, Set<Atom> allAtoms) {
00181 Map<Atom, ForgeLiteral> map = new LinkedHashMap<Atom, ForgeLiteral>();
00182 Object x = partitions.put(t, map);
00183 assert x == null;
00184 List<ForgeLiteral> lits = fconv.findLiteralsForType(t);
00185
00186 for (ForgeLiteral lit : lits) {
00187 Atom a = lit2atom.get(lit.name());
00188 if (a == null)
00189 continue;
00190 x = map.put(a, lit);
00191 assert x == null;
00192 }
00193
00194
00195 Set<Atom> availAtoms = new HashSet<Atom>(allAtoms);
00196 availAtoms.removeAll(map.keySet());
00197
00198
00199 for (ForgeLiteral lit : lits) {
00200 Atom a = lit2atom.get(lit.name());
00201 if (a != null)
00202 continue;
00203 a = nextAtomForLiteral(t, lit.type(), deps, new HashSet<Atom>(availAtoms));
00204 availAtoms.remove(a);
00205 lit2atom.put(lit.name(), a);
00206 x = map.put(a, lit);
00207 assert x == null;
00208 }
00209 }
00210
00211 private Set<Atom> processFirst(ForgeType.Unary t) {
00212 Set<Atom> atoms = new HashSet<Atom>();
00213 HashMap<Atom, ForgeLiteral> at2lit = new HashMap<Atom, ForgeLiteral>();
00214 int idx = 0;
00215 for (ForgeLiteral lit : fconv.findLiteralsForType(t)) {
00216 Atom atom = new Atom(idx++);
00217 lit2atom.put(lit.name(), atom);
00218 at2lit.put(atom, lit);
00219 atoms.add(atom);
00220 }
00221 partitions.put(t, at2lit);
00222 return Collections.unmodifiableSet(atoms);
00223 }
00224
00225 private Map<ForgeDomain, Set<ForgeDomain>> createDependencies(List<ForgeType.Unary> types) {
00226 Map<ForgeDomain, Set<ForgeDomain>> deps = new HashMap<ForgeDomain, Set<ForgeDomain>>();
00227 for (ForgeType.Unary type : types) {
00228 for (ForgeDomain t1 : type.tupleTypes()) {
00229 if (!deps.containsKey(t1))
00230 deps.put(t1, new HashSet<ForgeDomain>());
00231 for (ForgeDomain t2 : type.tupleTypes()) {
00232 if (t1 == t2)
00233 continue;
00234 deps.get(t1).add(t2);
00235 }
00236 }
00237 }
00238 return deps;
00239 }
00240
00241 protected Atom nextAtomForLiteral(Unary partition, ForgeDomain litType,
00242 Map<ForgeDomain, Set<ForgeDomain>> deps, Set<Atom> availAtoms) {
00243
00244 for (ForgeDomain d : deps.get(litType)) {
00245 for (ForgeLiteral l : fconv.findLiteralsForType(d)) {
00246 Atom aa = lit2atom.get(l.name());
00247 if (aa != null) {
00248 availAtoms.remove(aa);
00249 }
00250 }
00251 }
00252 assert !availAtoms.isEmpty();
00253 return availAtoms.iterator().next();
00254 }
00255
00256
00257
00258
00259
00260
00261
00262
00263
00264
00265
00266
00267
00268
00269
00270
00271
00272
00273
00274
00275
00276
00277
00278
00279
00280
00281
00282
00283
00284
00285
00286
00287
00288
00289
00290
00291
00292
00293
00294
00295
00296
00297
00298
00299
00300
00301
00302
00303
00304
00305
00306
00307
00308
00309
00310
00311
00312
00313
00314
00315
00316
00317
00318
00319
00320
00321
00322
00323
00324
00325
00326
00327
00328
00329
00330
00331
00332
00333
00334
00335
00336
00337
00338
00339
00340
00341
00342
00343
00344
00345
00346
00347
00348
00349
00350
00351
00352
00353
00354
00355
00356
00357
00358
00359
00360
00361
00362
00363
00364
00365 @Override
00366 protected Universe createUniverse() {
00367 partitionDomains();
00368 Log.debug(printPartitions());
00369 Collection<Object> atoms = new LinkedList<Object>();
00370 for (Atom a : lit2atom.values()) {
00371 if (atoms.contains(a))
00372 continue;
00373 atoms.add(a);
00374 }
00375 return new Universe(atoms);
00376 }
00377
00378 private String printPartitions() {
00379 StringBuilder sb = new StringBuilder();
00380 for (Entry<Unary, Map<Atom, ForgeLiteral>> e : partitions.entrySet()) {
00381 sb.append("partition: " + e.getKey()).append("\n");
00382 for (Entry<Atom, ForgeLiteral> atoms : e.getValue().entrySet()) {
00383 sb.append(String.format(" %2s: %s\n", atoms.getKey(), atoms.getValue()));
00384 }
00385 }
00386 return sb.toString();
00387
00388
00389
00390
00391
00392
00393
00394
00395
00396
00397
00398
00399
00400
00401
00402
00403
00404
00405
00406
00407 }
00408
00409 @Override
00410 protected Bounds createBounds() {
00411 ForgeBounds forgeBounds = fconv.forgeBounds();
00412 reporter.creatingKodkodUniverse();
00413 Universe univ = createUniverse();
00414
00415 reporter.creatingKodkodBounds();
00416 TupleFactory f = univ.factory();
00417 Bounds b = new Bounds(univ);
00418
00419
00420 for (Entry<String, Relation> e : lit2rel.entrySet()) {
00421 String litName = e.getKey();
00422 b.boundExactly(e.getValue(), f.setOf(lit2atom.get(litName)));
00423 }
00424
00425
00426 for (InstanceDomain dom : program.instanceDomains()) {
00427 List<ForgeLiteral> instLiterals = fconv.findLiteralsForType(dom);
00428 TupleSet bound = f.noneOf(dom.arity());
00429 if (!instLiterals.isEmpty()) {
00430 Object[] atoms = new Object[instLiterals.size()];
00431 int idx = 0;
00432 for (ForgeLiteral lit : instLiterals) {
00433 atoms[idx++] = lit2atom.get(lit.name());
00434 }
00435 bound = f.setOf(atoms);
00436 }
00437 b.boundExactly((Relation) type2expr.get(dom), bound);
00438 }
00439
00440
00441 for (GlobalVariable var : program.globalVariables()) {
00442 ForgeConstant lower = forgeBounds.initialLowerBound(var);
00443 ForgeConstant upper = lower;
00444 if (forgeScene.isSpecField(var)) {
00445 upper = forgeBounds.initialUpperBound(var);
00446 }
00447 TupleSet lowerTupleSet = conv2tuples(lower, f);
00448 TupleSet upperTupleSet = conv2tuples(upper, f);
00449 Relation rel = (Relation) var2rel.get(var.name());
00450 if (modifies.contains(var)) {
00451 Relation preRel = (Relation) var2rel.get(var.name() + "_pre");
00452 b.bound(preRel, lowerTupleSet, upperTupleSet);
00453 ForgeConstant postLower = getPostLower(var, lower);
00454 ForgeConstant postUpper = getPostUpper(var, postLower);
00455 b.bound(rel, conv2tuples(postLower, f), conv2tuples(postUpper, f));
00456 } else {
00457 b.bound(rel, lowerTupleSet, upperTupleSet);
00458 }
00459 }
00460
00461
00462 boundLocalVar(forgeScene.thisVar(), f, b);
00463 for (LocalVariable var : forgeScene.args())
00464 boundLocalVar(var, f, b);
00465 boundLocalVar(forgeScene.returnVar(), f, b);
00466
00467
00468 for (Integer i : ints) {
00469 b.boundExactly(i, f.setOf(new Atom(i)));
00470 }
00471
00472 reporter.end();
00473 return b;
00474 }
00475
00476 @Override
00477 protected IEvaluator getEval(Iterator<Solution> solutions) {
00478 return new KodkodIntEval(solutions);
00479 }
00480
00481 @Override
00482 protected Object convAtom(ForgeAtom a) {
00483 return lit2atom.get(a.name());
00484 }
00485
00486 }