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

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
ctx = None )

Definition at line 9359 of file z3py.py.

9359 def __init__(self, ctx= None):
9360 self.ctx = _get_ctx(ctx)
9361 self.pctx = Z3_mk_parser_context(self.ctx.ref())
9362 Z3_parser_context_inc_ref(self.ctx.ref(), self.pctx)
9363
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 9364 of file z3py.py.

9364 def __del__(self):
9365 if self.ctx.ref() is not None and self.pctx is not None and Z3_parser_context_dec_ref is not None:
9366 Z3_parser_context_dec_ref(self.ctx.ref(), self.pctx)
9367 self.pctx = None
9368
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 9372 of file z3py.py.

9372 def add_decl(self, decl):
9373 Z3_parser_context_add_decl(self.ctx.ref(), self.pctx, decl.as_ast())
9374
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 9369 of file z3py.py.

9369 def add_sort(self, sort):
9370 Z3_parser_context_add_sort(self.ctx.ref(), self.pctx, sort.as_ast())
9371
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 9375 of file z3py.py.

9375 def from_string(self, s):
9376 return AstVector(Z3_parser_context_from_string(self.ctx.ref(), self.pctx, s), self.ctx)
9377
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 9360 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ pctx

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

Definition at line 9361 of file z3py.py.