mirror of
https://github.com/Z3Prover/z3
synced 2025-08-17 00:32:16 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
9879d8aa62
1 changed files with 9 additions and 3 deletions
|
@ -485,7 +485,13 @@ namespace test_mapi
|
||||||
// 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 (uint j = 0; j < 9; j++)
|
for (uint j = 0; j < 9; j++)
|
||||||
cols_c[j] = ctx.MkDistinct(X[j]);
|
{
|
||||||
|
IntExpr[] column = new IntExpr[9];
|
||||||
|
for (uint i = 0; i < 9; i++)
|
||||||
|
column[i] = X[i][j];
|
||||||
|
|
||||||
|
cols_c[j] = ctx.MkDistinct(column);
|
||||||
|
}
|
||||||
|
|
||||||
// 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][];
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue