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 9519 of file z3py.py.

Constructor & Destructor Documentation

__init__()

__init__	(		self,
			ctx = None )

Definition at line 9520 of file z3py.py.

    def __init__(self, ctx= None):
        self.ctx = _get_ctx(ctx)
        self.pctx = Z3_mk_parser_context(self.ctx.ref())
        Z3_parser_context_inc_ref(self.ctx.ref(), self.pctx)
 

__del__()

__del__

(

self

)

Definition at line 9525 of file z3py.py.

    def __del__(self):
        if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None:
            Z3_parser_context_dec_ref(self.ctx.ref(), self.pctx)
            self.pctx = None
 

Member Function Documentation

add_decl()

add_decl	(		self,
			decl )

Definition at line 9533 of file z3py.py.

    def add_decl(self, decl):
        Z3_parser_context_add_decl(self.ctx.ref(), self.pctx, decl.as_ast())
 

add_sort()

add_sort	(		self,
			sort )

Definition at line 9530 of file z3py.py.

    def add_sort(self, sort):
        Z3_parser_context_add_sort(self.ctx.ref(), self.pctx, sort.as_ast())
 

from_string()

from_string	(		self,
			s )

Definition at line 9536 of file z3py.py.

    def from_string(self, s):
        return AstVector(Z3_parser_context_from_string(self.ctx.ref(), self.pctx, s), self.ctx)
 

Field Documentation

ctx

ctx = _get_ctx(ctx)

Definition at line 9521 of file z3py.py.

pctx

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

Definition at line 9522 of file z3py.py.