00001
00005 package edu.mit.csail.sdg.squander.engine;
00006
00007 import java.util.HashMap;
00008 import java.util.Map;
00009 import java.util.Stack;
00010
00011 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00012 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00013 import edu.mit.csail.sdg.squander.engine.ISquanderResult.IEvaluator;
00014 import edu.mit.csail.sdg.util.collections.UniqueList;
00015 import forge.program.BinaryExpression;
00016 import forge.program.BooleanDomain;
00017 import forge.program.ConditionalExpression;
00018 import forge.program.ExpressionVisitor;
00019 import forge.program.ForgeExpression;
00020 import forge.program.ForgeLiteral;
00021 import forge.program.ForgeType;
00022 import forge.program.ForgeVariable;
00023 import forge.program.IntegerDomain;
00024 import forge.program.LocalVariable;
00025 import forge.program.OldExpression;
00026 import forge.program.ProjectionExpression;
00027 import forge.program.QuantifyExpression;
00028 import forge.program.UnaryExpression;
00029 import forge.solve.ForgeBounds;
00030
00035 public class SquanderEval2 extends ExpressionVisitor<ObjTupleSet> {
00036
00037 static interface BinFunc<R, T> {
00038 public static BinFunc<Boolean, Boolean> AND = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 && b2; }};
00039 public static BinFunc<Boolean, Boolean> OR = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 || b2; }};
00040 public static BinFunc<Boolean, Boolean> XOR = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 != b2; }};
00041 public static BinFunc<Boolean, Boolean> IFF = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 == b2; }};
00042 public static BinFunc<Boolean, Boolean> IMPLIES = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 || !b2; }};
00043
00044 public static BinFunc<Boolean, Integer> GT = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 > b2; }};
00045 public static BinFunc<Boolean, Integer> GTE = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 >= b2; }};
00046 public static BinFunc<Boolean, Integer> LT = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 < b2; }};
00047 public static BinFunc<Boolean, Integer> LTE = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 <= b2; }};
00048
00049 public static BinFunc<Integer, Integer> PLUS = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 + b2; }};
00050 public static BinFunc<Integer, Integer> MINUS = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 - b2; }};
00051 public static BinFunc<Integer, Integer> TIMES = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 * b2; }};
00052 public static BinFunc<Integer, Integer> DIVIDE = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 / b2; }};
00053 public static BinFunc<Integer, Integer> MOD = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 % b2; }};
00054
00055 public R exe(T b1, T b2);
00056 }
00057
00058 private ForgeConverter fconv;
00059 private Heap2Bounds heap2lit;
00060
00061 private boolean hasSolution = false;
00062 private Stack<StackElem> quantStack = new Stack<StackElem>();
00063 private Map<ForgeVariable, ObjTupleSet> assignments = new HashMap<ForgeVariable, ObjTupleSet>();
00064
00065 public Map<ForgeVariable, ObjTupleSet> getAssignments() {
00066 return assignments;
00067 }
00068
00069 public ISquanderResult.IEvaluator getEvaluator() {
00070 return new ISquanderResult.IEvaluator() {
00071
00072 @Override
00073 public String trace() {
00074 return assignments.toString();
00075 }
00076
00077 @Override
00078 public boolean hasSolution() {
00079 return hasSolution;
00080 }
00081
00082 @Override
00083 public String unsatCore() {
00084 return "unknown";
00085 }
00086
00087 @Override
00088 public IEvaluator nextSolution() {
00089 throw new RuntimeException("not supported");
00090 }
00091
00092 @Override
00093 public String stats() {
00094 return "unknown stats";
00095 }
00096
00097 @Override
00098 public ObjTupleSet evaluate(ForgeVariable var) {
00099 return assignments.get(var);
00100 }
00101 };
00102 }
00103
00108 public ObjTupleSet eval(ForgeExpression expr, ForgeConverter fconv) {
00109 this.fconv = fconv;
00110 this.heap2lit = fconv.heap2Lit();
00111 this.quantStack = new Stack<StackElem>();
00112 ObjTupleSet val = expr.accept(this);
00113 hasSolution = true;
00114 return val;
00115 }
00116
00117 @Override
00118 protected ObjTupleSet visit(BinaryExpression expr) {
00119 switch (expr.op()) {
00120 case AND:
00121 return visitBoolBinExpr(expr, BinFunc.AND);
00122 case OR:
00123 return visitBoolBinExpr(expr, BinFunc.OR);
00124 case XOR:
00125 return visitBoolBinExpr(expr, BinFunc.XOR);
00126 case IMPLIES:
00127 return visitBoolBinExpr(expr, BinFunc.IMPLIES);
00128 case IFF:
00129 return visitBoolBinExpr(expr, BinFunc.IFF);
00130 case EQUALS:
00131 return visitEquals(expr);
00132 case GT:
00133 return visitIntBinExpr(expr, BinFunc.GT);
00134 case GTE:
00135 return visitIntBinExpr(expr, BinFunc.GTE);
00136 case LT:
00137 return visitIntBinExpr(expr, BinFunc.LT);
00138 case LTE:
00139 return visitIntBinExpr(expr, BinFunc.LTE);
00140 case PLUS:
00141 return visitIntBinExpr(expr, BinFunc.PLUS);
00142 case MINUS:
00143 return visitIntBinExpr(expr, BinFunc.MINUS);
00144 case TIMES:
00145 return visitIntBinExpr(expr, BinFunc.TIMES);
00146 case DIVIDE:
00147 return visitIntBinExpr(expr, BinFunc.DIVIDE);
00148 case MODULO:
00149 return visitIntBinExpr(expr, BinFunc.MOD);
00150 case JOIN:
00151 return visitJoin(expr);
00152 case PRODUCT:
00153 return visitProduct(expr);
00154 case UNION:
00155 return visitRelUnion(expr);
00156 case DIFFERENCE:
00157 return visitDiff(expr);
00158 case SUBSET:
00159 return visitSubset(expr);
00160 case INTERSECTION:
00161 return visitIntersection(expr);
00162 default:
00163 throw new RuntimeException("Unsupported bin operation: " + expr.op() + " in " + expr);
00164 }
00165 }
00166
00167 @Override
00168 protected ObjTupleSet visit(ConditionalExpression expr) {
00169 ForgeExpression cond = expr.condition();
00170 ObjTupleSet condEval = cond.accept(this);
00171 if (boolValue(condEval))
00172 return expr.thenExpr().accept(this);
00173 else
00174 return expr.elseExpr().accept(this);
00175 }
00176
00177 @Override
00178 protected ObjTupleSet visit(ForgeLiteral expr) {
00179 return objAtom(fconv.lit2obj(expr));
00180 }
00181
00182 @Override
00183 protected ObjTupleSet visit(ForgeType expr) {
00184 return fconv.extent(expr);
00185 }
00186
00187 @Override
00188 protected ObjTupleSet visit(ForgeVariable expr) {
00189 if (expr instanceof LocalVariable)
00190 return visitLocalVariable((LocalVariable) expr);
00191 else
00192 return visitVariable(expr);
00193 }
00194
00195 @Override
00196 protected ObjTupleSet visit(OldExpression expr) {
00197 return visit(expr.variable());
00198 }
00199
00200 @Override
00201 protected ObjTupleSet visit(ProjectionExpression expr) {
00202
00203 throw new RuntimeException("not implemented");
00204 }
00205
00206 @Override
00207 protected ObjTupleSet visit(QuantifyExpression expr) {
00208 switch (expr.op()) {
00209 case UNION:
00210 return visitUnion(expr);
00211 case ALL:
00212 return visitAll(expr);
00213 case SOME:
00214 return visitExists(expr);
00215 default:
00216 throw new RuntimeException("Unsupported quantify expression: " + expr.op() + " in " + expr);
00217 }
00218 }
00219
00220 @Override
00221 protected ObjTupleSet visit(UnaryExpression expr) {
00222 switch (expr.op()) {
00223 case NOT: {
00224 ObjTupleSet res = expr.sub().accept(this);
00225 return boolAtom(!boolValue(res));
00226 }
00227 case SOME: {
00228 ObjTupleSet res = expr.sub().accept(this);
00229 return boolAtom(!res.isEmpty());
00230 }
00231 case NO: {
00232 ObjTupleSet res = expr.sub().accept(this);
00233 return boolAtom(res.isEmpty());
00234 }
00235 case LONE: {
00236 ObjTupleSet res = expr.sub().accept(this);
00237 return boolAtom(res.isEmpty() || res.isTuple());
00238 }
00239 case ONE: {
00240 ObjTupleSet res = expr.sub().accept(this);
00241 return boolAtom(res.isTuple());
00242 }
00243 case CLOSURE: {
00244 ObjTupleSet res = expr.sub().accept(this);
00245 return visitClosure(res);
00246
00247
00248 }
00249 default: {
00250 throw new RuntimeException("Unsupported unary operation: " + expr.op() + " in " + expr);
00251 }
00252 }
00253 }
00254
00255
00256
00257 private ObjTupleSet visitVariable(ForgeVariable var) {
00258 ObjTupleSet b = heap2lit.getBound(var);
00259 assert b != null : "bound not specified for variable " + var;
00260 return b;
00261 }
00262
00263 private ObjTupleSet visitLocalVariable(LocalVariable var) {
00264 StackElem elem = searchStack(var);
00265 if (elem != null)
00266 return new ObjTupleSet(elem.val);
00267 else
00268 return visitVariable(var);
00269 }
00270
00271 private StackElem searchStack(LocalVariable var) {
00272 for (int i = quantStack.size() - 1; i >= 0; i--) {
00273 StackElem elem = quantStack.get(i);
00274 if (elem.var.equals(var))
00275 return elem;
00276 }
00277 return null;
00278 }
00279
00280 @SuppressWarnings("unused")
00281 private ObjTupleSet visitAssignment(BinaryExpression expr) {
00282 ForgeExpression lhs = expr.left();
00283 assert lhs instanceof ForgeVariable : "lhs of an assignment expression must be ForgeVariable;";
00284 ObjTupleSet val = expr.right().accept(this);
00285 assignments.put((ForgeVariable)lhs, val);
00286 return boolAtom(true);
00287 }
00288
00289 private ObjTupleSet visitEquals(BinaryExpression expr) {
00290
00291 ObjTupleSet lhsVal = expr.left().accept(this);
00292 ObjTupleSet rhsVal = expr.right().accept(this);
00293 return boolAtom(lhsVal.equals(rhsVal));
00294 }
00295
00296 private ObjTupleSet visitJoin(BinaryExpression expr) {
00297 ObjTupleSet lhs = expr.left().accept(this);
00298 ObjTupleSet rhs = expr.right().accept(this);
00299 return lhs.join(rhs);
00300 }
00301
00302 private ObjTupleSet visitProduct(BinaryExpression expr) {
00303 ObjTupleSet lhs = expr.left().accept(this);
00304 ObjTupleSet rhs = expr.right().accept(this);
00305 return lhs.product(rhs);
00306 }
00307
00308 private ObjTupleSet visitRelUnion(BinaryExpression expr) {
00309 ObjTupleSet lhs = expr.left().accept(this);
00310 ObjTupleSet rhs = expr.right().accept(this);
00311 return lhs.union(rhs);
00312 }
00313
00314 private ObjTupleSet visitDiff(BinaryExpression expr) {
00315 ObjTupleSet lhs = expr.left().accept(this);
00316 ObjTupleSet rhs = expr.right().accept(this);
00317 return lhs.diff(rhs);
00318 }
00319
00320
00321 private ObjTupleSet visitSubset(BinaryExpression expr) {
00322 ObjTupleSet lhs = expr.left().accept(this);
00323 ObjTupleSet rhs = expr.right().accept(this);
00324 return boolAtom(lhs.subsetOf(rhs));
00325 }
00326
00327 private ObjTupleSet visitIntersection(BinaryExpression expr) {
00328 ObjTupleSet lhs = expr.left().accept(this);
00329 ObjTupleSet rhs = expr.right().accept(this);
00330 return lhs.intersection(rhs);
00331 }
00332
00333 private ObjTupleSet visitClosure(ObjTupleSet res) {
00334 assert res.arity() == 2 : "Closure is allowed only on binary relations: " + res;
00335 ObjTupleSet ret = res;
00336 boolean changed;
00337 do {
00338 int size = ret.tuples().size();
00339 for (ObjTuple t : ret.tuples()) {
00340 ret = ret.union(new ObjTupleSet(t).join(ret));
00341 }
00342 changed = ret.tuples().size() != size;
00343 } while (changed);
00344 return ret;
00345 }
00346
00347 private ObjTupleSet visitBoolBinExpr(BinaryExpression expr, BinFunc<Boolean, Boolean> f) {
00348 assert expr.left().type().getClass() == BooleanDomain.class;
00349 assert expr.right().type().getClass() == BooleanDomain.class;
00350 ObjTupleSet lhs = expr.left().accept(this);
00351 ObjTupleSet rhs = expr.right().accept(this);
00352 Boolean b1 = boolValue(lhs);
00353 Boolean b2 = boolValue(rhs);
00354 boolean b = f.exe(b1, b2);
00355 return boolAtom(b);
00356 }
00357
00358 private <R> ObjTupleSet visitIntBinExpr(BinaryExpression expr, BinFunc<R, Integer> f) {
00359 assert expr.left().type().getClass() == IntegerDomain.class;
00360 assert expr.right().type().getClass() == IntegerDomain.class;
00361 ObjTupleSet lhs = expr.left().accept(this);
00362 ObjTupleSet rhs = expr.right().accept(this);
00363 Integer b1 = intValue(lhs);
00364 Integer b2 = intValue(rhs);
00365 R ret = f.exe(b1, b2);
00366 if (ret instanceof Integer)
00367 return intAtom((Integer) ret);
00368 else if (ret instanceof Boolean)
00369 return boolAtom((Boolean) ret);
00370 else
00371 throw new RuntimeException();
00372 }
00373
00374 private static class StackElem {
00375 LocalVariable var;
00376 ObjTuple val;
00377
00378 StackElem(LocalVariable var, ObjTuple val) {
00379 this.var = var;
00380 this.val = val;
00381 }
00382 }
00383
00384 private ObjTupleSet visitUnion(QuantifyExpression expr) {
00385 UniqueList<LocalVariable> locals = expr.decls().locals();
00386 assert locals.size() == 1 : "don't know how to handle UNION with more than 1 local var: " + expr;
00387 LocalVariable var = locals.get(0);
00388 ObjTupleSet dom = fconv.extent(var.type());
00389 ObjTupleSet result = new ObjTupleSet(dom.arity());
00390 for (ObjTuple val : dom.tuples()) {
00391 quantStack.push(new StackElem(var, val));
00392 ObjTupleSet sub = expr.sub().accept(this);
00393 if (boolValue(sub)) {
00394 result = result.union(val);
00395 }
00396 quantStack.pop();
00397 }
00398 return result;
00399 }
00400
00401 private ObjTupleSet visitAll(QuantifyExpression expr) {
00402 UniqueList<LocalVariable> locals = expr.decls().locals();
00403 assert locals.size() == 1 : "don't know how to handle ALL with more than 1 local var: " + expr;
00404 LocalVariable var = locals.get(0);
00405 ObjTupleSet dom = fconv.extent(var.type());
00406 for (ObjTuple val : dom.tuples()) {
00407 quantStack.push(new StackElem(var, val));
00408 ObjTupleSet sub = expr.sub().accept(this);
00409 quantStack.pop();
00410 if (!boolValue(sub))
00411 return boolAtom(false);
00412 }
00413 return boolAtom(true);
00414 }
00415
00416 private ObjTupleSet visitExists(QuantifyExpression expr) {
00417 UniqueList<LocalVariable> locals = expr.decls().locals();
00418 assert locals.size() == 1 : "don't know how to handle SOME with more than 1 local var: " + expr;
00419 LocalVariable var = locals.get(0);
00420 ObjTupleSet dom = fconv.extent(var.type());
00421 for (ObjTuple val : dom.tuples()) {
00422 quantStack.push(new StackElem(var, val));
00423 ObjTupleSet sub = expr.sub().accept(this);
00424 quantStack.pop();
00425 if (boolValue(sub))
00426 return boolAtom(true);
00427 }
00428 return boolAtom(false);
00429 }
00430
00431 private static ObjTupleSet boolAtom(boolean val) {
00432 ObjTupleSet ots = new ObjTupleSet(1);
00433 ots.add(new ObjTuple(val));
00434 return ots;
00435 }
00436
00437 private static ObjTupleSet intAtom(int val) {
00438 ObjTupleSet ots = new ObjTupleSet(1);
00439 ots.add(new ObjTuple(val));
00440 return ots;
00441 }
00442
00443 private static ObjTupleSet objAtom(Object obj) {
00444 ObjTupleSet ots = new ObjTupleSet(1);
00445 ots.add(new ObjTuple(obj));
00446 return ots;
00447 }
00448
00449 private static boolean boolValue(ObjTupleSet condEval) {
00450 if (condEval.isEmpty())
00451 return false;
00452 assert condEval.arity() == 1;
00453 assert condEval.tuples().size() == 1;
00454 return (Boolean) condEval.tuples().iterator().next().get(0);
00455 }
00456
00457 private static int intValue(ObjTupleSet condEval) {
00458 assert condEval.arity() == 1;
00459 assert condEval.tuples().size() == 1;
00460 return (Integer) condEval.tuples().iterator().next().get(0);
00461 }
00462
00463 }