mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Add Sudoku example.

Browse source
This commit is contained in:
Ben Laurie 2015-04-05 17:44:26 +01:00
parent 29606b5179
commit e8b8393c31
1 changed files with 77 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

77
examples/c++/example.cpp
View file

@ -974,6 +974,82 @@ void substitute_example() {
std::cout << new_f << std::endl; std::cout << new_f << std::endl;
} }
void sudoku_example() {
std::cout << "sudoku example\n";
context c;
// 9x9 matrix of integer variables
expr_vector x(c);
for (unsigned i = 0; i < 9; ++i)
for (unsigned j = 0; j < 9; ++j) {
std::stringstream x_name;
x_name << "x_" << i << '_' << j;
x.push_back(c.int_const(x_name.str().c_str()));
}
// each cell contains a value in {1, ..., 9}
solver s(c);
for (unsigned i = 0; i < 9; ++i)
for (unsigned j = 0; j < 9; ++j) {
s.add(x[i * 9 + j] >= 1 && x[i * 9 + j] <= 9);
}
// each row contains a digit at most once
for (unsigned i = 0; i < 9; ++i) {
expr_vector t(c);
for (unsigned j = 0; j < 9; ++j)
t.push_back(x[i * 9 + j]);
s.add(distinct(t));
}
// each column contains a digit at most once
for (unsigned j = 0; j < 9; ++j) {
expr_vector t(c);
for (unsigned i = 0; i < 9; ++i)
t.push_back(x[i * 9 + j]);
s.add(distinct(t));
}
// each 3x3 square contains a digit at most once
for (unsigned i0 = 0; i0 < 3; i0++) {
for (uint j0 = 0; j0 < 3; j0++) {
expr_vector t(c);
for (unsigned i = 0; i < 3; i++)
for (unsigned j = 0; j < 3; j++)
t.push_back(x[(i0 * 3 + i) * 9 + j0 * 3 + j]);
s.add(distinct(t));
}
}
// sudoku instance, we use '0' for empty cells
int instance[9][9] = {{0,0,0,0,9,4,0,3,0},
{0,0,0,5,1,0,0,0,7},
{0,8,9,0,0,0,0,4,0},
{0,0,0,0,0,0,2,0,8},
{0,6,0,2,0,1,0,5,0},
{1,0,2,0,0,0,0,0,0},
{0,7,0,0,0,0,5,2,0},
{9,0,0,0,6,5,0,0,0},
{0,4,0,9,7,0,0,0,0}};
for (unsigned i = 0; i < 9; i++)
for (unsigned j = 0; j < 9; j++)
if (instance[i][j] != 0)
s.add(x[i * 9 + j] == instance[i][j]);
std::cout << s.check() << std::endl;
std::cout << s << std::endl;
model m = s.get_model();
for (unsigned i = 0; i < 9; ++i) {
for (unsigned j = 0; j < 9; ++j)
std::cout << m.eval(x[i * 9 + j]);
std::cout << '\n';
}
}
int main() { int main() {
try { try {
demorgan(); std::cout << "\n"; demorgan(); std::cout << "\n";
@ -1012,6 +1088,7 @@ int main() {
expr_vector_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n";
exists_expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n";
substitute_example(); std::cout << "\n"; substitute_example(); std::cout << "\n";
sudoku_example(); std::cout << "\n";
std::cout << "done\n"; std::cout << "done\n";
} }
catch (exception & ex) { catch (exception & ex) {