Skip to content

Commit 7b1ead0

Browse files
Yoni Zoharyoni206
authored andcommitted
merging
1 parent dd79405 commit 7b1ead0

1 file changed

Lines changed: 4 additions & 13 deletions

File tree

src/api/python/cvc5.pxi

Lines changed: 4 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -880,16 +880,7 @@ cdef class DatatypeSelector:
880880
# ----------------------------------------------------------------------------
881881

882882
cdef class Op:
883-
"""
884-
A cvc5 operator.
885-
886-
An operator is a term that represents certain operators,
887-
instantiated with its required parameters, e.g.,
888-
a term of kind
889-
:py:obj:`BITVECTOR_EXTRACT <Kind.BITVECTOR_EXTRACT>`.
890-
891-
Wrapper class for :cpp:class:`cvc5::Op`.
892-
"""
883+
"""Wrapper class for :cpp:class:`cvc5::api::Op`."""
893884
cdef c_Op cop
894885
cdef TermManager tm
895886

@@ -910,10 +901,10 @@ cdef class Op:
910901

911902
def getKind(self):
912903
"""
913-
:return: The kind of this operator.
904+
:return: the kind of this operator.
914905
"""
915-
return Kind(<int> self.cop.getKind())
916-
906+
return kind(<int> self.cop.getKind())
907+
917908
def isIndexed(self):
918909
"""
919910
:return: True iff this operator is indexed.

0 commit comments

Comments
 (0)