mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Merge pull request #8722 from Toby-Shi-cloud/master

Browse source 
Add `parser_context` in C++ API
This commit is contained in:
Nikolaj Bjorner 2026-02-21 16:26:00 -08:00 • committed by GitHub
commit 919cd5c86c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 38 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -868,6 +868,44 @@ namespace z3 {
};
class parser_context : public object {
Z3_parser_context m_pc;
public:
explicit parser_context(context & c):object(c), m_pc(Z3_mk_parser_context(c)) { Z3_parser_context_inc_ref(ctx(), m_pc); }
~parser_context() override { if (m_pc) Z3_parser_context_dec_ref(ctx(), m_pc); }
explicit operator bool() const { return m_pc; }
operator Z3_parser_context() const { return m_pc; }
parser_context(const parser_context &o):object(o), m_pc(o.m_pc) { Z3_parser_context_inc_ref(ctx(), m_pc); }
parser_context &operator=(const parser_context &o) {
if (this != &o) {
if (m_pc) Z3_parser_context_dec_ref(*m_ctx, m_pc);
Z3_parser_context_inc_ref(*o.m_ctx, o.m_pc);
object::operator=(o);
m_pc = o.m_pc;
}
return *this;
}
/**
\brief Add a sort declaration.
*/
void add_sort(const sort & s) { Z3_parser_context_add_sort(ctx(), m_pc, s); check_error(); }
/**
\brief Add a function declaration.
*/
void add_sort(const func_decl & f) { Z3_parser_context_add_decl(ctx(), m_pc, f); check_error(); }
/**
\brief Parse a string of SMTLIB2 commands. Return assertions.
*/
expr_vector parse_string(const char * s) {
auto result = Z3_parser_context_from_string(ctx(), m_pc, s);
m_ctx->check_error();
return expr_vector(ctx(), result);
}
};
/**
\brief forward declarations
*/