From c8c5f30b49405fe2ae9bcd74021f84258f91ed5d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 May 2013 21:30:31 -0700 Subject: [PATCH] Add new C++ APIs for creating forall/exists expressions. Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 25 +++++++++ src/api/c++/z3++.h | 106 +++++++++++++++++++++++---------------- 2 files changed, 88 insertions(+), 43 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index bec8c59a1..55dbebe27 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -907,6 +907,7 @@ void enum_sort_example() { } void expr_vector_example() { + std::cout << "expr_vector example\n"; context c; const unsigned N = 10; @@ -928,6 +929,29 @@ void expr_vector_example() { std::cout << "solution\n" << m; } +void exists_expr_vector_example() { + std::cout << "exists expr_vector example\n"; + context c; + const unsigned N = 10; + + expr_vector xs(c); + expr x(c); + expr b(c); + b = c.bool_val(true); + + for (unsigned i = 0; i < N; i++) { + std::stringstream x_name; + x_name << "x_" << i; + x = c.int_const(x_name.str().c_str()); + xs.push_back(x); + b = b && x >= 0; + } + + expr ex(c); + ex = exists(xs, b); + std::cout << ex << std::endl; +} + int main() { try { demorgan(); std::cout << "\n"; @@ -964,6 +988,7 @@ int main() { incremental_example3(); std::cout << "\n"; enum_sort_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n"; + exists_expr_vector_example(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a044149e3..a255c2d97 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -249,6 +249,8 @@ namespace z3 { array & operator=(array const & s); public: array(unsigned sz):m_size(sz) { m_array = new T[sz]; } + template + array(ast_vector_tpl const & v); ~array() { delete[] m_array; } unsigned size() const { return m_size; } T & operator[](int i) { assert(0 <= i); assert(static_cast(i) < m_size); return m_array[i]; } @@ -939,49 +941,6 @@ namespace z3 { inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); } inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); } - // Basic functions for creating quantified formulas. - // The C API should be used for creating quantifiers with patterns, weights, many variables, etc. - inline expr forall(expr const & x, expr const & b) { - check_context(x, b); - Z3_app vars[] = {(Z3_app) x}; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr forall(expr const & x1, expr const & x2, expr const & b) { - check_context(x1, b); check_context(x2, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; - Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x, expr const & b) { - check_context(x, b); - Z3_app vars[] = {(Z3_app) x}; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x1, expr const & x2, expr const & b) { - check_context(x1, b); check_context(x2, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { - check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); - Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; - Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); - } - template class cast_ast; template<> class cast_ast { @@ -1043,6 +1002,67 @@ namespace z3 { friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } }; + template + template + array::array(ast_vector_tpl const & v) { + m_array = new T[v.size()]; + m_size = v.size(); + for (unsigned i = 0; i < m_size; i++) { + m_array[i] = v[i]; + } + } + + // Basic functions for creating quantified formulas. + // The C API should be used for creating quantifiers with patterns, weights, many variables, etc. + inline expr forall(expr const & x, expr const & b) { + check_context(x, b); + Z3_app vars[] = {(Z3_app) x}; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & b) { + check_context(x1, b); check_context(x2, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr forall(expr_vector const & xs, expr const & b) { + array vars(xs); + Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x, expr const & b) { + check_context(x, b); + Z3_app vars[] = {(Z3_app) x}; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & b) { + check_context(x1, b); check_context(x2, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr const & x1, expr const & x2, expr const & x3, expr const & x4, expr const & b) { + check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); + Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + inline expr exists(expr_vector const & xs, expr const & b) { + array vars(xs); + Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); + } + class func_entry : public object { Z3_func_entry m_entry; void init(Z3_func_entry e) {