mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 01:46:15 +00:00
Code Activity

add shorthands for creating uninterpreted sorts to context API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-27 09:30:37 -07:00
parent e483efd3f4
commit 562ed61a24
1 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -203,7 +203,12 @@ 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 create an uninterpreted sort with the name given by the string or symbol.
*/
sort uninterpreted_sort(char const* name);
sort uninterpreted_sort(symbol const& name);
func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range); 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, unsigned arity, sort const * domain, sort const & range);
func_decl function(symbol const& name, sort_vector const& domain, sort const& range); func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
@ -1637,6 +1642,13 @@ 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 sort context::uninterpreted_sort(char const* name) {
Z3_symbol _name = Z3_mk_string_symbol(*this, name);
return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
}
inline sort context::uninterpreted_sort(symbol const& name) {
return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
}
inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) { inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
array<Z3_sort> args(arity); array<Z3_sort> args(arity);