diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/expr/expr_manager.i | 13 | ||||
| -rw-r--r-- | src/util/unsat_core.i | 2 |
2 files changed, 15 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>; diff --git a/src/util/unsat_core.i b/src/util/unsat_core.i index 060ee3300..c69dade8f 100644 --- a/src/util/unsat_core.i +++ b/src/util/unsat_core.i @@ -9,6 +9,8 @@ #endif /* SWIGJAVA */ %} +%ignore CVC4::operator<<(std::ostream&, const UnsatCore&); + #ifdef SWIGJAVA // Instead of UnsatCore::begin() and end(), create an |