mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32: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 aa74dc6679
commit 47190ae7e5
3 changed files with 30 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1024,14 +1024,17 @@ void polymorphic_datatype_example() {
symbol is_pair_name = ctx.str_symbol("is-pair");
symbol first_name = ctx.str_symbol("first");
symbol second_name = ctx.str_symbol("second");
symbol field_names[2] = {first_name, second_name};
sort field_sorts[2] = {alpha, beta}; // Use type variables
sort _field_sorts[2] = {alpha, beta};
sort_vector field_sorts(ctx);
field_sorts.push_back(alpha); // Use type variables
field_sorts.push_back(beta); // Use type variables
constructors cs(ctx);
cs.add(mk_pair_name, is_pair_name, 2, field_names, field_sorts);
sort pair = ctx.datatype(pair_name, cs);
cs.add(mk_pair_name, is_pair_name, 2, field_names, _field_sorts);
sort pair = ctx.datatype(pair_name, field_sorts, cs);
std::cout << "Created parametric datatype: " << pair << "\n";
// Instantiate Pair with concrete types: (Pair Int Real)