diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-27 18:05:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-27 16:05:07 -0700 |
commit | 4df14f1e09549be607123c66b7dd206e8e244c89 (patch) | |
tree | 3104897629ebe9efe4d14983ad89fb0d8778d4f2 /src/expr/expr.i | |
parent | 449cf281987eb8a2d43a572817db5c870a010c08 (diff) |
Add the Expr-level sequence datatype (#4526)
This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.
Diffstat (limited to 'src/expr/expr.i')
-rw-r--r-- | src/expr/expr.i | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/expr/expr.i b/src/expr/expr.i index 14ccf213c..14228d7c5 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -146,6 +146,7 @@ namespace CVC4 { %template(getConstBoolean) CVC4::Expr::getConst<bool>; %template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>; %template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>; +%template(getConstExprSequence) CVC4::Expr::getConst<CVC4::ExprSequence>; %template(getConstFloatingPoint) CVC4::Expr::getConst<CVC4::FloatingPoint>; %template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>; %template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>; |