diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-07-31 23:50:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-31 23:50:40 -0700 |
| commit | 0c78ef9adbddbc7ed875c3c3a41f60e48abdd17f (patch) | |
| tree | 14bb779d85d59a8c49b8187b07840cdfcf94ea32 /src/api/cvc4cpp.h | |
| parent | 0f040cbc2b068d3f22f6d46ec35aff3ab720ec28 (diff) | |
Add SyGuS Python API (#4812)
This commit extends the Python API with support for SyGuS functionality.
This required the addition of a nullary constructor for `Grammar` in the C++ API.
A unit test is also included, and is a translation of the corresponding C++ API unit test.
Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter).
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 997616ae3..edd74280a 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1954,6 +1954,11 @@ class CVC4_PUBLIC Grammar */ void addRules(Term ntSymbol, std::vector<Term> rules); + /** + * Nullary constructor. Needed for the Cython API. + */ + Grammar(); + private: /** * Constructor. |