mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-24 14:41:28 +00:00
Code Activity

fix C++ example and add polymorphic interface for C++

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-29 03:08:49 -07:00
parent 6efffa0054
commit c88295a7c7
3 changed files with 30 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -327,6 +327,15 @@ namespace z3 {
*/
sort datatype(symbol const& name, constructors const& cs);
/**
\brief Create a parametric recursive datatype.
\c name is the name of the recursive datatype
\c params - the sort parameters of the datatype
\c cs - the \c n constructors used to define the datatype
References to the datatype and mutually recursive datatypes can be created using \ref datatype_sort.
*/
sort datatype(symbol const &name, sort_vector const &params, constructors const &cs);
/**
\brief Create a set of mutually recursive datatypes.
\c n - number of recursive datatypes
@ -3616,6 +3625,16 @@ namespace z3 {
return sort(*this, s);
}
inline sort context::datatype(symbol const &name, sort_vector const& params, constructors const &cs) {
array<Z3_sort> _params(params);
array<Z3_constructor> _cs(cs.size());
for (unsigned i = 0; i < cs.size(); ++i)
_cs[i] = cs[i];
Z3_sort s = Z3_mk_polymorphic_datatype(*this, name, _params.size(), _params.ptr(), cs.size(), _cs.ptr());
check_error();
return sort(*this, s);
}
inline sort_vector context::datatypes(
unsigned n, symbol const* names,
constructor_list *const* cons) {