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

Add expr_vector example

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-05-07 08:10:43 -07:00
parent a7269f56f9
commit 157b5f0d9c
1 changed files with 23 additions and 0 deletions
Show stats 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; 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() { int main() {
try { try {
demorgan(); std::cout << "\n"; demorgan(); std::cout << "\n";
@ -941,6 +963,7 @@ int main() {
incremental_example2(); std::cout << "\n"; incremental_example2(); std::cout << "\n";
incremental_example3(); std::cout << "\n"; incremental_example3(); std::cout << "\n";
enum_sort_example(); std::cout << "\n"; enum_sort_example(); std::cout << "\n";
expr_vector_example(); std::cout << "\n";
std::cout << "done\n"; std::cout << "done\n";
} }
catch (exception & ex) { catch (exception & ex) {