summaryrefslogtreecommitdiff
path: root/src/expr/expr.i
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-05-27 18:05:07 -0500
committerGitHub <noreply@github.com>2020-05-27 16:05:07 -0700
commit4df14f1e09549be607123c66b7dd206e8e244c89 (patch)
tree3104897629ebe9efe4d14983ad89fb0d8778d4f2 /src/expr/expr.i
parent449cf281987eb8a2d43a572817db5c870a010c08 (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.i1
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>;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback