diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/cvc4.i | 1 | ||||
| -rw-r--r-- | src/expr/expr.i | 23 | ||||
| -rw-r--r-- | src/expr/expr_manager.i | 3 | ||||
| -rw-r--r-- | src/util/Makefile.am | 1 | ||||
| -rw-r--r-- | src/util/array_store_all.i | 6 |
5 files changed, 31 insertions, 3 deletions
diff --git a/src/cvc4.i b/src/cvc4.i index bc9f5a5af..b13a555e6 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -103,6 +103,7 @@ using namespace CVC4; %include "util/bitvector.i" %include "util/subrange_bound.i" %include "util/array.i" +%include "util/array_store_all.i" %include "util/hash.i" %include "expr/type.i" diff --git a/src/expr/expr.i b/src/expr/expr.i index 9b6c55703..34f074a6d 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -30,3 +30,26 @@ namespace CVC4 { }/* CVC4 namespace */ %include "expr/expr.h" + +%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; +%template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>; +%template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>; +%template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>; +%template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>; +%template(getConstSubrangeBounds) CVC4::Expr::getConst<CVC4::SubrangeBounds>; +%template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>; +%template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>; +%template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>; +%template(getConstBitVectorSignExtend) CVC4::Expr::getConst<CVC4::BitVectorSignExtend>; +%template(getConstBitVectorZeroExtend) CVC4::Expr::getConst<CVC4::BitVectorZeroExtend>; +%template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>; +%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>; +%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>; +%template(getConstDatatype) CVC4::Expr::getConst<CVC4::Datatype>; +%template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>; +%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>; +%template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>; +%template(getConstString) CVC4::Expr::getConst<std::string>; +%template(getConstBoolean) CVC4::Expr::getConst<bool>; + +%include "expr/expr.h" diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 178f00ccd..0d82c7aa8 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -17,9 +17,6 @@ %include "expr/expr_manager.h" -%template(mkConst) CVC4::ExprManager::mkConst< CVC4::Rational >; - - %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>; diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 8b0b2164f..432e6ef26 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -170,6 +170,7 @@ EXTRA_DIST = \ exception.i \ language.i \ array.i \ + array_store_all.i \ ascription_type.i \ rational.i \ hash.i diff --git a/src/util/array_store_all.i b/src/util/array_store_all.i new file mode 100644 index 000000000..afc14d089 --- /dev/null +++ b/src/util/array_store_all.i @@ -0,0 +1,6 @@ +%{ +#include "util/array_store_all.h" +%} + +%include "expr/type.i" +%include "util/array_store_all.h" |