diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2021-06-18 23:41:41 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-19 06:41:41 +0000 |
| commit | 5e6117cc183513bf676b36078e6507b31caa6ff0 (patch) | |
| tree | 9ddbf762fc03e325f70a542ad0fe0991a6cb3b9e /src/api/python/cvc5.pxd | |
| parent | 8f98fded91cb6b7a0099d10bd4c5155e9e9ef9b6 (diff) | |
Adding python API test part 5 (#6743)
This commit (follow #6553) adds more functions and unit tests for python API.
Subsequent PR will include additional missing functions and unit tests.
1. Adding getNullSort() and mkEmptyBag() functions.
2. Allowing mkOp() with a list of arguments (previously allowed at most 2).
3. Allowing mkString() with additional boolean argument useEscSequences.
4. Corresponding changes to the tests.
Diffstat (limited to 'src/api/python/cvc5.pxd')
| -rw-r--r-- | src/api/python/cvc5.pxd | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 9d980267d..623b2f943 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -153,6 +153,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Solver(Options*) except + Sort getBooleanSort() except + Sort getIntegerSort() except + + Sort getNullSort() except + Sort getRealSort() except + Sort getRegExpSort() except + Sort getRoundingModeSort() except + @@ -178,10 +179,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": 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 + Op mkOp(Kind kind, uint32_t arg) except + Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except + + Op mkOp(Kind kind, const vector[uint32_t]& args) except + # Sygus related functions Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except + Term mkSygusVar(Sort sort, const string& symbol) except + @@ -207,9 +208,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkRegexpEmpty() except + Term mkRegexpSigma() except + Term mkEmptySet(Sort s) except + + Term mkEmptyBag(Sort s) except + Term mkSepNil(Sort sort) except + Term mkString(const string& s) except + Term mkString(const wstring& s) except + + Term mkString(const string& s, bint useEscSequences) except + Term mkEmptySequence(Sort sort) except + Term mkUniverseSet(Sort sort) except + Term mkBitVector(uint32_t size) except + |