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 new example

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-05-27 17:45:56 -07:00
parent 09945dc2cb
commit edb2f8554d
1 changed files with 24 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -952,6 +952,26 @@ void exists_expr_vector_example() {
std::cout << ex << std::endl; std::cout << ex << std::endl;
} }
void substitute_example() {
std::cout << "substitute example\n";
context c;
expr x(c);
x = c.int_const("x");
expr f(c);
f = (x == 2) || (x == 1);
std::cout << f << std::endl;
expr two(c), three(c);
two = c.int_val(2);
three = c.int_val(3);
Z3_ast from[] = { two };
Z3_ast to[] = { three };
expr new_f(c);
new_f = to_expr(c, Z3_substitute(c, f, 1, from, to));
std::cout << new_f << std::endl;
}
int main() { int main() {
try { try {
demorgan(); std::cout << "\n"; demorgan(); std::cout << "\n";
@ -983,12 +1003,13 @@ int main() {
tactic_example9(); std::cout << "\n"; tactic_example9(); std::cout << "\n";
tactic_qe(); std::cout << "\n"; tactic_qe(); std::cout << "\n";
tst_visit(); std::cout << "\n"; tst_visit(); std::cout << "\n";
incremental_example1(); std::cout << "\n"; incremental_example1(); std::cout << "\n";
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"; 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";
std::cout << "done\n"; std::cout << "done\n";
} }
catch (exception & ex) { catch (exception & ex) {