mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

adding PB operators to Python API. remove tabs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-10-28 17:13:24 -07:00
parent 7f5495b134
commit 559f373588
2 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -7337,7 +7337,7 @@ def PbLe(args, k):
_args, sz = _to_ast_array(args)
_coeffs = (ctypes.c_int * len(coeffs))()
for i in range(len(coeffs)):
_coeffs[i] = coeffs[i]
_coeffs[i] = coeffs[i]
return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)

28
src/api/python/z3printer.py
View file

@ -843,16 +843,16 @@ class Formatter:
return seq1(self.pp_name(a), [ self.pp_sort(a.domain()), self.pp_expr(a.arg(0), d+1, xs) ])
def pp_atmost(self, a, d, f, xs):
k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
return seq1(self.pp_name(a), [seq3([ self.pp_expr(ch, d+1, xs) for ch in a.children()]), to_format(k)])
k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
return seq1(self.pp_name(a), [seq3([ self.pp_expr(ch, d+1, xs) for ch in a.children()]), to_format(k)])
def pp_pbcmp(self, a, d, f, xs):
chs = a.children()
rchs = range(len(chs))
k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
ks = [Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, i+1) for i in rchs]
ls = [ seq3([self.pp_expr(chs[i], d+1,xs), to_format(ks[i])]) for i in rchs]
return seq1(self.pp_name(a), [seq3(ls), to_format(k)])
chs = a.children()
rchs = range(len(chs))
k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
ks = [Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, i+1) for i in rchs]
ls = [ seq3([self.pp_expr(chs[i], d+1,xs), to_format(ks[i])]) for i in rchs]
return seq1(self.pp_name(a), [seq3(ls), to_format(k)])
def pp_app(self, a, d, xs):
@ -889,12 +889,12 @@ class Formatter:
return self.pp_map(a, d, xs)
elif k == Z3_OP_CONST_ARRAY:
return self.pp_K(a, d, xs)
elif k == Z3_OP_PB_AT_MOST:
return self.pp_atmost(a, d, f, xs)
elif k == Z3_OP_PB_LE:
return self.pp_pbcmp(a, d, f, xs)
elif k == Z3_OP_PB_GE:
return self.pp_pbcmp(a, d, f, xs)
elif k == Z3_OP_PB_AT_MOST:
return self.pp_atmost(a, d, f, xs)
elif k == Z3_OP_PB_LE:
return self.pp_pbcmp(a, d, f, xs)
elif k == Z3_OP_PB_GE:
return self.pp_pbcmp(a, d, f, xs)
elif z3.is_pattern(a):
return self.pp_pattern(a, d, xs)
elif self.is_infix(k):