mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Fix sudoku Java example

Browse source
This commit is contained in:
Richard Bradley 2019-07-31 23:32:38 +01:00
parent a2b18a37ec
commit 04e0b767c3
1 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
examples/java/JavaExample.java
View file

@ -521,8 +521,13 @@ class JavaExample
// each column contains a digit at most once // each column contains a digit at most once
BoolExpr[] cols_c = new BoolExpr[9]; BoolExpr[] cols_c = new BoolExpr[9];
for (int j = 0; j < 9; j++) for (int j = 0; j < 9; j++) {
cols_c[j] = ctx.mkDistinct(X[j]); IntExpr[] col = new IntExpr[9];
for (int i = 0; i < 9; i++) {
col[i] = X[i][j];
}
cols_c[j] = ctx.mkDistinct(col);
}
// each 3x3 square contains a digit at most once // each 3x3 square contains a digit at most once
BoolExpr[][] sq_c = new BoolExpr[3][]; BoolExpr[][] sq_c = new BoolExpr[3][];
@ -557,12 +562,10 @@ class JavaExample
BoolExpr instance_c = ctx.mkTrue(); BoolExpr instance_c = ctx.mkTrue();
for (int i = 0; i < 9; i++) for (int i = 0; i < 9; i++)
for (int j = 0; j < 9; j++) for (int j = 0; j < 9; j++)
if (0 != instance[i][j])
instance_c = ctx.mkAnd( instance_c = ctx.mkAnd(
instance_c, instance_c,
(BoolExpr) ctx.mkITE( ctx.mkEq(X[i][j], ctx.mkInt(instance[i][j])));
ctx.mkEq(ctx.mkInt(instance[i][j]),
ctx.mkInt(0)), ctx.mkTrue(),
ctx.mkEq(X[i][j], ctx.mkInt(instance[i][j]))));
Solver s = ctx.mkSolver(); Solver s = ctx.mkSolver();
s.add(sudoku_c); s.add(sudoku_c);