00001 package edu.mit.csail.sdg.squander.forge_examples;
00002
00003 import java.util.Collections;
00004 import java.util.HashMap;
00005 import java.util.Map;
00006
00007 import forge.cfg.ForgeCFG;
00008 import forge.program.ForgeExpression;
00009 import forge.program.ForgeProcedure;
00010 import forge.program.ForgeProgram;
00011 import forge.program.GlobalVariable;
00012 import forge.program.InstanceDomain;
00013 import forge.program.InstanceLiteral;
00014 import forge.program.LocalVariable;
00015 import forge.solve.ForgeBounds;
00016 import forge.solve.ForgeConstant;
00017 import forge.solve.ForgeSolution;
00018 import forge.solve.ForgeSolver;
00019 import forge.solve.InstanceAtom;
00020 import forge.solve.IntegerAtom;
00021 import forge.solve.SolveOptions;
00022 import forge.solve.ForgeConstant.Tuple;
00023 import forge.util.SystemOutReporter;
00024
00031 public class BinarySearchTree {
00032
00033 private ForgeProgram program;
00034 private InstanceDomain node;
00035 private InstanceDomain bst;
00036
00037 private InstanceLiteral nodeInsts[];
00038 private InstanceLiteral bstInst;
00039
00040 private GlobalVariable root;
00041 private GlobalVariable key;
00042 private GlobalVariable left;
00043 private GlobalVariable right;
00044 private GlobalVariable parent;
00045
00046 private LocalVariable minRet;
00047
00048 private ForgeProcedure minProc;
00049
00054 public BinarySearchTree() {
00055 program = new ForgeProgram();
00056
00057 node = program.newInstanceDomain("Node");
00058 bst = program.newInstanceDomain("BST");
00059
00060 bstInst = program.newInstanceLiteral("bst", bst);
00061 int nNodes = 6;
00062 nodeInsts = new InstanceLiteral[nNodes];
00063 for (int i = 0; i < nNodes; i++) {
00064 nodeInsts[i] = program.newInstanceLiteral("node" + Integer.toString(i), node);
00065 }
00066
00067 root = program.newGlobalVariable("root", bst.product(node));
00068 key = program.newGlobalVariable("key", node.product(program.integerDomain()));
00069 left = program.newGlobalVariable("left", node.product(node));
00070 right = program.newGlobalVariable("right", node.product(node));
00071 parent = program.newGlobalVariable("parent", node.product(node));
00072
00073 minRet = program.newLocalVariable("min_return", program.integerDomain());
00074
00075 minProc = program.newProcedure("min", program.emptyDecls(), minRet);
00076 }
00077
00082 public void runMin() {
00083 ForgeCFG cfg = cfgMin();
00084 System.out.println(cfg);
00085 ForgeSolver solver = new ForgeSolver(cfg, options());
00086 ForgeBounds bounds = bounds();
00087 ForgeSolution solution = solver.run(bounds);
00088 if (solution.trace() == null) {
00089 System.out.println("NO SOLUTION");
00090 return;
00091 }
00092 ForgeConstant x = solution.trace().evaluate(minRet);
00093 System.out.println(((IntegerAtom) x.tuples().iterator().next().atoms().get(0)).value());
00094 }
00095
00099 private static SolveOptions options() {
00100 SolveOptions options = new SolveOptions.Builder(1).reporter(
00101 SystemOutReporter.REPORTER).build();
00102 return options;
00103 }
00104
00108 private ForgeCFG cfgMin() {
00109 LocalVariable k = program.newLocalVariable("k", node);
00110 LocalVariable l = program.newLocalVariable("l", node);
00111 ForgeExpression condition = minRet.one().and(k.join(key).eq(minRet).forSome(k)).and(
00112 l.join(key).gte(minRet).forAll(l));
00113 return ForgeCFG.specification(minProc, Collections.<GlobalVariable> emptySet(), condition);
00114 }
00115
00120 private ForgeBounds bounds() {
00121 Map<InstanceDomain, Integer> dom2bound = new HashMap<InstanceDomain, Integer>();
00122 dom2bound.put(bst, 0);
00123 dom2bound.put(node, 0);
00124 ForgeBounds bounds = new ForgeBounds(program, 4, dom2bound);
00125 int nNodes = 6;
00126 InstanceAtom[] nodeAtoms = new InstanceAtom[nNodes];
00127 for (int i = 0; i < nNodes; i++) {
00128 nodeAtoms[i] = bounds.instanceAtom(nodeInsts[i]);
00129 }
00130 InstanceAtom bstAtom = bounds.instanceAtom(bstInst);
00131
00132 Tuple rootBound = bstAtom.product(nodeAtoms[0]);
00133 bounds.boundInitial(root, rootBound, rootBound);
00134
00135 ForgeConstant leftBound = (nodeAtoms[0].product(nodeAtoms[1])).union(
00136 nodeAtoms[2].product(nodeAtoms[4])).union(nodeAtoms[1].product(nodeAtoms[5]));
00137 bounds.boundInitial(left, leftBound, leftBound);
00138
00139 ForgeConstant rightBound = (nodeAtoms[0].product(nodeAtoms[2])).union(nodeAtoms[1]
00140 .product(nodeAtoms[3]));
00141 bounds.boundInitial(right, rightBound, rightBound);
00142
00143 ForgeConstant parentBound = (nodeAtoms[1].product(nodeAtoms[0])).union(
00144 nodeAtoms[2].product(nodeAtoms[0])).union(nodeAtoms[3].product(nodeAtoms[1]))
00145 .union(nodeAtoms[4].product(nodeAtoms[2]))
00146 .union(nodeAtoms[5].product(nodeAtoms[1]));
00147 bounds.boundInitial(parent, parentBound, parentBound);
00148
00149 ForgeConstant keyBound = (nodeAtoms[0].product(bounds.intAtom(5))).union(
00150 nodeAtoms[1].product(bounds.intAtom(3))).union(
00151 nodeAtoms[2].product(bounds.intAtom(7))).union(
00152 nodeAtoms[3].product(bounds.intAtom(4))).union(
00153 nodeAtoms[4].product(bounds.intAtom(6))).union(
00154 nodeAtoms[5].product(bounds.intAtom(2)));
00155 bounds.boundInitial(key, keyBound, keyBound);
00156
00157 return bounds;
00158 }
00159
00160 public static void main(String[] args) {
00161 BinarySearchTree b = new BinarySearchTree();
00162 b.runMin();
00163 }
00164
00165 }