diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-02 16:26:34 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 16:26:34 -0500 |
| commit | 947b7a0211c92ec02e8df9ec97c1db4138300184 (patch) | |
| tree | b27158d83eb29e46befaa543a7d2018183dc0c3b /src/api/python/cvc5.pxd | |
| parent | 4732f17fb971f3843e47dc9bd942bf06bd40aaf0 (diff) | |
| parent | 87b204084e86b534571f16250ca4871150b2a783 (diff) | |
Merge branch 'master' into rm-bv-div-zero-const-refsrm-bv-div-zero-const-refs
Diffstat (limited to 'src/api/python/cvc5.pxd')
| -rw-r--r-- | src/api/python/cvc5.pxd | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index fdcbfa997..2ad8cef5c 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -176,6 +176,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort mkTupleSort(const vector[Sort]& sorts) except + Term mkTerm(Op op) except + Term mkTerm(Op op, const vector[Term]& children) except + + Term mkTuple(const vector[Sort]& sorts, const vector[Term]& terms) except + Op mkOp(Kind kind) except + Op mkOp(Kind kind, Kind k) except + Op mkOp(Kind kind, const string& arg) except + @@ -388,6 +389,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term operator*() except + const_iterator begin() except + const_iterator end() except + + + bint isConstArray() except + bint isBooleanValue() except + bint getBooleanValue() except + bint isStringValue() except + @@ -398,6 +401,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": string getRealValue() except + bint isBitVectorValue() except + string getBitVectorValue(uint32_t base) except + + bint isAbstractValue() except + + string getAbstractValue() except + bint isFloatingPointPosZero() except + bint isFloatingPointNegZero() except + bint isFloatingPointPosInf() except + @@ -406,7 +411,15 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isFloatingPointValue() except + tuple[uint32_t, uint32_t, Term] getFloatingPointValue() except + + bint isSetValue() except + + set[Term] getSetValue() except + + bint isSequenceValue() except + vector[Term] getSequenceValue() except + + bint isUninterpretedValue() except + + pair[Sort, int32_t] getUninterpretedValue() except + + bint isTupleValue() except + + vector[Term] getTupleValue() except + + cdef cppclass TermHashFunction: TermHashFunction() except + |