mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 14:43:23 +00:00
Code Activity

Pull out the solver.

Browse source
This commit is contained in:
Ben Laurie 2015-04-05 17:57:21 +01:00
parent e8b8393c31
commit 0f467eb599
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -989,8 +989,9 @@ void sudoku_example() {
x.push_back(c.int_const(x_name.str().c_str())); x.push_back(c.int_const(x_name.str().c_str()));
} }
// each cell contains a value in {1, ..., 9}
solver s(c); solver s(c);
// each cell contains a value in {1, ..., 9}
for (unsigned i = 0; i < 9; ++i) for (unsigned i = 0; i < 9; ++i)
for (unsigned j = 0; j < 9; ++j) { for (unsigned j = 0; j < 9; ++j) {
s.add(x[i * 9 + j] >= 1 && x[i * 9 + j] <= 9); s.add(x[i * 9 + j] >= 1 && x[i * 9 + j] <= 9);