Z3
Loading...
Searching...
No Matches
ParserContext Class Reference

Public Member Functions

 __init__ (self, ctx=None)
 __del__ (self)
 add_sort (self, sort)
 add_decl (self, decl)
 from_string (self, s)

Data Fields

 ctx = _get_ctx(ctx)
 pctx = Z3_mk_parser_context(self.ctx.ref())

Detailed Description

Definition at line 9460 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
ctx = None )

Definition at line 9461 of file z3py.py.

9461 def __init__(self, ctx= None):
9462 self.ctx = _get_ctx(ctx)
9463 self.pctx = Z3_mk_parser_context(self.ctx.ref())
9464 Z3_parser_context_inc_ref(self.ctx.ref(), self.pctx)
9465
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__()

__del__ ( self)

Definition at line 9466 of file z3py.py.

9466 def __del__(self):
9467 if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None:
9468 Z3_parser_context_dec_ref(self.ctx.ref(), self.pctx)
9469 self.pctx = None
9470
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.

Member Function Documentation

◆ add_decl()

add_decl ( self,
decl )

Definition at line 9474 of file z3py.py.

9474 def add_decl(self, decl):
9475 Z3_parser_context_add_decl(self.ctx.ref(), self.pctx, decl.as_ast())
9476
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()

add_sort ( self,
sort )

Definition at line 9471 of file z3py.py.

9471 def add_sort(self, sort):
9472 Z3_parser_context_add_sort(self.ctx.ref(), self.pctx, sort.as_ast())
9473
void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s)
Add a sort declaration.

◆ from_string()

from_string ( self,
s )

Definition at line 9477 of file z3py.py.

9477 def from_string(self, s):
9478 return AstVector(Z3_parser_context_from_string(self.ctx.ref(), self.pctx, s), self.ctx)
9479
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.

Field Documentation

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 9462 of file z3py.py.

◆ pctx

pctx = Z3_mk_parser_context(self.ctx.ref())

Definition at line 9463 of file z3py.py.