Skip to content

Commit e21f035

Browse files
daniel-larrazdaniel-larraz
committed
Formatting with black
1 parent f30316e commit e21f035

1 file changed

Lines changed: 25 additions & 75 deletions

File tree

‎cvc5_pythonic_api/cvc5_pythonic.py‎

Lines changed: 25 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -1832,9 +1832,7 @@ def __getitem__(self, i):
18321832
"""
18331833
if _is_int(i):
18341834
i = IntVal(i, self.ctx)
1835-
return _to_expr_ref(
1836-
self.ctx.tm.mkTerm(Kind.SEQ_NTH, self.ast, i.ast), self.ctx
1837-
)
1835+
return _to_expr_ref(self.ctx.tm.mkTerm(Kind.SEQ_NTH, self.ast, i.ast), self.ctx)
18381836

18391837
def at(self, i):
18401838
"""Return the sequence at index i
@@ -2257,9 +2255,7 @@ def IndexOf(s, substr, offset=None):
22572255
return ArithRef(
22582256
ctx.tm.mkTerm(Kind.STRING_INDEXOF, s.ast, substr.ast, offset.ast), ctx
22592257
)
2260-
return ArithRef(
2261-
ctx.tm.mkTerm(Kind.SEQ_INDEXOF, s.ast, substr.ast, offset.ast), ctx
2262-
)
2258+
return ArithRef(ctx.tm.mkTerm(Kind.SEQ_INDEXOF, s.ast, substr.ast, offset.ast), ctx)
22632259

22642260

