diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-11 10:07:29 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-11 12:07:29 -0600 |
commit | fcaf464a7f6281d882eb7790b5901a3797e861dc (patch) | |
tree | f70f7a88aa9704c7a0506fd8a0e6fdb69667414b /src | |
parent | 5d1c52999d78d5e825654d729279df8c49488133 (diff) |
Fix mkConst<RoundingMode>() for Python bindings (#3447)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_manager.i | 3 |
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" |