MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / __abs__

Method __abs__

lean_py/z3/core.py:499–510  ·  view source on GitHub ↗
(self)

Source from the content-addressed store, hash-verified

497 return self
498
499 def __abs__(self) -> ArithRef:
500 zero = _coerce_arith(0, self._sort)
501 cond = BoolRef(
502 BinOpNode(BinOp.GE, self._ast, zero._ast),
503 self._vars,
504 )
505 neg = ArithRef(UnOpNode(UnOp.NEG, self._ast), self._sort, self._vars) # type: ignore[arg-type]
506 return ArithRef(
507 IteNode(cond._ast, self._ast, neg._ast),
508 self._sort, # type: ignore[arg-type]
509 self._vars,
510 )
511
512 def is_int(self) -> bool:
513 return isinstance(self._sort._ast_sort, IntASTSort)

Callers

nothing calls this directly

Calls 6

BinOpNodeClass · 0.90
UnOpNodeClass · 0.90
IteNodeClass · 0.90
_coerce_arithFunction · 0.85
BoolRefClass · 0.85
ArithRefClass · 0.85

Tested by

no test coverage detected