22652261
def Replace(s, src, dst):
@@ -4145,9 +4141,7 @@ def __add__(self, other):
41454141
BitVec(32)
41464142
"""
41474143
a, b = _coerce_exprs(self, other)
4148-
return BitVecRef(
4149-
self.ctx.tm.mkTerm(Kind.BITVECTOR_ADD, a.ast, b.ast), self.ctx
4150-
)
4144+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_ADD, a.ast, b.ast), self.ctx)
41514145

41524146
def __radd__(self, other):
41534147
"""Create the SMT expression `other + self`.
@@ -4157,9 +4151,7 @@ def __radd__(self, other):
41574151
10 + x
41584152
"""
41594153
a, b = _coerce_exprs(self, other)
4160-
return BitVecRef(
4161-
self.ctx.tm.mkTerm(Kind.BITVECTOR_ADD, b.ast, a.ast), self.ctx
4162-
)
4154+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_ADD, b.ast, a.ast), self.ctx)
41634155

41644156
def __mul__(self, other):
41654157
"""Create the SMT expression `self * other`.
@@ -4199,9 +4191,7 @@ def __sub__(self, other):
41994191
BitVec(32)
42004192
"""
42014193
a, b = _coerce_exprs(self, other)
4202-
return BitVecRef(
4203-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SUB, a.ast, b.ast), self.ctx
4204-
)
4194+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SUB, a.ast, b.ast), self.ctx)
42054195

42064196
def __rsub__(self, other):
42074197
"""Create the SMT expression `other - self`.
@@ -4211,9 +4201,7 @@ def __rsub__(self, other):
42114201
10 - x
42124202
"""
42134203
a, b = _coerce_exprs(self, other)
4214-
return BitVecRef(
4215-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SUB, b.ast, a.ast), self.ctx
4216-
)
4204+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SUB, b.ast, a.ast), self.ctx)
42174205

42184206
def __or__(self, other):
42194207
"""Create the SMT expression bitwise-or `self | other`.
@@ -4226,9 +4214,7 @@ def __or__(self, other):
42264214
BitVec(32)
42274215
"""
42284216
a, b = _coerce_exprs(self, other)
4229-
return BitVecRef(
4230-
self.ctx.tm.mkTerm(Kind.BITVECTOR_OR, a.ast, b.ast), self.ctx
4231-
)
4217+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_OR, a.ast, b.ast), self.ctx)
42324218

42334219
def __ror__(self, other):
42344220
"""Create the SMT expression bitwise-or `other | self`.
@@ -4238,9 +4224,7 @@ def __ror__(self, other):
42384224
10 | x
42394225
"""
42404226
a, b = _coerce_exprs(self, other)
4241-
return BitVecRef(
4242-
self.ctx.tm.mkTerm(Kind.BITVECTOR_OR, b.ast, a.ast), self.ctx
4243-
)
4227+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_OR, b.ast, a.ast), self.ctx)
42444228

42454229
def __and__(self, other):
42464230
"""Create the SMT expression bitwise-and `self & other`.
@@ -4253,9 +4237,7 @@ def __and__(self, other):
42534237
BitVec(32)
42544238
"""
42554239
a, b = _coerce_exprs(self, other)
4256-
return BitVecRef(
4257-
self.ctx.tm.mkTerm(Kind.BITVECTOR_AND, a.ast, b.ast), self.ctx
4258-
)
4240+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_AND, a.ast, b.ast), self.ctx)
42594241

42604242
def __rand__(self, other):
42614243
"""Create the SMT expression bitwise-or `other & self`.
@@ -4265,9 +4247,7 @@ def __rand__(self, other):
42654247
10 & x
42664248
"""
42674249
a, b = _coerce_exprs(self, other)
4268-
return BitVecRef(
4269-
self.ctx.tm.mkTerm(Kind.BITVECTOR_AND, b.ast, a.ast), self.ctx
4270-
)
4250+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_AND, b.ast, a.ast), self.ctx)
42714251

42724252
def __xor__(self, other):
42734253
"""Create the SMT expression bitwise-xor `self ^ other`.
@@ -4280,9 +4260,7 @@ def __xor__(self, other):
42804260
BitVec(32)
42814261
"""
42824262
a, b = _coerce_exprs(self, other)
4283-
return BitVecRef(
4284-
self.ctx.tm.mkTerm(Kind.BITVECTOR_XOR, a.ast, b.ast), self.ctx
4285-
)
4263+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_XOR, a.ast, b.ast), self.ctx)
42864264

42874265
def __rxor__(self, other):
42884266
"""Create the SMT expression bitwise-xor `other ^ self`.
@@ -4292,9 +4270,7 @@ def __rxor__(self, other):
42924270
10 ^ x
42934271
"""
42944272
a, b = _coerce_exprs(self, other)
4295-
return BitVecRef(
4296-
self.ctx.tm.mkTerm(Kind.BITVECTOR_XOR, b.ast, a.ast), self.ctx
4297-
)
4273+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_XOR, b.ast, a.ast), self.ctx)
42984274

42994275
def __pos__(self):
43004276
"""Return `self`.
@@ -4431,9 +4407,7 @@ def __le__(self, other):
44314407
'(bvule x y)'
44324408
"""
44334409
a, b = _coerce_exprs(self, other)
4434-
return BoolRef(
4435-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SLE, a.ast, b.ast), self.ctx
4436-
)
4410+
return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SLE, a.ast, b.ast), self.ctx)
44374411

44384412
def __lt__(self, other):
44394413
"""Create the SMT expression (signed) `other < self`.
@@ -4449,9 +4423,7 @@ def __lt__(self, other):
44494423
'(bvult x y)'
44504424
"""
44514425
a, b = _coerce_exprs(self, other)
4452-
return BoolRef(
4453-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SLT, a.ast, b.ast), self.ctx
4454-
)
4426+
return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SLT, a.ast, b.ast), self.ctx)
44554427

44564428
def __gt__(self, other):
44574429
"""Create the SMT expression (signed) `other > self`.
@@ -4467,9 +4439,7 @@ def __gt__(self, other):
44674439
'(bvugt x y)'
44684440
"""
44694441
a, b = _coerce_exprs(self, other)
4470-
return BoolRef(
4471-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SGT, a.ast, b.ast), self.ctx
4472-
)
4442+
return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SGT, a.ast, b.ast), self.ctx)
44734443

44744444
def __ge__(self, other):
44754445
"""Create the SMT expression (signed) `other >= self`.
@@ -4485,9 +4455,7 @@ def __ge__(self, other):
44854455
'(bvuge x y)'
44864456
"""
44874457
a, b = _coerce_exprs(self, other)
4488-
return BoolRef(
4489-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SGE, a.ast, b.ast), self.ctx
4490-
)
4458+
return BoolRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SGE, a.ast, b.ast), self.ctx)
44914459

44924460
def __rshift__(self, other):
44934461
"""Create the SMT expression (arithmetical) right shift `self >> other`
@@ -4533,9 +4501,7 @@ def __lshift__(self, other):
45334501
4
45344502
"""
45354503
a, b = _coerce_exprs(self, other)
4536-
return BitVecRef(
4537-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SHL, a.ast, b.ast), self.ctx
4538-
)
4504+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SHL, a.ast, b.ast), self.ctx)
45394505

45404506
def __rrshift__(self, other):
45414507
"""Create the SMT expression (arithmetical) right shift `other` >> `self`.
@@ -4565,9 +4531,7 @@ def __rlshift__(self, other):
45654531
'(bvshl #b00000000000000000000000000001010 x)'
45664532
"""
45674533
a, b = _coerce_exprs(self, other)
4568-
return BitVecRef(
4569-
self.ctx.tm.mkTerm(Kind.BITVECTOR_SHL, b.ast, a.ast), self.ctx
4570-
)
4534+
return BitVecRef(self.ctx.tm.mkTerm(Kind.BITVECTOR_SHL, b.ast, a.ast), self.ctx)
45714535

45724536

45734537
class BitVecNumRef(BitVecRef):
@@ -4826,9 +4790,7 @@ def Extract(high, low, a):
48264790
)
48274791
_assert(is_bv(a), "Third argument must be an SMT bit-vector expression")
48284792
return BitVecRef(
4829-
a.ctx.tm.mkTerm(
4830-
a.ctx.tm.mkOp(Kind.BITVECTOR_EXTRACT, high, low), a.ast
4831-
),
4793+
a.ctx.tm.mkTerm(a.ctx.tm.mkOp(Kind.BITVECTOR_EXTRACT, high, low), a.ast),
48324794
a.ctx,
48334795
)
48344796

@@ -7327,9 +7289,7 @@ def RoundTowardPositive(ctx=None):
73277289
fpMul(RTP(), x, y)
73287290
"""
73297291
ctx = _get_ctx(ctx)
7330-
return FPRMRef(
7331-
ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_POSITIVE), ctx
7332-
)
7292+
return FPRMRef(ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_POSITIVE), ctx)
73337293

