From edb2f8554d7418b8a202db374d810a66a18774eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 May 2013 17:45:56 -0700 Subject: [PATCH] Add new example Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 55dbebe27..77f7702f2 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -952,6 +952,26 @@ void exists_expr_vector_example() { 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() { try { demorgan(); std::cout << "\n"; @@ -983,12 +1003,13 @@ int main() { tactic_example9(); std::cout << "\n"; tactic_qe(); std::cout << "\n"; tst_visit(); std::cout << "\n"; - incremental_example1(); std::cout << "\n"; - incremental_example2(); std::cout << "\n"; - incremental_example3(); std::cout << "\n"; + incremental_example1(); std::cout << "\n"; + incremental_example2(); std::cout << "\n"; + incremental_example3(); std::cout << "\n"; enum_sort_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n"; + substitute_example(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) {