src/expr/expr_manager.i

   1 %{
   2 #include "expr/expr_manager.h"
   3 %}
   4
   5 %ignore CVC4::ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
   6 %ignore CVC4::stats::getStatisticsRegistry(ExprManager*);
   7 %ignore CVC4::ExprManager::getResourceManager();
   8 %ignore CVC4::ExprManager::mkRecordType(const Record& rec);
   9 %ignore CVC4::ExprManager::safeFlushStatistics(int fd) const;
  10
  11 #ifdef SWIGJAVA
  12
  13 %typemap(javaout) CVC4::Expr {
  14   return new Expr(this, $jnicall, true);
  15 }
  16
  17 %typemap(javaout) CVC4::Type {
  18   return new Type(this, $jnicall, true);
  19 }
  20
  21 %typemap(javaout) CVC4::ArrayType {
  22   return new ArrayType(this, $jnicall, true);
  23 }
  24
  25 %typemap(javaout) CVC4::BitVectorType {
  26   return new BitVectorType(this, $jnicall, true);
  27 }
  28
  29 %typemap(javaout) CVC4::BooleanType {
  30   return new BooleanType(this, $jnicall, true);
  31 }
  32
  33 %typemap(javaout) CVC4::ConstructorType {
  34   return new ConstructorType(this, $jnicall, true);
  35 }
  36
  37 %typemap(javaout) const CVC4::Datatype& {
  38   return new Datatype(this, $jnicall, false);
  39 }
  40
  41 %typemap(javaout) CVC4::DatatypeType {
  42   return new DatatypeType(this, $jnicall, true);
  43 }
  44
  45 %typemap(javaout) std::vector<CVC4::DatatypeType> {
  46   return new vectorDatatypeType(this, $jnicall, true);
  47 }
  48
  49 %typemap(javaout) CVC4::FloatingPointType {
  50   return new FloatingPointType(this, $jnicall, true);
  51 }
  52
  53 %typemap(javaout) CVC4::FunctionType {
  54   return new FunctionType(this, $jnicall, true);
  55 }
  56
  57 %typemap(javaout) CVC4::SelectorType {
  58   return new SelectorType(this, $jnicall, true);
  59 }
  60
  61 %typemap(javaout) CVC4::StringType {
  62   return new StringType(this, $jnicall, true);
  63 }
  64
  65 %typemap(javaout) CVC4::RegExpType {
  66   return new RegExpType(this, $jnicall, true);
  67 }
  68
  69 %typemap(javaout) CVC4::RealType {
  70   return new RealType(this, $jnicall, true);
  71 }
  72
  73 %typemap(javaout) CVC4::SetType {
  74   return new SetType(this, $jnicall, true);
  75 }
  76
  77 %typemap(javaout) CVC4::SExprType {
  78   return new SExprType(this, $jnicall, true);
  79 }
  80
  81 %typemap(javaout) CVC4::SortType {
  82   return new SortType(this, $jnicall, true);
  83 }
  84
  85 %typemap(javaout) CVC4::SortConstructorType {
  86   return new SortConstructorType(this, $jnicall, true);
  87 }
  88
  89 %typemap(javaout) CVC4::TesterType {
  90   return new TesterType(this, $jnicall, true);
  91 }
  92
  93 %typemap(javaout) CVC4::IntegerType {
  94   return new IntegerType(this, $jnicall, true);
  95 }
  96
  97 %typemap(javaout) CVC4::RoundingModeType {
  98   return new RoundingModeType(this, $jnicall, true);
  99 }
 100
 101 %javamethodmodifiers CVC4::ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) "public";
 102
 103 #endif /* SWIGJAVA */
 104
 105 %include "expr/expr_manager.h"
 106
 107 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>;
 108 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
 109 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
 110 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorBitOf>;
 111 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRepeat>;
 112 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorExtract>;
 113 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateLeft>;
 114 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSignExtend>;
 115 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorZeroExtend>;
 116 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateRight>;
 117 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::IntToBitVector>;
 118 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPoint>;
 119 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointSize>;
 120 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPIEEEBitVector>;
 121 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPFloatingPoint>;
 122 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPReal>;
 123 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPSignedBitVector>;
 124 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPUnsignedBitVector>;
 125 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPGeneric>;
 126 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToUBV>;
 127 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>;
 128 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
 129 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
 130 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>;
 131 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
 132 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
 133 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
 134 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>;
 135 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::ExprSequence>;
 136 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>;
 137 #ifdef SWIGPYTHON
 138 /* The python bindings cannot differentiate between bool and other basic
 139  * types like enum and int. Therefore, we rename mkConst for the bool
 140  * case into mkBoolConst.
 141 */
 142 %template(mkBoolConst) CVC4::ExprManager::mkConst<bool>;
 143 %template(mkRoundingMode) CVC4::ExprManager::mkConst<RoundingMode>;
 144
 145 // These cases have trouble too.  Remove them for now.
 146 //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 147 #else
 148 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 149 %template(mkConst) CVC4::ExprManager::mkConst<bool>;
 150 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>;
 151 #endif