Z3
Public Member Functions | Data Fields
ParserContext Class Reference

Public Member Functions

def __init__
 
def __del__ (self)
 
def add_sort (self, sort)
 
def add_decl (self, decl)
 
def from_string (self, s)
 

Data Fields

 ctx
 
 pctx
 

Detailed Description

Definition at line 9273 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  ctx = None 
)

Definition at line 9274 of file z3py.py.

9274  def __init__(self, ctx= None):
9275  self.ctx = _get_ctx(ctx)
9276  self.pctx = Z3_mk_parser_context(self.ctx.ref())
9277  Z3_parser_context_inc_ref(self.ctx.ref(), self.pctx)
9278 
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.
def __del__ (   self)

Definition at line 9279 of file z3py.py.

9279  def __del__(self):
9280  if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None:
9281  Z3_parser_context_dec_ref(self.ctx.ref(), self.pctx)
9282  self.pctx = None
9283 
def __del__(self)
Definition: z3py.py:9279
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

def add_decl (   self,
  decl 
)

Definition at line 9287 of file z3py.py.

9287  def add_decl(self, decl):
9288  Z3_parser_context_add_decl(self.ctx.ref(), self.pctx, decl.as_ast())
9289 
def add_decl(self, decl)
Definition: z3py.py:9287
void Z3_API Z3_parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f)
Add a function declaration.
def add_sort (   self,
  sort 
)

Definition at line 9284 of file z3py.py.

9284  def add_sort(self, sort):
9285  Z3_parser_context_add_sort(self.ctx.ref(), self.pctx, sort.as_ast())
9286 
def add_sort(self, sort)
Definition: z3py.py:9284
void Z3_API Z3_parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s)
Add a sort declaration.
def from_string (   self,
  s 
)

Definition at line 9290 of file z3py.py.

9290  def from_string(self, s):
9291  return AstVector(Z3_parser_context_from_string(self.ctx.ref(), self.pctx, s), self.ctx)
9292 
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.
def from_string(self, s)
Definition: z3py.py:9290

Field Documentation

ctx

Definition at line 9275 of file z3py.py.

Referenced by ParserContext.from_string().

pctx