00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.util.Stack;
00008
00009 import edu.mit.csail.sdg.squander.utils.Utils;
00010 import edu.mit.csail.sdg.util.collections.UniqueList;
00011 import forge.program.BinaryExpression;
00012 import forge.program.BooleanDomain;
00013 import forge.program.ConditionalExpression;
00014 import forge.program.ExpressionVisitor;
00015 import forge.program.ForgeExpression;
00016 import forge.program.ForgeVariable;
00017 import forge.program.GlobalVariable;
00018 import forge.program.IntegerDomain;
00019 import forge.program.LocalVariable;
00020 import forge.program.ProjectionExpression;
00021 import forge.program.QuantifyExpression;
00022 import forge.program.UnaryExpression;
00023 import forge.solve.ForgeBounds;
00024 import forge.solve.ForgeConstant;
00025 import forge.solve.ForgeConstant.Tuple;
00026
00027 public abstract class MyExprEvaluator extends ExpressionVisitor<ForgeConstant> {
00028
00029 protected static interface BinFunc<R, T> {
00030 public static BinFunc<Boolean, Boolean> AND = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 && b2; }};
00031 public static BinFunc<Boolean, Boolean> OR = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 || b2; }};
00032 public static BinFunc<Boolean, Boolean> XOR = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 != b2; }};
00033 public static BinFunc<Boolean, Boolean> IFF = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 == b2; }};
00034 public static BinFunc<Boolean, Boolean> IMPLIES = new BinFunc<Boolean, Boolean>() { public Boolean exe(Boolean b1, Boolean b2) { return b1 || !b2; }};
00035
00036 public static BinFunc<Boolean, Integer> GT = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 > b2; }};
00037 public static BinFunc<Boolean, Integer> GTE = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 >= b2; }};
00038 public static BinFunc<Boolean, Integer> LT = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 < b2; }};
00039 public static BinFunc<Boolean, Integer> LTE = new BinFunc<Boolean, Integer>() { public Boolean exe(Integer b1, Integer b2) { return b1 <= b2; }};
00040
00041 public static BinFunc<Integer, Integer> PLUS = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 + b2; }};
00042 public static BinFunc<Integer, Integer> MINUS = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 - b2; }};
00043 public static BinFunc<Integer, Integer> TIMES = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 * b2; }};
00044 public static BinFunc<Integer, Integer> DIVIDE = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 / b2; }};
00045 public static BinFunc<Integer, Integer> MOD = new BinFunc<Integer, Integer>() { public Integer exe(Integer b1, Integer b2) { return b1 % b2; }};
00046
00047 public R exe(T b1, T b2);
00048 }
00049
00050 protected static class StackElem {
00051 LocalVariable var;
00052 ForgeConstant val;
00053
00054 StackElem(LocalVariable var, ForgeConstant val) {
00055 this.var = var;
00056 this.val = val;
00057 }
00058 }
00059
00060 protected ForgeBounds bounds;
00061 protected final Stack<StackElem> quantStack = new Stack<StackElem>();
00062
00063 public MyExprEvaluator(ForgeBounds bounds) {
00064 this.bounds = bounds;
00065 }
00066
00067 @Override
00068 protected ForgeConstant visit(BinaryExpression expr) {
00069 switch (expr.op()) {
00070 case AND:
00071 return visitBoolBinExpr(expr, BinFunc.AND);
00072 case OR:
00073 return visitBoolBinExpr(expr, BinFunc.OR);
00074 case XOR:
00075 return visitBoolBinExpr(expr, BinFunc.XOR);
00076 case IMPLIES:
00077 return visitBoolBinExpr(expr, BinFunc.IMPLIES);
00078 case IFF:
00079 return visitBoolBinExpr(expr, BinFunc.IFF);
00080 case EQUALS:
00081 return visitEquals(expr);
00082 case GT:
00083 return visitIntBinExpr(expr, BinFunc.GT);
00084 case GTE:
00085 return visitIntBinExpr(expr, BinFunc.GTE);
00086 case LT:
00087 return visitIntBinExpr(expr, BinFunc.LT);
00088 case LTE:
00089 return visitIntBinExpr(expr, BinFunc.LTE);
00090 case PLUS:
00091 return visitIntBinExpr(expr, BinFunc.PLUS);
00092 case MINUS:
00093 return visitIntBinExpr(expr, BinFunc.MINUS);
00094 case TIMES:
00095 return visitIntBinExpr(expr, BinFunc.TIMES);
00096 case DIVIDE:
00097 return visitIntBinExpr(expr, BinFunc.DIVIDE);
00098 case MODULO:
00099 return visitIntBinExpr(expr, BinFunc.MOD);
00100 case JOIN:
00101 return visitJoin(expr);
00102 case PRODUCT:
00103 return visitProduct(expr);
00104 case UNION:
00105 return visitRelUnion(expr);
00106 case DIFFERENCE:
00107 return visitDiff(expr);
00108 case SUBSET:
00109 return visitSubset(expr);
00110 default:
00111 throw new RuntimeException("Unsupported bin operation: " + expr.op() + " in " + expr);
00112 }
00113 }
00114
00115 @Override
00116 protected ForgeConstant visit(ConditionalExpression expr) {
00117 ForgeExpression cond = expr.condition();
00118 ForgeConstant condEval = cond.accept(this);
00119 if (Utils.boolValue(condEval))
00120 return expr.thenExpr().accept(this);
00121 else
00122 return expr.elseExpr().accept(this);
00123 }
00124
00125 @Override
00126 protected ForgeConstant visit(ForgeVariable expr) {
00127 if (expr instanceof LocalVariable)
00128 return visitLocalVariable((LocalVariable) expr);
00129 else
00130 return visitGlobalVariable((GlobalVariable) expr);
00131 }
00132
00133 @Override
00134 protected ForgeConstant visit(ProjectionExpression expr) {
00135
00136 throw new RuntimeException("not implemented");
00137 }
00138
00139 @Override
00140 protected ForgeConstant visit(QuantifyExpression expr) {
00141 switch (expr.op()) {
00142 case UNION:
00143 return visitUnion(expr);
00144 case ALL:
00145 return visitAll(expr);
00146 case SOME:
00147 return visitExists(expr);
00148 default:
00149 throw new RuntimeException("Unsupported quantify expression: " + expr.op() + " in " + expr);
00150 }
00151 }
00152
00153 @Override
00154 protected ForgeConstant visit(UnaryExpression expr) {
00155 switch (expr.op()) {
00156 case NOT: {
00157 ForgeConstant res = expr.sub().accept(this);
00158 return bounds.boolAtom(!Utils.boolValue(res));
00159 }
00160 case SOME: {
00161 ForgeConstant res = expr.sub().accept(this);
00162 return bounds.boolAtom(!res.isEmpty());
00163 }
00164 case NO: {
00165 ForgeConstant res = expr.sub().accept(this);
00166 return bounds.boolAtom(res.isEmpty());
00167 }
00168 case LONE: {
00169 ForgeConstant res = expr.sub().accept(this);
00170 return bounds.boolAtom(res.isEmpty() || res.isTuple());
00171 }
00172 case ONE: {
00173 ForgeConstant res = expr.sub().accept(this);
00174 return bounds.boolAtom(res.isTuple());
00175 }
00176 case CLOSURE: {
00177 ForgeConstant res = expr.sub().accept(this);
00178 return visitClosure(res);
00179
00180
00181 }
00182 default: {
00183 throw new RuntimeException("Unsupported unary operation: " + expr.op() + " in " + expr);
00184 }
00185 }
00186 }
00187
00188
00189
00190 protected abstract ForgeConstant visitGlobalVariable(GlobalVariable var);
00191 protected abstract ForgeConstant visitLocalVariable(LocalVariable var);
00192
00193 protected StackElem searchStack(LocalVariable var) {
00194 for (int i = quantStack.size() - 1; i >= 0; i--) {
00195 StackElem elem = quantStack.get(i);
00196 if (elem.var.equals(var))
00197 return elem;
00198 }
00199 return null;
00200 }
00201
00202 private ForgeConstant visitEquals(BinaryExpression expr) {
00203 ForgeConstant lhs = expr.left().accept(this);
00204 ForgeConstant rhs = expr.right().accept(this);
00205 return bounds.boolAtom(lhs.equals(rhs));
00206 }
00207
00208 private ForgeConstant visitJoin(BinaryExpression expr) {
00209 ForgeConstant lhs = expr.left().accept(this);
00210 ForgeConstant rhs = expr.right().accept(this);
00211 return lhs.join(rhs);
00212 }
00213
00214 private ForgeConstant visitProduct(BinaryExpression expr) {
00215 ForgeConstant lhs = expr.left().accept(this);
00216 ForgeConstant rhs = expr.right().accept(this);
00217 return lhs.product(rhs);
00218 }
00219
00220 private ForgeConstant visitRelUnion(BinaryExpression expr) {
00221 ForgeConstant lhs = expr.left().accept(this);
00222 ForgeConstant rhs = expr.right().accept(this);
00223 return lhs.union(rhs);
00224 }
00225
00226 private ForgeConstant visitDiff(BinaryExpression expr) {
00227 ForgeConstant lhs = expr.left().accept(this);
00228 ForgeConstant rhs = expr.right().accept(this);
00229 return lhs.difference(rhs);
00230 }
00231
00232
00233 private ForgeConstant visitSubset(BinaryExpression expr) {
00234 ForgeConstant lhs = expr.left().accept(this);
00235 ForgeConstant rhs = expr.right().accept(this);
00236 return bounds.boolAtom(lhs.subsetOf(rhs));
00237 }
00238
00239 private ForgeConstant visitClosure(ForgeConstant res) {
00240 assert res.arity() == 2 : "Closure is allowed only on binary relations: " + res;
00241 ForgeConstant ret = res;
00242 boolean changed;
00243 do {
00244 int size = ret.tuples().size();
00245 for (Tuple t : ret.tuples()) {
00246 ret = ret.union(t.join(ret));
00247 }
00248 changed = ret.tuples().size() != size;
00249 } while (changed);
00250 return ret;
00251 }
00252
00253 private ForgeConstant visitBoolBinExpr(BinaryExpression expr, BinFunc<Boolean, Boolean> f) {
00254 assert expr.left().type().getClass() == BooleanDomain.class;
00255 assert expr.right().type().getClass() == BooleanDomain.class;
00256 ForgeConstant lhs = expr.left().accept(this);
00257 ForgeConstant rhs = expr.right().accept(this);
00258 Boolean b1 = Utils.boolValue(lhs);
00259 Boolean b2 = Utils.boolValue(rhs);
00260 boolean b = f.exe(b1, b2);
00261 return bounds.boolAtom(b);
00262 }
00263
00264 private <R> ForgeConstant visitIntBinExpr(BinaryExpression expr, BinFunc<R, Integer> f) {
00265 assert expr.left().type().getClass() == IntegerDomain.class;
00266 assert expr.right().type().getClass() == IntegerDomain.class;
00267 ForgeConstant lhs = expr.left().accept(this);
00268 ForgeConstant rhs = expr.right().accept(this);
00269 Integer b1 = Utils.intValue(lhs);
00270 Integer b2 = Utils.intValue(rhs);
00271 R ret = f.exe(b1, b2);
00272 if (ret instanceof Integer)
00273 return bounds.intAtom((Integer) ret);
00274 else if (ret instanceof Boolean)
00275 return bounds.boolAtom((Boolean) ret);
00276 else
00277 throw new RuntimeException();
00278 }
00279
00280 private ForgeConstant visitUnion(QuantifyExpression expr) {
00281 UniqueList<LocalVariable> locals = expr.decls().locals();
00282 assert locals.size() == 1 : "don't know how to handle UNION with more than 1 local var: " + expr;
00283 LocalVariable var = locals.get(0);
00284 ForgeConstant dom = bounds.extent(var.type());
00285 ForgeConstant result = bounds.empty(dom.arity());
00286 for (Tuple val : dom.tuples()) {
00287 quantStack.push(new StackElem(var, val));
00288 ForgeConstant sub = expr.sub().accept(this);
00289 if (Utils.boolValue(sub)) {
00290 result = result.union(val);
00291 }
00292 quantStack.pop();
00293 }
00294 return result;
00295 }
00296
00297 private ForgeConstant visitAll(QuantifyExpression expr) {
00298 UniqueList<LocalVariable> locals = expr.decls().locals();
00299 assert locals.size() == 1 : "don't know how to handle ALL with more than 1 local var: " + expr;
00300 LocalVariable var = locals.get(0);
00301 ForgeConstant dom = bounds.extent(var.type());
00302 for (Tuple val : dom.tuples()) {
00303 quantStack.push(new StackElem(var, val));
00304 ForgeConstant sub = expr.sub().accept(this);
00305 quantStack.pop();
00306 if (!Utils.boolValue(sub))
00307 return bounds.boolAtom(false);
00308 }
00309 return bounds.boolAtom(true);
00310 }
00311
00312 private ForgeConstant visitExists(QuantifyExpression expr) {
00313 UniqueList<LocalVariable> locals = expr.decls().locals();
00314 assert locals.size() == 1 : "don't know how to handle SOME with more than 1 local var: " + expr;
00315 LocalVariable var = locals.get(0);
00316 ForgeConstant dom = bounds.extent(var.type());
00317 for (Tuple val : dom.tuples()) {
00318 quantStack.push(new StackElem(var, val));
00319 ForgeConstant sub = expr.sub().accept(this);
00320 quantStack.pop();
00321 if (Utils.boolValue(sub))
00322 return bounds.boolAtom(true);
00323 }
00324 return bounds.boolAtom(false);
00325 }
00326
00327 }