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