Definition at line 9451 of file z3py.py.
◆ __init__()
__init__ |
( |
| self, |
|
|
| ctx = None ) |
Definition at line 9452 of file z3py.py.
9452 def __init__(self, ctx= None):
9453 self.ctx = _get_ctx(ctx)
9456
void Z3_API Z3_parser_context_inc_ref(Z3_context c, Z3_parser_context pc)
Increment the reference counter of the given Z3_parser_context object.
Z3_parser_context Z3_API Z3_mk_parser_context(Z3_context c)
Create a parser context.
◆ __del__()
Definition at line 9457 of file z3py.py.
9457 def __del__(self):
9458 if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None:
9460 self.pctx = None
9461
void Z3_API Z3_parser_context_dec_ref(Z3_context c, Z3_parser_context pc)
Decrement the reference counter of the given Z3_parser_context object.
◆ add_decl()
Definition at line 9465 of file z3py.py.
9465 def add_decl(self, decl):
9467
void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f)
Add a function declaration.
◆ add_sort()
Definition at line 9462 of file z3py.py.
9462 def add_sort(self, sort):
9464
void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s)
Add a sort declaration.
◆ from_string()
Definition at line 9468 of file z3py.py.
9468 def from_string(self, s):
9470
Z3_ast_vector Z3_API Z3_parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s)
Parse a string of SMTLIB2 commands. Return assertions.
◆ ctx
◆ pctx