From b2810592e6bbd84c521b821a47fd0f33c75f4a96 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Feb 2013 08:29:01 -0800 Subject: [PATCH] Add enumeration_sort method to C++ API. Add as_expr method to goal class in C++ API. Add enum_sort_example to C++ examples/c++/example.cpp Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 24 ++++++++++++++++++++ src/api/c++/z3++.h | 48 +++++++++++++++++++++++++++++++++++----- 2 files changed, 66 insertions(+), 6 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 1f127e8e4..ab5d0132c 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -883,6 +883,29 @@ void incremental_example3() { std::cout << s.check(a2) << "\n"; } +void enum_sort_example() { + std::cout << "enumeration sort example\n"; + context ctx; + const char * enum_names[] = { "a", "b", "c" }; + func_decl_vector enum_consts(ctx); + func_decl_vector enum_testers(ctx); + sort s = ctx.enumeration_sort("enumT", 3, enum_names, enum_consts, enum_testers); + // enum_consts[0] is a func_decl of arity 0. + // we convert it to an expression using the operator() + expr a = enum_consts[0](); + expr b = enum_consts[1](); + expr x = ctx.constant("x", s); + expr test = (x==a) && (x==b); + std::cout << "1: " << test << std::endl; + tactic qe(ctx, "ctx-solver-simplify"); + goal g(ctx); + g.add(test); + expr res(ctx); + apply_result result_of_elimination = qe.apply(g); + goal result_goal = result_of_elimination[0]; + std::cout << "2: " << result_goal.as_expr() << std::endl; +} + int main() { try { demorgan(); std::cout << "\n"; @@ -917,6 +940,7 @@ int main() { incremental_example1(); std::cout << "\n"; incremental_example2(); std::cout << "\n"; incremental_example3(); std::cout << "\n"; + enum_sort_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 5af4bf60b..3382b8b00 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -63,6 +63,11 @@ namespace z3 { class statistics; class apply_result; class fixedpoint; + template class ast_vector_tpl; + typedef ast_vector_tpl ast_vector; + typedef ast_vector_tpl expr_vector; + typedef ast_vector_tpl sort_vector; + typedef ast_vector_tpl func_decl_vector; inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); } inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); } @@ -190,7 +195,13 @@ namespace z3 { Example: Given a context \c c, c.array_sort(c.int_sort(), c.bool_sort()) is an array sort from integer to Boolean. */ sort array_sort(sort d, sort r); - + /** + \brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. + \c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements, + and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. + */ + sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts); + func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, sort const & domain, sort const & range); @@ -414,6 +425,7 @@ namespace z3 { bool is_const() const { return arity() == 0; } + expr operator()() const; expr operator()(unsigned n, expr const * args) const; expr operator()(expr const & a) const; expr operator()(int a) const; @@ -1020,11 +1032,6 @@ 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; } }; - typedef ast_vector_tpl ast_vector; - typedef ast_vector_tpl expr_vector; - typedef ast_vector_tpl sort_vector; - typedef ast_vector_tpl func_decl_vector; - class func_entry : public object { Z3_func_entry m_entry; void init(Z3_func_entry e) { @@ -1261,6 +1268,19 @@ namespace z3 { unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); } bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; } bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; } + expr as_expr() const { + unsigned n = size(); + if (n == 0) + return ctx().bool_val(false); + else if (n == 1) + return operator[](0); + else { + array args(n); + for (unsigned i = 0; i < n; i++) + args[i] = operator[](i); + return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr())); + } + } friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; } }; @@ -1437,6 +1457,17 @@ namespace z3 { inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); } inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); } inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); } + inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) { + array _enum_names(n); + for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); } + array _cs(n); + array _ts(n); + Z3_symbol _name = Z3_mk_string_symbol(*this, name); + sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr())); + check_error(); + for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); } + return s; + } inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) { array args(arity); @@ -1538,6 +1569,11 @@ namespace z3 { return expr(ctx(), r); } + inline expr func_decl::operator()() const { + Z3_ast r = Z3_mk_app(ctx(), *this, 0, 0); + ctx().check_error(); + return expr(ctx(), r); + } inline expr func_decl::operator()(expr const & a) const { check_context(*this, a); Z3_ast args[1] = { a };