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 import java.util.SortedMap;
00007 import java.util.TreeMap;
00008
00009 import forge.cfg.ForgeCFG;
00010 import forge.program.ForgeExpression;
00011 import forge.program.ForgeProcedure;
00012 import forge.program.ForgeProgram;
00013 import forge.program.GlobalVariable;
00014 import forge.program.InstanceDomain;
00015 import forge.program.InstanceLiteral;
00016 import forge.program.LocalVariable;
00017 import forge.solve.ForgeAtom;
00018 import forge.solve.ForgeBounds;
00019 import forge.solve.ForgeConstant;
00020 import forge.solve.ForgeSolution;
00021 import forge.solve.ForgeSolver;
00022 import forge.solve.InstanceAtom;
00023 import forge.solve.IntegerAtom;
00024 import forge.solve.SolveOptions;
00025 import forge.solve.ForgeConstant.Tuple;
00026 import forge.util.SystemOutReporter;
00027
00032 public class TopologicalSort {
00033 final int num = 16;
00034 final int width = 4;
00035 final ForgeProgram program;
00036 final InstanceDomain node;
00037 final InstanceDomain list;
00038 final InstanceLiteral[] nodes = new InstanceLiteral[num];
00039 final GlobalVariable value, next, elems;
00040 final ForgeProcedure proc;
00041 final LocalVariable out;
00042
00043 public TopologicalSort() {
00044 program = new ForgeProgram();
00045 node = program.newInstanceDomain("Node");
00046 list = program.newInstanceDomain("List");
00047 out = program.newLocalVariable("out", list);
00048
00049 for (int i = 0; i < num; i++)
00050 nodes[i] = program.newInstanceLiteral("node"+i, node);
00051
00052 value = program.newGlobalVariable("value", node.product(program.integerDomain()));
00053 next = program.newGlobalVariable("next", node.product(node));
00054 elems = program.newGlobalVariable("elems", list.product(program.integerDomain()).product(node));
00055
00056 proc = program.newProcedure("sort", program.emptyDecls(), out);
00057 }
00058
00059 ForgeExpression condition() {
00060 ForgeExpression list = out.join(elems);
00061 LocalVariable i1 = program.newLocalVariable("i1", program.integerDomain());
00062 LocalVariable i2 = program.newLocalVariable("i5", program.integerDomain());
00063 LocalVariable i3 = program.newLocalVariable("i6", program.integerDomain());
00064
00065 LocalVariable n1 = program.newLocalVariable("n1", node);
00066
00067 return out.one()
00068 .and(i1.join(list).lone().forAll(i1))
00069 .and(list.join(n1).one().forAll(n1))
00070 .and(i2.lt(i3)
00071
00072
00073 .implies(i2.join(list).in(i3.join(list).join(next)).not())
00074 .forAll(i2)
00075 .forAll(i3))
00076 ;
00077 }
00078
00079 ForgeCFG cfg() {
00080 return ForgeCFG.specification(proc, Collections.singleton(elems), condition());
00081 }
00082
00083 ForgeBounds bounds() {
00084 Map<InstanceDomain, Integer> dom2bound = new HashMap<InstanceDomain, Integer>();
00085 dom2bound.put(node, 0);
00086 dom2bound.put(list, 1);
00087 ForgeBounds bounds = new ForgeBounds(program, width, dom2bound);
00088
00089
00090 InstanceAtom[] a = new InstanceAtom[num];
00091 for (int i = 0; i < num; i++)
00092 a[i] = bounds.instanceAtom(nodes[i]);
00093
00094
00095 ForgeConstant next = a[0].product(a[1]);
00096 for (int i = 1; i < num - 1; i++) {
00097 next = next.union(a[i].product(a[i+1]));
00098 if (i + 2 < num)
00099 next = next.union(a[i].product(a[i+2]));
00100 }
00101
00102 System.err.println("Next: " + next);
00103 bounds.boundInitial(this.next, next, next);
00104 return bounds;
00105 }
00106
00107 void run() {
00108
00109 SolveOptions options = new SolveOptions.Builder(1).reporter(SystemOutReporter.REPORTER).build();
00110 ForgeSolver solver = new ForgeSolver(cfg(), options);
00111 ForgeSolution solution = solver.run(bounds());
00112 if (solution.trace() == null) {
00113 System.err.println("no trace");
00114 return;
00115 }
00116
00117 ForgeConstant value = solution.trace().evaluate(out.join(elems));
00118
00119 SortedMap<Integer, ForgeAtom> map = new TreeMap<Integer, ForgeAtom>();
00120 for (Tuple tuple : value.tuples()) {
00121 map.put(((IntegerAtom) tuple.atoms().get(0)).value(), tuple.atoms().get(1));
00122 }
00123 System.err.println("Sorting: " + map.values());
00124 }
00125
00126 public static void main(String[] args) {
00127 TopologicalSort sort = new TopologicalSort();
00128 sort.run();
00129 }
00130 }