From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 31 Aug 2013 01:00:56 +0000 (-0400)
Subject: Add ability to mkConst(TupleSelect) and friends in language bindings
X-Git-Tag: cvc5-1.0.0~7287^2~32
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c2972fc63ca6d49ffeaf0e8a9a39cad733790cd7;p=cvc5.git

Add ability to mkConst(TupleSelect) and friends in language bindings
---

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index a386af5ee..a2ff0337a 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -34,6 +34,10 @@
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Predicate>;