00001
00005 package edu.mit.csail.sdg.squander.engine.kk;
00006
00007 import java.util.LinkedList;
00008 import java.util.List;
00009 import java.util.Map;
00010 import java.util.Map.Entry;
00011
00012 import kodkod.ast.Relation;
00013 import kodkod.instance.Bounds;
00014 import kodkod.instance.Tuple;
00015 import kodkod.instance.TupleFactory;
00016 import kodkod.instance.TupleSet;
00017 import kodkod.instance.Universe;
00018 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00019 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00020 import edu.mit.csail.sdg.squander.engine.ISquander;
00021 import forge.program.ForgeLiteral;
00022 import forge.program.ForgeType;
00023 import forge.program.ForgeVariable;
00024 import forge.program.GlobalVariable;
00025 import forge.program.InstanceDomain;
00026 import forge.program.InstanceLiteral;
00027 import forge.program.LocalVariable;
00028 import forge.program.ForgeType.Unary;
00029
00037 public class SquanderKodkodPart2Impl extends SquanderKodkodPartImpl {
00038
00039 public SquanderKodkodPart2Impl() { }
00040
00041 @Override
00042 protected Bounds createBounds() {
00043 reporter.creatingKodkodUniverse();
00044 Universe univ = createUniverse();
00045
00046 reporter.creatingKodkodBounds();
00047 TupleFactory f = univ.factory();
00048 Bounds b = new Bounds(univ);
00049
00050
00051 for (Entry<String, Relation> e : lit2rel.entrySet()) {
00052 String litName = e.getKey();
00053 Atom atom = lit2atom.get(litName);
00054 assert atom != null;
00055 b.boundExactly(e.getValue(), f.setOf(atom));
00056 }
00057
00058
00059 for (InstanceDomain dom : program.instanceDomains()) {
00060 List<ForgeLiteral> instLiterals = fconv.findLiteralsForType(dom);
00061 TupleSet bound = f.noneOf(dom.arity());
00062 if (!instLiterals.isEmpty()) {
00063 Object[] atoms = new Object[instLiterals.size()];
00064 int idx = 0;
00065 for (ForgeLiteral lit : instLiterals) {
00066 atoms[idx++] = lit2atom.get(lit.name());
00067 }
00068 bound = f.setOf(atoms);
00069 }
00070 b.boundExactly((Relation)type2expr.get(dom), bound);
00071 }
00072
00073
00074 for (GlobalVariable var : program.globalVariables()) {
00075 TupleSet[] lowup = getBounds(var, f);
00076 Relation rel = (Relation) var2rel.get(var.name());
00077 if (modifies.contains(var)) {
00078 Relation preRel = (Relation) var2rel.get(var.name() + "_pre");
00079 b.bound(preRel, lowup[0], lowup[1]);
00080
00081 TupleSet[] lu = getPostLowerUpper(var, lowup[0], f);
00082 b.bound(rel, lu[0], lu[1]);
00083 } else {
00084 b.bound(rel, lowup[0], lowup[1]);
00085 }
00086 }
00087
00088
00089 boundLocalVar(forgeScene.thisVar(), f, b);
00090 for (LocalVariable var : forgeScene.args())
00091 boundLocalVar(var, f, b);
00092 boundLocalVar(forgeScene.returnVar(), f, b);
00093
00094
00095 for (Integer i : ints) {
00096 Atom atom = lit2atom.get(Integer.toString(i));
00097 assert atom != null;
00098 b.boundExactly(i, f.setOf(atom));
00099 }
00100
00101 return b;
00102 }
00103
00104 private TupleSet[] getPostLowerUpper(GlobalVariable var, TupleSet lowerInitial, TupleFactory f) {
00105 TupleSet l = getPostLower(var, lowerInitial, f);
00106 TupleSet u = getPostUpper(var, l, f);
00107 return new TupleSet[] { l, u };
00108 }
00109
00110 protected TupleSet getPostLower(GlobalVariable g, TupleSet initialBound, TupleFactory f) {
00111 ObjTupleSet ots = modVal.get(g);
00112 if (ots == null)
00113 return f.noneOf(g.arity());
00114 List<ForgeLiteral> lits = new LinkedList<ForgeLiteral>(fconv.findLiteralsForType(g.type().domain()));
00115 for (ObjTuple t : ots.tuples()) {
00116 assert t.arity() == 1;
00117 if (t.arity() == 1) {
00118 InstanceLiteral l = forgeScene.instLitForObj(t.get(0));
00119 assert l != null;
00120 lits.remove(l);
00121 }
00122 }
00123
00124 TupleSet res = f.noneOf(g.arity());
00125 for (ForgeLiteral lit : lits) {
00126 TupleSet ts = f.setOf(f.tuple(lit2atom.get(lit.name())));
00127 TupleSet filtered = ts.product(join(ts, initialBound, f));
00128 res.addAll(filtered);
00129 }
00130 return res;
00131 }
00132
00133 protected TupleSet getPostUpper(GlobalVariable var, TupleSet postLower, TupleFactory f) {
00134 TupleSet extent = getExtent(var, f);
00135 ObjTupleSet upper = upperBounds.get(var);
00136 if (upper != null)
00137 extent = conv2tuples(upper, f);
00138 ObjTupleSet ots = modVal.get(var);
00139 if (ots == null)
00140 return extent;
00141 TupleSet mod = conv2tuples(ots, f);
00142 mod = mod.product(join(mod, extent, f));
00143 mod.addAll(postLower);
00144 return mod;
00145 }
00146
00147 private TupleSet join(TupleSet ts1, TupleSet ts2, TupleFactory f) {
00148 int arity = ts1.arity() + ts2.arity() - 2;
00149 TupleSet result = f.noneOf(arity);
00150 for (Tuple t1 : ts1)
00151 for (Tuple t2 : ts2)
00152 if (t1.atom(t1.arity() - 1) == t2.atom(0)) {
00153 Object[] atoms = new Object[arity];
00154 for (int i = 0; i < t1.arity() - 1; i++) atoms[i] = t1.atom(i);
00155 for (int i = 1; i < t2.arity(); i++) atoms[t1.arity() + i - 2] = t2.atom(i);
00156 result.add(f.tuple(atoms));
00157 }
00158 return result;
00159 }
00160
00161 @Override
00162 protected void boundLocalVar(LocalVariable var, TupleFactory f, Bounds b) {
00163 if (var == null)
00164 return;
00165 TupleSet[] lowup = getBounds(var, f);
00166 Relation rel = (Relation) var2rel.get(relName(var));
00167 b.bound(rel, lowup[0], lowup[1]);
00168 }
00169
00170 private TupleSet[] getBounds(ForgeVariable var, TupleFactory f) {
00171 TupleSet[] result = new TupleSet[2];
00172 ObjTupleSet bnd = fconv.heap2Lit().bounds().get(var.name());
00173 TupleSet lowerTupleSet;
00174 TupleSet upperTupleSet;
00175 if (bnd != null) {
00176 lowerTupleSet = conv2tuples(bnd, f);
00177 upperTupleSet = lowerTupleSet;
00178 } else {
00179 lowerTupleSet = f.noneOf(var.arity());
00180 upperTupleSet = getExtent(var, f);
00181 }
00182 result[0] = lowerTupleSet;
00183 result[1] = upperTupleSet;
00184 return result;
00185 }
00186
00187 private TupleSet getExtent(ForgeVariable var, TupleFactory f) {
00188
00189 ForgeType t = var.type();
00190 TupleSet result = null;
00191 for (int i = 0; i < t.arity(); i++) {
00192 ForgeType.Unary colType = (Unary) t.projectType(i);
00193 Map<Atom, ForgeLiteral> part = partitions.get(colType);
00194 assert part != null;
00195 TupleSet tuple = f.noneOf(1);
00196 for (Atom a : part.keySet()) {
00197 tuple.add(f.tuple(a));
00198 }
00199 if (result == null)
00200 result = tuple;
00201 else
00202 result = result.product(tuple);
00203 }
00204 if (result == null)
00205 result = f.noneOf(var.arity());
00206 return result;
00207 }
00208
00209 protected TupleSet conv2tuples(ObjTupleSet fc, TupleFactory f) {
00210 List<kodkod.instance.Tuple> kkTuples = new LinkedList<kodkod.instance.Tuple>();
00211 l: for (ObjTuple t : fc.tuples()) {
00212 Object[] atoms = new Object[t.arity()];
00213 int idx = 0;
00214 for (Object obj : t.tuple()) {
00215 String litName = getLitNameForObject(obj);
00216 Atom atom = lit2atom.get(litName);
00217 if (atom == null)
00218 continue l;
00219 atoms[idx++] = atom;
00220 }
00221 kkTuples.add(f.tuple(atoms));
00222 }
00223 if (kkTuples.isEmpty())
00224 return f.noneOf(fc.arity());
00225 else
00226 return f.setOf(kkTuples);
00227 }
00228
00229 private String getLitNameForObject(Object obj) {
00230 if (obj == null)
00231 return "null";
00232 if (obj instanceof Integer)
00233 return Integer.toString((Integer) obj);
00234 if (obj instanceof Boolean)
00235 return Boolean.toString((Boolean) obj);
00236 return forgeScene.instLitForObj(obj).name();
00237 }
00238 }