projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 5d1c529)
Fix mkConst<RoundingMode>() for Python bindings (#3447)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 11 Nov 2019 18:07:29 +0000 (10:07 -0800)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 11 Nov 2019 18:07:29 +0000 (12:07 -0600)
src/expr/expr_manager.i patch | blob | history

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 2736e9135a50211dc163a262480b54116355d37f..7cc63525922e79584c04f7a4ac6d3f3cce808eb5 100644 (file)
--- 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"