instr-to-kodkod/src/Main.java


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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);
   }
}