mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 05:49:13 +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 67dcb8bcc1
commit bc28de931b
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)

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) {

7
src/ast/euf/ho_matcher.h
View file

@ -100,14 +100,14 @@ namespace euf {
class match_goals {
protected:
ast_manager &m;
ho_matcher& ho;
ast_manager &m;
match_goal* m_expensive = nullptr, *m_cheap = nullptr;
match_goal* pop(match_goal*& q);
public:
match_goals(ho_matcher& em, ast_manager &m) : m(m), ho(em) {}
match_goals(ho_matcher& em, ast_manager& m) : ho(em), m(m) {}
bool empty() const { return m_cheap == nullptr && m_expensive == nullptr; }
void reset() { m_cheap = m_expensive = nullptr; }
void push(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t);
@ -158,7 +158,6 @@ namespace euf {
};
class unitary_patterns {
ast_manager& m;
array_util a;
vector<expr_ref_vector> m_patterns;
vector<svector<lbool>> m_is_unitary;
@ -181,7 +180,7 @@ namespace euf {
}
public:
unitary_patterns(ast_manager& m) : m(m), a(m) {}
unitary_patterns(ast_manager& m) : a(m) {}
bool is_unitary(unsigned offset, expr* p) const {
return find(offset, p) == l_true;