summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-11-11 10:07:29 -0800
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-11-11 12:07:29 -0600
commitfcaf464a7f6281d882eb7790b5901a3797e861dc (patch)
treef70f7a88aa9704c7a0506fd8a0e6fdb69667414b /src
parent5d1c52999d78d5e825654d729279df8c49488133 (diff)
Fix mkConst<RoundingMode>() for Python bindings (#3447)
Diffstat (limited to 'src')
-rw-r--r--src/expr/expr_manager.i3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 2736e9135..7cc635259 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -52,7 +52,6 @@
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateRight>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::IntToBitVector>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPoint>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointSize>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPIEEEBitVector>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPFloatingPoint>;
@@ -77,12 +76,14 @@
* case into mkBoolConst.
*/
%template(mkBoolConst) CVC4::ExprManager::mkConst<bool>;
+%template(mkRoundingMode) CVC4::ExprManager::mkConst<RoundingMode>;
// These cases have trouble too. Remove them for now.
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
#else
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
%template(mkConst) CVC4::ExprManager::mkConst<bool>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>;
#endif
%include "expr/expr_manager.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback