diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-13 23:31:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-13 23:31:13 -0600 |
| commit | 08289dd911aff28110baf0fd815fd912f8b76fd3 (patch) | |
| tree | 74cb9775532373b6f24e54bfaf471dc1ef0bae24 /src/expr | |
| parent | d84d67018234bb6bb24dd9183a888892c3bfd4d7 (diff) | |
Update sygus v1 parser to use ParseOp utility (#3756)
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/datatype.cpp | 13 | ||||
| -rw-r--r-- | src/expr/datatype.h | 8 | ||||
| -rw-r--r-- | src/expr/datatype.i | 2 |
3 files changed, 22 insertions, 1 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 7e5fb6d7d..4d2467f84 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -252,7 +252,18 @@ void Datatype::addSygusConstructor(Expr op, } addConstructor(c); } - + +void Datatype::addSygusConstructor(Kind k, + const std::string& cname, + const std::vector<Type>& cargs, + std::shared_ptr<SygusPrintCallback> spc, + int weight) +{ + ExprManagerScope ems(*d_em); + Expr op = d_em->operatorOf(k); + addSygusConstructor(op, cname, cargs, spc, weight); +} + void Datatype::setTuple() { PrettyCheckArgument( !isResolved(), this, "cannot set tuple to a finalized Datatype"); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index dccda5ad4..1ae59f00c 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -630,6 +630,14 @@ class CVC4_PUBLIC Datatype { const std::vector<Type>& cargs, std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); + /** + * Same as above, with builtin kind k. + */ + void addSygusConstructor(Kind k, + const std::string& cname, + const std::vector<Type>& cargs, + std::shared_ptr<SygusPrintCallback> spc = nullptr, + int weight = -1); /** set that this datatype is a tuple */ void setTuple(); diff --git a/src/expr/datatype.i b/src/expr/datatype.i index 6bd5eb82c..83e21793c 100644 --- a/src/expr/datatype.i +++ b/src/expr/datatype.i @@ -9,6 +9,8 @@ #endif /* SWIGJAVA */ %} +%include "expr/kind.i" + %extend std::vector< CVC4::Datatype > { /* These member functions have slightly different signatures in * different swig language packages. The underlying issue is that |