73347294

73357295
def RTP(ctx=None):
@@ -7358,9 +7318,7 @@ def RoundTowardNegative(ctx=None):
73587318
fpMul(RTN(), x, y)
73597319
"""
73607320
ctx = _get_ctx(ctx)
7361-
return FPRMRef(
7362-
ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_NEGATIVE), ctx
7363-
)
7321+
return FPRMRef(ctx.tm.mkRoundingMode(pc.RoundingMode.ROUND_TOWARD_NEGATIVE), ctx)
73647322

73657323

73667324
def RTN(ctx=None):
@@ -8259,9 +8217,7 @@ def fpFP(sgn, exp, sig, ctx=None):
82598217
_assert(sgn.sort().size() == 1, "sort mismatch")
82608218
ctx = _get_ctx(ctx)
82618219
_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
8262-
bv = BitVecRef(
8263-
ctx.tm.mkTerm(Kind.BITVECTOR_CONCAT, sgn.ast, exp.ast, sig.ast), ctx
8264-
)
8220+
bv = BitVecRef(ctx.tm.mkTerm(Kind.BITVECTOR_CONCAT, sgn.ast, exp.ast, sig.ast), ctx)
82658221
sort = FPSort(exp.size(), sig.size() + 1)
82668222
return fpBVToFP(bv, sort)
82678223

@@ -8344,9 +8300,7 @@ def fpFPToFP(rm, v, sort, ctx=None):
83448300
_assert(is_fp(v), "Second argument must be a SMT floating-point expression.")
83458301
_assert(is_fp_sort(sort), "Third argument must be a SMT floating-point sort.")
83468302
ctx = _get_ctx(ctx)
8347-
to_fp_op = ctx.tm.mkOp(
8348-
Kind.FLOATINGPOINT_TO_FP_FROM_FP, sort.ebits(), sort.sbits()
8349-
)
8303+
to_fp_op = ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_FP, sort.ebits(), sort.sbits())
83508304
return FPRef(ctx.tm.mkTerm(to_fp_op, rm.ast, v.ast), ctx)
83518305

83528306

@@ -8459,9 +8413,7 @@ def fpToSBV(rm, x, s, ctx=None):
84598413
_assert(is_bv_sort(s), "Third argument must be SMT bit-vector sort")
84608414
ctx = _get_ctx(ctx)
84618415
return BitVecRef(
8462-
ctx.tm.mkTerm(
8463-
ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_SBV, s.size()), rm.ast, x.ast
8464-
),
8416+
ctx.tm.mkTerm(ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_SBV, s.size()), rm.ast, x.ast),
84658417
ctx,
84668418
)
84678419

@@ -8489,9 +8441,7 @@ def fpToUBV(rm, x, s, ctx=None):
84898441
_assert(is_bv_sort(s), "Third argument must be SMT bit-vector sort")
84908442
ctx = _get_ctx(ctx)
84918443
return BitVecRef(
8492-
ctx.tm.mkTerm(
8493-
ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_UBV, s.size()), rm.ast, x.ast
8494-
),
8444+
ctx.tm.mkTerm(ctx.tm.mkOp(Kind.FLOATINGPOINT_TO_UBV, s.size()), rm.ast, x.ast),
84958445
ctx,
84968446
)
84978447

0 commit comments

Comments
 (0)