diff options
Diffstat (limited to 'src/expr/expr_manager.i')
| -rw-r--r-- | src/expr/expr_manager.i | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index df99af56d..2736e9135 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -51,17 +51,17 @@ %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorZeroExtend>; %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>; -//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPReal>; -//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPSignedBitVector>; -//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPUnsignedBitVector>; -//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPGeneric>; -//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToUBV>; -//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>; +%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>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPReal>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPSignedBitVector>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPUnsignedBitVector>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPGeneric>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToUBV>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>; |