mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 23:35:46 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2013-05-07 17:58:53 +01:00
commit 2751d97027
1 changed files with 23 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -906,6 +906,28 @@ void enum_sort_example() {
std::cout << "2: " << result_goal.as_expr() << std::endl;
}
void expr_vector_example() {
context c;
const unsigned N = 10;
expr_vector x(c);
for (unsigned i = 0; i < N; i++) {
std::stringstream x_name;
x_name << "x_" << i;
x.push_back(c.int_const(x_name.str().c_str()));
}
solver s(c);
for (unsigned i = 0; i < N; i++) {
s.add(x[i] >= 1);
}
std::cout << s << "\n" << "solving...\n" << s.check() << "\n";
model m = s.get_model();
std::cout << "solution\n" << m;
}
int main() {
try {
demorgan(); std::cout << "\n";
@ -941,6 +963,7 @@ int main() {
incremental_example2(); std::cout << "\n";
incremental_example3(); std::cout << "\n";
enum_sort_example(); std::cout << "\n";
expr_vector_example(); std::cout << "\n";
std::cout << "done\n";
}
catch (exception & ex) {