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

add concat to z3++, codeplex request

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-08 21:29:48 -07:00
parent 901d8a9f5b
commit 4a9d97bd02
2 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -205,6 +205,9 @@ void bitvector_example1() {
// using unsigned <= // using unsigned <=
prove(ule(x - 10, 0) == ule(x, 10)); 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));
} }
/** /**

7
src/api/c++/z3++.h
View file

@ -655,6 +655,7 @@ namespace z3 {
friend expr ite(expr const & c, expr const & t, expr const & e); friend expr ite(expr const & c, expr const & t, expr const & e);
friend expr distinct(expr_vector const& args); 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) { friend expr operator==(expr const & a, expr const & b) {
check_context(a, b); check_context(a, b);
@ -1109,6 +1110,12 @@ namespace z3 {
return expr(ctx, r); 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 { class func_entry : public object {
Z3_func_entry m_entry; Z3_func_entry m_entry;
void init(Z3_func_entry e) { void init(Z3_func_entry e) {