From 4a9d97bd02e1faba9dad80c8b725bb85b4901c59 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 May 2015 21:29:48 -0700 Subject: [PATCH] add concat to z3++, codeplex request Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 3 +++ src/api/c++/z3++.h | 7 +++++++ 2 files changed, 10 insertions(+) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 9f4f9431c..ce15bf37d 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -205,6 +205,9 @@ void bitvector_example1() { // using unsigned <= prove(ule(x - 10, 0) == ule(x, 10)); + + expr y = c.bv_const("y", 32); + prove(implies(concat(x, y) == concat(y, x), x == y)); } /** diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f43ba83e5..ca93d28d9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -655,6 +655,7 @@ namespace z3 { friend expr ite(expr const & c, expr const & t, expr const & e); friend expr distinct(expr_vector const& args); + friend expr concat(expr const& a, expr const& b); friend expr operator==(expr const & a, expr const & b) { check_context(a, b); @@ -1108,6 +1109,12 @@ namespace z3 { ctx.check_error(); return expr(ctx, r); } + + inline expr concat(expr const& a, expr const& b) { + Z3_ast r = Z3_mk_concat(ctx, (Z3_app) a, (Z3_app) b); + ctx.check_error(); + return expr(ctx, r); + } class func_entry : public object { Z3_func_entry m_entry;