Initial commit.

1 files changed, 82 insertions, 0 deletions

diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
new file mode 100644
index 0000000..d692ecd
--- /dev/null
+++ b/instr-to-kodkod/src/Main.java
@@ -0,0 +1,82 @@
+/* FIXME: Finer imports */
+import kodkod.ast.*;
+
+import kodkod.engine.*;
+import kodkod.engine.config.*;
+import kodkod.engine.satlab.*;
+
+import kodkod.instance.*;
+public class Main
+{
+   private static Formula get_formula (final VHDLModel model)
+   {
+      final Variable w;
+
+      w = Variable.unary("w");
+
+      return
+         w.join
+         (
+            model.get_predicate_as_relation("is_accessed_by")
+         ).no().forSome(w.oneOf(model.get_type_as_relation("waveform")));
+   }
+
+   public static void main (final String... args)
+   {
+      final VHDLModel model;
+
+      final Universe univ;
+      final TupleFactory tf;
+      final Bounds bounds;
+
+      final Solver solver;
+      final Solution sol;
+
+      if (args.length != 1)
+      {
+         System.out.println("Use: java Main <instructions_file>");
+
+         return;
+      }
+
+      model = new VHDLModel();
+
+      try
+      {
+         VHDLLevel.add_to_model(model, "./structural_level.data");
+      }
+      catch (final Exception e)
+      {
+         System.err.println("[E] Could not load structural level:");
+         e.printStackTrace();
+
+         return;
+      }
+
+      try
+      {
+         model.parse_file(args[0]);
+      }
+      catch (final Exception e)
+      {
+         System.err.println("[E] Could not load instructions:");
+         e.printStackTrace();
+
+         return;
+      }
+
+      univ = new Universe(model.get_atoms());
+      tf = univ.factory();
+      bounds = new Bounds(univ);
+
+      model.add_to_bounds(bounds, tf);
+
+      solver = new Solver();
+      solver.options().setSolver(SATFactory.DefaultSAT4J);
+      solver.options().setReporter(new ConsoleReporter());
+
+      sol = solver.solve(get_formula(model), bounds);
+
+      System.out.println(sol);
+   }
+}