diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-11 17:04:29 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-11 17:04:29 -0500 |
commit | 69c092f9e2ac6d9628f4de3e0038c1f021b3c7c6 (patch) | |
tree | 8e07794e8040d2ff65c9d4148c60a0f8dfb0f311 /src/expr | |
parent | a7b5b506a1b84b23bdb4263150590d15af8193fa (diff) |
Minor fixes to language bindings. (Resolves #607.)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager.i | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index fccadf43c..66930cf55 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -52,6 +52,18 @@ %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSignExtend>; %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::UninterpretedConstant>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>; @@ -63,6 +75,7 @@ %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Predicate>; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RegExp>; %template(mkConst) CVC4::ExprManager::mkConst<bool>; |