diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic')
2 files changed, 121 insertions, 1 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath index ea427d90..a2655410 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath | |||
@@ -5,6 +5,6 @@ | |||
5 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> | 5 | <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> |
6 | <classpathentry kind="src" path="src"/> | 6 | <classpathentry kind="src" path="src"/> |
7 | <classpathentry kind="src" path="xtend-gen"/> | 7 | <classpathentry kind="src" path="xtend-gen"/> |
8 | <classpathentry kind="lib" path="C:/Applications/z3-4.8.7-x64-win/bin/com.microsoft.z3.jar"/> | 8 | <classpathentry kind="lib" path="lib/com.microsoft.z3.jar"/> |
9 | <classpathentry kind="output" path="bin"/> | 9 | <classpathentry kind="output" path="bin"/> |
10 | </classpath> | 10 | </classpath> |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java new file mode 100644 index 00000000..a3d25ccf --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java | |||
@@ -0,0 +1,120 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | ||
2 | |||
3 | import java.util.HashMap; | ||
4 | |||
5 | import com.microsoft.z3.*; | ||
6 | |||
7 | public class ExampleRecreation { | ||
8 | |||
9 | |||
10 | public static void sudoku(Context ctx) { | ||
11 | |||
12 | // 9 * 9 int matrix | ||
13 | IntExpr[][] X = new IntExpr[9][]; | ||
14 | for (int i = 0; i < 9; i++) { | ||
15 | X[i] = new IntExpr[9]; | ||
16 | for (int j = 0; j < 9; j++) { | ||
17 | X[i][j] = (IntExpr) ctx.mkConst(ctx.mkSymbol("x_" + (i + 1) + "_" + (j + 1)), ctx.getIntSort()); | ||
18 | } | ||
19 | } | ||
20 | |||
21 | // Cell value from 1 - 9 | ||
22 | BoolExpr[][] cells = new BoolExpr[9][]; | ||
23 | for (int i = 0; i < 9; i++) { | ||
24 | cells[i] = new BoolExpr[9]; | ||
25 | for (int j = 0; j < 9; j++) { | ||
26 | cells[i][j] = ctx.mkAnd(ctx.mkLe(ctx.mkInt(1), X[i][j]), ctx.mkLe(X[i][j], ctx.mkInt(9))); | ||
27 | } | ||
28 | } | ||
29 | |||
30 | // Each value in a row is distinct | ||
31 | BoolExpr[] row = new BoolExpr[9]; | ||
32 | for (int i = 0; i < 9; i++) { | ||
33 | row[i] = ctx.mkDistinct(X[i]); | ||
34 | } | ||
35 | |||
36 | // Each value in a col is distinct | ||
37 | BoolExpr[] col = new BoolExpr[9]; | ||
38 | for (int j = 0; j < 9; j++) { | ||
39 | IntExpr[] one_col = new IntExpr[9]; | ||
40 | for (int i = 0; i < 9; i++) { | ||
41 | one_col[i] = X[i][j]; | ||
42 | } | ||
43 | col[j] = ctx.mkDistinct(one_col); | ||
44 | } | ||
45 | |||
46 | |||
47 | // Each value in a 3*3 square is distinct | ||
48 | BoolExpr[][] squares = new BoolExpr[3][]; | ||
49 | for (int x = 0; x < 3; x++) { | ||
50 | squares[x] = new BoolExpr[3]; | ||
51 | for (int y = 0; y < 3; y++) { | ||
52 | IntExpr[] square = new IntExpr[9]; | ||
53 | for (int i = 0; i < 3; i++) { | ||
54 | for (int j = 0; j < 3; j++) { | ||
55 | square[3 * i + j] = X[3 * x + i][3 * y + j]; | ||
56 | } | ||
57 | } | ||
58 | squares[x][y] = ctx.mkDistinct(square); | ||
59 | } | ||
60 | } | ||
61 | |||
62 | // Combine all conditions | ||
63 | BoolExpr sudoku = ctx.mkTrue(); | ||
64 | for (BoolExpr[] e: cells) { | ||
65 | sudoku = ctx.mkAnd(ctx.mkAnd(e), sudoku); | ||
66 | } | ||
67 | sudoku = ctx.mkAnd(ctx.mkAnd(row), sudoku); | ||
68 | sudoku = ctx.mkAnd(ctx.mkAnd(col), sudoku); | ||
69 | for (BoolExpr[] e: squares) { | ||
70 | sudoku = ctx.mkAnd(ctx.mkAnd(e), sudoku); | ||
71 | } | ||
72 | |||
73 | int[][] instance = { { 0, 0, 0, 0, 9, 4, 0, 3, 0 }, | ||
74 | { 0, 0, 0, 5, 1, 0, 0, 0, 7 }, { 0, 8, 9, 0, 0, 0, 0, 4, 0 }, | ||
75 | { 0, 0, 0, 0, 0, 0, 2, 0, 8 }, { 0, 6, 0, 2, 0, 1, 0, 5, 0 }, | ||
76 | { 1, 0, 2, 0, 0, 0, 0, 0, 0 }, { 0, 7, 0, 0, 0, 0, 5, 2, 0 }, | ||
77 | { 9, 0, 0, 0, 6, 5, 0, 0, 0 }, { 0, 4, 0, 9, 7, 0, 0, 0, 0 } }; | ||
78 | |||
79 | // Set assertions enforced by the instance | ||
80 | BoolExpr inst = ctx.mkTrue(); | ||
81 | for (int i = 0; i < 9; i++) { | ||
82 | for (int j = 0; j < 9; j++) { | ||
83 | inst = ctx.mkAnd(inst, (BoolExpr) ctx.mkITE(ctx.mkEq(ctx.mkInt(instance[i][j]), ctx.mkInt(0)), ctx.mkTrue(), ctx.mkEq(X[i][j], ctx.mkInt(instance[i][j])))); | ||
84 | } | ||
85 | } | ||
86 | |||
87 | Solver s = ctx.mkSolver(); | ||
88 | s.add(sudoku); | ||
89 | s.add(inst); | ||
90 | |||
91 | if (s.check() == Status.SATISFIABLE) { | ||
92 | Model m = s.getModel(); | ||
93 | Expr[][] solution = new Expr[9][9]; | ||
94 | for (int i = 0; i < 9; i++) { | ||
95 | for (int j = 0; j < 9; j++) { | ||
96 | solution[i][j] = m.evaluate(X[i][j], false); | ||
97 | } | ||
98 | } | ||
99 | |||
100 | System.out.println("Sudoku solution:\n"); | ||
101 | for (int i = 0; i < 9; i++) { | ||
102 | for (int j = 0; j < 9; j++) { | ||
103 | System.out.print(solution[i][j] + " "); | ||
104 | } | ||
105 | System.out.println(); | ||
106 | } | ||
107 | } | ||
108 | else { | ||
109 | System.out.println("No solution"); | ||
110 | } | ||
111 | } | ||
112 | |||
113 | public static void main (String []args) { | ||
114 | HashMap<String, String> cfg = new HashMap<String, String>(); | ||
115 | cfg.put("model", "true"); | ||
116 | Context ctx = new Context(cfg); | ||
117 | sudoku(ctx); | ||
118 | } | ||
119 | |||
120 | } \ No newline at end of file | ||