diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-11-10 13:10:16 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-10 21:10:16 +0000 |
| commit | 4877909b806329e5e0e14dcfc3c404b8e4f6c0af (patch) | |
| tree | 3dcc6162d289261328c8bf2e808f1e76fd4f8eae /src/api/cpp/cvc5.cpp | |
| parent | e57c53e8a3c518a00cf52f199d14fbec94bdaca8 (diff) | |
api: Add Solver::mkRegexpAll(). (#7614)
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index ae0ee2ceb..4dcfb466e 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5796,6 +5796,19 @@ Term Solver::mkReal(int64_t num, int64_t den) const CVC5_API_TRY_CATCH_END; } +Term Solver::mkRegexpAll() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + Node res = d_nodeMgr->mkNode( + cvc5::kind::REGEXP_STAR, + d_nodeMgr->mkNode(cvc5::kind::REGEXP_ALLCHAR, std::vector<cvc5::Node>())); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::mkRegexpNone() const { CVC5_API_TRY_CATCH_BEGIN; |