aboutsummaryrefslogtreecommitdiffstats
path: root/Framework
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-05-06 16:13:02 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-05-06 16:13:02 -0400
commit23358f567ac0fa37868c7d85a0b715c24c788b63 (patch)
tree863d760cfdbc040011e5f1a67eb722975094e938 /Framework
parentPS language update (diff)
downloadVIATRA-Generator-23358f567ac0fa37868c7d85a0b715c24c788b63.tar.gz
VIATRA-Generator-23358f567ac0fa37868c7d85a0b715c24c788b63.tar.zst
VIATRA-Generator-23358f567ac0fa37868c7d85a0b715c24c788b63.zip
Adjust classpath for Z3 in viatra2logic
Diffstat (limited to 'Framework')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath2
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExampleRecreation.java120
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 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic;
2
3import java.util.HashMap;
4
5import com.microsoft.z3.*;
6
7public 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.1) at 2024-06-02 21:47:00 +0000