diff options
author | Martin Brain <martin.brain@cs.ox.ac.uk> | 2014-12-03 21:29:43 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-03 21:58:28 -0500 |
commit | cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 (patch) | |
tree | 582afecddf7d64953d8562ab57dd915db6cc852f /src/expr/node_manager.h | |
parent | 2121eaac7e63875f1e6ba53076535d25fd561c04 (diff) |
Floating point infrastructure.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f4c3a1999..f52c7732f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -685,6 +685,9 @@ public: /** Get the (singleton) type for RegExp. */ inline TypeNode regexpType(); + /** Get the (singleton) type for rounding modes. */ + inline TypeNode roundingModeType(); + /** Get the bound var list type. */ inline TypeNode boundVarListType(); @@ -764,6 +767,11 @@ public: */ inline TypeNode mkSExprType(const std::vector<TypeNode>& types); + /** Make the type of floating-point with <code>exp</code> bit exponent and + <code>sig</code> bit significand */ + inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + inline TypeNode mkFloatingPointType(FloatingPointSize fs); + /** Make the type of bitvectors of size <code>size</code> */ inline TypeNode mkBitVectorType(unsigned size); @@ -980,6 +988,11 @@ inline TypeNode NodeManager::regexpType() { return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE)); } +/** Get the (singleton) type for rounding modes. */ +inline TypeNode NodeManager::roundingModeType() { + return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE)); +} + /** Get the bound var list type. */ inline TypeNode NodeManager::boundVarListType() { return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); @@ -1066,6 +1079,14 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); } +inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) { + return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig))); +} + +inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) { + return TypeNode(mkTypeConst<FloatingPointSize>(fs)); +} + inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType, |