mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

make parameters accessible from expressions. Issue #896

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-12 09:56:49 -08:00
parent b3dabc7ccf
commit 6fcba26ea6
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/python/z3/z3.py
View file

@ -868,6 +868,9 @@ class ExprRef(AstRef):
_args, sz = _to_ast_array((a, b)) _args, sz = _to_ast_array((a, b))
return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx) return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
def params(self):
return self.decl().params()
def decl(self): def decl(self):
"""Return the Z3 function declaration associated with a Z3 application. """Return the Z3 function declaration associated with a Z3 application.