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.Stack;
00020 import java.util.Map.Entry;
00021
00022 import kodkod.ast.Decl;
00023 import kodkod.ast.Decls;
00024 import kodkod.ast.ExprToIntCast;
00025 import kodkod.ast.Expression;
00026 import kodkod.ast.Formula;
00027 import kodkod.ast.IfExpression;
00028 import kodkod.ast.IntConstant;
00029 import kodkod.ast.IntExpression;
00030 import kodkod.ast.IntToExprCast;
00031 import kodkod.ast.Node;
00032 import kodkod.ast.Relation;
00033 import kodkod.ast.Variable;
00034 import kodkod.engine.Evaluator;
00035 import kodkod.engine.Proof;
00036 import kodkod.engine.Solution;
00037 import kodkod.engine.Solver;
00038 import kodkod.engine.satlab.ReductionStrategy;
00039 import kodkod.engine.satlab.SATFactory;
00040 import kodkod.engine.ucore.AdaptiveRCEStrategy;
00041 import kodkod.instance.Bounds;
00042 import kodkod.instance.TupleFactory;
00043 import kodkod.instance.TupleSet;
00044 import kodkod.instance.Universe;
00045 import kodkod.util.nodes.PrettyPrinter;
00046 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00047 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00048 import edu.mit.csail.sdg.squander.annotations.Options;
00049 import edu.mit.csail.sdg.squander.engine.ForgeConverter;
00050 import edu.mit.csail.sdg.squander.engine.ISquander;
00051 import edu.mit.csail.sdg.squander.engine.SquanderEval2;
00052 import edu.mit.csail.sdg.squander.engine.SquanderImpl;
00053 import edu.mit.csail.sdg.squander.engine.ISquanderResult.IEvaluator;
00054 import edu.mit.csail.sdg.squander.log.Log;
00055 import edu.mit.csail.sdg.squander.options.GlobalOptions;
00056 import edu.mit.csail.sdg.squander.spec.ForgeScene;
00057 import edu.mit.csail.sdg.squander.spec.Tr;
00058 import edu.mit.csail.sdg.squander.spec.Spec.SpecCase;
00059 import forge.program.BinaryExpression;
00060 import forge.program.BooleanLiteral;
00061 import forge.program.ConditionalExpression;
00062 import forge.program.ExpressionVisitor;
00063 import forge.program.ForgeExpression;
00064 import forge.program.ForgeLiteral;
00065 import forge.program.ForgeProgram;
00066 import forge.program.ForgeType;
00067 import forge.program.ForgeVariable;
00068 import forge.program.GlobalVariable;
00069 import forge.program.InstanceDomain;
00070 import forge.program.InstanceLiteral;
00071 import forge.program.IntegerDomain;
00072 import forge.program.IntegerLiteral;
00073 import forge.program.LocalDecls;
00074 import forge.program.LocalVariable;
00075 import forge.program.OldExpression;
00076 import forge.program.ProjectionExpression;
00077 import forge.program.QuantifyExpression;
00078 import forge.program.UnaryExpression;
00079 import forge.program.ForgeType.Tuple;
00080 import forge.program.ForgeType.Unary;
00081 import forge.program.QuantifyExpression.Op;
00082 import forge.solve.ForgeAtom;
00083 import forge.solve.ForgeBounds;
00084 import forge.solve.ForgeConstant;
00085 import forge.solve.IntegerAtom;
00086 import forge.transform.ExpressionDescender;
00087
00094 public class SquanderKodkodImpl extends SquanderImpl {
00095
00096
00097
00098
00099
00100 static class DiscoverHigherOrderQuant extends ExpressionDescender {
00101 static final DiscoverHigherOrderQuant instance = new DiscoverHigherOrderQuant();
00102
00103 boolean higherOrderFound = false;
00104
00105 @Override
00106 protected void descend(QuantifyExpression expr) {
00107 List<String> declMults = Tr.absolutelyTerribleHack.get(expr.decls());
00108 if (declMults == null) {
00109 super.descend(expr);
00110 return;
00111 }
00112 for (String mult : declMults) {
00113 if ("DECL_SET".equals(mult)) {
00114 higherOrderFound = true;
00115 return;
00116 }
00117 }
00118 super.descend(expr);
00119 }
00120
00121 }
00122
00123
00124
00125
00126
00127
00132 class KodkodEval implements IEvaluator {
00133
00134 protected final Iterator<Solution> solutions;
00135 protected Solution solution;
00136
00137 public KodkodEval(Iterator<Solution> solutions) {
00138 this.solutions = solutions;
00139 this.solution = solutions.next();
00140 }
00141
00142 @Override
00143 public String unsatCore() {
00144 Proof proof = solution.proof();
00145 if (proof == null)
00146 return "unknown";
00147 ReductionStrategy strategy = new AdaptiveRCEStrategy(proof.log());
00148 proof.minimize(strategy);
00149 int minCore = proof.highLevelCore().size();
00150 StringBuilder sb = new StringBuilder();
00151 sb.append("Core (size="+minCore+"):\n");
00152 for(Node n : proof.highLevelCore().values()) {
00153 sb.append(PrettyPrinter.print(n, 0)).append("\n");
00154 }
00155 return sb.toString();
00156 }
00157
00158 @Override
00159 public ObjTupleSet evaluate(ForgeVariable var) {
00160 return evaluateExpr(var);
00161 }
00162
00163 public ObjTupleSet evaluateExpr(ForgeExpression expr) {
00164 Evaluator eval = new Evaluator(solution.instance());
00165 Tr2KK tr = new Tr2KK();
00166 Node n = expr.accept(tr);
00167 if (n instanceof Formula) {
00168 boolean res = eval.evaluate((Formula)n);
00169 return ObjTupleSet.singleTuple(res);
00170 } else if (n instanceof Expression) {
00171 TupleSet ts = eval.evaluate((Expression) n);
00172 return makeConst(ts);
00173 } else if (n instanceof IntExpression) {
00174 int res = eval.evaluate((IntExpression) n);
00175 return ObjTupleSet.singleTuple(res);
00176 }
00177 throw new RuntimeException("unknown expression");
00178 }
00179
00180 protected ObjTupleSet makeConst(TupleSet ts) {
00181 ObjTupleSet res = new ObjTupleSet(ts.arity());
00182 for (kodkod.instance.Tuple t : ts) {
00183 ObjTuple fTuple = new ObjTuple();
00184 for (int i = 0; i < t.arity(); i++) {
00185 Object obj = t.atom(i);
00186 Object fAtom;
00187 if (obj instanceof Integer)
00188 fAtom = obj;
00189 else if (obj instanceof Boolean)
00190 fAtom = obj;
00191 else if ("true".equals(obj))
00192 fAtom = true;
00193 else if ("false".equals(obj))
00194 fAtom = false;
00195 else
00196 fAtom = forgeScene.objForLit(obj.toString());
00197 fTuple = ObjTuple.product(fTuple, fAtom);
00198 }
00199 if (fTuple.arity() != 0)
00200 res.add(fTuple);
00201 }
00202 return res;
00203 }
00204
00205 @Override
00206 public boolean hasSolution() {
00207 return solution != null && solution.instance() != null;
00208 }
00209
00210 @Override
00211 public IEvaluator nextSolution() {
00212 if (solutions.hasNext()) {
00213 solution = solutions.next();
00214 } else {
00215 solution = null;
00216 }
00217 return this;
00218 }
00219
00220 @Override
00221 public String trace() {
00222 return solution.toString();
00223 }
00224
00225 @Override
00226 public String stats() {
00227 return solution.stats().toString();
00228 }
00229
00230 }
00231
00232
00233
00234
00235
00239 class Tr2KK extends ExpressionVisitor<Node> {
00240
00241 private class StackElem {
00242 final String name;
00243 final Expression var;
00244
00245 StackElem(String name, Expression var) {
00246 this.name = name;
00247 this.var = var;
00248 }
00249 }
00250
00251 private final Stack<StackElem> quantStack = new Stack<StackElem>();
00252
00253 @Override
00254 protected Expression visit(ForgeType ftype) {
00255 Expression expr = type2expr.get(ftype);
00256 if (expr == null) {
00257 expr = visitForgeType(ftype);
00258 type2expr.put(ftype, expr);
00259 }
00260 return expr;
00261 }
00262
00263 private Expression visitForgeType(ForgeType ftype) {
00264 Expression expr = null;
00265 for (Tuple t : ftype.tupleTypes()) {
00266 Expression tt = null;
00267 for (int i = 0; i < t.arity(); i++) {
00268 Expression projType = type2expr.get(t.projectType(i));
00269 if (projType == null)
00270 projType = Expression.NONE;
00271 if (tt == null)
00272 tt = projType;
00273 else
00274 tt = tt.product(projType);
00275 }
00276 if (expr == null)
00277 expr = tt;
00278 else
00279 expr = expr.union(tt);
00280 }
00281 return expr;
00282 }
00283
00284 @Override
00285 protected Node visit(ForgeLiteral lit) {
00286 if (lit instanceof IntegerLiteral) {
00287 int val = ((IntegerLiteral) lit).value();
00288 return IntConstant.constant(val);
00289 }
00290 return lit2rel.get(lit.name());
00291 }
00292
00293 @Override
00294 protected Expression visit(ForgeVariable var) {
00295 if (var.isGlobal()) {
00296 return getRelForVarAndCheck(var);
00297 } else {
00298 StackElem elem = searchStack(var.name());
00299 if (elem != null)
00300 return elem.var;
00301 else {
00302
00303 return getRelForVarAndCheck(var);
00304 }
00305 }
00306 }
00307
00308 @Override
00309 protected Node visit(UnaryExpression expr) {
00310 switch (expr.op()) {
00311 case NOT: {
00312 Formula sub = node2form(expr.sub().accept(this));
00313 return sub.not();
00314 }
00315 case SOME: {
00316 Expression sub = node2expr(expr.sub().accept(this));
00317 return sub.some();
00318 }
00319 case NO: {
00320 Expression sub = node2expr(expr.sub().accept(this));
00321 return sub.no();
00322 }
00323 case LONE: {
00324 Expression sub = node2expr(expr.sub().accept(this));
00325 return sub.lone();
00326 }
00327 case ONE: {
00328 Expression sub = node2expr(expr.sub().accept(this));
00329 return sub.one();
00330 }
00331 case CLOSURE: {
00332 Expression sub = node2expr(expr.sub().accept(this));
00333 return sub.closure();
00334 }
00335 case NEG: {
00336 Node subNode = expr.sub().accept(this);
00337 return node2int(subNode).negate();
00338 }
00339 case CARDINALITY: {
00340 Node subNode = expr.sub().accept(this);
00341 return node2expr(subNode).count();
00342 }
00343 case BIT_NOT: {
00344 Node subNode = expr.sub().accept(this);
00345 return node2int(subNode).not();
00346 }
00347 case SUM: {
00348 Node sumNode = expr.sub().accept(this);
00349 Variable v = Variable.unary("k");
00350 return node2int(v).sum(v.oneOf(node2expr(sumNode)));
00351 }
00352 default: {
00353 throw new RuntimeException("Unsupported unary operation: " + expr.op() + " in "
00354 + expr);
00355 }
00356 }
00357 }
00358
00359 @Override
00360 protected Node visit(BinaryExpression expr) {
00361 switch (expr.op()) {
00362 case AND: {
00363 Formula lhs = node2form(expr.left().accept(this));
00364 Formula rhs = node2form(expr.right().accept(this));
00365 return lhs.and(rhs);
00366 } case OR: {
00367 Formula lhs = node2form(expr.left().accept(this));
00368 Formula rhs = node2form(expr.right().accept(this));
00369 return lhs.or(rhs);
00370 } case XOR: {
00371 Formula lhs = node2form(expr.left().accept(this));
00372 Formula rhs = node2form(expr.right().accept(this));
00373 return lhs.and(rhs.not()).or(lhs.not().and(rhs));
00374 } case IMPLIES: {
00375 Formula lhs = node2form(expr.left().accept(this));
00376 Formula rhs = node2form(expr.right().accept(this));
00377 return lhs.implies(rhs);
00378 } case IFF: {
00379 Formula lhs = node2form(expr.left().accept(this));
00380 Formula rhs = node2form(expr.right().accept(this));
00381 return lhs.iff(rhs);
00382 } case EQUALS: {
00383 Node leftNode = expr.left().accept(this);
00384 Node rightNode = expr.right().accept(this);
00385 if ((leftNode instanceof IntExpression) && (rightNode instanceof IntExpression)) {
00386 IntExpression lhs = (IntExpression) leftNode;
00387 IntExpression rhs = (IntExpression) rightNode;
00388 return lhs.eq(rhs);
00389 }
00390 Expression lhs = node2expr(leftNode);
00391 Expression rhs = node2expr(rightNode);
00392 return lhs.eq(rhs);
00393 } case GT: {
00394 Node lhs = expr.left().accept(this);
00395 Node rhs = expr.right().accept(this);
00396 return node2int(lhs).gt(node2int(rhs));
00397 } case GTE: {
00398 Node lhs = expr.left().accept(this);
00399 Node rhs = expr.right().accept(this);
00400 return node2int(lhs).gte(node2int(rhs));
00401 } case LT: {
00402 Node lhs = expr.left().accept(this);
00403 Node rhs = expr.right().accept(this);
00404 return node2int(lhs).lt(node2int(rhs));
00405 } case LTE: {
00406 Node lhs = expr.left().accept(this);
00407 Node rhs = expr.right().accept(this);
00408 return node2int(lhs).lte(node2int(rhs));
00409 } case PLUS: {
00410 Node lhs = expr.left().accept(this);
00411 Node rhs = expr.right().accept(this);
00412 return node2int(lhs).plus(node2int(rhs));
00413 } case MINUS: {
00414 Node lhs = expr.left().accept(this);
00415 Node rhs = expr.right().accept(this);
00416 return node2int(lhs).minus(node2int(rhs));
00417 } case TIMES: {
00418 Node lhs = expr.left().accept(this);
00419 Node rhs = expr.right().accept(this);
00420 return node2int(lhs).multiply(node2int(rhs));
00421 } case DIVIDE: {
00422 Node lhs = expr.left().accept(this);
00423 Node rhs = expr.right().accept(this);
00424 return node2int(lhs).divide(node2int(rhs));
00425 } case MODULO: {
00426 Node lhs = expr.left().accept(this);
00427 Node rhs = expr.right().accept(this);
00428 return node2int(lhs).modulo(node2int(rhs));
00429 } case JOIN: {
00430 Expression lhs = node2expr(expr.left().accept(this));
00431 Expression rhs = node2expr(expr.right().accept(this));
00432 return lhs.join(rhs);
00433 } case PRODUCT: {
00434 Expression lhs = node2expr(expr.left().accept(this));
00435 Expression rhs = node2expr(expr.right().accept(this));
00436 return lhs.product(rhs);
00437 } case UNION: {
00438 Expression lhs = node2expr(expr.left().accept(this));
00439 Expression rhs = node2expr(expr.right().accept(this));
00440 return lhs.union(rhs);
00441 } case DIFFERENCE: {
00442 Expression lhs = node2expr(expr.left().accept(this));
00443 Expression rhs = node2expr(expr.right().accept(this));
00444 return lhs.difference(rhs);
00445 } case SUBSET: {
00446 Expression lhs = node2expr(expr.left().accept(this));
00447 Expression rhs = node2expr(expr.right().accept(this));
00448 return lhs.in(rhs);
00449 } case OVERRIDE: {
00450 Expression lhs = node2expr(expr.left().accept(this));
00451 Expression rhs = node2expr(expr.right().accept(this));
00452 return lhs.override(rhs);
00453 } case INTERSECTION: {
00454 Expression lhs = node2expr(expr.left().accept(this));
00455 Expression rhs = node2expr(expr.right().accept(this));
00456 return lhs.intersection(rhs);
00457 } default:
00458 throw new RuntimeException("Unsupported bin operation: " + expr.op() + " in " + expr);
00459 }
00460 }
00461
00462 @Override
00463 protected Node visit(ConditionalExpression expr) {
00464 Formula cond = node2form(expr.condition().accept(this));
00465 Node thenNode = expr.thenExpr().accept(this);
00466 Node elseNode = expr.elseExpr().accept(this);
00467 return cond.thenElse(node2expr(thenNode), node2expr(elseNode));
00468 }
00469
00470 @Override
00471 protected Node visit(ProjectionExpression expr) {
00472 Node sub = expr.sub().accept(this);
00473 IntExpression[] cols = new IntExpression[expr.columns().size()];
00474 int idx = 0;
00475 for (int col : expr.columns()) {
00476 cols[idx++] = IntConstant.constant(col);
00477 }
00478 return node2expr(sub).project(cols);
00479 }
00480
00481 @Override
00482 protected Node visit(QuantifyExpression expr) {
00483 if (!GlobalOptions.INSTANCE.desugar_quants)
00484 return visit2(expr);
00485 if (expr.op() == Op.UNION)
00486 return visit2(expr);
00487 LocalDecls localDecls = expr.decls();
00488
00489 List<String> mults = Tr.absolutelyTerribleHack.get(localDecls);
00490 if (mults != null) {
00491 for (String mult : mults) {
00492 if ("DECL_SET".equals(mult))
00493 return visit2(expr);
00494 }
00495 }
00496
00497 expr.sub().accept(DiscoverHigherOrderQuant.instance);
00498 if (!DiscoverHigherOrderQuant.instance.higherOrderFound)
00499 return visit2(expr);
00500
00501
00502 List<LocalVariable> locals = new ArrayList<LocalVariable>(localDecls.locals().size());
00503 List<List<ForgeLiteral>> literals = new ArrayList<List<ForgeLiteral>>(locals.size());
00504 for (LocalVariable var : localDecls.locals()) {
00505 List<ForgeLiteral> lits = fconv.findLiteralsForType((Unary) var.type());
00506 if (lits.size() > 0) {
00507 locals.add(var);
00508 literals.add(lits);
00509 }
00510 }
00511 int nLocals = locals.size();
00512 if (nLocals == 0)
00513 return trueRelation;
00514 Node result = null;
00515 int[] idx = new int[nLocals];
00516 while (true) {
00517 for (int i = 0; i < nLocals; i++) {
00518 ForgeLiteral lit = literals.get(i).get(idx[i]);
00519 Expression litExpr = node2expr(lit.accept(this));
00520 quantStack.push(new StackElem(locals.get(i).name(), litExpr));
00521 }
00522 Node f = expr.sub().accept(this);
00523 if (result == null) {
00524 result = f;
00525 } else {
00526 switch (expr.op()) {
00527
00528
00529
00530 case ALL:
00531 result = node2form(result).and(node2form(f));
00532 break;
00533 case SOME:
00534 result = node2form(result).or(node2form(f));
00535 break;
00536 default:
00537 throw new RuntimeException("Unsupported quantify expression: " + expr.op() + " in " + expr);
00538 }
00539 }
00540 for (int i = 0; i < nLocals; i++)
00541 quantStack.pop();
00542 boolean broke = false;
00543 for (int i = nLocals - 1; i >= 0; i--) {
00544 if (idx[i] + 1 < literals.get(i).size()) {
00545 idx[i]++;
00546 broke = true;
00547 break;
00548 }
00549 }
00550 if (!broke)
00551 break;
00552 }
00553 return result;
00554 }
00555
00556 protected Node visit2(QuantifyExpression expr) {
00557 LocalDecls localDecls = expr.decls();
00558 List<String> mults = Tr.absolutelyTerribleHack.get(localDecls);
00559 int nLocals = localDecls.locals().size();
00560 List<Variable> vars = new ArrayList<Variable>(nLocals);
00561 Decls decls = null;
00562 int idx = 0;
00563 for (LocalVariable var : localDecls.locals()) {
00564 Variable kkVar = Variable.nary(var.name(), var.arity());
00565 Expression varType = visit(var.type());
00566 Decl decl;
00567 if (mults != null && "DECL_SET".equals(mults.get(idx++)))
00568 decl = kkVar.setOf(varType);
00569 else
00570 decl = kkVar.oneOf(varType);
00571
00572 if (decls == null)
00573 decls = decl;
00574 else
00575 decls = decls.and(decl);
00576 quantStack.push(new StackElem(kkVar.name(), kkVar));
00577 vars.add(kkVar);
00578 }
00579 try {
00580 Node node = expr.sub().accept(this);
00581 Formula f = node2form(node);
00582 switch (expr.op()) {
00583 case UNION:
00584 return f.comprehension(decls);
00585 case ALL:
00586 return fix(f.forAll(decls));
00587 case SOME:
00588 return fix(f.forSome(decls));
00589 case SUM:
00590 return node2int(node).sum(decls);
00591 default:
00592 throw new RuntimeException("Unsupported quantify expression: " + expr.op() + " in " + expr);
00593 }
00594 } finally {
00595 for (int i = 0; i < nLocals; i++)
00596 quantStack.pop();
00597 }
00598 }
00599
00600
00601
00602
00603
00604
00605
00606
00607
00608
00609
00610
00611
00612
00613
00614
00615 private Node fix(Formula quantFormula) {
00616
00617
00618
00619
00620
00621
00622
00623
00624
00625
00626
00627
00628
00629
00630
00631
00632
00633
00634
00635
00636
00637
00638
00639 return quantFormula;
00640 }
00641
00642 @Override
00643 protected Expression visit(OldExpression expr) {
00644 ForgeVariable var = expr.variable();
00645 assert var.isGlobal() : "you can only refer to global variables in the pre-state";
00646 Expression rel = var2rel.get(relName(var) + "_pre");
00647 if (rel == null)
00648 rel = getRelForVarAndCheck(var);
00649 return rel;
00650 }
00651
00652 private Expression getRelForVarAndCheck(ForgeVariable var) {
00653 Expression rel = var2rel.get(relName(var));
00654 assert rel != null : "relation for " + var.name() + " not found";
00655 return rel;
00656 }
00657
00658 private StackElem searchStack(String varName) {
00659 for (int i = quantStack.size() - 1; i >= 0; i--) {
00660 StackElem elem = quantStack.get(i);
00661 if (elem.name.equals(varName))
00662 return elem;
00663 }
00664 return null;
00665 }
00666
00667 }
00668
00669
00670
00671 protected Set<GlobalVariable> modifies;
00672 protected ForgeConverter fconv;
00673 protected ForgeScene forgeScene;
00674 protected ForgeProgram program;
00675
00676 protected Map<String, Relation> lit2rel;
00677 protected Map<ForgeType, Expression> type2expr;
00678 protected Map<String, Expression> var2rel;
00679 protected Map<ForgeVariable, ObjTupleSet> modVal;
00680 protected Map<ForgeVariable, ObjTupleSet> lowerBounds;
00681 protected Map<ForgeVariable, ObjTupleSet> upperBounds;
00682
00683 protected Set<Integer> ints;
00684 protected Relation trueRelation;
00685 protected Relation falseRelation;
00686 protected SpecCase cs;
00687
00688 public SquanderKodkodImpl() {
00689 modVal = new HashMap<ForgeVariable, ObjTupleSet>();
00690 lowerBounds = new HashMap<ForgeVariable, ObjTupleSet>();
00691 upperBounds = new HashMap<ForgeVariable, ObjTupleSet>();
00692 }
00693
00694 @Override
00695 protected Set<GlobalVariable> getModsForPostState(ForgeConverter fconv, SpecCase sc) {
00696 return sc.frame().modifiable();
00697 }
00698
00699 @Override
00700 protected ForgeExpression getPreSpec(SpecCase cs) {
00701 this.cs = cs;
00702
00703 return cs.pre().and(cs.spec().abstractConstraint());
00704 }
00705
00706 @Override
00707 protected ForgeExpression getPostSpec(SpecCase cs, ForgeConverter fconv) {
00708 this.cs = cs;
00709 Set<GlobalVariable> unmod = new HashSet<GlobalVariable>();
00710 unmod.addAll(fconv.forgeScene().program().globalVariables());
00711 unmod.removeAll(cs.frame().modifiable());
00712 ForgeExpression well = cs.spec().wellformedPost(unmod);
00713
00714 ForgeExpression post = cs.spec().abstractConstraint()
00715 .and(cs.post())
00716 .and(cs.spec().funcConstraint())
00717 .and(well);
00718
00719 for (GlobalVariable g : cs.frame().modifiable()) {
00720 ForgeExpression expr = cs.frame().instSelector(g);
00721 if (expr == null)
00722 continue;
00723 ForgeExpression lower = cs.frame().lowerBound(g);
00724 ForgeExpression upper = cs.frame().upperBound(g);
00725 SquanderEval2 se = new SquanderEval2();
00726 try {
00727 ObjTupleSet instMod = se.eval(expr, fconv);
00728 modVal.put(g, instMod);
00729 if (lower != null) {
00730 try {
00731 ObjTupleSet up = se.eval(lower, fconv);
00732 lowerBounds.put(g, instMod.product(up));
00733 } catch (Throwable t) {
00734 Log.warn("Could not evaluate lower bound expression " + lower + ": " + t.getMessage());
00735 post = post.and(cs.frame().lowerCond(g));
00736 }
00737 }
00738 if (upper != null) {
00739 try {
00740 ObjTupleSet up = se.eval(upper, fconv);
00741 upperBounds.put(g, instMod.product(up));
00742 } catch (Throwable t) {
00743 Log.warn("Could not evaluate upper bound expression " + upper + ": " + t.getMessage());
00744 post = post.and(cs.frame().upperCond(g));
00745 }
00746 }
00747 } catch (Throwable t) {
00748 Log.warn("Could not evaluate instance selector expression " + expr + ": " + t.getMessage());
00749 post = post.and(cs.frame().modCond(g));
00750 }
00751 }
00752
00753 return post;
00754 }
00755
00756 @Override
00757 protected IEvaluator exeSpec(ForgeExpression spec, Set<GlobalVariable> modifies, ForgeConverter fconv) {
00758 this.modifies = modifies;
00759 this.fconv = fconv;
00760 this.forgeScene = fconv.forgeScene();
00761 this.program = forgeScene.program();
00762
00763 init();
00764
00765 createRelations();
00766 Formula formula = convertSpec(spec);
00767
00768 Bounds bounds = createBounds();
00769
00770 Log.log(printBoundsSummary(bounds));
00771
00772 Solver solver = new Solver();
00773 Log.log("Using bitwidth: " + fconv.heap2Lit().minBW());
00774 solver.options().setBitwidth(fconv.heap2Lit().minBW());
00775 solver.options().setFlatten(false);
00776 solver.options().setReporter(GlobalOptions.INSTANCE.reporter.kkReporter());
00777 if (GlobalOptions.INSTANCE.unsat_core) {
00778 solver.options().setLogTranslation(1);
00779 solver.options().setSolver(SATFactory.MiniSatProver);
00780 } else {
00781 solver.options().setLogTranslation(0);
00782 solver.options().setSolver(GlobalOptions.INSTANCE.sat_solver);
00783 }
00784
00785 boolean solveAll = false;
00786 Options opts = fconv.javaScene().methodSpec().options();
00787 if (opts != null)
00788 solveAll = opts.solveAll();
00789
00790 if (solveAll)
00791 solver.options().setSymmetryBreaking(1000);
00792
00793 Log.debug("==============================================");
00794 Log.debug("------------- Solving kk formula -------------");
00795 Log.debug("==============================================");
00796 Log.debug(PrettyPrinter.print(formula, 2));
00797 Log.debug("\n" + bounds);
00798 IEvaluator eval;
00799 if (solveAll)
00800 eval = getEval(solver.solveAll(formula, bounds));
00801 else
00802 eval = getEval(Collections.singleton(solver.solve(formula, bounds)).iterator());
00803 return eval;
00804 }
00805
00806 private String printBoundsSummary(Bounds bounds) {
00807 List<Entry<Relation, TupleSet>> bnds = new ArrayList<Entry<Relation,TupleSet>>();
00808 bnds.addAll(bounds.upperBounds().entrySet());
00809 Collections.sort(bnds, new Comparator<Entry<Relation, TupleSet>>() {
00810 @Override
00811 public int compare(Entry<Relation, TupleSet> o1, Entry<Relation, TupleSet> o2) {
00812 return -(new Integer(o1.getValue().size()).compareTo(o2.getValue().size()));
00813 }
00814 });
00815 StringBuilder sb = new StringBuilder();
00816 sb.append("Bound stats: \n");
00817 sb.append("-----------------------------------------------------\n");
00818 for (Entry<Relation, TupleSet> e : bnds) {
00819 if (e.getKey().arity() == 1 && e.getValue().size() <= 1)
00820 continue;
00821 sb.append(String.format("%40s (%s) : %s\n", e.getKey().name(), e.getKey().arity(), e.getValue().size()));
00822 }
00823 return sb.toString();
00824 }
00825
00826 protected IEvaluator getEval(Iterator<Solution> solution) {
00827 KodkodEval kodkodEval = new KodkodEval(solution);
00828 return kodkodEval;
00829 }
00830
00831 protected void init() {
00832 lit2rel = new LinkedHashMap<String, Relation>();
00833 type2expr = new LinkedHashMap<ForgeType, Expression>();
00834 type2expr.put(program.integerDomain(), Expression.INTS);
00835 var2rel = new LinkedHashMap<String, Expression>();
00836 ints = new HashSet<Integer>();
00837 }
00838
00839 protected Formula convertSpec(ForgeExpression spec) {
00840 Node node = spec.accept(new Tr2KK());
00841 return node2form(node);
00842 }
00843
00844 protected void createRelations() {
00845
00846
00847 List<ForgeLiteral> literals = new LinkedList<ForgeLiteral>();
00848 literals.addAll(program.instanceLiterals());
00849 literals.add(program.trueLiteral());
00850 literals.add(program.falseLiteral());
00851 for (ForgeLiteral lit : literals) {
00852 Relation rel = Relation.unary(lit.name());
00853 lit2rel.put(lit.name(), rel);
00854
00855
00856
00857
00858
00859
00860 }
00861 this.trueRelation = lit2rel.get(program.trueLiteral().name());
00862 this.falseRelation = lit2rel.get(program.falseLiteral().name());
00863
00864
00865 for (InstanceDomain dom : program.instanceDomains()) {
00866 type2expr.put(dom, Relation.nary(dom.name(), dom.arity()));
00867 }
00868
00869
00870 for (GlobalVariable g : program.globalVariables()) {
00871 addRelForVar(g, relName(g));
00872 if (modifies.contains(g))
00873 addRelForVar(g, relName(g) + "_pre");
00874 }
00875
00876
00877 if (forgeScene.thisVar() != null)
00878 addRelForVar(forgeScene.thisVar(), relName(forgeScene.thisVar()));
00879 for (LocalVariable var : forgeScene.args())
00880 addRelForVar(var, relName(var));
00881 if (forgeScene.returnVar() != null)
00882 addRelForVar(forgeScene.returnVar(), relName(forgeScene.returnVar()));
00883 }
00884
00885 protected Bounds createBounds() {
00886 ForgeBounds forgeBounds = fconv.forgeBounds();
00887 reporter.creatingKodkodUniverse();
00888 Universe univ = createUniverse();
00889
00890 reporter.creatingKodkodBounds();
00891 TupleFactory f = univ.factory();
00892 Bounds b = new Bounds(univ);
00893
00894
00895 for (Entry<String, Relation> e : lit2rel.entrySet()) {
00896 b.boundExactly(e.getValue(), f.setOf(e.getKey()));
00897 }
00898
00899
00900 for (InstanceDomain dom : program.instanceDomains()) {
00901 List<ForgeLiteral> instLiterals = fconv.findLiteralsForType(dom);
00902 TupleSet bound = f.noneOf(dom.arity());
00903 if (!instLiterals.isEmpty()) {
00904 Object[] atoms = new Object[instLiterals.size()];
00905 int idx = 0;
00906 for (ForgeLiteral lit : instLiterals) {
00907 atoms[idx++] = lit.name();
00908 }
00909 bound = f.setOf(atoms);
00910 }
00911 b.boundExactly((Relation)type2expr.get(dom), bound);
00912 }
00913
00914
00915 for (GlobalVariable var : program.globalVariables()) {
00916 ForgeConstant lower = forgeBounds.initialLowerBound(var);
00917 ForgeConstant upper = lower;
00918 if (forgeScene.isSpecField(var)) {
00919 upper = forgeBounds.initialUpperBound(var);
00920 }
00921 TupleSet lowerTupleSet = conv2tuples(lower, f);
00922 TupleSet upperTupleSet = conv2tuples(upper, f);
00923 Relation rel = (Relation) var2rel.get(relName(var));
00924 if (modifies.contains(var)) {
00925 Relation preRel = (Relation) var2rel.get(relName(var) + "_pre");
00926 b.bound(preRel, lowerTupleSet, upperTupleSet);
00927 ForgeConstant postLower = getPostLower(var, lower);
00928 ForgeConstant postUpper = getPostUpper(var, postLower);
00929 b.bound(rel, conv2tuples(postLower, f), conv2tuples(postUpper, f));
00930 } else {
00931 b.bound(rel, lowerTupleSet, upperTupleSet);
00932 }
00933 }
00934
00935
00936 boundLocalVar(forgeScene.thisVar(), f, b);
00937 for (LocalVariable var : forgeScene.args())
00938 boundLocalVar(var, f, b);
00939 boundLocalVar(forgeScene.returnVar(), f, b);
00940
00941
00942 for (Integer i : ints) {
00943 b.boundExactly(i, f.setOf(i));
00944 }
00945
00946 return b;
00947 }
00948
00949 protected ForgeConstant getPostLower(GlobalVariable g, ForgeConstant initialBound) {
00950 ForgeBounds forgeBounds = fconv.forgeBounds();
00951 ObjTupleSet ots = modVal.get(g);
00952 if (ots == null)
00953 return forgeBounds.empty(g.arity());
00954 List<ForgeLiteral> lits = new LinkedList<ForgeLiteral>(fconv.findLiteralsForType(g.type().domain()));
00955 for (ObjTuple t : ots.tuples()) {
00956 assert t.arity() == 1;
00957 if (t.arity() == 1) {
00958 InstanceLiteral l = forgeScene.instLitForObj(t.get(0));
00959 assert l != null;
00960 lits.remove(l);
00961 }
00962 }
00963
00964 ForgeConstant res = forgeBounds.empty(g.arity());
00965 for (ForgeLiteral lit : lits) {
00966 ForgeAtom atom = lit2atom(lit, forgeBounds);
00967 res = res.union(atom.product(atom.join(initialBound)));
00968 }
00969 return res;
00970 }
00971
00972 private ForgeAtom lit2atom(ForgeLiteral lit, ForgeBounds forgeBounds) {
00973 ForgeAtom atom;
00974 if (lit instanceof IntegerLiteral)
00975 atom = forgeBounds.intAtom(((IntegerLiteral) lit).value());
00976 else if (lit instanceof BooleanLiteral)
00977 atom = forgeBounds.boolAtom(((BooleanLiteral) lit).value());
00978 else
00979 atom = forgeBounds.instanceAtom((InstanceLiteral) lit);
00980 return atom;
00981 }
00982
00983 protected ForgeConstant getPostUpper(GlobalVariable var, ForgeConstant postLower) {
00984 ForgeConstant extent = getExtent(var, postLower);
00985 ObjTupleSet upper = upperBounds.get(var);
00986 if (upper != null)
00987 extent = fconv.conv2fc(upper, fconv.forgeBounds());
00988 ObjTupleSet ots = modVal.get(var);
00989 if (ots == null)
00990 return extent;
00991 ForgeConstant mod = fconv.conv2fc(ots, fconv.forgeBounds());
00992 return mod.product(mod.join(extent)).union(postLower);
00993 }
00994
00995 protected Universe createUniverse() {
00996 Collection<Object> atoms = new LinkedList<Object>();
00997
00998 for (InstanceLiteral lit : program.instanceLiterals())
00999 atoms.add(lit.name());
01000
01001 if (forgeScene.isEnsureAllInts()) {
01002 for (int val = fconv.minInt(); val <= fconv.maxInt(); val++) {
01003 atoms.add(val);
01004 ints.add(val);
01005 }
01006 } else {
01007 int maxInt = fconv.maxInt();
01008 int minInt = fconv.minInt();
01009 for (int intValue : forgeScene.ints()) {
01010 if (intValue > maxInt || intValue < minInt)
01011 continue;
01012 atoms.add(intValue);
01013 ints.add(intValue);
01014 }
01015 }
01016
01017 atoms.add(program.trueLiteral().name());
01018 atoms.add(program.falseLiteral().name());
01019 return new Universe(atoms);
01020 }
01021
01022
01023
01024
01025
01027 protected Formula node2form(Node node) {
01028 if (node == trueRelation) return Formula.TRUE;
01029 if (node == falseRelation) return Formula.FALSE;
01030 if (node instanceof Formula)
01031 return (Formula) node;
01032 if (node instanceof IfExpression) {
01033 IfExpression ifExpr = (IfExpression) node;
01034 if (ifExpr.thenExpr().equals(trueRelation) &&
01035 ifExpr.elseExpr().equals(falseRelation)) {
01036 return ifExpr.condition();
01037 }
01038 }
01039 if (node instanceof Expression)
01040 return ((Expression) node).in(trueRelation);
01041 throw new RuntimeException("don't know how to convert " + node.getClass().getSimpleName() + " to formula");
01042 }
01043
01045 protected IntExpression node2int(Node node) {
01046 if (node instanceof Expression)
01047 return ((Expression) node).sum();
01048 if (node instanceof IntExpression)
01049 return (IntExpression) node;
01050 if (node instanceof IntToExprCast)
01051 return ((IntToExprCast) node).intExpr();
01052 throw new RuntimeException("don't know how to convert " + node.getClass().getSimpleName() + " to int");
01053 }
01054
01056 protected Expression node2expr(Node node) {
01057 if (node instanceof Expression)
01058 return (Expression)node;
01059 if (node instanceof IntExpression)
01060 return ((IntExpression) node).toExpression();
01061 if (node instanceof ExprToIntCast)
01062 return ((ExprToIntCast) node).expression();
01063 if (node instanceof Formula)
01064 return form2expr((Formula) node);
01065 throw new RuntimeException("don't know how to convert " + node.getClass().getSimpleName() + " to expression");
01066 }
01067
01069 protected Expression form2expr(Formula form) {
01070 if (form == Formula.TRUE) return trueRelation;
01071 if (form == Formula.FALSE) return falseRelation;
01072 return form.thenElse(trueRelation, falseRelation);
01073 }
01074
01075 protected ForgeConstant getExtent(GlobalVariable var, ForgeConstant lower) {
01076 String name = var.name();
01077 ForgeType type = var.type();
01078 ForgeBounds forgeBounds = fconv.forgeBounds();
01079 if (name.endsWith("[]__elems")) {
01080
01081 assert type.arity() == 3 :
01082 "expected arity 3 for array elems but actual arity is " + var.arity();
01083 assert type.projectType(1) instanceof IntegerDomain :
01084 "expected the 2nd col to be IntegerDomain but is " + type.projectType(1).getClass();
01085 int upperBound = findMaxArrayLength(var);
01086 return forgeBounds.extent(type.projectType(0))
01087 .product(nonnegs(upperBound))
01088 .product(forgeBounds.extent(type.projectType(2)));
01089 } else if (name.endsWith("[]__length")) {
01090
01091 assert type.arity() == 2 :
01092 "expected arity 2 for array length relation but actual arity is " + var.arity();
01093 assert type.projectType(1) instanceof IntegerDomain :
01094 "expected the 2nd col to be IntegerDomain but is " + type.projectType(1).getClass();
01095 return forgeBounds.extent(type.projectType(0)).product(nonnegs());
01096 } else {
01097 ForgeConstant fc = forgeBounds.extent(var.type());
01098 if (forgeScene.isOneField(var)) {
01099 for (forge.solve.ForgeConstant.Tuple t : lower.tuples()) {
01100 ForgeAtom src = t.atoms().get(0);
01101 fc = fc.difference(src.product(src.join(fc))).union(t);
01102 }
01103 }
01104 return fc;
01105 }
01106 }
01107
01108 protected int findMaxArrayLength(GlobalVariable var) {
01109 String lenVarName = var.name().replace("[].elems", "[].length");
01110 GlobalVariable len = forgeScene.global(lenVarName);
01111 assert len != null : "could not find the corresponding length variable for " + var.name();
01112 if (modifies.contains(len))
01113 return Integer.MAX_VALUE;
01114 ForgeConstant fc = fconv.forgeBounds().initialUpperBound(len);
01115 int max = 0;
01116 for (forge.solve.ForgeConstant.Tuple t : fc.tuples()) {
01117 IntegerAtom a = (IntegerAtom) t.atoms().get(1);
01118 if (a.value() > max)
01119 max = a.value();
01120 }
01121 return max - 1;
01122 }
01123
01124 protected ForgeConstant.Unary nonnegs() {
01125 return nonnegs(fconv.forgeBounds().maxIntValue());
01126 }
01127
01128 protected ForgeConstant.Unary nonnegs(int upperBound) {
01129 ForgeBounds forgeBounds = fconv.forgeBounds();
01130 ForgeConstant.Unary nonnegs = forgeBounds.empty();
01131
01132 int n = Math.min(forgeBounds.maxIntValue(), upperBound);
01133 for (int i = 0; i <= n; i++) {
01134 nonnegs = nonnegs.union(forgeBounds.intAtom(i));
01135 }
01136 return nonnegs;
01137 }
01138
01139 protected void boundLocalVar(LocalVariable var, TupleFactory f, Bounds b) {
01140 if (var == null)
01141 return;
01142 ForgeConstant lower = fconv.forgeBounds().initialLowerBound(var);
01143 ForgeConstant upper = fconv.forgeBounds().initialUpperBound(var);
01144 TupleSet lowerBound = conv2tuples(lower, f);
01145 TupleSet upperBound = conv2tuples(upper, f);
01146 Relation rel = (Relation) var2rel.get(relName(var));
01147 b.bound(rel, lowerBound, upperBound);
01148 }
01149
01150 protected void addRelForVar(ForgeVariable var, String name) {
01151 Relation rel = Relation.nary(name, var.arity());
01152 var2rel.put(name, rel);
01153 }
01154
01155 protected String relName(ForgeVariable var) {
01156 return var.name();
01157
01158
01159
01160 }
01161
01162 protected TupleSet conv2tuples(ForgeConstant fc, TupleFactory f) {
01163 List<kodkod.instance.Tuple> kkTuples = new LinkedList<kodkod.instance.Tuple>();
01164 l: for (ForgeConstant.Tuple t : fc.tuples()) {
01165 Object[] atoms = new Object[t.arity()];
01166 int idx = 0;
01167 for (ForgeAtom a : t.atoms()) {
01168 Object atom = convAtom(a);
01169 if (atom == null)
01170 continue l;
01171 atoms[idx++] = atom;
01172 }
01173 kkTuples.add(f.tuple(atoms));
01174 }
01175
01176 if (kkTuples.isEmpty())
01177 return f.noneOf(fc.arity());
01178 else
01179 return f.setOf(kkTuples);
01180 }
01181
01182 protected Object convAtom(ForgeAtom a) {
01183 if (a instanceof IntegerAtom) {
01184 int val = ((IntegerAtom) a).value();
01185 if (!ints.contains(val))
01186 return null;
01187 return val;
01188 }
01189 return a.name();
01190 }
01191
01192 protected TupleSet conv2tuples(ObjTupleSet fc, TupleFactory f) {
01193 List<kodkod.instance.Tuple> kkTuples = new LinkedList<kodkod.instance.Tuple>();
01194 for (ObjTuple t : fc.tuples()) {
01195 Object[] atoms = new Object[t.arity()];
01196 int idx = 0;
01197 for (Object a : t.atoms()) {
01198 ForgeLiteral lit = forgeScene.forgeLitForObj(a);
01199 assert lit != null;
01200 Object atom = lit.name();
01201 if (lit instanceof IntegerLiteral)
01202 atom = ((IntegerLiteral)lit).value();
01203 atoms[idx++] = atom;
01204 }
01205 kkTuples.add(f.tuple(atoms));
01206 }
01207
01208 if (kkTuples.isEmpty())
01209 return f.noneOf(fc.arity());
01210 else
01211 return f.setOf(kkTuples);
01212 }
01213
01214 }