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

add tuple shortcut and example to C++ API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-03 12:40:18 -07:00
parent 21a3b9c8e2
commit 5ba939ad5e
2 changed files with 33 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -920,6 +920,16 @@ void enum_sort_example() {
std::cout << "2: " << result_goal.as_expr() << std::endl; std::cout << "2: " << result_goal.as_expr() << std::endl;
} }
void tuple_example() {
std::cout << "tuple example\n";
context ctx;
const char * names[] = { "first", "second" };
sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() };
func_decl_vector projs(ctx);
func_decl pair = ctx.tuple_sort("pair", 2, names, sorts, projs);
std::cout << pair << "\n";
}
void expr_vector_example() { void expr_vector_example() {
std::cout << "expr_vector example\n"; std::cout << "expr_vector example\n";
context c; context c;
@ -1179,6 +1189,7 @@ int main() {
incremental_example2(); std::cout << "\n"; incremental_example2(); std::cout << "\n";
incremental_example3(); std::cout << "\n"; incremental_example3(); std::cout << "\n";
enum_sort_example(); std::cout << "\n"; enum_sort_example(); std::cout << "\n";
tuple_example(); std::cout << "\n";
expr_vector_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n";
exists_expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n";
substitute_example(); std::cout << "\n"; substitute_example(); std::cout << "\n";

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

@ -267,6 +267,15 @@ namespace z3 {
and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. 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); sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
/**
\brief Return a tuple constructor.
\c name is the name of the returned constructor,
\c n are the number of arguments, \c names and \c sorts are their projected sorts.
\c projs is an output paramter. It contains the set of projection functions.
*/
func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
/** /**
\brief create an uninterpreted sort with the name given by the string or symbol. \brief create an uninterpreted sort with the name given by the string or symbol.
*/ */
@ -2432,6 +2441,19 @@ namespace z3 {
for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); } 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; return s;
} }
inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
array<Z3_symbol> _names(n);
array<Z3_sort> _sorts(n);
for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
array<Z3_func_decl> _projs(n);
Z3_symbol _name = Z3_mk_string_symbol(*this, name);
Z3_func_decl tuple;
sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
check_error();
for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
return func_decl(*this, tuple);
}
inline sort context::uninterpreted_sort(char const* name) { inline sort context::uninterpreted_sort(char const* name) {
Z3_symbol _name = Z3_mk_string_symbol(*this, name); Z3_symbol _name = Z3_mk_string_symbol(*this, name);
return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name)); return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));